2-\textsc{sat} : reconnaître une formule insatisfiable

Cette formule est celle qui épuise les quatre affectations de deux variables : chacune est interdite par exactement une clause. Elle est donc insatisfiable, et l'énumération le confirme.

Ce que voit le graphe des implications. Les huit arcs sont :

non x -> y      non y -> x        (x ou y)
non x -> non y  y     -> x        (x ou non y)
x     -> y      non y -> non x    (non x ou y)
x     -> non y  y     -> non x    (non x ou non y)

Le calcul mesuré donne une seule composante : les quatre littéraux $x$, $\neg x$, $y$, $\neg y$ sont tous dans $C_0$.

On peut le voir à la main : $x\to y\to x$ donne un cycle entre $x$ et $y$ ; $x\to \neg y\to \neg x$ et $\neg x\to y\to x$ ferment le tour. Les quatre littéraux s'impliquent mutuellement. En particulier $x$ et $\neg x$ sont ensemble : le critère du chapitre déclare la formule insatisfiable.

Le sens de « tous dans la même composante ». Une composante fortement connexe du graphe des implications est un paquet de littéraux qui doivent recevoir la même valeur. Ici, le paquet contient $x$ et $\neg x$ : on exige $x\equiv \neg x$. Ce n'est pas « on n'a pas trouvé de modèle », c'est « la contrainte est contradictoire », et l'algorithme le prouve — un certificat d'insatisfiabilité que le retour sur trace, lui, ne fournirait pas.