Un problème complet, du français au graphique

Une seule ligne : ajouter le couple à la liste des paires anti-affines.

La famille anti-affinite passe de 6 à 9 clauses, une par hôte pour la nouvelle paire. Le modèle passe de 140 à 143 clauses.

C'est tout l'intérêt d'avoir gardé les familles séparées et de les avoir produites par compréhension : une contrainte nouvelle de l'énoncé se traduit par une modification locale, et le reste du modèle ne bouge pas.

Il faut interdire tous les groupes de 6 services sur un même hôte, soit $\binom{30}{6}$ groupes.

$\binom{30}{6} = 593\,775$ clauses par hôte. Avec dix hôtes, près de six millions de clauses pour une seule phrase de l'énoncé.

C'est inutilisable, et c'est prévisible en une multiplication faite avant d'écrire le code. L'encodage séquentiel du chapitre 3, en $O(n \times k)$ clauses avec des variables auxiliaires, donnerait ici quelques milliers de clauses au total.

La leçon : compter avant de générer. C'est ce que fait l'étape 2 de ce chapitre, et c'est la raison pour laquelle elle existe.

Parce que cette contrainte n'aide en rien à créer la contradiction.

Le raisonnement qui rend le problème impossible est un comptage : sept services réclament chacun au moins une place, il n'y en a que six. Autoriser un service à occuper deux hôtes ne libérerait aucune place ; cela en consommerait davantage.

Retirer la contrainte « un hôte au plus » laisse donc le problème tout aussi insatisfiable, et le noyau, qui ne garde que ce qui est nécessaire, l'écarte.

C'est le genre d'information qu'un noyau donne gratuitement, et qu'une relecture manuelle du modèle ne donnerait qu'au prix d'un raisonnement.

Parce que le solveur a déjà vérifié la solution contre les clauses, et qu'il ne se trompe pas. Refaire ce contrôle ne teste que le solveur, qui n'est pas en cause.

Ce qui reste à tester est le seul endroit où une erreur peut se cacher : la traduction de l'énoncé en clauses. Une contrainte oubliée est absente de la formule, donc absente du raisonnement du solveur, donc invisible dans un contrôle qui repasse par la formule.

Le contrôle doit donc repartir des phrases de l'énoncé, une par une, et les appliquer au placement relu. C'est le seul moyen d'attraper un oubli.

SAT ne sait pas optimiser, il faut donc poser plusieurs questions.

Ajouter, pour chaque hôte, une variable $v_h$ signifiant « l'hôte $h$ est vide », liée aux placements par les clauses $(\neg v_h \vee \neg x_{s,h})$ pour chaque service $s$.

Puis demander successivement : existe-t-il une solution avec au moins 1 hôte vide, avec au moins 2, avec au moins 3 ? Chaque question est une contrainte de cardinalité sur les $v_h$, et la dernière réponse positive donne l'optimum.

Deux remarques. La recherche dichotomique réduit le nombre d'appels. Et si la sortie doit être un compromis entre plusieurs objectifs, il vaut mieux passer à MaxSAT, conçu pour cela.

Ici, oui. Vingt et une variables et cent quarante clauses se résolvent en quelques dizaines d'étapes. Aucune des techniques des chapitres 8 et 9 ne changerait le résultat, ni le temps perceptible.

Dix fois plus grand, non. Avec 70 services et 30 hôtes, deux choses se produisent dans cet ordre : l'encodage de cardinalité explose, puis, une fois celui-ci corrigé, le solveur naïf s'effondre parce qu'il repropage la formule entière à chaque affectation.

Le bon réflexe est donc d'abord de revoir l'encodage, ensuite seulement de prendre un vrai solveur. Ils se branchent au même endroit du code : la fonction resoudre est remplacée par un appel à une bibliothèque, et tout le reste du chapitre, modélisation, relecture, contrôle, dessin, reste inchangé.