2. Résolution propositionnelle

Les tables de vérité et les transformations en sommes de monômes ou produits de clauses permettent de répondre aux questions : une formule est-elle valide ? et un raisonnement est-il correct ? Cependant le temps de réponse de ces méthodes augmente exponentiellement avec le nombre de variables. Pour illustrer cela, considérons la conséquence suivante :

a⇒b, b⇒c, c⇒d, d⇒e, e⇒f, f⇒g, g⇒h, h⇒i, i⇒j $$\models$$ a⇒j

En utilisant une table de vérité il faut tester 2¹⁰ = 1024 lignes. Or par déduction, en utilisant la transitivité de l'implication, nous savons immédiatement que le raisonnement ci-dessus est correct. Ainsi, en logique propositionnelle, les déductions peuvent s'avérer très utile, voir nécessaire lorsque la taille du problème à traiter est importante. Nous étudions maintenant un système de déduction très simple. Dans ce système, les hypothèses et les formules déduites ne sont pas des formules quelconques mais des clauses, c'est-à-dire des disjonctions de littéraux. De plus, le système comporte une seule règle appelée la résolution.

Plan :

Nous introduisons d'abord la méthode de résolution inventée en 1965 par J. Alan Robinson [23] dans le cadre plus général de la recherche de preuve au premier ordre. Nous présentons ensuite une procédure pour calculer tous les résolvants possibles, c'est-à-dire toutes les applications possibles de la règle de résolution : la stratégie complète. Puis, nous étudions l'algorithme DPLL, proposé dans les années soixante par Martin Davis, Hilary Putnam, George W. Logemann et Donald W. Loveland [10,9]. En utilisant la notion de résolution, des méthodes de simplifications et le branchement/retour arrière, cet algorithme prouve efficacement si une formule a un modèle ou non. Bien qu'inventé il y a plus de quarante ans, il est toujours à la base de la plupart des solveurs SAT complets actuels. Notons que dans ce chapitre nous adoptons la notation booléenne plus concise.

2.1 Résolution

Nous souhaitons prouver que a + c est une conséquence de a + b et $\overline{{b}}$ + c, c'est-à-dire a + b, $\overline{{b}}$ + c $\models$ a + c. En utilisant la propriété 1.2.27, il suffit de démontrer que la formule (a + b).($\overline{{b}}$ + c)⇒(a + c) est valide. Pour cela, nous pouvons utiliser une table de vérité (8 lignes) ou alors une simplification de formules comme dans l'exercice 13. Ces deux méthodes sont fastidieuses même pour des formules aussi simples (3 variables uniquement). En utilisant la règle de résolution présentée dans ce chapitre, nous déduisons directement la clause a + c à partir des deux clauses a + b et $\overline{{b}}$ + c.

Nous donnons maintenant la définition de la résolution et certaines propriétés utiles qui en dérivent. Nous prouvons ensuite la cohérence et la complétude pour la réfutation de notre système basé sur la déduction. La cohérence nous permet d'affirmer que si une clause C est obtenue par résolution à partir d'un ensemble Γ de clauses alors elle en est conséquence, c'est-à-dire tout modèle de Γ est modèle de C. La complétude pour la réfutation nous permet d'affirmer que si $\bot$ est conséquence de Γ, autrement dit si Γ est insatisfaisable, alors $\bot$ peut être retrouvé par résolution à partir de Γ.

2.1.1 Définitions

Dans un premier temps nous introduisons les notions nécessaires à la définition de la résolution. Nous rappelons que les notions de clauses et littéraux sont définies dans la section 1.4 du chapitre précédent (page ). Comme nous le verrons dans la suite deux clauses qui ont le même ensemble de littéraux jouent le même rôle dans la résolution. Aussi, nous définissons deux clauses égales comme étant deux clauses avec le même ensemble de littéraux.

Définition 2.1.1 (Éléments d'une clause, clauses égales et sous-clauses)  

• Un littéral est élément d'une clause, s'il est élément de l'ensemble des littéraux de la clause.
• Une clause A est incluse dans une clause B, si tous les littéraux de la clause A sont éléments de la clause B. Dans ce cas, A est une sous-clause de B.
• Deux clauses sont égales si elles ont le même ensemble de littéraux.

Exemple 2.1.2   Nous illustrons les notions introduites par des exemples simples :

Notation : Nous notons s(A) l'ensemble des littéraux de la clause A. Par convention $\bot$ est la clause vide et s($\bot$) = ∅.

Exemple 2.1.3   s($\overline{{q}}$ + p + r + p + $\overline{{p}}$) =

Dans l'exercice 37 nous demandons de formaliser ce qu'est une clause et son ensemble de littéraux. Nous introduisons la notion de littéral complémentaire, noté L^c pour un littéral L, afin de manipuler dans nos raisonnements uniquement des littéraux. En effet, la négation ne suffit pas car $\overline{{\overline{L}}}$ est équivalent à L mais n'est pas un littéral : un littéral est une variable ou la négation d'une variable mais la double négation d'une variable n'est pas un littéral.

Définition 2.1.4 (Littéral complémentaire)   Notons L^c le littéral complémentaire d'un littéral L, défini par :

• Si L est une variable, L^c est la négation de L.
• Si L est la négation d'une variable, L^c est obtenue en enlevant la négation de L.

Exemple 2.1.5   x^c = $\overline{{x}}$ et $\overline{{x}}^{c}_{}$ = x.

Nous présentons le calcul de résolvant entre deux clauses, ce qui constitue l'unique règle du système de résolution.

Définition 2.1.6 (Résolvant)   Soient A et B deux clauses. La clause C est un résolvant de A et B si et seulement s'il y a un littéral L tel que L∈s(A), L^c∈s(B) et s(C) = (s(A) - {L})∪(s(B) - {L^c}). Nous utilisons la représentation suivante lorsque C est un résolvant de A et B :

$$\inferrule{A \ B}{C}$$

Si la clause C est un résolvant de A et B, alors nous disons que C est engendrée par A et B, et que A et B sont les parents de la clause C.

Exemple 2.1.7   Nous proposons quelques exemples de résolution :

Propriété 2.1.8   Si l'un des parents d'un résolvant est valide, le résolvant est valide ou contient l'autre parent.

Preuve : Cette preuve est demandée dans l'exercice 40.$\Box$

Étant données deux clauses A et B, la formule A + B n'est pas une clause si l'un des deux opérandes de la disjonction est la clause vide. Par exemple $\bot$ + p n'est pas une clause, bien que les deux opérandes de la disjonction soient des clauses. Aussi nous introduisons un nouvel opérande, $\tilde{+}$, afin de combiner la disjonction et l'élimination de $\bot$. Cet opérande va nous permettre de simplifier la définition de résolvant.

Définition 2.1.9 ( C$\tilde{+}$D)   Soient C et D deux clauses. Nous notons C$\tilde{+}$D la clause suivante :

• Si C = $\bot$ alors C$\tilde{+}$D = D,
• sinon si D = $\bot$ alors C$\tilde{+}$D = C sinon C$\tilde{+}$D = C + D.

Ajouter le littéral L à la clause C, c'est construire C$\tilde{+}$L. Munis de cette définition, nous pouvons reformuler plus simplement la règle de résolution.

Définition 2.1.10 (Résolvant)   Soient A et B deux clauses. La clause C est un résolvant de A et B si et seulement s'il y a un littéral L tel que :

• L est élément de la clause A, L^c est élément de la clause B
• C est égale à la clause A'$\tilde{+}$B' où A' = A - {L} est obtenue en enlevant L de A et B' = B - {L^c} est obtenue en enlevant L^c de B.

La combinaison de résolutions successives permet de générer de nouvelles clauses. Une clause issue de ces résolvants sera une preuve par résolution de cette clause à partir d'un ensemble de clauses.

Définition 2.1.11 (Preuve)   Soient Γ un ensemble de clauses et C une clause. Une preuve de C à partir de Γ est une liste de clauses qui se termine par C. Toute clause de la preuve est égale à un élément de Γ ou est un résolvant de deux clauses la précédant dans la preuve. La clause C est déduite de Γ, notée Γ $\vdash$ C, s'il y a une preuve de C à partir de Γ.

Exemple 2.1.12   Soit Γ l'ensemble de clauses $\overline{p}$ + q, p + $\overline{q}$,$\overline{p}$ + $\overline{q}$, p + q. Nous montrons que Γ $\vdash$ $\bot$ par la preuve suivante :

Nous pouvons aussi voir une preuve comme un arbre dont les feuilles sont les hypothèses et dont les sommets internes sont obtenus par construction des résolvants.

Définition 2.1.13 (Taille de preuve)   Une preuve P de C à partir d'un ensemble de clauses Γ est de taille n si elle contient n lignes.

La taille de la preuve donnée dans l'example 2.1.12 est 8, ce qui n'est pas forcément intuitif sur la représentation en arbre. Nous utiliserons les deux propriétés énoncées ci-dessous souvent de manière implicite dans les preuves.

Propriété 2.1.14 (Monotonie et composition)   Soient Γ, Δ deux ensembles de clauses et A, B deux clauses.

1. Monotonie de la déduction : Si Γ $\vdash$ A et si Γ est inclus dans Δ alors Δ $\vdash$ A
2. Composition des déductions : Si Γ $\vdash$ A, Γ $\vdash$ B et si C est un résolvant de A et B alors Γ $\vdash$ C.

Preuve : Demandée dans l'exercice 39. $\Box$

2.1.2 Cohérence

La cohérence de la résolution signifie que si une clause C est obtenue après une à plusieurs applications de la règle de résolution à un ensemble de clauses Γ alors tout modèle de Γ est aussi modèle de C (autrement dit, C est une conséquence de Γ). La première partie de la preuve consiste à démontrer la cohérence d'une application de la règle de résolution (théorème 2.1.15). Nous généralisons ensuite par induction dans le théorème 2.1.16.

Théorème 2.1.15 (Cohérence de la règle de résolution)   Si C est un résolvant de A et B alors A, B $\models$ C.

Preuve : Supposons que C soit un résolvant de A et B. Par définition il y a un littéral L tel que L∈s(A), L^c∈s(B), s(C) = (s(A) - {L})∪(s(B) - {L^c}). Soit v une assignation modèle de A et B, c'est-à-dire, [A]_v = 1 et [B]_v = 1. Montrons que v est modèle de C. Nous distinguons deux cas possibles :

$\Box$

Théorème 2.1.16 (Cohérence de la déduction)   Soient Γ un ensemble de clauses et C une clause. Si Γ $\vdash$ C alors Γ $\models$ C.

Preuve : Supposons que Γ $\vdash$ C. Par définition, il existe une preuve P de C à partir de Γ. Supposons que pour toute preuve de D à partir de Γ, plus courte que P, nous avons Γ $\models$ D. Montrons que Γ $\models$ C. Nous avons deux cas possibles :

$\Box$

Corollaire 2.1.17   D'après le théorème 2.1.16, si Γ $\vdash$ $\bot$ alors Γ $\models$ $\bot$, autrement dit Γ est insatisfaisable.

2.1.3 Complétude pour la réfutation

La complétude pour la réfutation est la propriété suivante : si Γ est un ensemble insatisfaisable de clauses, alors il y a une preuve de la clause vide à partir de Γ. Nous montrons dans la suite de cette section la complétude pour la réfutation lorsque Γ est un ensemble fini de clauses.

Nous prouvons la complétude réfutationnelle par récurrence sur le nombre de variables. Pour cela, nous construisons à partir de Γ deux ensembles de clauses contenant tous deux une variable en moins. Plus précisément, nous construisons les ensembles Γ[L : = 1] et Γ[L : = 0] en assignant un littéral L de Γ à vrai et à faux, respectivement. Nous étudions ensuite les propriétés de ces deux ensembles par rapport à Γ (lemmes 2.1.22 et 2.1.23). Ces propriétés seront utilisées lors du pas de récurrence.

Définition 2.1.18 ( Γ[L : = 1])   Soient Γ un ensemble de clauses et L un littéral. Γ[L : = 1] est l'ensemble de clauses obtenu en supprimant les clauses dont L est élément et en enlevant L^c des autres clauses. Nous posons Γ[L : = 0] = Γ[L^c : = 1].

Γ[L : = x] est égal à l'ensemble de clauses obtenu en donnant à L la valeur x (x = 0 ou x = 1) et en simplifiant le résultat obtenu.

Exemple 2.1.19   Soit Γ l'ensemble de clauses $\overline{p}$ + q,$\overline{q}$ + r, p + q, p + r. Nous avons :

• Γ[p : = 1] =
  
  
  
  
• Γ[p : = 0] =
  
  
  
  

Afin de donner une intuition de comment calculer Γ[p : = 1] et Γ[p : = 0], nous considérons le produit de clauses suivant ($\overline{p}$ + q)($\overline{q}$ + r)(p + q)(p + r) et observons :

• ($\overline{1}$ + q)($\overline{q}$ + r)(1 + q)(1 + r) =
  
  
  
  
• ($\overline{0}$ + q)($\overline{q}$ + r)(0 + q)(0 + r) =
  
  
  
  

Nous notons v[L : = 1] l'assignation qui donne à L la valeur 1, à L^c la valeur 0 et ne change pas la valeur des autres littéraux.

Définition 2.1.20 (v[L : = 1])   Soit une assignation v, l'assignation v[L : = 1] est l'assignation identique à v sauf éventuellement pour x la variable de L. Si L = x alors v[L : = 1](x) = 1, si L = $\overline{x}$ alors v[L : = 1](x) = 0.

Nous posons v[L : = 0] = v[L^c : = 1]. La propriété suivante se déduit du fait que si Γ a un modèle v, alors v donne soit la valeur 1 soit la valeur 0 au littéral L.

Propriété 2.1.21   Soient Γ un ensemble de clauses et L un littéral. Γ a un modèle si et seulement si Γ[L : = 1] ou Γ[L : = 0] a un modèle.

Preuve :

⇒

Supposons que l'assignation v soit modèle de Γ. Nous considérons deux cas selon la valeur de L dans cette assignation.

1. Supposons que v donne à L la valeur 1 et montrons que v est modèle de Γ[L : = 1]. Soit C une clause de Γ[L : = 1]. Il y a dans Γ une clause C' telle que C est obtenue en enlevant L^c de C'. Puisque v est modèle de Γ, v est modèle de C' donc d'un littéral qui n'est pas L^c (car L^c vaut 0 dans cette assignation). Par suite v est modèle de C. Puisque C est une clause quelconque de Γ[L : = 1], v est modèle de Γ[L : = 1].
2. Supposons que v donne à L la valeur 0. Nous nous ramenons au cas précédent en échangeant L et L^c et nous montrons que v est modèle de Γ[L : = 0].

⇐

Nous considérons deux cas suivant que Γ[L : = 1] ou Γ[L : = 0] a un modèle.

1. Supposons que l'assignation v soit modèle de Γ[L : = 1]. Montrons que v[L : = 1] est modèle de Γ. Soit C une clause de Γ.
   1. Supposons que L soit un littéral de C, alors v[L : = 1] est modèle de C puisque cette assignation donne à L la valeur 1.
   2. Supposons que L ne soit pas un littéral de C. Alors il y a une clause C' élément de Γ[L : = 1] telle que C' est obtenue en enlevant L^c de C. La variable de L n'est pas une variable de C'. Par suite v et v[L : = 1] donnent la même valeur à C'. Puisque v est modèle de Γ[L : = 1], v est modèle de C' donc v[L : = 1] est modèle de C'. Puisque C' est incluse dans C, v[L : = 1] est modèle de C.
   Puisque C est une clause quelconque de Γ, v[L : = 1] est modèle de Γ.
2. Supposons que l'assignation v est modèle de Γ[L : = 0]. Par une preuve analogue, nous montrons que v[L : = 0] est modèle de Γ.

$\Box$

Lemme 2.1.22   Soient Γ un ensemble de clauses, C une clause et L un littéral. Si Γ[L : = 1] $\vdash$ C alors Γ $\vdash$ C ou Γ $\vdash$ C$\tilde{+}$L^c.

Rappel : L'opération $\tilde{+}$ est introduite dans la définition 2.1.9.

Preuve : Partant d'une preuve de C à partir de Γ[L : = 1], nous obtenons une preuve de C ou de C$\tilde{+}$L^c à partir de Γ en ajoutant le littéral L^c aux clauses où nous l'avions enlevé. Formalisons cette ébauche de preuve. Supposons que Γ[L : = 1] $\vdash$ C. Il y a une preuve P de C à partir de Γ[L : = 1]. Supposons que pour toute preuve de D à partir de Γ[L : = 1], plus courte que P, nous avons Γ $\vdash$ D ou Γ $\vdash$ D$\tilde{+}$L^c. Nous avons deux cas possibles :

1. C est élément de Γ[L : = 1]. Donc il y a une clause C' élément de Γ telle que s(C') = s(C) ou s(C') = s(C)∪{L^c}. Examinons ces deux cas.
   1. Supposons s(C') = s(C). Par définition des preuves, Γ $\vdash$ C.
   2. Supposons s(C') = s(C)∪{L^c}. Nous avons s(C') = s(C$\tilde{+}$L^c) donc par définition des preuves, Γ $\vdash$ C$\tilde{+}$L^c.
2. C est résolvant de 2 clauses A et B précédant C dans la preuve P. Donc par hypothèse de récurrence :
   • Γ $\vdash$ A ou Γ $\vdash$ A$\tilde{+}$L^c.
   • Γ $\vdash$ B ou Γ $\vdash$ B$\tilde{+}$L^c.
   Ce qui donne 4 cas à examiner.
   1. Supposons Γ $\vdash$ A et Γ $\vdash$ B. Puisque C est résolvant de A et B, d'après la propriété 2.1.14, nous avons Γ $\vdash$ C.
   2. Supposons Γ $\vdash$ A et Γ $\vdash$ B$\tilde{+}$L^c. Puisque C est résolvant de A et B, il existe M tel que M∈A et M^c∈B et s(C) = (s(A) - {M})∪(s(B) - {M^c}). Aucune clause de Γ[L : = 1] ne comporte le littéral L^c. Donc B qui en est déduite, ne comporte pas le littéral L^c (voir exercice 41) et par suite L^c $\not=$M^c. Par conséquent (s(B) - {M^c})∪{L^c} = (s(B)∪{L^c}) - {M^c} = s(B$\tilde{+}$L^c) - {M^c}. Nous avons donc s(C$\tilde{+}$L^c) = (s(A) - {M})∪(s(B) - {M^c})∪{L^c} = (s(A) - {M})∪(s(B$\tilde{+}$L^c) - {M^c}). D'après la dernière égalité, C$\tilde{+}$L^c est un résolvant de A et B$\tilde{+}$L^c. Donc par la propriété 2.1.14, Γ $\vdash$ C$\tilde{+}$L^c.
   3. Supposons Γ $\vdash$ A$\tilde{+}$L^c et Γ $\vdash$ B, en échangeant ci-dessus le rôle de A et B, nous obtenons Γ $\vdash$ C$\tilde{+}$L^c.
   4. Supposons Γ $\vdash$ A$\tilde{+}$L^c et Γ $\vdash$ B$\tilde{+}$L^c, comme ci-dessus nous obtenons Γ $\vdash$ C$\tilde{+}$L^c.
   Par suite dans les quatre cas, nous avons Γ $\vdash$ C ou Γ $\vdash$ C$\tilde{+}$L^c.

$\Box$

Lemme 2.1.23   Soient Γ un ensemble de clauses, C une clause et L un littéral. Si Γ[L : = 0] $\vdash$ C alors Γ $\vdash$ C ou Γ $\vdash$ C$\tilde{+}$L.

Preuve : Supposons Γ[L : = 0] $\vdash$ C. Puisque Γ[L : = 0] = Γ[L^c : = 1] et que L^cc = L, d'après le lemme 2.1.22 nous avons Γ $\vdash$ C ou Γ $\vdash$ C$\tilde{+}$L.$\Box$

Théorème 2.1.24   Soit Γ un ensemble fini de clauses. Si Γ est insatisfaisable alors Γ $\vdash$ $\bot$.

Preuve : Supposons que Γ est insatisfaisable. Soit n le nombre de variables de Γ. Nous montrons que Γ $\vdash$ $\bot$ par récurrence sur n. Supposons que pour tout ensemble Δ de clauses insatisfaisable avec moins de n variables, nous avons Δ $\vdash$ $\bot$.

Cas de base :

Supposons que n soit nul. Donc Γ = ∅ ou Γ = {$\bot$}. Le premier cas est impossible, car l'ensemble vide est valide (toute assignation en est modèle). Donc Γ = {$\bot$} et par suite Γ $\vdash$ $\bot$.

Induction :

Supposons que n soit non nul. Soit x une variable figurant dans Γ. D'après la propriété 2.1.21, Γ[x : = 0] et Γ[x : = 1] sont insatisfaisables. Puisque la variable x ne figure pas dans ces deux ensembles de clauses, l'hypothèse de récurrence s'applique, donc : Γ[x : = 0] $\vdash$ $\bot$ et Γ[x : = 1] $\vdash$ $\bot$. Des lemmes 2.1.22 et 2.1.23, nous déduisons soit Γ $\vdash$ $\bot$, soit Γ $\vdash$ $\overline{x}$ et Γ $\vdash$ x. Dans le premier cas, la preuve est terminée. Dans le deuxième cas, puisque $\bot$ est un résolvant de $\overline{x}$ et x, nous avons également Γ $\vdash$ $\bot$.

$\Box$

Corollaire 2.1.25   Soit Γ un ensemble fini de clauses. Γ est insatisfaisable si et seulement si Γ $\vdash$ $\bot$.

Preuve : Ce corollaire est une conséquence immédiate du lemme ci-dessus et de la remarque faite au début du paragraphe 2.1.3.$\Box$

2.1.4 Réduction d'un ensemble de clauses

Réduire un ensemble de clauses, c'est lui enlever les clauses valides et les clauses contenant une autre clause de l'ensemble. Un ensemble de clauses est réduit s'il n'est plus réductible.

Définition 2.1.26 (Ensemble de clauses réduit)   Un ensemble de clauses est réduit s'il ne contient aucune clause valide et aucune clause n'est incluse dans une autre clause.

Exemple 2.1.27   La réduction de l'ensemble de clauses {p + q + $\overline{{p}}$, p + r, p + r + $\overline{{s}}$, r + q} donne l'ensemble réduit :

Propriété 2.1.28   Un ensemble de clauses E est équivalent à l'ensemble de clauses réduit obtenu à partir de E.

Preuve :

$\Box$

2.1.5 Clauses minimales pour la déduction

Définition 2.1.29 (Clause minimale pour la déduction)   Soit Γ un ensemble de clauses. Une clause minimale pour la déduction de Γ est une clause non valide déduite de Γ et ne contenant strictement aucune clause déduite de Γ.

Exemple 2.1.30   Considérons l'ensemble de clauses Γ = {a + $\overline{{b}}$, b + c + d} la clause a + c + d est minimale pour la déduction. Par contre si on rajoute la clause $\overline{{a}}$ + c à Γ alors a + c + d n'est pas minimale car nous pouvons déduire c + d qui est inclus dans la clause a + c + d.

L'algorithme de la stratégie complète, présenté dans le paragraphe suivant, construit, à partir d'un ensemble Γ de clauses, l'ensemble des clauses minimales pour la déduction de Γ.

Propriété 2.1.31   Soit Θ l'ensemble des clauses minimales pour la déduction de l'ensemble de clauses Γ. L'ensemble Γ est insatisfaisable si et seulement si $\bot$∈Θ.

Preuve :

• Supposons $\bot$∈Θ, alors Γ $\vdash$ $\bot$, donc par cohérence de la résolution, Γ est insatisfaisable.
• Supposons Γ insatisfaisable, par complétude de la résolution, Γ $\vdash$ $\bot$. Par suite $\bot$ est minimale pour la déduction de Γ, donc $\bot$∈Θ.

$\Box$

2.1.6 Clauses minimales pour la conséquence

Définition 2.1.32 (Clause minimale pour la conséquence)   Soit Γ un ensemble de clauses. Une clause minimale pour la conséquence de Γ est une clause non valide conséquence de Γ et ne contenant strictement aucune clause conséquence de Γ.

Exemple 2.1.33   Considérons l'ensemble de clauses Γ = {a + d,$\overline{{a}}$ + b,$\overline{{b}}$ + c}. La clause d + c est minimale pour la conséquence de Γ.

Conséquence :

d + c est une conséquence de Γ car dans tout modèle de Γ soit d est vrai soit c est vrai. Pour s'en convaincre essayons de construire un modèle où d et c sont faux. Dans ce cas pour satisfaire la première et la dernière clause de Γ, il faut que a = 1 et b = 0 dans le modèle ce qui rend faux la seconde clause de Γ.

Minimalité :

Il existe des modèles de Γ qui ne sont pas modèles de d (respectivement c) : a = 1, d = 0, c = 1 et b = 1 (respectivement a = 0, d = 1, c = 0 et b = 0).

Nous montrons ci-dessous, qu'une clause est minimale pour la déduction d'un ensemble de clauses si et seulement si elle est minimale pour la conséquence de ce même ensemble de clauses.

Propriété 2.1.34   Soit Γ un ensemble de clauses. Pour toute clause C non valide, conséquence de Γ, il existe une sous-clause de C déduite de Γ.

Preuve : Soient C une clause non valide, conséquence de Γ et Γ' = Γ∪{L^c | L∈C}. Une assignation v est modèle de Γ' si et seulement si v est modèle de Γ et n'est pas modèle de C, donc, puisque C est conséquence de Γ, Γ' est insatisfaisable. De plus, par complétude réfutationnelle, nous obtenons Γ' $\vdash$ $\bot$.

Nous montrons la propriété (P) suivante : pour toute clause D déduite de Γ' :

• Soit D est le complémentaire d'un littéral de C.
• Soit il existe une clause E telle que E⊂C et D∪E est déductible de Γ.

En appliquant la propriété (P) à la clause vide qui est déduite de Γ', il en résulte qu'il existe une sous-clause de C déduite de Γ.

La preuve de la propriété (P) est une preuve par induction sur la longueur n de la preuve par résolution de D. Le cas de base pour n = 0 est immédiat, car D∈Γ. Supposons que pour toute preuve de longueur inférieure à n la propriété (P) soit vraie. Nous distinguons deux cas :

1. Supposons D∈Γ', donc soit D est le complémentaire d'un littéral de C, soit D∈Γ et par suite D est déduite de Γ, donc la propriété (P) est vraie.
2. Supposons D $\not\in$Γ'. Donc D est le résolvant de deux clauses E et F ayant une preuve de longueur inférieure à n. Par suite, il existe un littéral L avec L∈E, L^c∈F et D = (E - {L})∪(F - {L^c}). Puisque C n'est pas valide, la résolution ne peut pas être appliquée à deux clauses qui sont des littéraux complémentaires de ceux de C. Donc au moins l'une des clauses E, F n'est pas un littéral complémentaire d'un littéral de C. Supposons que cette clause non complémentaire d'un littéral de C soit la clause E. Par hypothèse de récurrence, il existe une clause G telle que G⊂C et E∪G est déductible de Γ. Nous distinguons deux cas, suivant que F soit ou ne soit pas le complémentaire d'un littéral de C.
   1. F est le complémentaire d'un littéral de C. Dans ce cas, F est le littéral L^c et D = E - {L}. De plus, comme L∈E, nous avons L $\not\in$D et E = D∪{L}. Ensuite, puisque G⊂C, nous avons (G - {L})⊂C. Puisque E∪G = D∪{L}∪G et F = {L^c} sont déductibles de Γ (par hypothèse de récurrence) et D∪(G - {L}) est un résolvant de E∪G et F, nous pouvons conclure que D∪(G - {L}) est déductible de Γ. Ainsi, la propriété est vérifiée pour D.
   2. F n'est pas le complémentaire d'un littéral de C. Par hypothèse de récurrence, il existe une clause H telle que H⊂C et F∪H est déductible de Γ. Puisque G⊂C et H⊂C, nous avons G∪H⊂C. Puisque E∪G ainsi que F∪H sont déductibles de Γ et que D est un résolvant de E et F, alors D∪(G∪H) est un résolvant de E∪G et de F∪H et par suite est aussi déductible de Γ. Donc la propriété (P) est vérifiée pour D.

$\Box$

Remarquons que cette propriété généralise la propriété de la complétude réfutationnelle, si la clause vide est conséquence d'un ensemble de clauses, alors elle en est déduite.

Théorème 2.1.35   Soit Γ un ensemble de clauses. Une clause est minimale pour la déduction de Γ si et seulement si elle est minimale pour la conséquence de Γ.

Preuve : Nous effectuons une preuve par double implications.

⇒

Soit C une clause minimale pour la déduction de Γ. Par cohérence de la résolution, Γ $\models$ C. Nous supposons que C ne soit pas minimale pour la conséquence et cherchons une contradiction. Dans ce cas, il existerait une clause D, sous-clause stricte de C et conséquence de Γ. Puisque C n'est pas valide, D aussi n'est pas valide, d'après la propriété 2.1.34, il existerait E sous-clause de D déduite de Γ. Donc, contrairement à l'hypothèse, C ne serait pas minimale pour la déduction. Par suite, C est minimale pour la conséquence.

⇐

Soit C minimale pour la conséquence de Γ. Puisque C n'est pas valide, d'après la propriété 2.1.34, il existe D, une sous-clause de C déduite de Γ. Par cohérence de la résolution, D est conséquence de Γ. Et puisque C est minimale, D = C, donc C est déduite de Γ. Nous supposons que C ne soit pas minimale pour la déduction. Il existerait D, sous-clause stricte de C, déduite de Γ. Par cohérence de la résolution, D serait conséquence de Γ. Donc, contrairement à l'hypothèse, C ne serait pas minimale pour la conséquence. Par suite, C est minimale pour la déduction.

$\Box$

2.2 Stratégie complète

Pour savoir si un ensemble fini Γ de clauses est contradictoire, il y a une méthode simple mais peu efficace : construire toutes les clauses que nous pouvons déduire de Γ. D'après le corollaire 2.1.25, Γ est contradictoire si et seulement si la clause vide a été construite. Il faut préciser ce que nous entendons par construire toutes les clauses déduites de Γ. Si nous considérons comme différentes les clauses qui s'écrivent différemment, deux clauses ont une infinité de résolvants. Par exemple les clauses p + $\overline{{q}}$ et r + q ont comme résolvants la clause p + r mais aussi les clauses r + p, p + r + p, p + … + p + r + ... + r. Donc l'ensemble des clauses déduites de Γ est infini. Aussi, il faut, comme précédemment, considérer comme égales deux clauses, qui ont le même ensemble de littéraux (voir définition 2.1.1) : avec cette définition de l'égalité de deux clauses, l'ensemble des résolvants de deux clauses est fini ainsi que l'ensemble des clauses déduites de Γ. Supposons que l'ensemble des littéraux de Γ ait n éléments, comme les clauses déduites de Γ ne comportent que des littéraux de Γ (voir exercice 41), il y a donc au plus 2ⁿ clauses déduites de Γ. Pour simplifier la suite, comme ci-dessus, nous confondons une clause et son ensemble de littéraux.

2.2.1 Algorithme de la stratégie complète

Soit Γ un ensemble de clauses. Pour obtenir l'ensemble des clauses minimales déduites de Γ, on construit deux suites d'ensembles de clauses Δ_i(i≥0) et Θ_i(i≥0) en s'arrêtant au premier indice k tel que Δ_k = ∅.

1. Δ₀ est obtenu en réduisant Γ et Θ₀ est l'ensemble vide.
2. Δ_i+1 est obtenu de la façon suivante
   1. Nous construisons l'ensemble des résolvants entre les clauses de Δ_i et celles de Δ_i∪Θ_i puis nous réduisons cet ensemble.
   2. Nous enlevons de cet ensemble de résolvants, les clauses qui contiennent une clause de Δ_i∪Θ_i.
3. Θ_i+1 est obtenu en enlevant de l'ensemble Δ_i∪Θ_i les clauses qui contiennent une clause de Δ_i+1.

Nous illustrons notre algorithme par deux exemples.

Exemple 2.2.1   Nous appliquons l'algorithme à l'ensemble de clauses a + b + $\overline{{a}}$, a + b, a + b + c, a + $\overline{b}$,$\overline{a}$ + b,$\overline{a}$ + $\overline{b}$. L'algorithme effectue alors le calcul suivant. L'ensemble Δ₀ comprend les clauses :

L'ensemble Θ₀ est vide. L'algorithme calcule les résolvants non valides suivants :

Donc l'ensemble Δ₁ comprend les mêmes clauses que nous numérotons de 5 à 8.

L'ensemble Θ₁ est

L'ensemble Δ₂ comprend la clause :



L'ensemble Θ₂ est



L'ensemble Δ₃ est



L'ensemble Θ₃ est égal à



Nous notons que l'algorithme a construit la preuve suivante :

Nous pouvons utiliser la représentation ci-dessous sous forme de tableau représentant la construction de ces ensembles.

k	Δk	Θk	Δk∪Θk	Résolvants de Δk et Δk∪Θk
0
1
2
3

Comme le montre cet exemple, les clauses de Δ_i ont des preuves de hauteur i, et celles de Θ_i des preuves de hauteur inférieure à i.

Exemple 2.2.2   L'application de la stratégie complète sur l'ensemble {a, c,$\overline{{a}}$ + $\overline{{b}}$,$\overline{{c}}$ + e} nous donne l'ensemble {a, c, e,$\overline{{b}}$}.

k	Δk	Θk	Δk∪Θk	Résolvants de Δk et Δk∪Θk
0
1
2

Nous montrons que l'algorithme se termine et qu'il est correct, c'est-à-dire que l'ensemble Θ_k est l'ensemble des clauses minimales déduites de Γ. D'après la propriété 2.1.31, Γ est insatisfaisable si et seulement si la clause vide est élément de Θ_k.

2.2.2 Arrêt de l'algorithme

Soit n le nombre de littéraux de Γ. Les clauses éléments des Δ_i sont des clauses déduites de Γ, donc, comme nous l'avons rappelé ci-dessus, elles ne comportent que des littéraux de Γ. Par suite, l'ensemble $\bigcup_{{ i < k}}^{}$Δ_i comprend au plus 2ⁿ clauses. D'après l'algorithme, les ensembles Δ_i sont non vides pour i < k. Nous montrons ci-dessous que ces ensembles sont disjoints. Par conséquent k≤2ⁿ + 1, autrement dit l'algorithme s'arrête.

Propriété 2.2.3   Soit i≤k. Toute clause de $\bigcup_{{j \le i}}^{}$Δ_j contient une clause de Δ_i∪Θ_i.

Preuve : Nous effectuons une preuve par induction.

• Pour i = 0 la propriété est triviale car Θ₀ = ∅.
• Supposons la propriété vraie au rang i et montrons qu'elle reste vraie au rang i + 1. Soit C∈$\bigcup_{{j \le i+1}}^{}$Δ_j. Montrons que C contient une clause de Δ_i+1∪Θ_i+1. Nous examinons tous les cas possibles pour C.
  1. C∈Δ_i+1. Donc C contient une clause de Δ_i+1∪Θ_i+1.
  2. C∈$\bigcup_{{j \le i}}^{}$Δ_j. Par hypothèse de récurrence, C contient une clause D∈Δ_i∪Θ_i. Nous distinguons deux situations pour D.
     1. D∈Θ_i+1. Donc C contient une clause de Δ_i+1∪Θ_i+1.
     2. D $\not\in$Θ_i+1. Par construction de Θ_i+1, puisque D∈Δ_i∪Θ_i et que D $\not\in$Θ_i+1, c'est que D contient une clause de Δ_i+1. Or C contient D, donc C contient aussi une clause de Δ_i+1∪Θ_i+1.

$\Box$

Propriété 2.2.4   Pour tout i≤k, les ensembles Δ_i sont disjoints entre eux.

Preuve : Nous effectuons une récurrence sur les ensembles Δ_j avec 0≤j≤i et i≤k.

Case de base :

Si i = 0, il n'y a qu'un seul ensemble, donc la propriété est vérifiée.

Récurrence :

Soit i < k. Supposons que tous les ensembles Δ_j où j≤i sont disjoints entre eux.

Montrons que Δ_i+1 est disjoint de ces ensembles.
Soit C∈Δ_i+1. Supposons, au contraire, que C∈$\bigcup_{{j \le i}}^{}$Δ_j. D'après la propriété précédente, C inclut une clause de Δ_i∪Θ_i. Donc par construction de Δ_i+1, C $\not\in$Δ_i+1, contradiction. Par suite, C $\not\in$$\bigcup_{{j \le i}}^{}$Δ_j.

$\Box$

2.2.3 Le résultat de l'algorithme est équivalent à l'ensemble initial de clauses

Nous montrons ci-dessous que l'ensemble Θ_k est équivalent à Γ.

Propriété 2.2.5   Pour tout i < k, les ensembles Δ_i∪Θ_i et Δ_i+1∪Θ_i+1 sont équivalents.

Preuve :

1. Toute clause de Δ_i+1∪Θ_i+1 est conséquence de Δ_i∪Θ_i. En effet toute clause de Δ_i+1∪Θ_i+1 est élément de Δ_i∪Θ_i ou résolvant de deux éléments de cet ensemble, donc est conséquence de cet ensemble.
2. Toute clause de Δ_i∪Θ_i est conséquence de Δ_i+1∪Θ_i+1. Soit C∈Δ_i∪Θ_i. Nous distinguons deux cas possibles :
   1. C∈Θ_i+1, ainsi C est conséquence de Δ_i+1∪Θ_i+1.
   2. C $\not\in$Θ_i+1, ainsi C contient une clause de Δ_i+1 donc est conséquence de Δ_i+1∪Θ_i+1.

$\Box$

Propriété 2.2.6   Les ensembles Γ et Θ_k sont équivalents.

Preuve : Par définition Δ₀ est l'ensemble obtenu par réduction de Γ, d'après la propriété 2.1.28, ces deux ensembles sont équivalents. Puisque Θ₀ est vide, Γ est équivalent à Δ₀∪Θ₀. D'après la propriété 2.2.5 et par récurrence, Δ₀∪Θ₀ est équivalent à l'ensemble de clauses Δ_k∪Θ_k. Puisque l'algorithme termine quand Δ_k est l'ensemble vide, les ensembles Γ et Θ_k sont équivalents.$\Box$

2.2.4 Le résultat de l'algorithme est l'ensemble des clauses minimales pour la déduction de l'ensemble initial de clauses

Nous montrons que l'ensemble Θ_k est l'ensemble des clauses minimales pour la déduction de Γ.

Propriété 2.2.7   Toute clause de Δ_i (où i≤k) a une preuve sans tautologie de hauteur i à partir de Γ. Toute clause de Θ_i (où i≤k) a une preuve sans tautologie de hauteur inférieure à i à partir de Γ.

Preuve : Nous effectuons une preuve par récurrence sur i.

• Pour i = 0, c'est évident.
• Admettons cette propriété au rang i et montrons qu'elle reste vraie au rang i + 1. Soit C∈Δ_i+1, par construction C est un résolvant entre une clause D∈Δ_i et une clause E∈Δ_i∪Θ_i et C n'est pas une tautologie. Par hypothèse de récurrence, D a une preuve, sans tautologie, de hauteur i , à partir de Γ, et E a une preuve, sans tautologie, de hauteur au plus i, à partir de Γ. Donc C a une preuve, sans tautologie, de hauteur i + 1, à partir de Γ. Soit C∈Θ_i+1, par construction C∈Δ_i∪Θ_i, donc par hypothèse de récurrence, C a une preuve sans tautologie à partir de Γ de hauteur au plus i.

$\Box$

Propriété 2.2.8   Pour tout i≤k, l'ensemble Δ_i∪Θ_i est réduit.

Preuve : Nous faisons un raisonnement par récurrence.

• Pour i = 0, c'est évident car l'ensemble Δ₀ est obtenu par réduction de Γ et que Θ₀ = ∅.
• Supposons que l'ensemble Δ_i∪Θ_i soit réduit. Montrons qu'il en est de même de l'ensemble Δ_i+1∪Θ_i+1. Par construction, l'ensemble Δ_i+1 est réduit. Par construction, l'ensemble Θ_i+1 est un sous-ensemble de Δ_i∪Θ_i, donc par hypothèse de récurrence, il est réduit. Supposons que l'ensemble Δ_i+1∪Θ_i+1 ne soit pas réduit, il n'y a que deux possibilités :
  1. C∈Δ_i+1 contient une clause D∈Θ_i+1 : par construction de Θ_i+1, D∈Δ_i∪Θ_i, ce qui implique, par construction C $\not\in$Δ_i+1. Nous avons une contradiction.
  2. C∈Θ_i+1 contient une clause D∈Δ_i+1 : par construction de Θ_i+1, ce cas est aussi impossible.

Par suite, l'ensemble Δ_i+1∪Θ_i+1 est réduit.$\Box$

Propriété 2.2.9   Pour tout i≤k, Θ_i⊂$\bigcup_{{j < i}}^{}$Δ_j.

Preuve : Nous montrons le résultat par induction sur i.

• Pour i = 0, la propriété est vraie car Θ₀ est vide.
• Supposons que pour i < k, nous avons : Θ_i⊂$\bigcup_{{j < i}}^{}$Δ_j. Par construction, Θ_i+1 est un sous-ensemble de Δ_i∪Θ_i. En utilisant l'hypothèse de récurrence, c'est donc un sous-ensemble de $\bigcup_{{j < i+1}}^{}$Δ_j.

$\Box$

Propriété 2.2.10   Pour tout i≤k, un résolvant non valide de deux clauses de Θ_i contient une clause de Δ_i∪Θ_i.

Preuve : Par induction sur i nous avons :

• Pour i = 0, la propriété est vraie car Θ₀ est vide.
• Supposons la propriété vérifiée pour i < k. Soient C, D∈Θ_i+1 ayant un résolvant E non valide. Montrons que E contient une clause de Δ_i+1∪Θ_i+1. D'après la propriété 2.2.9, C, D∈$\bigcup_{{j < i+1}}^{}$Δ_j. Nosu distinguons deux cas possibles :
  1. Supposons C∈Δ_i ou D∈Δ_i. Nous avons deux cas :
     1. E∈Δ_i+1, donc E contient un élément de Δ_i+1∪Θ_i+1
     2. E $\not\in$Δ_i+1, donc, par construction, soit E contient une autre clause de Δ_i+1 donc de Δ_i+1∪Θ_i+1, soit E contient une clause F∈Δ_i∪Θ_i. Nous distinguons deux cas pour F :
        1. F∈Θ_i+1 donc E contient F∈Δ_i+1∪Θ_i+1.
        2. F $\not\in$Θ_i+1 donc, par construction de cet ensemble, F inclut une clause G∈Δ_i+1. Donc E contient G∈Δ_i+1∪Θ_i+1.
        Ainsi dans ces deux cas, E contient une clause élément de Δ_i+1∪Θ_i+1.
  2. Supposons C $\not\in$Δ_i et D $\not\in$Δ_i. Puisque les clauses de Θ_i+1 sont des clauses de Δ_i∪Θ_i, nous avons donc C, D∈Θ_i. Par hypothèse de récurrence, E contient une clause F∈Δ_i∪Θ_i. Comme dans le cas précédent, nous en déduisons que E contient une clause de Δ_i+1∪Θ_i+1.

Par suite, dans ces deux cas, E contient une clause de Δ_i+1∪Θ_i+1.$\Box$

Propriété 2.2.11   Si la clause C contient une clause de Δ_i∪Θ_i alors, pour tout j tel que i≤j≤k, C contient une clause de Δ_j∪Θ_j.

Preuve : La preuve est une récurrence élémentaire sur j.

• Pour j = i, la propriété est triviale.
• Supposons que C contient une clause D∈Δ_j∪Θ_j où i≤j < k. Montrons que C contient une clause de Δ_j+1∪Θ_j+1. Nous distinguons deux cas pour D.
  1. D∈Θ_j+1 : donc C contient une clause de Δ_j+1∪Θ_j+1.
  2. D $\not\in$Θ_j+1. Par construction de Θ_j+1, D contient E où E∈Δ_j+1. Donc C contient une clause de Δ_j+1∪Θ_j+1.
  Ainsi dans les deux cas, C contient une clause de Δ_j+1∪Θ_j+1.

$\Box$

Propriété 2.2.12   Toute clause non valide déduite de Γ contient un élément de Θ_k.

Preuve : Supposons que toute clause non valide ayant une preuve de longueur inférieure à n à partir de Γ contienne un élément de Θ_k. Soit C une clause non valide déduite de Γ par une preuve de longueur n. Montrons que C contient une clause de Θ_k. Soit C∈Γ, soit C est résolvant de deux clauses D et E précédant C dans la preuve de C. Examinons ces deux cas.

1. C∈Γ. Puisque C n'est pas valide et que Δ₀ est obtenu par réduction de Γ, C contient une clause de Δ₀. Puisque Θ₀ est vide, C contient une clause de Δ₀∪Θ₀. D'après la propriété 2.2.11, C contient une clause de Δ_k∪Θ_k donc de Θ_k, puisque Δ_k est vide.
2. C est résolvant de D et E, clauses déduites de Γ par des preuves de longueurs inférieures à n. D'après la propriété 2.1.8, si D et E étaient valides, il en serait de même de C, donc l'une des clauses D, E n'est pas valide.
   1. Supposons E valide. Donc D n'est pas valide et, par hypothèse de récurrence, contient D'∈Θ_k. Puisque, d'après cette même propriété 2.1.8, C contient D, C contient un élément de Θ_k.
   2. Supposons D valide. De façon analogue, C contient un élément de Θ_k.
   3. Supposons que ni D, ni E ne soient valides. Par hypothèse de récurrence, D contient D'∈Θ_k et E contient E'∈Θ_k. Puisque C est résolvant de D et E, il existe un littéral L tel que L∈D, L^c∈E et C = (D - {L})∪(E - {L^c}). Examinons les deux cas exhaustifs suivants :
      1. Supposons L $\not\in$D' ou L^c $\not\in$E'. Nous avons D'⊂C ou E'⊂C. Par suite, C contient un élément de Θ_k.
      2. Supposons L∈D' et L^c∈E'. Soit C' = (D' - {L})∪(E' - {L^c}). C' est un résolvant de D' et E' et C contient C'. D'après la propriété 2.2.10, puisque D' et E' sont éléments de Θ_k, C' est élément de Δ_k∪Θ_k, donc de Θ_k, puisque Δ_k est vide. Donc C contient un élément de Θ_k.

Ainsi dans tous les cas, C contient un élément de Θ_k.$\Box$

Propriété 2.2.13   Θ_k est l'ensemble des clauses minimales pour la déduction de Γ.

Preuve :

1. Soit C une clause minimale pour la déduction de Γ. Montrons que C∈Θ_k. Puisque C est une clause non valide déduite de Γ, d'après la propriété 2.2.12, C contient une clause D∈Θ_k. D'après la propriété 2.2.7, la clause D est aussi déduite de Γ et puisque C est minimale pour la déduction de Γ et que C contient D, nous avons C = D, donc C∈Θ_k.
2. Soit C∈Θ_k. Montrons que C est minimale pour la déduction de Γ. Supposons, au contraire, que C contienne strictement une clause D déduite de Γ. D'après la propriete 2.2.12, D contient une clause de Θ_k, donc C∈Θ_k contient strictement une clause de Θ_k. Par suite, l'ensemble Θ_k ne serait pas réduit, ce qui contredit la propriété 2.2.8. En effet d'après cette propriété, l'ensemble Δ_k∪Θ_k est réduit et, puisque Δ_k est vide, l'ensemble Θ_k est réduit.

$\Box$

2.3 Algorithme de Davis-Putnam-Logemann-Loveland

La méthode de Davis-Putnam-Logemann-Loveland ( DPLL) fut crée en 1960 par Martin Davis et Hillary Putnam, puis améliorée en 1962 par Martin Davis, George Logemann et Donald Loveland. L'algorithme DPLL permet de décider si un ensemble de clauses est satisfaisable. Bien que cet algorithme date de plus de 50 ans, de nombreuses variantes en sont encore étudiées, car il est bien meilleur que ceux précedemment étudiés (table de vérité, transformation en somme de monômes ou produit de sommes, stratégie complète). Nous remarquons d'abord qu'il y a deux types de transformations de formules :

1. Celles qui préservent le sens, c'est-à-dire transforment une formule en une autre formule équivalente.
2. Celles qui préservent seulement la satisfaisabilité, c'est-à-dire transforment une formule satisfaisable en une autre formule satisfaisable.

L'efficacité de l'algorithme DPLL vient de l'utilisation des transformations préservant seulement la satisfaisabilité, car ces transformations sont moins coûteuses que celles préservant le sens. Nous introduisons d'abord la suppression des clauses contenant des littéraux isolés, puis la résolution unitaire et enfin la simplification des clauses valides. Ces transformations constituent les briques de base de l'algorithme DPLL. L'idée principale de cet algorithme, partant d'un ensemble de clauses «irréductibles », est de choisir une variable et de considérer les deux situations possibles : le cas où elle est vraie et le cas où elle est fausse. Ainsi les deux ensembles de clauses obtenus peuvent éventuellement se simplifier, sinon le choix d'une nouvelle variable est nécessaire. Dans le pire des cas il s'agit de construire la table de vérité correspondante aux clauses, mais en pratique de nombreuses simplifications apparaissent et permettent à cet algorithme de conclure efficacement.

2.3.1 Suppression des clauses contenant des littéraux isolés

Comme nous ne cherchons pas à préserver l'équivalence de formule mais la satisfiabilité, nous avons la liberté de choisir la valeur de certaines variables. En particulier une variable qui n'apparaît que sous la forme d'un littéral positif ou négatif sera dite isolée. Nous pouvons alors affecter la valeur adéquate à cette variable afin de rendre vraies toutes les occurrences du littéral associé, ceci sans changer la satisfiabilité de l'ensemble de clauses considéré.

Définition 2.3.1 (Littéral isolé)   Soient Γ un ensemble de clauses et L un littéral élément d'une clause de Γ, L est un littéral isolé (relativement à Γ), si aucune clause de Γ ne comporte de littéral complémentaire de L.

Lemme 2.3.2   La suppression des clauses qui comportent un littéral isolé, préserve la satisfaisabilité.

La preuve est demandée dans l'exercice 48.

Exemple 2.3.3   Soit Γ l'ensemble de clauses {p + q + r,$\overline{q}$ + $\overline{r}$, q + s,$\overline{s}$ + t}.

2.3.2 Résolution unitaire

Définition 2.3.4   Une clause unitaire est une clause qui ne comporte qu'un littéral.

Les clauses unitaires sont aussi des clauses particulières qui sont :

• soit isolées et donc seront traitées par la simplification précédente,
• soit de potentiels résolvants, dans ce cas il faut effectuer la résolution dite «unitaire » de ces clauses.

Lemme 2.3.5   Soit Γ un ensemble de clauses. Soit L l'ensemble des littéraux des clauses unitaires de Γ. Soit Θ l'ensemble de clauses ainsi obtenu à partir de Γ :

• Si L comporte deux littéraux complémentaires, alors Θ = {$\bot$}.
• Sinon Θ est obtenu ainsi :

  •

  Nous enlevons les clauses qui comportent un élément de L.

  •

  À l'intérieur des clauses restantes nous enlevons les littéraux complémentaires des éléments de L.

Γ a un modèle si et seulement si Θ en a un.

La preuve est demandée dans l'exercice 49.

Exemple 2.3.6  

• Soit Γ l'ensemble de clauses : p + q,$\overline{{p}}$,$\overline{{q}}$.
  
  
  
  
• Soit Γ l'ensemble de clauses : a + b + $\overline{d}$,$\overline{a}$ + c + $\overline{d}$,$\overline{b}$, d,$\overline{c}$.
  
  
  
  
• Soit Γ l'ensemble de clauses : p, q, p + r,$\overline{p}$ + r, q + $\overline{r}$,$\overline{q}$ + s.
  
  
  
  

2.3.3 Suppression des clauses valides

Enfin la dernière transformation utilisée dans l'algorithme DPLL est de simplement enlever les clauses valides d'un ensemble de clauses. Ceci peut paraître une évidence mais cette transformation est une des idées centrales de cet algorithme, une fois une variable affectée à une valeur, elle est implicitement utilisée dans la suppression de clauses contenant des littéraux isolés.

Lemme 2.3.7   Soit Γ un ensemble de clauses. Soit Θ l'ensemble de clauses obtenu en supprimant les clauses valides de Γ. Γ a un modèle si et seulement si Θ en a un.

Preuve :

• Supposons que Γ a un modèle v, comme Θ est un sous-ensemble des clauses de Γ, v est aussi modèle de Θ. Donc, Θ a un modèle.
• Supposons que Θ a un modèle v. Soit v' une assignation de Γ telle que v'(x) = v(x) pour toute variable x présente à la fois dans Γ et Θ. Soit C une clause de Γ. Si C est aussi une clause de Θ, alors v' est un modèle de C car v et v' donnent la même valeur à C. Si C n'est pas une clause de Θ, alors C est valide, en conséquence toute assignation, v' en particulier, est modèle de C. D'où, Γ a un modèle: v'.

$\Box$

2.3.4 L'algorithme

Nous donnons une version de l'algorithme DPLL dans la figure 2.1 dans la fonction Algo_DPLL. Nous pouvons constater dans l'algorithme que nous supprimons une seule fois les clauses valides avant de réellement commencer les simplifications. Cela se justifie par le fait que l'algorithme ne pourra pas produire de nouvelles clauses valides. En effet, il ne fait qu'enlever des littéraux des clauses initialement données. Par suite, il est inutile d'enlever des clauses valides lors de l'étape de réduction, puisqu'il n'y aura plus de telles clauses. La fonction DPLL teste d'abord si la clause vide a été générée, puis effectue les simplifications possibles avant de choisir une variable pour appliquer récursivement la même fonction dans le cas où cette variable est affectée à vraie et dans le cas où elle est affectée à faux.

Figure 2.1: Algorithme de Davis-Putnam-Logemann-Loveland.

bool fonction Algo_DPLL( Γ : ensemble de clauses)
0	Supprimer les clauses valides de Γ.
	Si Γ = ∅, retourner (vrai).
	Sinon retourner (DPLL(Γ))
bool fonction DPLL( Γ : ensemble de clauses non valides)
La fonction retourne vrai si et seulement si Γ est satisfaisable
1	Si $\bot$∈Γ, retourner(faux).
	Si Γ = ∅, retourner (vrai).
2	Réduire Γ : il suffit d'enlever toute clause contenant une autre clause.
3	Enlever de Γ les clauses comportant des littéraux isolés (cf. paragraphe 2.3.1).
	Si l'ensemble Γ a été modifié, aller en 1.
4	Appliquer à Γ la résolution unitaire (cf paragraphe 2.3.2).
	Si l'ensemble Γ a été modifié, aller en 1.
5	Choisir x une variable quelconque de Γ
	retourner (DPLL( Γ[x : = 0]) ou alors DPLL( Γ[x : = 1]))

 

Pour obtenir une trace de l'algorithme, nous supprimons les clauses valides, en abrégé VAL, puis nous dessinons l'arbre des appels avec l'argument de la fonction ainsi que les ensembles obtenus par les étapes 2 (réduction, en abrégé RE), 3 (enlèvement des clauses ayant des littéraux isolés, en abrégé ELI) et 4 (résolution unitaire, abrégé en RU). À cause du «ou alors», il est inutile de poursuivre la construction de cet arbre dès que la réponse vrai (attachée à un ensemble vide) a été obtenue.

Exemple 2.3.8   Nous illustrons l'application de cet algorithme sur deux ensembles de clauses.

• Soit Γ l'ensemble de clauses : $\overline{a}$ + $\overline{b}$, a + b,$\overline{a}$ + $\overline{c}$, a + c,$\overline{b}$ + $\overline{c}$, b + c. Nous donnons la trace de l'algorithme.
  
  
  
  

• Soit Γ l'ensemble de clauses : $\overline{p}$ + $\overline{q}$,$\overline{p}$ + s, p + q,$\overline{p}$ + $\overline{s}$. Nous donnons la trace de l'algorithme.

  
  
  
  
  

Théorème 2.3.9   L'algorithme Algo_DPLL est correct.

Preuve : La réduction et les transformations 2.3.1, 2.3.2 et 2.3.3 préservent l'existence d'un modèle, donc au pas 0 et 1, l'algorithme vérifie l'invariant suivant : la valeur courante de l'ensemble de clauses de Γ a un modèle si et seulement si Γ a un modèle. Nous en déduisons immédiatement que les réponses de l'algorithme, fournies au pas 0 ou 1, sont correctes. Au pas 5, pour les mêmes raisons, la valeur courante de l'ensemble de clauses de Γ, lors de l'appel de DPLL, a un modèle si et seulement si Γ a un modèle. Supposons les appels récursifs corrects :

• Si DPLL( Γ[x : = 0]) est vrai, par récurrence Γ[x : = 0] est satisfaisable donc Γ est satisfaisable (nous utilisons le résultat 2.1.21 : Γ est satisfaisable ssi Γ[x : = 0] est satisfaisable ou Γ[x : = 1] est satisfaisable), ce qui correspond à la valeur vrai de DPLL(Γ).
• Si DPLL( Γ[x : = 0]) est faux, par récurrence Γ[x : = 0] est insatisfaisable. Dans ce cas, DPLL(Γ) vaut DPLL( Γ[x : = 1]) :
  • Supposons que DPLL( Γ[x : = 1]) soit vrai alors par récurrence Γ[x : = 1] est satisfaisable donc Γ est satisfaisable, ce qui correspond à la valeur vrai de DPLL(Γ).
  • Supposons que DPLL( Γ[x : = 1]) soit faux, alors par récurrence Γ[x : = 1] est insatisfaisable. Donc Γ est insatisfaisable, ce qui correspond à la valeur faux de DPLL(Γ).

$\Box$

Théorème 2.3.10   L'algorithme Algo_DPLL se termine.

Preuve : Au pas 0, la fonction Algo_DPLL consiste en un test, puis soit le renvoi de la valeur vrai soit l'appel de la fonction DPLL(Γ). Le pas 0 consiste en la suppression de clauses de l'ensemble de départ, cet ensemble étant fini, le pas 0 termine. Donc, la fonction Algo_DPLL termine si la fonction DPLL(Γ) termine.

Considérons un appel de la fonction DPLL(Γ). Le pas 1 est constitué d'un test et d'instructions élémentaires, donc il termine. Le pas 2 consiste à réduire Γ qui est un ensemble fini. La réduction consistant à supprimer des clauses, elle termine. Le pas 3 consiste à supprimer des clauses, puis éventuellement retourner au pas 1. Le nombre de clauses étant fini, soit l'algorithme termine en 1, soit le pas 4 débute. De la même manière, le pas 4 consiste à supprimer des clauses et des variables, qui sont en nombres finis, puis éventuellement retourner au pas 1. Le nombre de clauses et de variables étant fini, soit l'algorithme termine en 1, soit le pas 5 débute. Le pas 5 consiste en un ou deux appels récursifs sur un ensemble de clauses où une variable a disparu (la valeur d'une variable est fixée). Ainsi, la récurrence en 5 se termine car à chaque appel récursif le nombre de variables diminue strictement. D'où, l'algorithme Algo_DPLL termine.$\Box$

Remarque 2.3.11 (Oubli de simplifications)   L'algorithme Algo_DPLL a été donné avec les étapes de « simplification» : suppression des clauses valides (0), réduction (2), enlèvement des littéraux isolés (3) et réduction unitaire (4). L'algorithme reste correct si nous omettons ces étapes, ou si nous ne faisons qu'une partie des simplifications, ce qui est souvent le cas lorsque nous faisons une trace de l'exécution sans machine. Car sans machine il est fréquent d'oublier des simplifications, ce qui ne nuit pas car l'algorithme reste correct.

Remarque 2.3.12 (Choix de la variable)   Un bon choix pour la variable x de l'étape (5), consiste à choisir la variable qui apparaît le plus souvent. Un meilleur choix consiste à choisir la variable qui va entraîner par la suite le plus de simplifications : il faut faire des compromis entre le temps passé à choisir la «bonne» variable et l'importance des simplifications induites par ce choix. Plusieurs heuristiques classique de choix de variable sont présenté dans le paragraphe 2.3.5.1.

2.3.5 Solveurs SAT

Le problème SAT est un problème de décision qui consiste à déterminer si une formule propositionnelle en forme normale conjonctive admet ou non un modèle. Ce problème est le problème NP-complet de référence [5]. Généralement, seule une version de ce problème, appelée 3-SAT, où toutes les clauses de la formule sont constituées d'exactement trois littéraux, est considérée, car des réductions linéaires existent pour passer de SAT à 3-SAT. Un exemple de réduction SAT vers 3-SAT est étudié dans l'exercice 50.

Des programmes performants sont dédiés à la résolution du problème SAT ^2.1. Ces programmes sont appelés des solveurs SAT et sont généralement classés en deux catégories :

• Les solveurs SAT «complets » sont généralement des versions améliorées de l'algorithme DPLL. Parmi les solveurs SAT complets les plus utilisés à l'heure actuelle, nous pouvons citer par exemple zchaff, satz, march ou encore GRASP.
• Les solveurs SAT «incomplets » sont des algorithmes de semi-décision qui finissent par trouver un modèle à la formule, s'il existe et qui ne termine pas dans le cas contraire. Ces algorithmes sont fondés sur des marches aléatoires dans l'espace d'état. Dans cette catégorie, nous pouvons citer les algorithmes par exemple WalkSAT et GSAT.

Nous décrivons maintenant, de manière non-exhaustive, les principales améliorations de l'algorithme DPLL utilisées dans les solveurs SAT complets.

2.3.5.1 Heuristique de branchement

Le choix de la prochaine variable à affecter a un impact important sur la taille de l'arbre de recherche développé par DPLL. Ainsi, le choix de l'heuristique de branchement est déterminant dans les algorithmes fondés sur DPLL. Les heuristiques de branchement sont souvent basées sur des arguments syntaxiques tels que la taille des clauses, le nombre d'occurences, etc. Parmi les heuristiques les plus connues, nous pouvons citer :

MOMS :

L'heuristique MOMS (pour Maximum Occurences in Clauses of Minimum Size) consiste, comme son nom l'indique, à sélectionner la variable ayant le plus d'occurences dans les clauses les plus courtes. Les choix effectués par cette heuristique favorisent la propagation unitaire.

JW :

L'heuristique JW (pour Jeroslow-Wang) utilise également la longueur des clauses. En effet, un poids est affecté à chaque littéral en fonction de la taille des clauses où il apparaît. La possibilité qu'une variable soit sélectionnée par JW est inversement proportionnelle à la somme des tailles des clauses où elle apparaît.

UP :

Contrairement aux deux heuristiques précédentes, l'heuristique UP (pour Unit Propagation) n'est pas fondée sur des arguments syntaxiques. Cette heuristique essaie de sélectionner une variable en prévoyant à l'avance son effet sur la recherche. Elle consiste à calculer un poids pour chaque variable en fonction des simplifications qu'elle génère par propagation unitaire.

2.3.5.2 Ajout de clauses

L'idée est d'ajouter des clauses, en pré-traitement, à l'ensemble initial de clauses . Le nouvel ensemble de clauses reste équivalent à l'ensemble initial. Par exemple, nous pouvons citer la résolution restreinte qui consiste à ajouter des résolvants de taille bornée. Ce type de méthode permet de réduire la taille de l'arbre recherche en amenant aux contradictions plus tôt dans la recherche.

2.3.5.3 Analyse des conflits et retour-arrière non chronologique

Lorsque l'algorithme DPLL atteint une contradiction (un conflit), il revient (chronologiquement) au dernier branchement de variable effectué. Or, ce branchement n'est pas nécessairement l'une des décisions à l'origine de la contradiction. L'analyse des conflits remédie à ce problème en tenant compte des décisions à l'origine du conflit. Cette analyse permet ainsi d'effectuer un retour-arrière non-chronologique, c'est-à-dire un retour direct au niveau, plus haut dans l'arbre, qui est à l'origine du conflit sans tester les niveaux intermédiaires.

2.3.5.4 Apprentissage

L'apprentissage consiste à analyser et apprendre les raisons qui ont amené à une contradiction : lorsqu'une assignation partielle amène à une contraction, il est possible d'isoler un sous-ensemble d'assignations et un sous-ensemble de clauses, qui sont responsables du conflit. À partir de ces assignations, il est possible de construire (d'apprendre) une clause qui est impliquée par ces clauses. Cette nouvelle clause est ajoutée à l'ensemble de clauses du problème. Les assignations pertinentes sont déterminées par un graphe de dépendance entre les clauses et les assignations, appelé graphe d'implication. Les clauses apprises permettent de ne pas refaire plusieurs fois les mêmes «erreurs » dans l'arbre de recherche.

2.3.5.5 Redémarrage

La plupart des solveurs SAT actuels utilisent une stratégie de redémarrage, qui consiste à redémarrer la recherche en prenant en compte de nouvelles clauses apprises durant la recherche précédente. La plupart des solveurs effectuent un redémarrage après qu'un seuil de clauses apprises soit atteint. Ainsi, à chaque redémarrage, le parcours de l'espace de recherche change car l'ensemble de clauses est modifié. Il faut noter que la plupart des solveurs effacent régulièrement les clauses apprises. Ainsi, le mixage des redémarrages et des oublis peut dans certains cas mettre en cause la complétude des solveurs. Un paramétrage des redémarrages est donc nécessaire pour garder cette dernière propriété. Le solveur Chaff, par exemple, augmente à chaque redémarrage le seuil au-delà duquel une clause est oubliée. Ainsi, de plus en plus de clauses sont gardées, ce qui assure la complétude.

2.3.5.6 Structures de données paresseuses

Dans les solveurs SAT modernes, 80% du temps de calcul est consommé par la propagation unitaire. Ainsi, des structures de données dites «paresseuses » ont été introduites dans le but d'optimiser la propagation unitaire.