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^[1],[2].

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)^[3]. Par exemple :

${\displaystyle (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 :

${\displaystyle (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^[4] :

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 ${\displaystyle \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 ${\displaystyle (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 ${\displaystyle (x_{0}\lor x_{2})}$dans la formule ci-dessus peut s'écrire ${\displaystyle (\neg x_{0}\rightarrow x_{2})}$, ou encore ${\displaystyle (\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 ${\displaystyle \neg x_{0}}$au sommet ${\displaystyle x_{2}}$et un arc du sommet ${\displaystyle \neg x_{2}}$au sommet ${\displaystyle 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 ${\displaystyle x_{i}}$n'est dans la même composante fortement connexe que son nœud complémentaire ${\displaystyle \neg x_{i}}$. On peut déduire de cette propriété un algorithme de complexité linéaire pour le problème^[5].

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^[6] et la NL-dureté^[7].

Appartenance à NL

D'après le théorème d'Immerman-Szelepcsényi, co-NL = NL, donc pour montrer que ${\displaystyle {\text{2-SAT}}}$ est dans NL, il suffit de montrer que le problème dual ${\displaystyle {\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 ${\displaystyle {\overline {\text{2-SAT}}}}$ en espace logarithmique :

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

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

NL-dureté

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

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

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

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

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

Supposons qu'il existe un chemin ${\displaystyle s=u_{0}\to u_{1}\to \ldots \to u_{n}=t}$ de s à t dans G. Pour tout i, on a ${\displaystyle \sigma (u_{i})=1}$ (par induction sur i):

• ${\displaystyle \psi =s\wedge \ldots }$, donc ${\displaystyle \sigma (s)=1}$.
• Soit i < n. Supposons avoir montré ${\displaystyle \sigma (u_{i})=1}$.

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

Donc ${\displaystyle \sigma (t)=\sigma (u_{n})=1}$. Or ${\displaystyle \psi =\neg t\wedge \ldots }$, donc ${\displaystyle \sigma (t)=0}$, d'où une contradiction. ${\displaystyle \langle G,~s,~t\rangle }$ est donc une instance positive de ${\displaystyle {\overline {\text{ST-CON}}}}$.

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

${\displaystyle \psi }$ est donc satisfiable.

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

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