Problème 2-SAT

Un article de Wikipédia, l'encyclopédie libre.
Sauter à la navigation Sauter à la recherche

En informatique théorique, le problème 2-SAT est un problème de décision. C'est un cas particulier 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 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 formule de Krom.

Définitions et exemples[modifier | modifier le code]

Restriction syntaxique[modifier | modifier le code]

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

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 :

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

Problème algorithmique[modifier | modifier le code]

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

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[modifier | modifier le code]

Graphe d'implication de la formule

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

L'idée est de remarquer qu'une clause de taille 2 peut toujours s'écrire comme une implication logique. Par exemple la clause dans la formule ci-dessus peut s'écrire , ou encore . 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 au sommet et un arc du sommet au sommet .

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 n'est dans la même composante fortement connexe que son nœud complémentaire . On peut déduire cette propriété un algorithme de complexité linéaire pour le problème[3].

Théorie de la complexité[modifier | modifier le code]

2017-fr.wp-orange-source.svg
Cette section ne cite pas suffisamment ses sources (novembre 2018)
Pour l'améliorer, ajoutez des références vérifiables [comment faire ?] ou le modèle {{Référence nécessaire}} sur les passages nécessitant une source.
Circle-icons-check.svg
Le fond de cette section est à vérifier (20 novembre 2018).

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

Appartenance à NL[modifier | modifier le code]

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

  choisir une variable parmi les variables de 
  
  tant que :
     si aucune clause de  ne contient le littéral 
        rejeter
     choisir une clause de la forme  ou 
     
  
  tant que :
     si aucune clause de  ne contient le littéral 
        rejeter
     choisir une clause de la forme  ou 
     
  accepter

est donc dans NL.

NL-dureté[modifier | modifier le code]

Comme est (co)NL-complet, il suffit de construire une réduction en espace logarithmique de vers 2-SAT pour montrer que 2-SAT est NL-dur.

Soient un graphe orienté et deux sommets de .

En associant à chaque sommet de G une variable propositionnelle, chaque arête entre deux sommets p et q correspond à la clause (ou ).

Soient et .

Supposons satisfiable. Soit une interprétation qui satisfait .

Supposons qu'il existe un chemin de s à t dans G. Pour tout i, on a (par induction sur i):

  • , donc .
  • Soit i < n. Supposons avoir montré .

est une arête de G, donc et . Comme , on a nécessairement .

Donc . Or , donc , d'où une contradiction. est donc une instance positive de .

Supposons que est une instance positive de . Soit l'interprétation telle que pour tout sommet u, si u est accessible depuis s et sinon. Supposons que ne satisfait pas . On a et ; il existe donc i tel que , ce qui correspond à une arête telle que et . est donc accessible depuis , mais pas , ce qui contredit .

est donc satisfiable.

peut être construite en espace logarithmique (en la taille de G) pour toute instance de .

est donc NL-complet.

Notes et références[modifier | modifier le code]

  1. Voir par exemple Sylvain Perifel, Complexité algorithmique, Ellipses, , 432 p. (ISBN 9782729886929, lire en ligne), chap. 3.2.3 (« Autres problèmes NP -complets »), p. 76.
  2. Denis Trystram, « Leçon 5. Le problème SAT et ses variantes »,
  3. 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, no 3,‎ , p. 121-123 (DOI 10.1016/0020-0190(79)90002-4, lire en ligne).
  4. (en) Papadimitriou, Computational complexity, Section 9.2, p. 185
  5. (en) Papadimitriou, Computational complexity, Theorem 16.2 (p. 398)