3-SAT vers clique

Un article de Wikipédia, l'encyclopédie libre.
Aller à : navigation, rechercher
image illustrant la logique image illustrant la théorie des graphes image illustrant l’informatique théorique
Cet article est une ébauche concernant la logique, la théorie des graphes et l’informatique théorique.

Vous pouvez partager vos connaissances en l’améliorant (comment ?) selon les recommandations des projets correspondants.

Ce modèle est-il pertinent ? Cliquez pour en voir d'autres.
Cet article ne cite pas suffisamment ses sources (octobre 2012).

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 » (modifier l'article, comment ajouter mes sources ?).

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 à clauses est satisfiable si et seulement si le graphe a une clique d'ordre .

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