Définition : NFF-Sat

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 ?

Sources :

1. Représentations de formules SAT pour la Résolution Séquentielle
2. Valuation Logic - Wikipédia
3. Satisfiability - Wikipédia
4. Negation normal form - Wikipédia