La résolution

L'idée

Pour montrer que $\Sigma \vDash A$, on peut montrer que $\Sigma \cup \{\lnot A\}$ est insatisfiable (chapitre 2, propriété 3). Les tables de vérité le font, mais en $2^n$ lignes. La résolution cherche directement la contradiction, en combinant les formules deux à deux avec une seule règle.

Elle travaille sur des clauses (chapitre 3). On met donc d'abord $\Sigma \cup \{\lnot A\}$ en FNC, et l'on sépare les clauses : on obtient un ensemble de clauses $S$, qui est satisfiable si et seulement si toutes ses clauses peuvent être vraies en même temps.

Une clause est vue comme un ensemble de littéraux : l'ordre ne compte pas, et un littéral répété ne compte qu'une fois. La clause vide, sans littéral, se note $\square$ ; elle est toujours fausse.

La règle

Énoncé

Si une clause contient un littéral $p$ et une autre son opposé $\lnot p$, on peut en tirer une nouvelle clause, leur résolvante, formée de tous les autres littéraux des deux :

On dit qu'on résout sur $p$.

La règle est correcte

Propriété. La résolvante est conséquence logique des deux clauses : $\{C \lor p,\; D \lor \lnot p\} \vDash C \lor D$.

Soit $v$ un modèle des deux clauses. Si $v(p) = 1$, alors $\lnot p$ est faux, donc $D$ est vraie dans $v$ (sinon $D \lor \lnot p$ serait fausse). Si $v(p) = 0$, alors $C$ est vraie de même. Dans les deux cas, $C \lor D$ est vraie.

Tout ce que la résolution produit est donc conséquence des clauses de départ. En particulier, si elle produit $\square$, qui n'a aucun modèle, les clauses de départ n'en avaient pas non plus.

La réfutation

Définition

Une réfutation de $S$ est une suite de clauses qui se termine par $\square$, où chaque clause est soit dans $S$, soit la résolvante de deux clauses précédentes.

Théorème (correction et complétude). Un ensemble fini de clauses $S$ est insatisfiable si et seulement si il a une réfutation.

Le sens « si » est la correction, démontrée ci-dessus. Le sens « seulement si », la complétude réfutationnelle, est admis : si $S$ est insatisfiable, la résolution finit toujours par trouver $\square$. Elle ne sert qu'à réfuter : elle ne produit pas toutes les conséquences d'un ensemble, mais elle trouve toujours la contradiction quand il y en a une.

La méthode

Pour montrer que $\Sigma \vDash A$ :

1. mettre chaque formule de $\Sigma$, et $\lnot A$, en FNC ;
2. réunir toutes les clauses obtenues dans $S$ ;
3. dériver $\square$ par résolution.

On présente la réfutation comme une liste numérotée, chaque résolvante avec son origine.

Quand on ne trouve pas la clause vide

Avec $n$ variables, il n'existe qu'un nombre fini de clauses différentes ($3^n$ : chaque variable apparaît positivement, négativement, ou pas). En ajoutant toutes les résolvantes possibles, on finit donc par ne plus rien produire de nouveau : on dit que l'ensemble est saturé. Si $\square$ n'y est pas, $S$ est satisfiable. La résolution est donc aussi une procédure de décision, mais une procédure lente : on lui préfère DPLL (chapitre 4) pour trouver un modèle.

Travailler efficacement

On allège la recherche sans rien perdre :

• tautologies : une clause qui contient $p$ et $\lnot p$ est toujours vraie ; on la retire ;
• subsomption : si une clause en contient une autre ($p \lor q \lor r$ contient $p \lor q$), la plus grande n'apporte rien ; on la retire ;
• stratégie unitaire : résoudre en priorité avec les clauses d'un seul littéral, qui raccourcissent les autres. C'est la propagation unitaire de DPLL.