Problème 2-SAT

En informatique théorique, le problème 2-SAT est un problème de décision. C'est une restriction du problème SAT qui peut être résolu en temps polynomial, alors que le problème général est NP complet. Le problème 2-SAT consiste à décider si une formule booléenne en forme normale conjonctive, dont toutes les clauses sont de taille 2, est satisfaisable. De telles formules sont appelées 2-CNF ou formules de KromModèle:,.

Définitions et exemples

Restriction syntaxique

On considère des formules en forme normale conjonctive, c'est-à-dire que ce sont des ET de OU de littéraux (un littéral est une variable ou la négation d'une variable). Par exemple :

$(x_1\vee \mathrm{\neg }{x}_2\vee \mathrm{\neg }{x}_3)\wedge (\mathrm{\neg }{x}_1\vee x_3\vee x_4\vee x_6)$

Pour le problème 2SAT, on se restreint le nombre de littéraux par clause est égal 2. Un exemple d'une telle formule est alors :

$(x_1\vee \mathrm{\neg }{x}_2)\wedge (\mathrm{\neg }{x}_1\vee x_3)$

Une formule en forme normale conjonctive avec 2 littéraux par clause s'appelle aussi une 2-CNF ou formule de Krom.

Problème algorithmique

Le problème de décision 2SAT est le suivant :

Entrée : Une formule en forme normale conjonctive avec 2 littéraux par clause ;

Question : Existe-t-il une assignation des variables, qui rende la formule vraie ? Autrement dit, la formule peut-elle être satisfaite ?

Dans les applications il est souvent nécessaire de pouvoir donner une solution explicite, et non pas seulement de décider si elle existe.

Graphe d'implication

Graphe d'implication de la formule $\genfrac{}{}{0ex}{}{(x_0\vee x_2)\wedge (x_0\vee \mathrm{\neg }{x}_3)\wedge (x_1\vee \mathrm{\neg }{x}_3)\wedge (x_1\vee \mathrm{\neg }{x}_4)\wedge (x_2\vee \mathrm{\neg }{x}_4)\wedge }{(x_0\vee \mathrm{\neg }{x}_5)\wedge (x_1\vee \mathrm{\neg }{x}_5)\wedge (x_2\vee \mathrm{\neg }{x}_5)\wedge (x_3\vee x_6)\wedge (x_4\vee x_6)\wedge (x_5\vee x_6).}$

On peut représenter une formule en forme normale conjonctive avec au plus 2 littéraux par clause par un graphe orienté appelé Modèle:Lien. La figure ci-contre montre un graphe d'implication pour la formule $\genfrac{}{}{0ex}{}{(x_0\vee x_2)\wedge (x_0\vee \mathrm{\neg }{x}_3)\wedge (x_1\vee \mathrm{\neg }{x}_3)\wedge (x_1\vee \mathrm{\neg }{x}_4)\wedge (x_2\vee \mathrm{\neg }{x}_4)\wedge }{(x_0\vee \mathrm{\neg }{x}_5)\wedge (x_1\vee \mathrm{\neg }{x}_5)\wedge (x_2\vee \mathrm{\neg }{x}_5)\wedge (x_3\vee x_6)\wedge (x_4\vee x_6)\wedge (x_5\vee x_6).}$

L'idée est de remarquer qu'une clause de taille 2 peut toujours s'écrire comme une implication logique. Par exemple la clause $(x_0\vee x_2)$dans la formule ci-dessus peut s'écrire $(\mathrm{\neg }{x}_0\to x_2)$, ou encore $(\mathrm{\neg }{x}_2\to x_0)$. On peut alors construire un graphe dont les sommets sont les littéraux, et dont les arêtes représentent les implications. C'est pourquoi il y a un arc du sommet $\mathrm{\neg }{x}_0$au sommet $x_2$et un arc du sommet $\mathrm{\neg }{x}_2$au sommet $x_0$.

C'est un Modèle:Lien et on peut montrer qu'une formule est satisfaisable si et seulement si dans son graphe d'adjacence aucun sommet $x_i$n'est dans la même composante fortement connexe que son nœud complémentaire $\mathrm{\neg }{x}_i$. On peut déduire de cette propriété un algorithme de complexité linéaire pour le problème.

Théorie de la complexité

Modèle:Section à sourcer Modèle:Section à vérifier 2-SAT est complet pour la classe de complexité NL, tout comme le problème de l'accessibilité dans un graphe. On donne ici des démonstrations pour l'appartenance à NL et la NL-dureté.

Appartenance à NL

D'après le théorème d'Immerman-Szelepcsényi, co-NL = NL, donc pour montrer que $\text{2-SAT}$ est dans NL, il suffit de montrer que le problème dual $\overline{\text{2-SAT}}$, le problème qui consiste à savoir si une formule en forme normale conjonctive avec 2 n'est pas satisfiable, est dans NL. L'algorithme non-déterministe suivant décide $\overline{\text{2-SAT}}$ en espace logarithmique :

  choisir une variable $x$ parmi les variables de $\varphi$
  $y=x$
  tant que $y\ne \mathrm{\neg }x$:
     si aucune clause de $\varphi$ ne contient le littéral $\mathrm{\neg }y$
        rejeter
     choisir une clause de la forme $\mathrm{\neg }y\vee z$ ou $z\vee \mathrm{\neg }y$
     $y=z$
  $y=\mathrm{\neg }x$
  tant que $y\ne x$:
     si aucune clause de $\varphi$ ne contient le littéral $\mathrm{\neg }y$
        rejeter
     choisir une clause de la forme $\mathrm{\neg }y\vee z$ ou $z\vee \mathrm{\neg }y$
     $y=z$
  accepter

$\text{2-SAT}$est donc dans NL.

NL-dureté

Comme $\overline{\text{ST-CON}}$ est (co)NL-complet, il suffit de construire une réduction en espace logarithmique de $\overline{\text{ST-CON}}$ vers 2-SAT pour montrer que 2-SAT est NL-dur.

Soient $G=(V,E)$ un graphe orienté et $s,t$ deux sommets de $G$.

En associant à chaque sommet de G une variable propositionnelle, chaque arête entre deux sommets p et q correspond à la clause $\mathrm{\neg }p\vee q$ (ou $p\to q$).

Soient $\varphi =\underset{(p,q)\in E}{\bigwedge }(\mathrm{\neg }p\vee q)$ et $\psi =s\wedge \mathrm{\neg }t\wedge \varphi$.

Supposons $\psi$ satisfiable. Soit $\sigma$ une interprétation qui satisfait $\psi$.

Supposons qu'il existe un chemin $s=u_0\to u_1\to \dots \to u_n=t$ de s à t dans G. Pour tout i, on a $\sigma (u_i)=1$ (par induction sur i):

• $\psi =s\wedge \dots$, donc $\sigma (s)=1$.
• Soit i < n. Supposons avoir montré $\sigma (u_i)=1$.

$(u_i,u_{i+1})$ est une arête de G, donc $\psi =\dots \wedge (\mathrm{\neg }{u}_i\vee u_{i+1})\wedge \dots$ et $\sigma \models \mathrm{\neg }{u}_i\vee u_{i+1}$. Comme $\sigma (u_i)=1$, on a nécessairement $\sigma (u_{i+1})=1$.

Donc $\sigma (t)=\sigma (u_n)=1$. Or $\psi =\mathrm{\neg }t\wedge \dots$, donc $\sigma (t)=0$, d'où une contradiction. $⟨G,s,t⟩$ est donc une instance positive de $\overline{\text{ST-CON}}$.

Supposons que $⟨G,s,t⟩$ est une instance positive de $\overline{\text{ST-CON}}$. Soit $\sigma$ l'interprétation telle que pour tout sommet u, $\sigma (u)=1$ si u est accessible depuis s et $\sigma (u)=0$ sinon. Supposons que $\sigma$ ne satisfait pas $\psi$. On a $\sigma (s)=1$ et $\sigma (t)=0$; il existe donc i tel que $\sigma \models ̸\mathrm{\neg }{u}_i\vee u_{i+1}$, ce qui correspond à une arête $(u_i,u_{i+1})$ telle que $\sigma (u_i)=1$ et $\sigma (u_{i+1})=0$. $u_i$ est donc accessible depuis $s$, mais pas $u_{i+1}$, ce qui contredit $(u_i,u_{i+1})\in E$.

$\psi$ est donc satisfiable.

$\psi$ peut être construite en espace logarithmique (en la taille de G) pour toute instance de $\overline{\text{ST-CON}}$.

$\text{2-SAT}$ est donc NL-complet.