Problème 3-SAT

Cet article ne cite pas suffisamment ses sources (février 2009).

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 ?

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

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 :

${\displaystyle (v_{1}\lor v_{2}\lor v_{3})\land (\neg v_{1}\lor v_{2}\lor v_{4})\land (\neg v_{1}\lor v_{2}\lor \neg v_{5})\land (\neg v_{3}\lor v_{4}\lor v_{5})}$

La formule ci-dessus a 4 clauses, 5 variables ${\displaystyle v_{1},v_{2},v_{3},v_{4},v_{5}}$ et trois littéraux par clauses. Il s'agit de déterminer si l'on peut attribuer une valeur Vrai ou Faux à chaque variable ${\displaystyle v_{i}}$de façon à rendre toute la formule vraie.

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

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

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

• 2-SAT, le problème restreint aux clauses de taille 2, qui est de complexité polynomiale

• Portail de l'informatique théorique
• Portail de la logique
• Portail de l’informatique