3-SAT vers clique

Un article de Wikipédia, l'encyclopédie libre.
Aller à : navigation, rechercher

Le 3-SAT vers clique est une question de logique mathématique et de théorie des graphes.

Réduction polynomiale[modifier | modifier le code]

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.