Informatique et mathématiques de l'ingénieur

Un solveur SAT est un moteur générique : il ne sait rien du problème, il ne connaît que des clauses. Tout ce qui décide de la réussite se joue donc avant lui, dans la traduction. Deux encodages du même problème, tous deux corrects, peuvent différer d'un facteur mille en temps de résolution. Ce chapitre donne la méthode, les encodages qu'il faut connaître, et les pièges qui font qu'une modélisation juste devient inutilisable.

La méthode, en quatre étapes

Modéliser, dans l'ordre

1. Choisir les variables. Écrire en français ce que signifie chacune, sous la forme « 

x_{\ldots}

vaut 1 si et seulement si … ». C'est l'étape qui décide de tout le reste.
2. Écrire les contraintes une par une, en langue naturelle d'abord, puis en clauses. Une contrainte de l'énoncé, un paragraphe de clauses.
3. Vérifier sur deux cas : une solution valide doit satisfaire la formule, une configuration interdite doit la violer.
4. Relire le modèle rendu par le solveur et le retraduire dans le problème. Une solution qu'on ne sait pas relire est une solution qu'on ne sait pas vérifier.

L'erreur qui ne se voit jamais

Un solveur ne se trompe pas. S'il répond SAT, la formule est satisfiable, et le modèle rendu la satisfait ; on peut le contrôler soi-même en un parcours.
Il ne dit rien, en revanche, sur la question de savoir si la formule décrit le problème. Une contrainte oubliée donne une réponse parfaitement correcte à une question qui n'était pas la bonne, et rien dans la sortie ne le signale. C'est la seule source d'erreur du domaine, et elle est entièrement humaine.

L'encodage direct

C'est le point de départ de presque toutes les modélisations : une variable par couple objet, valeur.

Encodage direct

Pour affecter à chacun de $n$ objets une valeur parmi $k$ , on pose $n \times k$ variables :

$x_{i,v}$ vaut 1 si et seulement si l'objet $i$ reçoit la valeur $v$ .

Il faut alors imposer explicitement que chaque objet reçoive exactement une valeur : rien dans les variables ne l'exprime.

Les variables ne portent aucune contrainte

Rien n'empêche

x_{3,\text{rouge}}

x_{3,\text{bleu}}

de valoir 1 en même temps. Le solveur ne voit pas que l'objet 3 ne peut avoir qu'une couleur : il voit deux variables booléennes indépendantes.
Oublier les clauses « exactement une valeur » est la faute de modélisation la plus fréquente, et elle produit des solutions absurdes que le solveur défend pourtant très bien.

Les contraintes de cardinalité

Elles reviennent partout : au moins un, au plus un, exactement $k$ , au plus $k$ .

Au moins un, et au plus un

Au moins un parmi $x_1, \ldots, x_n$  : une seule clause, $(x_1 \vee \cdots \vee x_n)$ .

Au plus un, encodage par paires : $(\neg x_i \vee \neg x_j)$ pour chaque paire $i < j$ , soit $\frac{n(n-1)}{2}$ clauses et aucune variable nouvelle.

L'encodage par paires est simple et parfait pour de petites valeurs de $n$ . Il devient déraisonnable quand $n$ grandit : pour $n = 1000$ , il produit près de cinq cent mille clauses pour une seule contrainte.

L'idée de l'encodage suivant est de faire circuler un signal. Les variables auxiliaires $s_i$ forment une chaîne de relais : $s_i$ signifie « un des $x_1, \ldots, x_i$ vaut déjà 1 ». Trois règles suffisent alors : allumer un $x_i$ allume le relais $s_i$ , un relais allumé reste allumé plus loin dans la chaîne, et il est interdit d'allumer un $x_i$ si le relais précédent l'est déjà.

Au plus un, encodage séquentiel

On introduit $n - 1$ variables auxiliaires, $s_i$ signifiant « un des $x_1, \ldots, x_i$ vaut déjà 1 ». Les clauses sont alors :

$(\neg x_1 \vee s_1)$

$(\neg x_i \vee s_i)$ , $(\neg s_{i-1} \vee s_i)$ et $(\neg x_i \vee \neg s_{i-1})$ pour $1 < i < n$

$(\neg x_n \vee \neg s_{n-1})$

soit $3n - 4$ clauses et $n - 1$ variables : linéaire au lieu de quadratique.

Le relais en marche

Poser $x_2 = 1$ . La clause $(\neg x_2 \vee s_2)$ devient unitaire et allume $s_2$ . La clause $(\neg s_2 \vee s_3)$ devient alors unitaire et allume $s_3$ , puis $s_4$ , et ainsi de suite jusqu'au bout de la chaîne.

Tentons maintenant $x_5 = 1$ . La clause $(\neg x_5 \vee \neg s_4)$ interdit cette combinaison, puisque $s_4$ est allumé : la clause est falsifiée, et le solveur le voit sans avoir rien à décider.

C'est ce parcours de proche en proche qui remplace les $\frac{n(n-1)}{2}$ clauses de l'encodage par paires. Le prix est un délai : là où l'encodage par paires interdit $x_5$ immédiatement, le séquentiel doit d'abord propager le long de la chaîne.

f(x) = x * (x - 1) / 2g(x) = 3*x - 4

Le coût des deux encodages de « au plus un ». Par paires, en n(n−1)/2, la courbe sort du cadre vers n = 29 ; en séquentiel, en 3n − 4, elle reste une droite. En dessous d'une dizaine de variables, l'encodage par paires reste préférable : il n'ajoute aucune variable.

Quel encodage, et quand

Jusqu'à une dizaine de variables : par paires. Il ne crée aucune variable, et le solveur propage dessus très efficacement.
Au-delà : séquentiel, ou l'un de ses raffinements. Le nombre de clauses devient le facteur limitant, et les variables auxiliaires se paient largement.
Le seuil exact dépend de l'instance, et il se mesure au lieu de se deviner : les deux encodages tiennent en quelques lignes de code, et essayer les deux coûte moins cher que d'en discuter.

Ce qu'un bon encodage préserve

Le critère n'est pas seulement le nombre de clauses, c'est la propagation. Un encodage est dit maintenir la cohérence d'arc si, dès qu'un

x_i

passe à 1, la propagation unitaire met tous les autres à 0 sans qu'aucune décision soit nécessaire.
L'encodage par paires a cette propriété. Poser

x_3 = 1

rend le littéral

\neg x_3

faux ; la clause

(\neg x_3 \vee \neg x_4)

ne tient donc plus qu'à son second littéral, elle est unitaire, et elle force

x_4 = 0

. Il en va de même pour toutes les autres, en une seule passe de propagation. L'encodage séquentiel conserve la propriété lui aussi, à travers la chaîne des relais.
Un encodage plus court mais qui ne propage pas est presque toujours un mauvais marché : le solveur devra deviner ce qu'il aurait pu déduire.

Colorer un graphe

Trois couleurs pour cinq sommets

Les variables. $x_{v,c}$ vaut 1 si et seulement si le sommet $v$ reçoit la couleur $c$ . Avec 5 sommets et 3 couleurs, cela fait 15 variables.

Chaque sommet a au moins une couleur. Une clause par sommet : $(x_{v,1} \vee x_{v,2} \vee x_{v,3})$ .

Chaque sommet a au plus une couleur. Trois clauses par sommet, par paires de couleurs.

Deux sommets adjacents diffèrent. Pour chaque arête $\{u, v\}$ et chaque couleur $c$  : $(\neg x_{u,c} \vee \neg x_{v,c})$ . Soit trois clauses par arête.

Graphe non orienté5 sommets, 6 arêtes

Le graphe à colorer, et une solution à trois couleurs. Le triangle A, B, C interdit d'en utiliser moins.

Voici, pour le seul triangle $A, B, C$ , les clauses que produit cet encodage. Cliquer sur les variables permet de constater qu'aucune couleur ne peut être partagée.

9 clausessatisfaiteunitaireen attente

c1(Arouge∨Avert∨Ableu)
c2(Brouge∨Bvert∨Bbleu)
c3(Crouge∨Cvert∨Cbleu)
c4(¬Arouge∨¬Brouge)⇒ Brouge = 0
c5(¬Avert∨¬Bvert)⇒ Avert = 0
c6(¬Ableu∨¬Bbleu)
c7(¬Arouge∨¬Crouge)⇒ Crouge = 0
c8(¬Avert∨¬Cvert)
c9(¬Ableu∨¬Cbleu)

ArougeAvertAbleuBrougeBvertBbleuCrougeCvertCbleu

vert = décidé, orange = déduit par propagation.

Propagation unitaire : Brouge = 0, Avert = 0, Crouge = 0. Ces valeurs ne sont pas des choix, elles sont imposées.

Les clauses du triangle, réduites aux arêtes A-B et A-C pour rester lisibles. Poser A en rouge rend unitaires les clauses d'arête et interdit le rouge à B et C, sans qu'aucun choix soit fait.

Les clauses « au plus une couleur » sont-elles nécessaires ?

Pour la question « ce graphe est-il 3-coloriable », non : un sommet à deux couleurs n'empêche pas d'en extraire une coloration valide, puisque les clauses d'arête interdisent déjà tout partage. On peut donc les omettre et gagner des clauses.
Pour la question « énumérer les colorations », oui : sans elles, une même coloration est comptée plusieurs fois.
La leçon générale : ce qu'un encodage peut omettre dépend de la question posée, pas du problème. Le chapitre 10 y revient, à propos du comptage de modèles.

Le sudoku, en entier

C'est l'exemple canonique parce qu'il est entièrement fait de contraintes « exactement un ».

Un sudoku ordinaire, chiffré

Les variables. $x_{l,c,v}$ vaut 1 si et seulement si la case en ligne $l$ , colonne $c$ contient la valeur $v$ . Soit $9 \times 9 \times 9 = 729$ variables.

Les contraintes, toutes de la même forme :

chaque case contient exactement une valeur : 81 contraintes sur 9 variables ;
chaque ligne contient chaque valeur exactement une fois : 81 contraintes ;
chaque colonne, de même : 81 contraintes ;
chaque bloc de 3 sur 3, de même : 81 contraintes.

Les indices de la grille de départ deviennent des clauses unitaires : une case donnée à 7 impose $x_{l,c,7}$ .

En encodage par paires, cela fait environ 11 000 clauses. Un solveur moderne résout une telle instance en quelques millisecondes, et il passe l'essentiel de ce temps en propagation unitaire, sans presque jamais décider.

Pourquoi le sudoku est facile pour un solveur

Parce que ses contraintes propagent. Chaque valeur posée en falsifie immédiatement des dizaines d'autres, ce qui rend beaucoup de clauses unitaires, ce qui pose de nouvelles valeurs, et ainsi de suite.
C'est exactement ce que fait un joueur humain quand il raisonne « il ne reste qu'une case possible pour le 4 dans ce bloc ». La différence est que le solveur le fait un million de fois par seconde, et qu'il sait revenir en arrière quand il a dû parier.

Un emploi du temps

Trois cours, deux salles, quatre créneaux

Les variables. $y_{i,s,t}$ vaut 1 si le cours $i$ se tient en salle $s$ au créneau $t$ . Ici $3 \times 2 \times 4 = 24$ variables.

Chaque cours a lieu exactement une fois : pour chaque $i$ , exactement une des 8 variables $y_{i,s,t}$ vaut 1.

Une salle accueille au plus un cours par créneau : pour chaque couple $(s, t)$ , au plus un des $y_{i,s,t}$ vaut 1. Huit contraintes « au plus un » sur trois variables.

Un enseignant ne se dédouble pas : si les cours 1 et 2 ont le même enseignant, alors pour chaque créneau $t$ , au plus un des $y_{1,s,t}$ et $y_{2,s',t}$ vaut 1, toutes salles confondues.

Une préférence, si on veut : « le cours 3 n'est pas au dernier créneau » se dit par des clauses unitaires $(\neg y_{3,s,4})$ .

Une contrainte souple n'a pas sa place dans SAT

« Autant que possible, éviter les cours à 8 heures » ne se traduit pas en clauses : une clause est satisfaite ou ne l'est pas, il n'y a pas de degré.
Deux issues honnêtes. Soit on durcit la préférence en contrainte stricte, et le problème peut devenir insatisfiable. Soit on change d'outil pour MaxSAT, qui cherche à satisfaire le plus grand nombre de clauses souples, et que le chapitre 10 présente.
Ce qu'il ne faut pas faire, c'est encoder une préférence comme une contrainte dure sans le dire : on obtient un UNSAT incompréhensible, sur un problème qui avait des solutions acceptables.

Écrire les clauses par programme

Passé une dizaine de variables, écrire les clauses à la main n'a plus de sens : une contrainte « au plus un » sur 40 variables en compte 780. Personne ne tape cela au clavier, et c'est précisément pourquoi le format DIMACS est fait pour être écrit par un programme.

main.py

Sortie

>_ Prêt à exécuter…

Ce que ce code change

Il rend la modélisation vérifiable. Une fonction exactement_un se teste une fois pour toutes, sur trois variables, et sert ensuite sur quarante sans risque d'oubli.
Il rend aussi le coût visible : la dernière boucle affiche le nombre de clauses produites, et l'on voit à quel moment l'encodage par paires devient déraisonnable. C'est le genre de mesure qui remplace avantageusement une discussion.

Relire la réponse

C'est la quatrième étape de la méthode, et celle qu'on saute. Un solveur ne rend pas une coloration : il rend une liste de littéraux. La retraduire fait partie de la modélisation, et c'est aussi le seul moment où l'on peut vérifier qu'on a modélisé ce qu'on croyait.

main.py

Sortie

>_ Prêt à exécuter…

Écrire le décodeur en même temps que l'encodeur

La fonction numero sert dans les deux sens : elle produit les clauses, et elle relit le modèle. Une seule définition, donc aucune chance qu'ils divergent.
Le contrôle final, lui, ne regarde pas la formule : il vérifie la solution contre l'énoncé, arête par arête. C'est le seul moyen d'attraper une contrainte oubliée, puisqu'une contrainte absente de la formule est aussi absente du raisonnement du solveur.
Vingt lignes, écrites une fois, qui transforment un « le solveur dit SAT » en « voici une solution, et elle est correcte ».

Quand le solveur répond UNSAT et qu'on ne comprend pas pourquoi

C'est la situation la plus fréquente en modélisation réelle, et la plus déroutante : le problème a manifestement des solutions, et le solveur affirme le contraire. Il a raison sur la formule ; c'est la formule qui est fausse.

La méthode, dans l'ordre

1. Vérifier sur un cas connu. Prendre une solution qu'on sait valide, la traduire en clauses unitaires, l'ajouter à la formule et relancer. Si le résultat est UNSAT, une contrainte du modèle interdit une solution légitime, et l'on tient le coupable.
2. Retirer les contraintes une à une. Commenter un groupe de clauses, relancer. Dès que la réponse redevient SAT, le groupe retiré contient l'erreur.
3. Demander un noyau insatisfiable. La plupart des solveurs savent rendre un sous-ensemble de clauses déjà insatisfiable à lui seul. C'est l'étape 2, faite automatiquement et beaucoup mieux.

Noyau insatisfiable

Un noyau insatisfiable est un sous-ensemble des clauses qui est déjà insatisfiable.

Il est minimal si en retirer n'importe quelle clause le rend satisfiable.

Un noyau, sur une formule minuscule

La formule ci-dessous compte cinq clauses et se révèle insatisfiable. Trois d'entre elles suffisent pourtant à l'expliquer.

Poser $x = 1$  : la clause $(\neg x \vee y)$ force $y = 1$ , et $(\neg x \vee \neg y)$ force $y = 0$ . Poser $x = 0$  : la clause $(x)$ est falsifiée. Aucune issue.

Le noyau est donc $\{(x), (\neg x \vee y), (\neg x \vee \neg y)\}$ . Les deux autres clauses, qui portent sur $z$ et $w$ , n'y sont pour rien : elles pourraient décrire la moitié du problème sans changer le verdict.

Sur une formule de dix mille clauses, cette réduction est la différence entre une relecture aveugle et un diagnostic.

5 clausesunitaireen attente

c1(x)⇒ x = 1
c2(¬x∨y)
c3(¬x∨¬y)
c4(z∨w)
c5(¬z∨w)

xyzw

vert = décidé, orange = déduit par propagation.

Propagation unitaire : x = 1. Ces valeurs ne sont pas des choix, elles sont imposées.

Cinq clauses, dont trois forment un noyau insatisfiable. Propager jusqu'au bout mène au conflit sans jamais toucher à z ni à w : ces deux variables sont hors de cause, et c'est exactement ce qu'un noyau permet de dire à un modélisateur perdu.

Les hypothèses, pour ne pas relancer dix fois

Les solveurs modernes acceptent des hypothèses : une liste de littéraux supposés vrais pour cette résolution seulement, sans modifier la formule.
Cela change la façon de travailler. Au lieu de recompiler un fichier par variante, on garde une seule formule en mémoire et on relance avec des hypothèses différentes. Le solveur conserve d'un appel à l'autre tout ce qu'il a appris, et les appels suivants sont bien plus rapides que le premier.
Et quand une résolution sous hypothèses échoue, le solveur rend le sous-ensemble des hypothèses responsable de l'échec, ce qui est un noyau insatisfiable ciblé sur ce qu'on voulait tester.

Un UNSAT n'est pas toujours une erreur

Il arrive que le problème n'ait réellement pas de solution, et c'est une information précieuse, à condition de la présenter comme telle : « aucun emploi du temps ne respecte ces contraintes » vaut mieux qu'un fichier vide.
La question à trancher est donc : le modèle est-il faux, ou l'énoncé est-il impossible ? Le noyau insatisfiable répond aux deux, puisqu'il nomme les contraintes en cause. Il ne reste qu'à demander à qui a écrit l'énoncé laquelle il accepte de relâcher.

Les symétries

Symétrie

Une symétrie d'une instance est une permutation des variables qui transforme toute solution en une autre solution.

Dans la coloration, permuter les noms des couleurs est une symétrie : toute solution en engendre $k!$ autres, identiques au renommage près. Dans l'emploi du temps, deux salles interchangeables en engendrent deux fois plus.

Les symétries coûtent surtout sur les instances insatisfiables

Sur une instance satisfiable, elles sont plutôt une aubaine : il y a beaucoup de solutions, et le solveur en trouve une plus vite.
Sur une instance insatisfiable, elles sont un désastre. Le solveur doit réfuter chaque configuration, et il refait

k!

fois le même raisonnement sur des variables aux noms différents, sans jamais s'apercevoir qu'il se répète.
C'est la raison pour laquelle certaines instances minuscules résistent des heures, alors qu'un humain voit la réponse en une phrase.

Casser une symétrie

On ajoute des clauses qui n'éliminent aucune solution essentiellement différente, mais interdisent les copies. Pour la coloration : imposer que le sommet 1 reçoive la couleur 1, que le sommet 2 reçoive la couleur 1 ou 2, et ainsi de suite.
Pourquoi cela ne perd aucune solution. Les noms des couleurs sont interchangeables. S'il existe une coloration valide où le sommet 1 est vert, on peut renommer partout « vert » en « couleur 1 » : les arêtes restent respectées, puisque le renommage est le même dans tout le graphe. Toute solution possède donc une copie qui satisfait les clauses ajoutées, et il suffit de chercher celle-là.
La formule reste équisatisfiable, et l'espace de recherche est divisé par

k!

. C'est l'une des interventions au meilleur rapport entre l'effort et le gain.

Le problème des pigeons

\mathrm{PHP}_n

Placer $n + 1$ pigeons dans $n$ casiers, un seul pigeon par casier. C'est évidemment impossible.

Variables : $p_{i,j}$ vaut 1 si le pigeon $i$ est dans le casier $j$ .

Clauses : chaque pigeon est quelque part, $(p_{i,1} \vee \cdots \vee p_{i,n})$  ; et deux pigeons ne partagent pas un casier, $(\neg p_{i,j} \vee \neg p_{k,j})$ .

L'exemple qui a occupé le domaine pendant trente ans

Un humain réfute

\mathrm{PHP}_n

en une phrase : il y a plus de pigeons que de casiers.
Un solveur fondé sur la résolution, c'est-à-dire tous les solveurs CDCL actuels, a besoin d'un nombre exponentiel d'étapes. Ce n'est pas un défaut d'implémentation : c'est un théorème, dû à Haken en 1985, et il vaut pour toute preuve par résolution, quelle qu'elle soit.

\mathrm{PHP}_{12}

, avec 13 pigeons et 12 casiers, soit 156 variables, met déjà en difficulté des solveurs qui traitent par ailleurs des instances d'un million de variables. C'est l'exemple à garder en tête chaque fois qu'on est tenté de croire qu'un petit problème est un problème facile.

Vérification rapideon peut se reprendre

1.Pour placer 8 reines sur un échiquier de 8 sur 8, combien de variables dans un encodage direct « une case, une valeur » ?

2.Un modèle de coloration oublie les clauses « chaque sommet a au moins une couleur ». Que rend le solveur ?

3.Ajouter des clauses de rupture de symétrie rend l'instance…

Exercices type

Combien de clauses pour « exactement un parmi 10 variables », en encodage par paires ?

Au moins un : 1 clause de 10 littéraux.

Au plus un : $\frac{10 \times 9}{2} = 45$ clauses de 2 littéraux.

Total : 46 clauses, aucune variable nouvelle.

En encodage séquentiel : $3 \times 10 - 4 = 26$ clauses, plus la clause « au moins un », mais aussi 9 variables auxiliaires. À cette taille, l'encodage par paires reste le meilleur choix : 46 clauses binaires sur lesquelles le solveur propage sans effort valent mieux que 27 clauses et 9 variables de plus.

Encoder « au plus deux parmi

x_1, x_2, x_3, x_4

La généralisation directe de l'encodage par paires : interdire tous les sous-ensembles de trois variables.

Il y a $\binom{4}{3} = 4$ tels sous-ensembles, d'où quatre clauses :

$(\neg x_1 \vee \neg x_2 \vee \neg x_3)$ , $(\neg x_1 \vee \neg x_2 \vee \neg x_4)$ , $(\neg x_1 \vee \neg x_3 \vee \neg x_4)$ , $(\neg x_2 \vee \neg x_3 \vee \neg x_4)$ .

En général, « au plus $k$ parmi $n$  » demande $\binom{n}{k+1}$ clauses par cette méthode, ce qui n'est praticable que pour de petites valeurs. Au-delà, on emploie un encodage à variables auxiliaires, du même esprit que le séquentiel, souvent construit sur un réseau de tri.

Une coloration à 2 couleurs d'un triangle est-elle satisfiable ? Le montrer sur les clauses

Trois sommets $A$ , $B$ , $C$ , deux couleurs. Variables $A_1, A_2, B_1, B_2, C_1, C_2$ .

Au moins une couleur : $(A_1 \vee A_2)$ , $(B_1 \vee B_2)$ , $(C_1 \vee C_2)$ .

Arêtes : $(\neg A_1 \vee \neg B_1)$ , $(\neg A_2 \vee \neg B_2)$ , et de même pour les paires $A, C$ et $B, C$ .

Supposons $A_1 = 1$ . Les clauses d'arête forcent $B_1 = 0$ et $C_1 = 0$ , donc par « au moins une » on obtient $B_2 = 1$ et $C_2 = 1$ . Mais l'arête $B, C$ contient $(\neg B_2 \vee \neg C_2)$ , qui est alors falsifiée.

Le cas $A_2 = 1$ est symétrique. La formule est donc insatisfiable, ce qui traduit exactement le fait qu'un triangle n'est pas biparti.

Noter que le raisonnement ci-dessus est mené uniquement par propagation unitaire, après une seule décision. C'est très exactement ce que fera DPLL au chapitre 7.

Pourquoi ajouter des clauses peut-il accélérer un solveur ?

Parce que le coût d'un solveur n'est pas dans le nombre de clauses, mais dans le nombre de décisions qu'il doit prendre et défaire.

Une clause supplémentaire qui rend une propagation possible remplace une décision, donc coupe une branche entière de la recherche. Les clauses de rupture de symétrie en sont l'exemple type : elles alourdissent la formule et divisent le travail.

C'est aussi tout le principe de CDCL, au chapitre 8 : le solveur ajoute lui-même des clauses pendant la recherche, chacune résumant une impasse qu'il ne refera plus.

La méthode

Écrire le sens de chaque variable en français avant d'écrire une seule clause.
Traiter chaque contrainte de l'énoncé séparément, et la nommer.
Ne jamais oublier les clauses « exactement un » : les variables ne les portent pas.
Compter les clauses d'une contrainte de cardinalité avant de l'écrire, pour choisir l'encodage.
Préférer un encodage qui propage à un encodage seulement plus court.
Chercher les symétries, et les casser quand l'instance risque d'être insatisfiable.
Vérifier la modélisation sur deux cas, un valide et un interdit, avant de lancer le solveur.

Synthèse

Le solveur ne se trompe jamais ; la traduction, si. C'est la seule source d'erreur.
L'encodage direct pose une variable par couple objet-valeur, et n'impose rien tout seul.
« Au moins un » est une clause ; « au plus un » par paires coûte $\frac{n(n-1)}{2}$ clauses.
L'encodage séquentiel de « au plus un » coûte $3n - 4$ clauses et $n - 1$ variables.
Un bon encodage se juge à ce qu'il fait propager, pas seulement à sa taille.
Colorer un graphe : au moins une couleur par sommet, et une clause par arête et par couleur.
Une contrainte souple n'a pas de place en SAT : la durcir, ou passer à MaxSAT.
Les symétries multiplient le travail sur les instances insatisfiables ; les casser coûte peu.
Le décodeur s'écrit en même temps que l'encodeur, et le contrôle final regarde l'énoncé, pas la formule.
Devant un UNSAT inattendu : ajouter une solution connue, retirer les contraintes une à une, demander un noyau insatisfiable.
Les hypothèses permettent de tester des variantes sans recompiler ni perdre ce que le solveur a appris.
$\mathrm{PHP}_n$ est évident pour un humain et exponentiel pour toute preuve par résolution.

Modéliser un problème en SAT

Ce que ce chapitre apporte