2-sat : construire le graphe et conclure

Le graphe a six sommets — un par littéral — et deux arcs par clause :

Clause	Premier arc	Second arc
$(x \lor y)$	$\neg x \to y$	$\neg y \to x$
$(\neg x \lor y)$	$x \to y$	$\neg y \to \neg x$
$(\neg y \lor z)$	$y \to z$	$\neg z \to \neg y$

Les composantes, calculées par Kosaraju (numérotation dans l'ordre topologique du quotient, exercice « Dérouler Kosaraju ») :


[non z] = C0   [non y] = C1   [non x] = C2   [x] = C3   [y] = C4   [z] = C5

Six composantes, toutes réduites à un littéral : aucune variable n'a ses deux littéraux ensemble. La formule est satisfiable.

Le modèle, par la règle du chapitre — affecter vrai au littéral dont la composante vient après dans l'ordre topologique :

$x$ est en $C_{3}$ , $\neg x$ en $C_{2}$ : $3 > 2$ , donc $x = V$ ;
$y$ en $C_{4}$ , $\neg y$ en $C_{1}$ : $y = V$ ;
$z$ en $C_{5}$ , $\neg z$ en $C_{0}$ : $z = V$ .

Vérification : $(V \lor V) \land (F \lor V) \land (F \lor V) = V$ . Le chapitre annonçait « $y = z = V$ convient, quel que soit $x$ » : l'algorithme rend l'un de ces modèles.

Pourquoi la règle « la composante d'après » et non l'inverse. Un arc $ℓ_{1} \to ℓ_{2}$ interdit la combinaison $ℓ_{1} = V$ , $ℓ_{2} = F$ . Si l'on affecte vrai à ce qui vient après dans l'ordre topologique, alors $ℓ_{1} = V$ signifie que la composante de $ℓ_{1}$ est « tardive », donc celle de $ℓ_{2}$ , qui vient après elle, l'est aussi : $ℓ_{2} = V$ . L'implication est respectée par construction. L'ordre topologique fait tout le travail.

Énoncé

Corrigé

Exercices semblables