Probleme – $2$-SAT est linéaire

1. Le graphe d'implication. Une clause $(a\vee b)$ équivaut à deux implications :

$$\neg a\Rightarrow b\text{et}\neg b\Rightarrow a.$$

On construit alors un graphe orienté dont les sommets sont les $2n$ littéraux $x_1,\neg x_1,\dots ,x_n,\neg x_n$, et où chaque clause donne les deux arcs ci-dessus. Le graphe a $2n$ sommets et $2m$ arcs : sa construction est en $\Theta (n+m)$.

2. Le critère.

Démonstration du sens facile (celui qui sert). Supposons $x$ et $\neg x$ dans la même composante fortement connexe. Il existe alors un chemin de $x$ vers $\neg x$ et un de $\neg x$ vers $x$. Or un arc du graphe est une implication vraie sous toute valuation satisfaisante : si $u\Rightarrow v$ est un arc et que $u$ est vrai, alors $v$ l'est. Par transitivité le long du chemin, $x$ vrai entraînerait $\neg x$ vrai, ce qui est contradictoire ; et $x$ faux entraînerait, par l'autre chemin, $x$ vrai. Aucune valuation ne convient.

L'autre sens donne en plus une valuation. On calcule les composantes fortement connexes et on les numérote dans l'ordre topologique du graphe réduit. On pose alors

$$x\text{ vrai}⟺\text{la composante de }x\text{ vient apreˋs celle de }\neg x.$$

On vérifie que cette affectation satisfait toute clause : sinon, il existerait un arc allant d'une composante « vraie » vers une composante « fausse », ce que l'ordre topologique interdit.

3. L'algorithme. Construire le graphe, calculer les composantes fortement connexes, tester le critère, et lire la valuation. Le calcul des composantes se fait par l'algorithme de Kosaraju : deux parcours en profondeur, l'un sur le graphe, l'autre sur son transposé, dans l'ordre inverse des dates de fin. C'est l'algorithme du chapitre chap:graphes-avances.

$$\text{Complexiteˊ totale}=\Theta (n+m).$$

Une précaution de programmation : sur des instances à un million de variables, un parcours en profondeur récursif déborde la pile d'appels. On l'écrit itératif, avec une pile explicite — c'est la transformation du chapitre chap:recursivite, avec la pile du chapitre chap:sequentielles.

4. Les mesures. L'implantation a d'abord été confrontée à une recherche exhaustive sur $2000$ formules aléatoires de $2$ à $7$ variables : même réponse dans tous les cas, et chacune des $1560$ valuations rendues a été vérifiée clause par clause. Puis, sur de grandes instances :

La comparaison qui donne la mesure de l'enjeu. $2$-sat avec un million six cent mille variables : $1,35$ seconde. $3$-sat avec vingt-deux variables, par recherche exhaustive : $16$ secondes. Une variable de plus par clause, et l'on passe de $10^6$ variables à $20$.

Ce que ce problème apporte au chapitre. La dernière ligne du tableau — « si le cas particulier s'y prête » — n'est pas une consolation vague. sat est np-complet ; sat restreint à deux littéraux par clause est linéaire. La np-complétude qualifie le problème général, et il arrive qu'une restriction naturelle change complètement la donne. Chercher cette restriction est souvent plus rentable que chercher un meilleur algorithme exponentiel.