Informatique et mathématiques de l'ingénieur

DPLL rencontre une contradiction, défait sa dernière décision, et repart sans rien retenir. S'il retombe cent fois sur la même impasse, il la redécouvre cent fois. CDCL corrige exactement cela, par deux gestes qui vont ensemble : analyser le conflit pour savoir qui l'a causé, et écrire une clause qui interdit de le refaire. Cette idée, apparue au milieu des années 1990, a fait passer les solveurs de quelques centaines de variables à plusieurs millions. C'est le cœur de tout ce qui tourne aujourd'hui.

Ce qui manque à DPLL

Deux gestes absents, et ils vont de pair

Savoir qui a causé le conflit. DPLL défait la dernière décision, qui n'est pas forcément la coupable. Si la contradiction ne doit rien à cette décision, la défaire ne corrige rien et la même impasse reviendra.
Retenir le résultat. Même quand il défait la bonne décision, DPLL ne garde aucune trace de ce qu'il a appris. Il repart avec exactement la formule de départ, et rien ne l'empêche de refaire le même chemin ailleurs dans l'arbre.
Le premier geste demande d'analyser le conflit ; le second d'en tirer une clause. C'est tout le contenu de ce chapitre.

Le graphe d'implication

Niveau de décision

Le niveau d'un littéral est le nombre de décisions prises quand il a reçu sa valeur.

Une décision ouvre un nouveau niveau. Tous les littéraux qu'elle fait propager portent ce même niveau.

Le niveau 0 est celui des littéraux affectés avant toute décision, par les clauses unitaires de la formule.

Antécédent

L'antécédent d'un littéral propagé est la clause qui l'a forcé.

Une décision n'a pas d'antécédent : rien ne l'imposait.

Graphe d'implication

Les sommets sont les littéraux affectés. Pour chaque littéral propagé, on trace un arc depuis chacun des autres littéraux de son antécédent, qui sont exactement ceux dont la fausseté l'a forcé.

Un sommet supplémentaire, noté $\bot$ , reçoit les arcs venant des littéraux de la clause falsifiée.

Voici le plus petit conflit qui vaille la peine d'être analysé. La formule est

$c_1 = (a \vee b)$ , $\quad c_2 = (\neg a \vee b)$ , $\quad c_3 = (a \vee \neg b)$ , $\quad c_4 = (\neg a \vee \neg b)$ , $\quad c_5 = (p \vee q)$ , $\quad c_6 = (\neg p \vee q)$

et le solveur a décidé $p = 1$ , puis $a = 1$ .

clause apprise : ¬aretour arrière au niveau 0

Le graphe d'implication au moment du conflit. Les nœuds pleins sont des décisions, les autres des propagations, et chaque flèche porte la clause qui l'a produite. La clause apprise nie les littéraux dont une flèche traverse la coupe ; elle redevient unitaire au niveau 0, où le solveur repart.

Lire ce graphe

Deux décisions, en cadre plein : $p = 1$ ouvre le niveau 1, $a = 1$ ouvre le niveau 2.

Deux propagations. $q = 1$ vient de $c_6 = (\neg p \vee q)$ , forcée par $p = 1$ . $b = 1$ vient de $c_2 = (\neg a \vee b)$ , forcée par $a = 1$ .

Le conflit vient de $c_4 = (\neg a \vee \neg b)$ , dont les deux littéraux sont faux puisque $a$ et $b$ valent 1.

Ce que le graphe montre immédiatement. Le niveau 1, avec $p$ et $q$ , n'a aucun arc vers le conflit. Ces deux variables n'y sont pour rien, et pourtant DPLL, en cas d'échec des deux valeurs de $a$ , remonterait jusqu'à $p$ pour refaire le même travail. C'est cette information que le graphe rend visible et que DPLL jette.

L'analyse de conflit

Coupe de conflit

Une coupe sépare les sommets du graphe en deux : du côté raison toutes les décisions, du côté conflit le sommet $\bot$ .

Les littéraux du côté raison dont un arc traverse la coupe forment une cause suffisante du conflit : les mettre tous à vrai en même temps mène nécessairement à la contradiction.

La clause apprise est la négation de cette conjonction, c'est-à-dire la disjonction des littéraux opposés.

Pourquoi la clause apprise est correcte

Elle n'ajoute aucune contrainte nouvelle : c'est une conséquence logique de la formule de départ.
En effet, chaque arc du graphe traduit une clause de la formule. Suivre les arcs depuis les littéraux traversant la coupe jusqu'au conflit, c'est dérouler une suite de propagations qui, toutes ensemble, aboutissent à une clause falsifiée. Aucun modèle ne peut donc mettre tous ces littéraux à vrai.
Ajouter la clause apprise à la formule ne change aucun modèle. Elle ne fait qu'expliciter ce que la formule disait déjà, sous une forme que la propagation saura employer.

Sur la figure précédente, la coupe retenue laisse $a = 1$ du côté raison et $b = 1$ du côté conflit. Un seul arc la traverse, celui qui part de $a = 1$ . La cause suffisante est donc «  $a = 1$  », et la clause apprise sa négation : $(\neg a)$ .

La même chose, par résolution

Ce n'est pas un hasard si le résultat ressemble à ce que produirait la règle du chapitre 6. L'analyse de conflit est une suite de résolutions, et il vaut la peine de la voir écrite ainsi.

L'analyse du conflit, écrite comme une résolution. On part de la clause falsifiée c4, et on la résout avec l'antécédent du dernier littéral propagé, ici c2 pour b. Le résultat est la clause apprise. Elle n'aboutit pas à la clause vide : c'est une déduction, pas une réfutation.

La recette, en une phrase

Partir de la clause falsifiée, et la résoudre avec l'antécédent du littéral affecté le plus récemment, tant qu'il reste plus d'un littéral du niveau courant.
Chaque résolution retire un littéral du niveau courant et le remplace par les raisons qui l'avaient forcé. Quand il n'en reste qu'un, on s'arrête : ce dernier littéral est le premier point d'implication unique, et la clause obtenue est la clause apprise.
Écrite ainsi, la correction de l'analyse ne demande plus de démonstration : c'est de la résolution, et la résolution est correcte.

Le premier point d'implication unique

Il existe plusieurs coupes possibles, donc plusieurs clauses apprises. Celle que retiennent tous les solveurs porte un nom.

Point d'implication unique

Un point d'implication unique, ou UIP, est un littéral du niveau courant par lequel passent tous les chemins allant de la décision de ce niveau jusqu'au conflit.

La décision elle-même en est toujours un. Le premier UIP est celui qui est le plus proche du conflit.

Voici l'exemple classique de la littérature, où la différence se voit. Six niveaux de décision, la décision $x_1 = 1$ au niveau 6, et deux chemins vers le conflit.

Les littéraux $x_9$ , $x_{10}$ et $x_{11}$ viennent de niveaux antérieurs. Ce qui les a produits n'a pas d'importance ici, et n'est pas dessiné : seul compte le fait qu'ils sont déjà affectés quand le niveau 6 commence.

clause apprise : ¬x4 ∨ x10 ∨ x11retour arrière au niveau 3

Pourquoi

x_4

et pas

x_1

Les deux sont des points d'implication uniques : tout chemin de $x_1$ vers le conflit passe par $x_4$ , et par $x_1$ trivialement.

En coupant sur $x_1$ , la décision, on apprend $\neg x_1 \vee x_9 \vee x_{10} \vee x_{11}$  : quatre littéraux.

En coupant sur $x_4$ , le premier UIP, on apprend $\neg x_4 \vee x_{10} \vee x_{11}$  : trois littéraux, et la figure l'affiche.

La clause du premier UIP est plus courte, donc plus contraignante, donc elle propagera plus souvent. C'est la raison du choix, et elle a été établie expérimentalement bien avant d'être comprise.

Le retrouver sans le chercher

Il n'y a pas à énumérer les coupes. La recette par résolution donne le premier UIP toute seule : on résout tant qu'il reste plus d'un littéral du niveau courant dans la clause, et on s'arrête dès qu'il n'en reste qu'un.
Ce littéral unique est le premier UIP, par construction. L'algorithme n'a jamais eu à savoir ce qu'était un UIP.

Et voici l'analyse écrite comme deux résolutions, à partir de la clause de conflit $c_6$ .

L'analyse du conflit précédent. On part de c6, la clause falsifiée, puis on élimine x6 par son antécédent c5, puis x5 par son antécédent c4. Il ne reste alors qu'un seul littéral du niveau 6, ¬x4 : c'est le premier UIP, et la clause obtenue est celle que la figure du graphe annonçait. Elle n'aboutit pas à la clause vide : c'est une déduction, pas une réfutation.

Le retour arrière non chronologique

Niveau de retour

Le solveur revient au deuxième plus haut niveau présent dans la clause apprise.

Pourquoi ce niveau précisément

La clause apprise contient exactement un littéral du niveau courant, le premier UIP. Tous les autres viennent de niveaux antérieurs.
En revenant au deuxième plus haut de ces niveaux, tous les littéraux de la clause sauf l'UIP sont encore affectés, et ils sont faux. La clause apprise devient donc unitaire : elle force immédiatement la négation de l'UIP.
Le solveur ne redescend donc pas au hasard : il revient exactement au point où sa nouvelle clause lui apprend quelque chose. Et cette valeur imposée n'est pas une décision, c'est une propagation.

Sur les deux exemples

Le petit. La clause apprise est $(\neg a)$ , qui ne contient qu'un seul niveau. Il n'y a pas de deuxième niveau : le retour se fait au niveau 0, et $a = 0$ y est propagé pour toujours. Le solveur vient d'établir un fait définitif.

Le canonique. La clause apprise est $\neg x_4 \vee x_{10} \vee x_{11}$ , avec $x_4$ au niveau 6, $x_{10}$ et $x_{11}$ au niveau 3. Le deuxième plus haut niveau est 3 : le solveur y revient, la clause devient unitaire, et $x_4 = 0$ est propagé.

Noter ce qui vient d'être sauté : les niveaux 4 et 5, qui n'apparaissent pas dans la clause apprise, ont été défaits d'un coup. DPLL serait remonté au niveau 5, puis 4, en refaisant le travail à chaque fois.

CDCL ne parcourt plus un arbre

C'est une conséquence qu'il faut accepter, parce qu'elle rend les dessins du chapitre précédent inutilisables.
Un retour arrière chronologique conserve la structure d'arbre : on descend, on remonte d'un cran, on repart. Un retour non chronologique saute plusieurs niveaux d'un coup et repart avec une formule qui a changé, puisqu'elle contient une clause de plus.
La recherche de CDCL est donc une suite d'états, pas un parcours d'arbre. On ne peut pas la dessiner comme un arbre, et c'est pourquoi ce chapitre trace des graphes d'implication et non des arbres de recherche.

L'algorithme complet

CDCL

Propager jusqu'au point fixe.
Pas de conflit et plus de variable libre : rendre le modèle.
Pas de conflit : décider d'une variable, ouvrir un niveau, retourner en 1.
Conflit au niveau 0 : rendre insatisfiable.
Conflit : analyser, apprendre la clause, revenir au niveau calculé, retourner en 1.

Ce que l'algorithme ne dit pas, et qui décide de tout

Trois choix restent ouverts, et ce sont eux qui séparent un solveur d'un autre.
Quelle variable décider, à l'étape 3.
Quelles clauses apprises garder, puisque les accumuler toutes finit par ralentir la propagation plus qu'elle ne l'accélère.
Quand tout recommencer, en gardant les clauses apprises mais en jetant les décisions.
Le chapitre suivant est entièrement consacré à ces trois réponses.

Ce que l'apprentissage change

La formule du chapitre précédent, refaite avec apprentissage

Reprenons $c_1$ à $c_6$ et le mauvais ordre de branchement, $p$ avant $a$ .

Décision $p = 1$ , niveau 1. Propagation $q = 1$ par $c_6$ . Décision $a = 1$ , niveau 2. Propagation $b = 1$ par $c_2$ . Conflit sur $c_4$ . Analyse : la clause apprise est $(\neg a)$ , et le retour se fait au niveau 0. Propagation $a = 0$ au niveau 0, définitivement. Puis $b = 1$ par $c_1$ , et $c_3 = (a \vee \neg b)$ est falsifiée. Conflit au niveau 0 : la formule est insatisfiable.

Deux décisions, contre six pour DPLL sur la même formule et le même ordre. Et surtout, la décision $p$ n'a servi à rien dans les deux cas : la différence est que CDCL ne l'a payée qu'une fois.

Les trois effets d'une clause apprise

Elle interdit de refaire l'impasse, où que ce soit dans la suite de la recherche. C'est l'effet évident.
Elle propage. Étant unitaire au niveau de retour, elle impose une valeur au lieu de laisser le solveur la décider. Une décision remplacée par une propagation, c'est une branche de moins.
Elle guide. Les variables qu'elle contient viennent d'être impliquées dans un conflit, donc elles sont contraintes. Les préférer pour les décisions suivantes est l'idée des heuristiques modernes, et c'est le sujet du chapitre 9.

Le plafond reste celui de Haken

CDCL apprend des clauses, et chaque clause apprise est obtenue par résolution. La preuve d'insatisfiabilité qu'il construit est donc une preuve par résolution.
Tout ce que le chapitre 6 a établi s'applique donc sans changement : sur le principe des tiroirs, sur les systèmes XOR encodés en clauses, CDCL est exponentiel, et aucun réglage n'y changera rien.
Ce que CDCL améliore n'est pas la puissance du système de preuve, c'est la vitesse à laquelle il trouve les preuves courtes quand elles existent. Sur les instances réelles, elles existent presque toujours, et c'est tout le secret de son succès.

Exercices type

Un conflit survient au niveau 5. La clause apprise est

(\neg x_2 \vee x_7 \vee \neg x_9)

, avec

x_2

au niveau 5,

x_7

au niveau 2,

x_9

au niveau 4. Où revient le solveur ?

Les niveaux présents dans la clause sont 5, 4 et 2. Le plus haut est 5, celui du premier UIP.

Le deuxième plus haut est 4 : c'est là que revient le solveur.

Vérification de l'intérêt : au niveau 4, les littéraux $x_7$ et $x_9$ sont encore affectés et faux, tandis que $x_2$ ne l'est plus. La clause n'a donc plus qu'un littéral libre, elle est unitaire, et elle propage $x_2 = 0$ .

Les niveaux 5 a été défait, ce qui est normal, mais aucun niveau entre 4 et 5 n'existait ici. Sur une clause où le deuxième niveau serait 2, les niveaux 3, 4 et 5 auraient été sautés d'un seul coup.

Combien de littéraux du niveau courant une clause apprise au premier UIP contient-elle ?

Exactement un.

C'est la définition même du critère d'arrêt : on résout tant qu'il en reste plus d'un, et on s'arrête dès qu'il n'en reste qu'un.

C'est aussi ce qui rend le retour arrière possible. Avec deux littéraux du niveau courant, revenir en arrière laisserait deux littéraux libres, la clause ne serait pas unitaire, et elle ne propagerait rien.

La clause apprise peut-elle rendre insatisfiable une formule qui ne l'était pas ?

Non, jamais. Elle est conséquence logique de la formule de départ.

Chaque étape de l'analyse est une résolution, et le chapitre 6 a établi qu'une résolvante est conséquence de ses parents. Par transitivité, la clause apprise est conséquence de la formule.

Ajouter une conséquence à une formule ne change aucun de ses modèles : la formule augmentée est équivalente à celle de départ, pas seulement équisatisfiable.

C'est ce qui autorise à accumuler des milliers de clauses apprises sans jamais douter du verdict final.

Sur le graphe canonique, quelle clause obtient-on en coupant juste après la décision

x_1

Du côté conflit se retrouvent alors tous les littéraux du niveau 6 sauf $x_1$  : $x_2, x_3, x_4, x_5, x_6$ et le conflit.

Les arcs qui traversent la coupe partent de $x_1$ , de $x_9$ , de $x_{10}$ et de $x_{11}$ . La clause apprise est donc

$\neg x_1 \vee x_9 \vee x_{10} \vee x_{11}$

Elle est correcte, comme toute clause obtenue par une coupe licite. Elle est simplement moins bonne : quatre littéraux au lieu de trois, donc moins contraignante, donc elle propagera moins souvent. Et le niveau de retour qu'elle induit est 3 également, sans gain.

Pourquoi le graphe d'implication ne contient-il jamais de circuit ?

Parce que les arcs suivent l'ordre chronologique des affectations.

Un arc va d'un littéral déjà affecté vers un littéral que sa fausseté vient de forcer. La cible est donc toujours postérieure à la source dans la pile des affectations.

Un circuit exigerait qu'un littéral soit antérieur à lui-même, ce qui est impossible. Le graphe est donc un graphe orienté sans circuit, ce qui garantit au passage que l'analyse de conflit termine : chaque résolution remonte d'un cran dans cet ordre.

CDCL apprend une clause à chaque conflit. Pourquoi ne les garde-t-il pas toutes ?

Parce qu'une clause coûte à chaque propagation. Le temps d'une propagation croît avec le nombre de clauses à examiner, et un solveur qui accumule des millions de clauses apprises finit par propager plus lentement qu'il ne gagne à les avoir.

L'arbitrage est donc permanent : garder ce qui sert, jeter le reste. Encore faut-il savoir mesurer ce qui sert, ce qui n'a rien d'évident sur une clause qui n'a pas encore resservi.

C'est l'une des trois questions ouvertes de l'algorithme, et le chapitre suivant donne la réponse retenue aujourd'hui.

Vérification rapideon peut se reprendre

1.Le niveau d'un littéral propagé est…

2.Combien de littéraux du niveau courant contient une clause apprise au premier UIP ?

3.Le solveur revient au…

4.La clause apprise est-elle une contrainte nouvelle ?

5.Pourquoi préférer la coupe au premier UIP plutôt qu'à la décision ?

6.CDCL échappe-t-il à la borne de Haken sur le principe des tiroirs ?

La méthode

Noter le niveau de chaque littéral au moment où il est affecté : sans cela, aucune analyse n'est possible.
Noter l'antécédent de chaque propagation, c'est-à-dire la clause qui l'a forcée.
Partir de la clause falsifiée pour analyser, jamais d'ailleurs.
Résoudre avec l'antécédent du littéral le plus récent, tant qu'il reste plus d'un littéral du niveau courant.
S'arrêter au premier UIP, c'est-à-dire dès qu'il n'en reste qu'un.
Revenir au deuxième plus haut niveau de la clause apprise, et laisser la propagation faire le reste.
Vérifier que la clause apprise propage au niveau de retour : sinon l'analyse est fausse.

Synthèse

Le niveau d'un littéral est le nombre de décisions prises quand il a été affecté.
L'antécédent d'un littéral propagé est la clause qui l'a forcé ; une décision n'en a pas.
Le graphe d'implication est sans circuit, parce que ses arcs suivent l'ordre des affectations.
Une coupe sépare les décisions du conflit ; les arcs qui la traversent donnent une cause suffisante.
La clause apprise est la négation de cette cause, donc une conséquence de la formule.
L'analyse de conflit est une suite de résolutions, partant de la clause falsifiée.
Le premier UIP est le littéral du niveau courant le plus proche du conflit ; il donne la clause la plus courte.
Une clause apprise au premier UIP contient exactement un littéral du niveau courant.
Le retour arrière se fait au deuxième plus haut niveau de la clause, où elle devient unitaire.
Une clause apprise interdit, propage et guide : trois effets, pas un seul.
CDCL ne parcourt plus un arbre : sa recherche est une suite d'états.
Il reste un moteur de résolution, donc la borne de Haken s'applique toujours.

CDCL : apprendre de ses échecs

Ce que ce chapitre apporte