Probleme – $2$-\textsc{sat} : pourquoi le saut se fait entre $2$ et $3$

1. Les deux arcs. La clause $({\ell }_1\vee {\ell }_2)$ est équivalente à $\neg {\ell }_1\to {\ell }_2$, et aussi à $\neg {\ell }_2\to {\ell }_1$ — c'est la même formule lue dans les deux sens. On pose donc les arcs

$$\neg {\ell }_1⟶{\ell }_2\text{et}\neg {\ell }_2⟶{\ell }_1.$$

Il en faut deux, et c'est le point de départ. Un seul arc encoderait une implication, pas une disjonction : on perdrait la moitié de l'information, et le graphe cesserait d'être symétrique — propriété dont la preuve a besoin. Le graphe obtenu vérifie : $u\to v$ est un arc si et seulement si $\neg v\to \neg u$ en est un. C'est la contraposée, devenue une symétrie du graphe.

<details class="group my-6 border border-gray-300 rounded-2xl bg-black/[0.03] overflow-hidden transition-all duration-300"><summary style="color:#1e3a8a" class="flex items-center justify-between p-4 cursor-pointer text-xs font-bold select-none"><div class="flex items-center"><i class="fa-solid fa-graduation-cap mr-2"></i>Démonstration</div><span class="transition-transform group-open:rotate-180"><i class="fa-solid fa-chevron-down"></i></span></summary><div style="color:#1d4ed8" class="force-blue p-4 pt-0 border-t border-gray-200 bg-black/[0.02] leading-relaxed font-sans text-xs select-text"> ($\Rightarrow$, par contraposée) Supposons $p$ et $\neg p$ dans la même composante fortement connexe : il existe un chemin $p⇝\neg p$ et un chemin $\neg p⇝p$. Or un arc $u\to v$ signifie « tout modèle qui rend $u$ vrai rend $v$ vrai », et cette propriété se transmet le long d'un chemin. Si un modèle rendait $p$ vraie, le premier chemin le forcerait à rendre $\neg p$ vraie ; s'il rendait $p$ fausse, donc $\neg p$ vraie, le second le forcerait à rendre $p$ vraie. Aucun modèle n'existe.

($\Leftarrow$) On construit un modèle. Contractons les composantes fortement connexes : le graphe quotient est sans circuit (chapitre chap:graphes-avances), donc admet un tri topologique. Posons $p:=V$ lorsque la composante de $p$ vient après celle de $\neg p$ dans ce tri, et $p:=F$ sinon — ce qui a un sens puisque les deux composantes sont distinctes par hypothèse. La symétrie du graphe garantit que cette affectation est cohérente, et qu'aucun arc ne mène d'un littéral vrai à un littéral faux ; toutes les clauses sont donc satisfaites.