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

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.

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.

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

Cette section ne cite pas suffisamment ses sources (novembre 2018). 

Pour l'améliorer, ajoutez des références de qualité et vérifiables (comment faire ?) ou le modèle {{Référence nécessaire}} sur les passages nécessitant une source.

Le fond de cette section est à vérifier (novembre 2018).

Améliorez-le ou discutez des points à vérifier. Si vous venez d’apposer le bandeau, merci d’indiquer ici les points à 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^[6] et la NL-dureté^[7].

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.

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.

• Portail de l'informatique théorique