Êtes-vous un étudiant de l'EPFL à la recherche d'un projet de semestre?
Travaillez avec nous sur des projets en science des données et en visualisation, et déployez votre projet sous forme d'application sur Graph Search.
Concept
Problème SAT
Résumé
vignette|Une instance du Sudoku peut être transformée en une formule de logique propositionnelle à satisfaire. Une assignation des variables propositionnelles donne une grille complétée.
En informatique théorique, le problème SAT ou problème de satisfaisabilité booléenne est le problème de décision, qui, étant donné une formule de logique propositionnelle, détermine s'il existe une assignation des variables propositionnelles qui rend la formule vraie.
Ce problème est important en théorie de la complexité. Il a été mis en lumière par le théorème de Cook, qui est à la base de la théorie de la NP-complétude et du problème P = NP. Le problème SAT a aussi de nombreuses applications notamment en satisfaction de contraintes, planification classique, model checking, diagnostic, et jusqu'au configurateur d'un PC ou de son système d'exploitation : on se ramène à des formules propositionnelles et on utilise un .
Logique propositionnelleLes formules de la logique propositionnelle sont construites à partir de variables propositionnelles et des connecteurs booléens "et" (), "ou" (), "non" (). Une formule est satisfaisable (on dit aussi satisfiable) s'il existe une assignation des variables propositionnelles qui rend la formule logiquement vraie. Par exemple :
La formule est satisfaisable car si prend la valeur faux, la formule est évaluée à vrai.
La formule n'est pas satisfaisable car aucune valeur de p ne peut rendre la formule vraie.
Forme normale conjonctive
Un littéral est une variable propositionnelle (littéral positif) ou la négation d'une variable propositionnelle (littéral négatif). Une clause est une disjonction de la forme où les sont des littéraux.
Une formule du calcul propositionnel est en forme normale conjonctive (ou forme clausale ou CNF sigle de l'anglais Conjunctive Normal Form) si elle est une conjonction de clauses.
Exemple
Soit l'ensemble de variables et la formule .
et sont des clauses avec deux littéraux par clause.
Leur conjonction est une forme normale conjonctive.
Source officielle
À propos de ce résultat
Cette page est générée automatiquement et peut contenir des informations qui ne sont pas correctes, complètes, à jour ou pertinentes par rapport à votre recherche. Il en va de même pour toutes les autres pages de ce site. Veillez à vérifier les informations auprès des sources officielles de l'EPFL.