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 Krom.

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}\lor \neg x_{2}\lor \neg x_{3})\land (\neg x_{1}\lor x_{3}\lor x_{4}\lor 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}\lor \neg x_{2})\land (\neg x_{1}\lor 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 $\scriptscriptstyle (x_{0}\lor x_{2})\land (x_{0}\lor \lnot x_{3})\land (x_{1}\lor \lnot x_{3})\land (x_{1}\lor \lnot x_{4})\land (x_{2}\lor \lnot x_{4})\land {} \atop \quad \scriptscriptstyle (x_{0}\lor \lnot x_{5})\land (x_{1}\lor \lnot x_{5})\land (x_{2}\lor \lnot x_{5})\land (x_{3}\lor x_{6})\land (x_{4}\lor x_{6})\land (x_{5}\lor 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é graphe d'implication (en). La figure ci-contre montre un graphe d'implication pour la formule $(x_{0}\lor x_{2})\land (x_{0}\lor \lnot x_{3})\land (x_{1}\lor \lnot x_{3})\land (x_{1}\lor \lnot x_{4})\land (x_{2}\lor \lnot x_{4})\land {} \atop \quad (x_{0}\lor \lnot x_{5})\land (x_{1}\lor \lnot x_{5})\land (x_{2}\lor \lnot x_{5})\land (x_{3}\lor x_{6})\land (x_{4}\lor x_{6})\land (x_{5}\lor 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}\lor x_{2})$dans la formule ci-dessus peut s'écrire $(\neg x_{0}\rightarrow x_{2})$, ou encore $(\neg x_{2}\rightarrow 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 $\neg x_{0}$au sommet $x_{2}$et un arc du sommet $\neg x_{2}$au sommet $x_{0}$.

C'est un graphe antisymétrique (en) 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 $\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é

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 $\phi$
  $y=x$
  tant que $y\neq \neg x$:
     si aucune clause de $\phi$ ne contient le littéral $\neg y$
        rejeter
     choisir une clause de la forme $\neg y\vee z$ ou $z\vee \neg y$
     $y=z$
  $y=\neg x$
  tant que $y\neq x$:
     si aucune clause de $\phi$ ne contient le littéral $\neg y$
        rejeter
     choisir une clause de la forme $\neg y\vee z$ ou $z\vee \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 $\neg p\vee q$ (ou $p\to q$).

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

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

Supposons qu'il existe un chemin $s=u_{0}\to u_{1}\to \ldots \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 \ldots$, 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 =\ldots \wedge (\neg u_{i}\vee u_{i+1})\wedge \ldots$ et $\sigma \models \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 =\neg t\wedge \ldots$, donc $\sigma (t)=0$, d'où une contradiction. $\langle G,~s,~t\rangle$ est donc une instance positive de ${\overline {\text{ST-CON}}}$.

Supposons que $\langle G,~s,~t\rangle$ 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 \not \models \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.