FNC, FND et SAT : les formes normales booléennes

Toute formule booléenne peut s'écrire sous deux formes normales : la FNC (forme normale conjonctive) et la FND (forme normale disjonctive). Le problème de savoir si une FNC est satisfiable (SAT) est le premier problème prouvé NP-complet.

Forme normale conjonctive (FNC)

Une FNC est une conjonction (ET) de clauses, où chaque clause est une disjonction (OU) de littéraux.

Exemple : $(a \vee \bar{b}) \wedge (\bar{a} \vee b \vee c)$ est une FNC.

Toute formule booléenne admet une FNC équivalente.

Forme normale disjonctive (FND)

Une FND est une disjonction (OU) de termes, où chaque terme est une conjonction (ET) de littéraux.

Exemple : $(a \wedge b) \vee (\bar{a} \wedge c)$ est une FND.

Toute formule booléenne admet une FND équivalente (construite depuis sa table de vérité).

Le problème SAT

SAT (satisfiability) : une FNC donnée admet-elle une affectation de valeurs aux variables qui la rend vraie ?

SAT est NP-complet (théorème de Cook-Levin, 1971). C'est le premier problème démontré NP-complet.

Variantes notables

• 3-SAT : chaque clause contient exactement 3 littéraux. Également NP-complet.
• 2-SAT : chaque clause contient 2 littéraux. Résolu en temps polynomial.
• HornSAT : FNC dont chaque clause contient au plus un littéral positif. Résolu en temps linéaire.

Transformer une formule en FNC

Toute formule propositionnelle se met en FNC via :

Attention : cette transformation peut produire une FNC de taille exponentielle par rapport à la formule initiale. Pour éviter cela, on utilise la transformation de Tseitin qui introduit des variables auxiliaires et produit une FNC de taille linéaire équisatisfiable (mais pas équivalente).

• 1. Éliminer les implications : $A \Rightarrow B \equiv \neg A \vee B$
• 2. Pousser les négations vers les atomes (De Morgan) : $\neg(A \wedge B) \equiv \neg A \vee \neg B$
• 3. Distribuer les OR sur les AND : $A \vee (B \wedge C) \equiv (A \vee B) \wedge (A \vee C)$
• 4. Simplifier (élimination des répétitions)

Les solveurs SAT modernes

Malgré la NP-complétude de SAT, des solveurs industriels (MiniSat, Glucose, Kissat) résolvent en pratique des instances de millions de variables en quelques secondes. Leurs secrets :

• DPLL : exploration par backtracking avec propagation unitaire
• CDCL (Conflict-Driven Clause Learning) : apprentissage de clauses à partir des conflits, évite de refaire les mêmes erreurs
• Heuristiques de branchement : VSIDS, phase saving
• Redémarrages : vider périodiquement la pile de décisions

Une question ou une suggestion ? Écrivez-nous.