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 :

${\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.

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

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