- 3-SAT vers clique
-
Le 3-SAT vers clique est une question de logique mathématique.
Réduction polynomiale
Pour réduire le problème 3-SAT vers celui de la clique, à chaque formule 3-CNF, on associe un graphe non orienté dont le nombre de sommets est trois fois le nombre de clauses de la manière suivante :
- à chacun des trois littéraux de chaque clause, on associe un sommet ;
- on relie les sommets par des arêtes de la manière suivante : deux sommets qui sont associés aux littéraux d'une même clause ne sont pas reliés par une arête, deux sommets qui sont associés à un littéral et sa négation ne sont pas reliés non plus, tous les autres couples de sommets sont reliés.
On démontre alors que la formule à k clauses est satisfiable si et seulement si le graphe a une clique d'ordre k.
Idée de la preuve :
Si la formule est satisfiable, il existe une assignation des variables pour laquelle la valeur d'au moins un littéral de chaque clause est VRAI. L'ensemble formé des sommets associés à l'un de ces littéraux par clause est une clique du graphe.
Si le graphe a une clique d'ordre k, elle contient exactement un sommet parmi les trois qui représentent les littéraux de chaque clause ; on peut définir une assignation des variables pour laquelle la valeur de ces littéraux est VRAI ; la valeur de la formule pour cette assignation est alors VRAI.
Wikimedia Foundation. 2010.
