Probleme – 2-\textsc{sat} : du critère au modèle

1. La construction. On numérote le littéral $x_i$ par le sommet $2i$ et $\neg x_i$ par $2i+1$ ; passer à la négation, c'est basculer le bit de poids faible.

(* Un litteral : (i, true) pour x_i, (i, false) pour non x_i. *)
let som (i, positif) = if positif then 2*i else 2*i + 1
let non (i, positif) = (i, not positif)

(* Graphe des implications d'une formule 2-SAT.
   Entrees : n variables, une liste de clauses (l1, l2).
   Sortie  : un graphe a 2n sommets et 2m arcs. Complexite : Theta(n + m). *)
let graphe_implications n clauses =
  let g = Array.make (2*n) [] in
  List.iter (fun (l1, l2) ->
    g.(som (non l1)) <- som l2 :: g.(som (non l1));   (* non l1 -> l2 *)
    g.(som (non l2)) <- som l1 :: g.(som (non l2))    (* non l2 -> l1 *)
  ) clauses;
  g

$2n$ sommets et $2m$ arcs : la construction est linéaire, et c'est déjà la moitié du résultat.

2. Le critère. On montre les deux sens.

Si $x_i$ et $\neg x_i$ sont dans la même composante, la formule est insatisfiable. Le graphe des implications a une propriété clé : tout modèle rend vrai le successeur de tout littéral vrai. En effet un arc $\ell \to {\ell }^{\prime }$ vient d'une clause $(\neg \ell \vee {\ell }^{\prime })$, qui interdit $\ell =V$ avec ${\ell }^{\prime }=F$. Par transitivité, dans un modèle, tous les littéraux accessibles depuis un littéral vrai sont vrais. Or dans une composante fortement connexe, tous les littéraux sont mutuellement accessibles : ils reçoivent donc tous la même valeur. Si $x_i$ et $\neg x_i$ y sont ensemble, on exige $x_i\equiv \neg x_i$ : impossible.

Sinon, la construction de la question 3 fournit un modèle, ce qui démontre l'autre sens.

3. L'algorithme. On exploite le fait que Kosaraju numérote les composantes dans l'ordre topologique du quotient.

(* Resout une instance de 2-SAT.
   Entrees : n variables, une liste de clauses a deux litteraux.
   Sortie  : None si insatisfiable, Some v avec v.(i) la valeur de x_i sinon.
   Complexite : Theta(n + m). *)
let deux_sat n clauses =
  let comp = kosaraju (graphe_implications n clauses) in
  let piege = ref false in
  for i = 0 to n - 1 do
    if comp.(2*i) = comp.(2*i + 1) then piege := true
  done;
  if !piege then None
  else Some (Array.init n (fun i -> comp.(2*i) > comp.(2*i + 1)))

Pourquoi ce modèle est correct. Soit un arc $\ell \to {\ell }^{\prime }$ avec $\ell$ affecté à vrai. Deux cas. Si $\ell$ et ${\ell }^{\prime }$ sont dans la même composante, ils ont la même valeur, et ${\ell }^{\prime }$ est vrai. Sinon, l'arc du quotient impose $\text{comp}(\ell )<\text{comp}({\ell }^{\prime })$ puisque la numérotation est topologique. Par ailleurs, $\ell$ vrai signifie $\text{comp}(\ell )>\text{comp}(\neg \ell )$. Le graphe des implications est antisymétrique — si $\ell \to {\ell }^{\prime }$ est un arc, $\neg {\ell }^{\prime }\to \neg \ell$ en est un aussi, car les deux viennent de la même clause —, d'où $\text{comp}(\neg {\ell }^{\prime })<\text{comp}(\neg \ell )$. En combinant :

$$\text{comp}({\ell }^{\prime })>\text{comp}(\ell )>\text{comp}(\neg \ell )>\text{comp}(\neg {\ell }^{\prime }),$$

donc ${\ell }^{\prime }$ est vrai lui aussi. Aucune clause n'est violée.

Vérification. Sur $20000$ formules tirées au hasard (de $2$ à $5$ variables, de $1$ à $8$ clauses) — $17205$ satisfiables et $2795$ insatisfiables —, la comparaison avec une force brute sur les $2^n$ affectations ne donne aucun désaccord, ni sur le verdict, ni sur la validité du modèle rendu.

Complexité : la construction est en $\Theta (n+m)$, Kosaraju aussi, l'extraction du modèle en $\Theta (n)$. Total $\Theta (n+m)$ — c'est la promesse du chapitre chap:logique.

4. Le mur de 3-sat. Une clause $({\ell }_1\vee {\ell }_2)$ équivaut à deux implications, chacune entre deux littéraux : c'est un arc. Une clause $({\ell }_1\vee {\ell }_2\vee {\ell }_3)$ équivaut à $\neg {\ell }_1\to ({\ell }_2\vee {\ell }_3)$ : la conclusion est une disjonction, pas un littéral. Un arc ne sait pas représenter cela.

On pourrait vouloir un hypergraphe, ou dédoubler les cas ; mais alors le raisonnement par composantes fortement connexes s'effondre, car la propriété « tous les littéraux d'une composante ont la même valeur » repose sur la transitivité de l'implication entre littéraux simples. Et le problème 3-sat, lui, est np-complet — le chapitre chap:decidabilite dira ce que cela signifie. Le saut de $2$ à $3$ n'est pas quantitatif : c'est le passage d'un arc à une disjonction.