La méthode de résolution

La leçon sur la sémantique de la logique propositionnelle a montré que la validité et la satisfaisabilité sont décidables par la table de vérité, à un coût qui double avec chaque variable, et a annoncé des méthodes qui n’exigeraient pas de la parcourir. La leçon sur la conséquence et l’équivalence sémantiques a ramené toute conséquence à une insatisfaisabilité : $\Gamma \models \varphi$ si et seulement si $\Gamma \cup \{\neg\varphi\}$ est insatisfaisable. Les leçons sur les formes normales et sur leur algorithme ont donné à toute formule une forme conjonctive, dont la validité se voit au premier coup d’œil, mais dont la satisfaisabilité ne se voit pas. S’il en est ainsi, il manque une procédure qui décide l’insatisfaisabilité d’une conjonction de clauses en opérant sur les clauses elles-mêmes. Cette procédure est la résolution, proposée par John Alan Robinson en 1965 à partir d’idées de Martin Davis et Hilary Putnam (1960) ; c’est le cœur des programmes qui décident aujourd’hui la satisfaisabilité de formules à des millions de variables. À la différence du système de l’unité de déduction, dont les relations avec la sémantique sont étudiées dans les leçons sur la correction et la complétude et sur le théorème de compacité, la résolution ne déduit pas de conclusions : elle réfute des ensembles. Cette leçon démontre qu’elle le fait de façon correcte et complète.

Comme dans les leçons précédentes, $p$, $q$, $r$, $s$ et $t$ nomment les variables $v_1$ à $v_5$ ; la lettre $v$ sans indice, ainsi que $w$, désignent des valuations ; et $V(\varphi)$ est l’ensemble des variables de $\varphi$.

Clauses et ensembles de clauses

Rappelons, d’après la leçon sur les formes normales, qu’un littéral est une variable ou la négation d’une variable, et que l’opposé d’un littéral $\ell$, noté $\ell^{*}$, est le littéral de la même variable et de l’autre signe ; deux littéraux opposés forment une paire complémentaire. Par le lemme de la négation d’un littéral, $v(\ell^{*}) = 1 - v(\ell)$ pour toute valuation $v$. Là, une clause était une disjonction de littéraux ; ici, il convient d’oublier l’ordre et les répétitions, qui n’altèrent pas la valeur, et de ne garder que l’ensemble.

Une clause est un ensemble fini de littéraux. La clause sans littéraux s’appelle la clause vide et se note $\Box$. Une valuation $v$ satisfait une clause $C$, ce que l’on note $v \models C$, si un littéral de $C$ vaut $1$ sous $v$ ; dans le cas contraire, $v$ la réfute. Une clause d’un seul littéral est dite unitaire. Les variables d’une clause forment l’ensemble $V(C)$ ; celles d’un ensemble $S$ de clauses, l’ensemble $V(S)$, réunion des précédents. Une valuation satisfait un ensemble $S$ de clauses, $v \models S$, si elle satisfait chacune de ses clauses ; $S$ est satisfaisable si une valuation le satisfait, et insatisfaisable dans le cas contraire. Enfin, si $S$ est un ensemble de clauses et $C$ une clause, $S \models C$ signifie que toute valuation qui satisfait $S$ satisfait $C$.

Deux cas extrêmes découlent de la définition, et il convient de les fixer. La clause vide n’a pas de littéraux ; par conséquent, aucun de ses littéraux ne vaut $1$, et aucune valuation ne la satisfait : $\Box$ est insatisfaisable, et tout ensemble qui la contient l’est aussi. L’ensemble vide de clauses, en revanche, n’a aucune clause à satisfaire, et toute valuation le satisfait. Il ne faut pas les confondre : $\{\Box\}$ est insatisfaisable et $\emptyset$ est satisfait par toutes les valuations.

Une clause qui contient une paire complémentaire est dite tautologique : elle n’impose aucune condition, et on peut la retirer de n’importe quel ensemble sans en altérer les modèles. Écrire les clauses comme des ensembles n’est pas un caprice de notation. Si de $(p \vee q)$ et $(p \vee \neg q)$ on veut obtenir $p$, la disjonction donne $(p \vee p)$, qui équivaut à $p$ mais n’est pas la même formule ; avec des ensembles, $\{p\} \cup \{p\} = \{p\}$, et la fusion des littéraux répétés se fait d’elle-même.