Problème 3-SAT
En informatique théorique, plus précisément en théorie de la complexité, le problème 3-SAT est un problème surtout utilisé pour démontrer que d'autres problèmes sont NP-difficiles. C'est l'un des 21 problèmes NP-complets de Karp[1].
Cet article ne cite pas suffisamment ses sources ().
Si vous disposez d'ouvrages ou d'articles de référence ou si vous connaissez des sites web de qualité traitant du thème abordé ici, merci de compléter l'article en donnant les références utiles à sa vérifiabilité et en les liant à la section « Notes et références ».
En pratique : Quelles sources sont attendues ? Comment ajouter mes sources ?
Description modifier
Il s'agit de la restriction du problème SAT aux formules qui sont des formes normales conjonctives avec au plus 3 littéraux (ou exactement 3 selon les sources[2]). Voici un exemple d'une telle forme normale conjonctive :
La formule ci-dessus a 4 clauses, 5 variables et trois littéraux par clauses. Il s'agit de déterminer si l'on peut attribuer une valeur Vrai ou Faux à chaque variable de façon à rendre toute la formule vraie.
NP-difficulté modifier
En 1972, Richard M. Karp réduit SAT à 3-SAT afin de démontrer que 3-SAT est NP-difficile[1]. Cette démonstration est présente dans beaucoup d'ouvrages d'algorithmique et de théorie de la complexité.
Utilisation pour les preuves de NP-complétude modifier
Comme 3-SAT est NP-difficile, 3-SAT a été utilisé pour prouver que d'autres problèmes sont NP-difficiles. Richard M. Karp, dans le même article, montre que le problème de coloration de graphes est NP-difficile en le réduisant à 3-SAT en temps polynomial[1].
Variantes modifier
Jan Kratochvil introduit en 1994 une restriction 3-SAT dite planaire qui est aussi NP-difficile[3]. Il s'agit de la restriction de 3-SAT où le graphe biparti composé des variables et des clauses, où on relie une variable à une clause si cette clause contient cette variable, est planaire. D'ailleurs, le problème est toujours NP-difficile si chaque clause contient 3 littéraux et chaque variable apparaît dans au plus 4 clauses[3].
not-all-equal 3-satisfiability (NAE3SAT) est la variante où on demande que les trois variables dans une clause n'aient pas toutes les trois la même valeur de vérité.
Voir aussi modifier
- 2-SAT, le problème restreint aux clauses de taille 2, qui est de complexité polynomiale
Notes et références modifier
- (en) Richard M. Karp, « Reducibility among Combinatorial Problems », dans Complexity of Computer Computations, Springer US, (ISBN 9781468420036, DOI 10.1007/978-1-4684-2001-2_9, lire en ligne), p. 85–103
- Pour « au plus 3 », voir (en) Sanjeev Arora et Boaz Barak, Computational Complexity : A Modern Approach, Cambridge University Press, (ISBN 0-521-42426-7), chap. 2.3 (« The Cook-Levin Theorem: Computation is Local ») p. 43.
- (en) « A special planar satisfiability problem and a consequence of its NP-completeness », Discrete Applied Mathematics, vol. 52, no 3, , p. 233–252 (ISSN 0166-218X, DOI 10.1016/0166-218X(94)90143-0, lire en ligne, consulté le )
