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

Description

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é

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

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

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

Notes et références

  1. a b et c (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
  2. 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.
  3. a et b (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 )