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 :
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 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
![](http://upload.wikimedia.org/wikipedia/commons/thumb/2/2f/Implication_graph.svg/300px-Implication_graph.svg.png)
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 de cette propriété un algorithme de complexité linéaire pour le problème[5].
Théorie de la complexité
![](http://upload.wikimedia.org/wikipedia/commons/thumb/a/a1/2017-fr.wp-orange-source.svg/25px-2017-fr.wp-orange-source.svg.png)
![](http://upload.wikimedia.org/wikipedia/commons/thumb/c/ce/Circle-icons-check.svg/20px-Circle-icons-check.svg.png)
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 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é
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
- ↑ (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
- ↑ A ne pas confondre avec les clauses de Horn qui sont aussi utilisées dans le problème SAT
- ↑ 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.
- ↑ Denis Trystram, « Leçon 5. Le problème SAT et ses variantes »,
- ↑ 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).
- ↑ (en) Papadimitriou, Computational complexity, Section 9.2, p. 185
- ↑ (en) Papadimitriou, Computational complexity, Theorem 16.2 (p. 398)
Portail de l'informatique théorique