La résolution, ou comment prouver qu'il n'y a rien

On retire $b$ et $\neg b$, puis on réunit le reste :

$(a \vee \neg c \vee c \vee d)$

Cette clause contient $c$ et $\neg c$ : elle est tautologique, donc toujours vraie et parfaitement inutile. Un solveur la jetterait immédiatement.

C'est un cas fréquent, et il vaut la peine de le repérer avant de calculer : dès que les deux clauses contiennent une seconde variable avec des signes opposés, la résolvante sera tautologique.

Résoudre les deux mêmes clauses sur le pivot $c$ donnerait en revanche $(a \vee b \vee \neg b \vee d)$, tautologique elle aussi.

Trois clauses, deux résolutions.

Première étape. $(x)$ et $(\neg x \vee y)$, pivot $x$, donnent $(y)$.

Deuxième étape. $(y)$ et $(\neg y)$, pivot $y$, donnent $\square$.

La formule est insatisfiable. Noter que les deux étapes emploient une clause unitaire : c'est de la résolution unitaire, donc exactement ce que la propagation aurait fait toute seule.

Non, et c'est structurel. La résolution produit toujours une clause dont les littéraux viennent des deux parents. Le littéral $y$ n'apparaît nulle part dans $(x)$, donc aucune suite de résolutions ne le fera surgir.

Pourtant $(x)$ entraîne bien $(x \vee y)$ : toute affectation qui satisfait la première satisfait la seconde.

C'est la différence entre complétude et complétude réfutationnelle. La résolution ne dérive pas toutes les conséquences ; elle dérive la clause vide quand elle est due, et c'est tout ce dont on a besoin.

Deux clauses contiennent $x$, deux contiennent $\neg x$ : il y a $2 \times 2 = 4$ résolvantes à produire.

$(a \vee c)$, $(a \vee d)$, $(b \vee c)$, $(b \vee d)$.

On supprime ensuite les quatre clauses d'origine. Bilan : 4 clauses remplacées par 4, ce qui est le cas neutre.

Avec 10 clauses de chaque côté, ce serait 20 remplacées par 100. C'est cette croissance qui a condamné Davis-Putnam, et c'est aussi pourquoi les solveurs modernes n'éliminent que les variables où $p \times q \leq p + q$, c'est-à-dire presque uniquement celles qui apparaissent deux ou trois fois.

Ne pas le croire sur parole. Lui demander un certificat DRAT, puis le passer à un vérificateur indépendant.

Le raisonnement est le même que pour une réponse SAT, où l'on vérifie le modèle en un parcours plutôt que de faire confiance à la recherche. La différence est que le certificat d'un UNSAT est beaucoup plus gros, et que le vérificateur fait un vrai travail.

Ce qu'on gagne : la confiance ne repose plus sur les dizaines de milliers de lignes du solveur, mais sur les quelques milliers du vérificateur, qui est simple, stable, et parfois démontré correct.

Parce que l'argument humain est un comptage : il y a $n+1$ pigeons pour $n$ casiers, donc deux pigeons partagent un casier.

La résolution ne sait pas compter. Elle ne dispose que d'une opération, éliminer une paire de littéraux opposés, et pour atteindre la contradiction elle doit en quelque sorte parcourir toutes les façons de placer les pigeons. Haken a démontré que ce parcours est nécessairement exponentiel.

La leçon est générale : un système de preuve n'est puissant que sur les arguments qu'il sait exprimer. Il existe des systèmes qui additionnent des contraintes et réfutent $\mathrm{PHP}_n$ en quelques lignes ; aucun n'a encore donné de solveur qui batte CDCL sur les instances réelles.