Informatique et mathématiques de l'ingénieur

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. 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.

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.

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

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.

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.

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.

Exercices type

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.

Vérification rapideon peut se reprendre

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

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

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

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

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

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

La méthode

Propager d'abord, toujours, avant de songer à décider.
Vérifier les deux arrêts après chaque propagation : une clause falsifiée, ou toutes satisfaites.
Ne décider que sur une variable libre, et se souvenir que c'est le seul geste coûteux.
Chercher les littéraux purs sur les petites formules traitées à la main : ils suppriment des branches entières.
Choisir la variable la plus contrainte plutôt que la première venue.
Compter les décisions, jamais les propagations, pour estimer le coût d'une recherche.
Lire un échec des deux branches comme une preuve portant sur ce qui précède, pas sur la variable branchée.

Synthèse

DPLL fait trois choses : propager, détecter conflit ou succès, et décider.
Propager ne perd aucun modèle : le littéral forcé figure dans tous les modèles atteignables.
Décider est le seul geste qui coupe des possibilités, donc le seul qui coûte.
Un littéral pur se pose sans brancher, mais sa détection est trop chère à grande échelle.
Le retour arrière chronologique défait la dernière décision, qui n'est pas forcément la coupable.
Un mauvais ordre de branchement fait refaire le même sous-arbre plusieurs fois.
Aucune heuristique n'est optimale partout ; elles se mesurent sur les instances qui intéressent.
DPLL est un moteur de résolution : son arbre se traduit en réfutation, et la borne de Haken s'applique.
Sur une instance réelle, il y a dix à mille propagations par décision.

DPLL : chercher, et savoir revenir en arrière

Ce que ce chapitre apporte

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

Exercices type

La méthode

Synthèse