Les cas où la difficulté disparaît

C'est du 2-SAT. Les six arcs :

$(x \vee y)$ donne $\neg x \rightarrow y$ et $\neg y \rightarrow x$. $(\neg x \vee y)$ donne $x \rightarrow y$ et $\neg y \rightarrow \neg x$. $(x \vee \neg y)$ donne $\neg x \rightarrow \neg y$ et $y \rightarrow x$.

Chercher les allers-retours. Depuis $x$ : $x \rightarrow y \rightarrow x$. Les sommets $x$ et $y$ sont donc dans une même composante. Cette composante contient-elle $\neg x$ ? Depuis $x$ on atteint $y$, et depuis $y$ on atteint $x$, sans jamais sortir de la paire. Donc non.

Satisfiable. Pour le modèle : $\neg x$ atteint $x$, par $\neg x \rightarrow y \rightarrow x$, alors que $x$ n'atteint pas $\neg x$. La composante de $x$ vient donc après celle de $\neg x$, d'où $x = 1$. De même $y = 1$.

Contrôle : $(1 \vee 1)$, $(0 \vee 1)$, $(1 \vee 0)$. Les trois clauses sont satisfaites.

Deux forçages, aucune contradiction.

Le premier chemin dit que supposer $x_1$ vrai mène à $x_1$ faux : donc $x_1 = 0$. Le second dit que supposer $x_3$ faux mène à $x_3$ vrai : donc $x_3 = 1$.

La formule reste parfaitement satisfiable en l'état de ces informations. Il faudrait, pour conclure à l'insatisfiabilité, trouver une variable dont les deux chemins existent simultanément.

C'est la confusion la plus fréquente sur 2-SAT : un chemin unique déduit, une paire de chemins réfute.

Oui : chaque clause a au plus un littéral positif. Les deux premières sont des règles, les deux dernières des faits.

Application de l'algorithme, en partant de tout à 0 :

$(a)$ est falsifiée, on pose $a = 1$. $(b)$ de même, $b = 1$. $(\neg a \vee \neg b \vee c)$ devient falsifiée, on pose $c = 1$. $(\neg c \vee d)$ devient falsifiée, on pose $d = 1$. Plus rien n'est falsifié.

Modèle : $a = b = c = d = 1$, et c'est le modèle minimal. Le calcul est du pur chaînage avant, exactement ce que fait un moteur de règles, et il n'a demandé aucune décision.

Non. La première clause contient deux littéraux positifs, $b$ et $c$. Elle se lit « si $a$ alors $b$ ou $c$ », et c'est précisément ce « ou » dans la conclusion qui fait sortir du fragment.

La différence n'est pas cosmétique : elle réintroduit le choix. Un moteur de règles sait dérouler « si $a$ alors $b$ » ; face à « si $a$ alors $b$ ou $c$ », il doit parier sur l'un des deux et savoir revenir en arrière. C'est toute la distance entre un chaînage avant linéaire et une recherche.

La seconde clause, elle, est bien de Horn.

Non. Il suffit d'une clause sans littéral positif que le modèle minimal falsifie.

Exemple : $(a) \wedge (\neg a \vee b) \wedge (\neg a \vee \neg b)$. Les trois clauses sont bien de Horn, avec respectivement un, un et zéro littéral positif.

Le déroulement : $(a)$ force $a = 1$, puis $(\neg a \vee b)$ force $b = 1$. La troisième clause, $(\neg a \vee \neg b)$, se retrouve alors entièrement fausse.

Insatisfiable, et détecté en deux propagations. Noter que la clause fautive est celle qui n'a aucun littéral positif : ce sont les seules qui peuvent échouer, puisque toutes les autres peuvent toujours être satisfaites en mettant leur conclusion à 1.

La contrainte exige un nombre pair de variables à 1. Il faut donc interdire les quatre affectations de parité impaire, une clause chacune.

Les affectations à exclure sont $(1,0,0)$, $(0,1,0)$, $(0,0,1)$ et $(1,1,1)$. Chacune donne la clause qui la nie :

$(\neg x \vee y \vee z)$, $(x \vee \neg y \vee z)$, $(x \vee y \vee \neg z)$, $(\neg x \vee \neg y \vee \neg z)$.

Quatre clauses, soit $2^{3-1}$. Noter au passage que ce sont exactement les clauses complémentaires de celles de $x \oplus y \oplus z = 1$ : chaque signe est inversé.

Additionner les trois équations. Chaque variable apparaît deux fois à gauche et s'annule, donc le membre de gauche vaut 0. À droite, $1 \oplus 0 \oplus 0 = 1$.

On obtient $0 = 1$ : le système est insatisfiable.

La vérification directe confirme : la deuxième équation impose $y = z$, la troisième impose $x = z$, donc $x = y$, ce qui contredit la première.

Ce raisonnement d'une ligne est hors de portée d'un solveur CDCL travaillant sur les douze clauses de l'encodage, qui devra les explorer. Sur un système de mille équations, l'écart devient insurmontable.

Non, pas au sens du théorème. Le fragment 2-SAT exige que toutes les clauses soient binaires, et douze exceptions suffisent à faire perdre la garantie.

Mais la lecture utile n'est pas là. Ces douze clauses sont les seules qui demandent un choix : une fois leurs littéraux fixés, tout le reste est du 2-SAT, donc résoluble en temps linéaire.

Autrement dit, la formule possède une porte dérobée naturelle, au sens du chapitre précédent, et il suffit d'explorer les combinaisons issues de ces douze clauses. C'est précisément le raisonnement qui explique pourquoi tant d'instances industrielles, formellement NP-complètes, se résolvent en quelques secondes.