Définition : NFF-Sat
Un problème de satisfaction de contraintes booléennes, aussi appelé problème de satisfiabilité, consiste à déterminer, pour un ensemble de contraintes définies sur des variables booléennes, s’il existe une assignation de valeurs aux variables satisfaisant toutes les contraintes.
Un peu de vocabulaire :
Définition : Forme normale négative
On dit d’une formule logique, qu’elle est en forme normale négative (FNN) si :
- Les négations se trouvent uniquement sur les littéraux.
- En plus de l’opérateur de négation, seul l’opérateur de conjonction (“et”) et de disjonction (“ou”) est autorisé.
Pour prendre un exemple :
- $\overline{A \wedge B}$ n’est pas sous forme normale négative.
- $\overline{A}\wedge B$ est sous forme normale négative.
Définition : Satisifiabilité
On dit d’une formule booléenne qu’elle est satisfiable s’il existe une assignation (ou valuation) des variables tel qu’elle rende la formule “vrai”.
Par exemple :
- $\overline{A}\wedge A$ n’est pas satisfiable
- $\overline{A}\lor A$ est satisfiable
Fun-Fact : Dans le deuxième cas, peu importe la valeur de notre seule variable A, notre formule est satisfiable, on peut dans ce cas parler de tautologie.
Le problème NFF-Sat :
Le problème NFF-Sat, ou NegLit-Sat peut se présenter en 2 lignes :
Soit $\mathcal{F}$ une formule booléenne telle que $\mathcal{F}$ est sous forme normale négative.
$\mathcal{F}$ est-elle satisfiable ?