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.

Notes et références

1. (en) Victor W. Marek, Introduction to Mathematics of Satisfiability, Boca Raton, CRC press, 350 p. (ISBN 978-1-4398-0167-3), chap. 9.5 (« Krom formulas and 2-SAT »), p. 185
2. A ne pas confondre avec les clauses de Horn qui sont aussi utilisées dans le problème SAT
3. Voir par exemple Sylvain Perifel, Complexité algorithmique, Ellipses, 2014, 432 p. (ISBN 9782729886929, lire en ligne), chap. 3.2.3 (« Autres problèmes NP -complets »), p. 76.
4. Denis Trystram, « Leçon 5. Le problème SAT et ses variantes », 2011
5. Bengt Aspvall, Michael F. Plass et Robert E. Tarjan, « A linear-time algorithm for testing the truth of certain quantified boolean formulas », Information Processing Letters, vol. 8, n^o 3,‎ 1979, p. 121-123 (DOI 10.1016/0020-0190(79)90002-4, lire en ligne).
6. (en) Papadimitriou, Computational complexity, Section 9.2, p. 185
7. (en) Papadimitriou, Computational complexity, Theorem 16.2 (p. 398)