DPLL : chercher, et savoir revenir en arrière

Le chapitre précédent a montré que la résolution suffit à démontrer, mais que l'appliquer aveuglément fait exploser la mémoire. DPLL renverse le compromis : au lieu de produire toutes les conséquences, il parie sur une valeur, en tire ce qu'il peut, et défait son pari s'il aboutit à une contradiction. C'est une recherche avec retour sur trace, et elle s'écrit récursivement, au sens du chapitre d'algorithmique sur la récursivité : un cas de base, un appel sur un problème plus petit, et une pile d'appels qui se défait quand une branche échoue. Trois lignes de pseudo-code, publiées en 1962, qui sont encore la charpente de tous les solveurs actuels. Ce chapitre les déroule, et surtout distingue ce qui, dans cette recherche, est un choix et ce qui n'en est pas.

Trois opérations, dont une seule est un pari

DPLL

Pour décider si une formule $F$ est satisfiable sous une affectation partielle :

Propager toutes les clauses unitaires jusqu'au point fixe.
Si une clause est falsifiée : échec, remonter.
Si toutes les clauses sont satisfaites : succès, rendre l'affectation.
Sinon, choisir une variable libre, lui donner une valeur, et recommencer. Si cette branche échoue, essayer l'autre valeur.

Décider et propager ne sont pas la même chose. C'est la distinction que tout le module a préparée, et c'est ici qu'elle paie.
Propager est une déduction : si une clause n'a plus qu'un littéral libre et que tous les autres sont faux, ce littéral doit être vrai. Aucun modèle n'est perdu, il n'y aura jamais à revenir dessus.
Décider est un pari : rien n'imposait cette valeur, et si la branche échoue il faudra essayer l'autre.
D'où la conséquence pratique qui gouverne toute l'ingénierie du domaine : seules les décisions coûtent. Une propagation, aussi longue soit-elle, ne double jamais le travail ; une décision, si.

Pourquoi la propagation ne fait perdre aucun modèle

Soit une clause

(\ell_1 \vee \cdots \vee \ell_k)

dont tous les littéraux sauf

\ell_1

sont déjà faux.
Un modèle qui prolonge l'affectation courante doit satisfaire cette clause, donc satisfaire l'un de ses littéraux. Les autres étant faux, il ne reste que

\ell_1

. Tout modèle atteignable met donc

\ell_1

à vrai.
Fixer

\ell_1

n'élimine ainsi aucune possibilité : c'est une déduction, et c'est ce qui autorise à la faire sans jamais prévoir de retour arrière.

Vérification rapideon peut se reprendre

Dans DPLL, laquelle de ces opérations est un pari qu'il faudra peut-être défaire ?

Une trace, déroulée

Prenons quatre clauses et suivons la recherche pas à pas.

$c_1 = (x \vee y)$ , $\quad c_2 = (\neg x \vee z)$ , $\quad c_3 = (\neg x \vee \neg z)$ , $\quad c_4 = (y \vee z)$

Aucune clause n'est unitaire : la propagation ne peut rien faire, et il faut décider.

6 étapes

L'arbre complet. Dérouler pas à pas montre l'ordre dans lequel le solveur le parcourt, et le moment où il revient en arrière.

La recherche sur (x ∨ y) ∧ (¬x ∨ z) ∧ (¬x ∨ ¬z) ∧ (y ∨ z). Dérouler pas à pas montre le seul moment intéressant : le passage de la branche gauche, qui échoue, à la branche droite. 2 décisions, 2 propagations, 1 conflit. La recherche aboutit à un modèle.

Ce qui se passe, étape par étape

Décision $x = 1$ . Un pari, rien ne l'imposait. La variable $x$ a été choisie parce qu'elle vient en premier ; un autre choix aurait donné un autre arbre.

Propagation $z = 1$ . La clause $c_2 = (\neg x \vee z)$ voit son premier littéral devenir faux : elle est unitaire, et impose $z$ . Ce n'est pas un choix.

Conflit sur $c_3$ . La clause $(\neg x \vee \neg z)$ a maintenant ses deux littéraux faux. La branche est morte, et il faut défaire la dernière décision.

Décision $x = 0$ . L'autre valeur du pari. C'est le retour arrière, et il ne coûte rien de plus qu'un changement de valeur.

Propagation $y = 1$ . La clause $c_1 = (x \vee y)$ devient unitaire.

Modèle. Il reste $z$ libre, et toutes les clauses sont satisfaites : $c_1$ par $y$ , $c_2$ et $c_3$ par $\neg x$ , $c_4$ par $y$ . La formule est satisfiable, par $x = 0$ , $y = 1$ , $z$ au choix.

Une variable libre dans un modèle n'est pas une erreur

DPLL s'arrête dès que toutes les clauses sont satisfaites, sans attendre que toutes les variables soient affectées. Ici

z

ne compte plus pour personne : les clauses où elle figure sont déjà satisfaites par d'autres littéraux.
Un solveur rendra pourtant une affectation complète, en donnant une valeur arbitraire aux variables restées libres. Les deux comportements sont corrects, et il vaut la peine de savoir que le solveur ne les a pas toutes décidées.

Vérification rapideon peut se reprendre

DPLL s'arrête et rend un modèle où z n'a pas de valeur. Que conclure ?

Et quand tout échoue

Voici l'autre issue, sur la formule la plus petite qui soit insatisfiable sans clause unitaire.

$c_1 = (x \vee y)$ , $\quad c_2 = (\neg x \vee y)$ , $\quad c_3 = (x \vee \neg y)$ , $\quad c_4 = (\neg x \vee \neg y)$

6 étapes

L'arbre complet. Dérouler pas à pas montre l'ordre dans lequel le solveur le parcourt, et le moment où il revient en arrière.

Les quatre clauses interdisent les quatre affectations, et les deux branches meurent de la même façon. Aucune valeur de x ne survit : la formule est insatisfiable. 2 décisions, 2 propagations, 2 conflits. Toutes les branches échouent : la formule est insatisfiable.

Ce qu'un échec de DPLL démontre. Quand les deux branches d'une décision échouent, la valeur de cette variable n'y était pour rien : c'est ce qui la précède qui est en cause.
Répété jusqu'à la racine, l'argument donne une preuve d'insatisfiabilité. Elle est même exactement une preuve par résolution, comme le chapitre précédent l'a suggéré : chaque conflit correspond à une clause dérivée, et l'arbre entier se traduit en une réfutation.
Autrement dit, DPLL est un moteur de résolution, qui choisit l'ordre des étapes par une recherche au lieu de les produire toutes. C'est ce qui lui rend la mémoire, et c'est aussi ce qui lui laisse la borne de Haken : sur le principe des tiroirs, son arbre est exponentiel.

Le littéral pur

Rappel

Un littéral est pur si son opposé n'apparaît dans aucune clause de la formule.

La règle, et pourquoi elle est sûre. Si $x$ est pur, on peut poser $x = 1$ sans risque et sans branchement.
La justification tient en une phrase. Poser $x$ à vrai satisfait toutes les clauses qui contiennent $x$ , et n'en gêne aucune autre, puisque $\neg x$ n'apparaît nulle part. Si un modèle existait avec $x = 0$ , le même modèle avec $x = 1$ en est encore un.
Ce n'est donc pas une décision : c'est une simplification qui ne coûte aucun retour arrière.

Une règle qui a disparu des solveurs modernes

Elle figure dans l'article de 1962 et dans tous les cours, et pourtant les solveurs actuels ne l'appliquent presque plus. La raison est comptable.
Détecter les littéraux purs demande de parcourir toute la formule après chaque affectation, puisque la pureté dépend des clauses encore actives. Sur un million de clauses, cela coûte plus cher que ce que la règle fait gagner.
Elle survit là où elle est bon marché : dans le prétraitement, où on la calcule une fois, et dans les solveurs de comptage de modèles, où elle joue un rôle différent. C'est un bon exemple d'une règle correcte et utile devenue non rentable à grande échelle.

Vérification rapideon peut se reprendre

1.Le littéral x est pur. Que peut-on faire ?

2.Pourquoi les solveurs modernes n'appliquent-ils presque plus la règle du littéral pur ?

Le choix de la variable

C'est le seul endroit où DPLL a une liberté, et c'est donc là que tout se joue.

Deux ordres sur la même formule

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

Cette formule est insatisfiable, et la contradiction se joue entièrement entre $a$ et $b$ . Les variables $p$ et $q$ n'y sont pour rien.

En commençant par $a$ , la contradiction apparaît en deux décisions, comme dans la figure précédente.

En commençant par $p$ , le solveur explore d'abord les valeurs de $p$ et de $q$ , qui ne mènent nulle part, et refait ensuite le raisonnement sur $a$ et $b$ dans chaque branche. Le travail est multiplié, sans qu'aucune information nouvelle ait été obtenue.

16 étapes

L'arbre complet. Dérouler pas à pas montre l'ordre dans lequel le solveur le parcourt, et le moment où il revient en arrière.

Le mauvais ordre. Le sous-arbre sur a et b est exploré deux fois à l'identique, parce que rien ne relie p à la contradiction. Six décisions au lieu de deux, pour la même conclusion. 6 décisions, 6 propagations, 4 conflits. Toutes les branches échouent : la formule est insatisfiable.

Ce que doit faire une bonne heuristique. Toucher vite à ce qui contraint. Trois idées classiques, du plus simple au plus efficace.
La plus fréquente. Choisir la variable qui apparaît dans le plus de clauses : elle en simplifie beaucoup d'un coup.
Les clauses les plus courtes d'abord. Une clause binaire est presque unitaire ; y toucher déclenche des propagations. C'est l'idée de l'heuristique de Jeroslow-Wang, qui pondère chaque littéral par $2^{-|C|}$ sur les clauses $C$ où il figure, donnant plus de poids aux clauses courtes.
Ce qui a récemment posé problème. C'est l'idée qui a tout changé, mais elle demande de garder une mémoire des conflits, ce que DPLL ne fait pas. Elle appartient au chapitre suivant.

Aucune heuristique n'est bonne partout

Il n'existe pas d'ordre universellement meilleur, et l'on sait le démontrer : pour toute heuristique fixée, il existe des formules sur lesquelles elle est exponentiellement pire qu'une autre.
Ce qui se mesure, en revanche, est le comportement en moyenne sur les instances qui intéressent. C'est pourquoi les heuristiques des solveurs actuels ne sont pas issues d'un théorème mais de trente ans de compétitions, et pourquoi elles changent encore.

Le retour arrière chronologique, et son gaspillage

Retour arrière chronologique

Quand une branche échoue, DPLL défait la dernière décision prise et essaie l'autre valeur. S'il l'a déjà essayée, il remonte encore d'un cran.

Le défaut qui a motivé tout le chapitre suivant

Reprendre la figure du mauvais ordre. Le conflit rencontré sous

a = 1

ne doit rien à

p

ni à

q

 : il vient de

c_2

et de

c_4

, où ces variables n'apparaissent pas.
DPLL l'ignore. Il défait

a

, puis

b

, puis remonte, et refait le même raisonnement dans l'autre branche de

p

. Il redécouvre une contradiction qu'il avait déjà rencontrée, parce qu'il n'a rien gardé de sa première rencontre.
Deux idées manquent, et elles arrivent ensemble au chapitre suivant : analyser le conflit pour savoir qui l'a causé, et retenir le résultat sous forme d'une clause. C'est le passage de DPLL à CDCL, et le gain se compte en ordres de grandeur.

Vérification rapideon peut se reprendre

Un conflit survient dans une branche, et la dernière décision n'apparaît dans aucune clause en cause. Que fait DPLL ?

L'implémentation, en trente lignes

Voici DPLL au complet, propagation comprise. Le solveur du chapitre 4 était déjà celui-ci.

main.py

Sortie

>_ Prêt à exécuter…

Ce que la trace montre, et ce qu'elle cache

Elle montre les décisions et les conflits, c'est-à-dire l'arbre de la première figure.
Elle cache les propagations, qui se font à l'intérieur de propage sans laisser de trace. C'est représentatif : sur une instance réelle, le nombre de propagations dépasse celui des décisions d'un facteur de dix à mille, et c'est précisément pour cela que la propagation est la partie qu'on optimise en premier. Le chapitre 9 y consacre l'essentiel de son propos.

Vérification rapideon peut se reprendre

Sur une instance réelle, le rapport entre propagations et décisions est de l'ordre de…

Mettre en pratique

L'arbre de recherche de DPLL a une taille que rien ne borne mieux que le nombre de variables. Le calculer dit ce que la propagation et les heuristiques ont à gagner.

Mesurer l'arbre de recherche

1.
Une formule porte sur 10 variables. Combien de feuilles l'arbre de recherche compte-t-il au pire ?
2.
Pour 30 variables, combien de MILLIARDS de feuilles cela fait-il au pire ? Donner la valeur à deux décimales.
3.
La propagation unitaire fixe 6 des 10 variables sans qu'aucune décision soit prise. Sur combien de variables les décisions portent-elles alors ?
4.
Combien de feuilles l'arbre compte-t-il alors au pire ?

L'écart entre la première et la dernière réponse est tout le sujet du chapitre : mille vingt-quatre feuilles contre seize. La propagation unitaire ne devine rien, elle ne fait que tirer les conséquences forcées de ce qui est déjà décidé, et elle divise l'espace de recherche par soixante- quatre au passage.

Une seule des trois opérations est un pari. La propagation unitaire et le littéral pur sont sûrs : ils ne peuvent pas faire perdre de modèle, et il n'y a donc jamais à revenir dessus. Seule la décision est un pari, et c'est la seule sur laquelle un retour arrière porte.
C'est pourquoi un solveur applique les deux premières jusqu'à épuisement avant de décider quoi que ce soit : tout ce qui est gratuit se prend d'abord.

Sur

(x) \wedge (\neg x \vee y) \wedge (\neg y \vee z)

, combien DPLL prend-il de décisions ?

Aucune.

La clause $(x)$ est unitaire dès le départ : elle impose $x = 1$ . La clause $(\neg x \vee y)$ devient alors unitaire et impose $y = 1$ , puis $(\neg y \vee z)$ impose $z = 1$ .

Toutes les clauses sont satisfaites, et le solveur n'a jamais eu à parier. C'est le cas idéal, et c'est exactement ce qui se produit sur une formule de Horn avec des faits, comme au chapitre 5.

DPLL peut-il rendre un modèle où certaines variables n'ont pas de valeur ?

Oui, et c'est correct. Il s'arrête dès que toutes les clauses sont satisfaites, ce qui peut arriver avant d'avoir touché à toutes les variables.

Une variable non affectée est une variable dont aucune clause n'a plus besoin : toutes celles où elle figure sont déjà satisfaites par d'autres littéraux. N'importe quelle valeur convient.

En pratique, un solveur complète l'affectation avant de la rendre, pour respecter le format attendu. Il vaut mieux le savoir quand on compare deux sorties : deux solveurs peuvent rendre des modèles différents sur la même instance sans qu'aucun des deux ne se trompe.

Dans

(a \vee b) \wedge (\neg b \vee c) \wedge (a \vee c)

, quels littéraux sont purs ?

Cherchons pour chaque littéral si son opposé apparaît.

$a$ figure dans $c_1$ et $c_3$  ; $\neg a$ n'apparaît nulle part : $a$ est pur. $b$ figure dans $c_1$ , $\neg b$ dans $c_2$  : ni l'un ni l'autre n'est pur. $c$ figure dans $c_2$ et $c_3$  ; $\neg c$ n'apparaît nulle part : $c$ est pur.

Poser $a = 1$ et $c = 1$ satisfait les trois clauses d'un coup, sans aucune décision et sans risque. La variable $b$ reste libre.

Pourquoi le retour arrière chronologique refait-il deux fois le même travail ?

Parce qu'il défait la dernière décision, qui n'est pas forcément la coupable.

Si le conflit vient d'une clause où la dernière décision n'apparaît même pas, la défaire ne corrige rien : le solveur va rencontrer la même contradiction dans l'autre branche, puis remonter encore, et ainsi de suite.

Le remède demande deux choses que DPLL n'a pas. Analyser le conflit pour identifier les décisions réellement en cause, ce qui permet de remonter directement au bon niveau. Et retenir une clause qui résume l'impasse, pour que la même contradiction ne soit pas redécouverte ailleurs.

C'est CDCL, et c'est le chapitre suivant.

Une propagation peut-elle faire perdre l'unique modèle d'une formule ?

Non, jamais, et c'est ce qui autorise à propager sans prévoir de retour arrière.

Une clause unitaire n'a plus qu'un littéral libre, tous les autres étant faux. Or tout modèle prolongeant l'affectation courante doit satisfaire cette clause, donc satisfaire l'un de ses littéraux, et il ne reste que celui-là.

La valeur imposée figure donc dans tous les modèles atteignables. Fixer cette valeur n'en élimine aucun.

C'est exactement l'inverse d'une décision, qui coupe la moitié des possibilités et doit pouvoir être défaite.

Trois opérations, dont une seule est un pari

Une trace, déroulée

Et quand tout échoue

Le littéral pur

Le choix de la variable

Le retour arrière chronologique, et son gaspillage

L'implémentation, en trente lignes

Mettre en pratique

Dans la bibliothèque d'exercices