Forme normale conjonctive

Article principal : Calcul des propositions.

En logique booléenne et en calcul des propositions, une forme normale conjonctive (FNC) est une normalisation d'une expression logique qui est une conjonction de clauses, autrement dit une conjonction de disjonction de littéraux. Les formules en FNC sont utilisée dans le cadre démonstration automatique de théorèmes ou encore dans la résolution du problème SAT.

Définition et exemples

Une expression logique est en FNC si et seulement si elle est une conjonction d'une ou plusieurs disjonction(s) d'un ou plusieurs littéraux. Tout comme dans une forme normale disjonctive (FND), les seuls opérateurs dans une FNC sont le et logique, le ou logique et la négation. L'opérateur non ne peut être utilisé que dans un littéral, c'est-à-dire qu'il ne peut que précéder une variable. Par exemple, toutes les expressions suivantes sont en FNC:

Exemples de formules en FNC  :

1. $A \and B$
2. $A\!$
3. $(A \or B) \and C$
4. $(A \or \neg B \or \neg C) \and (\neg D \or E \or F)$

Cependant, les expressions suivantes ne sont pas en FNC:

Contre exemples de formules en FNC  :

1. $\neg(A \and B)$ — la négation s'applique à toute la parenthèse plutôt que directement à une variable
2. $A \and (B \or (C \and D))$ — un et est imbriqué dans un ou

Conversions en FNC

Toute formule booléenne peut se réécrire sous la forme d'une formule en FNC qui possède la même valeur de vérité, donc logiquement équivalente.

D'autres transformations nécessitent l'introduction de variables (ou de propositions) supplémentaires, mais ont l'avantage de garantir que la taille de la formule résultante restera raisonnable.

Conversion équivalente

Convertir une expression vers une FNC requiert l'utilisation de règles de transformation logiques, comme l'élimination de double négations, les lois de De Morgan, et la loi de distributivité.

Transformation en FNC  :

$(\lnot (X_1 \lor X_2) \lor (X_3 \land X_4) ) \land (\lnot X_1 \lor X_2)$

$\equiv$

$(\lnot X_1 \lor X_3 ) \land (\lnot X_1 \lor X_4) \land (\lnot X_2 \lor X_3) \land (\lnot X_2 \lor X_4) \land (\lnot X_1 \lor X_2)$

L'application des lois de la distributivité peut dans certain cas faire grandir la formule de manière exponentielle.

Formule dont la CNF possède une taille exponentielle  :

la FNC d'une expression de la forme suivante, en Forme normale disjonctive, et qui comporte n termes :

$(X_1 \and Y_1) \or (X_2 \and Y_2) \or \dots \or (X_n \and Y_n)$

Dont la CNF, de taille 2ⁿ, est de la forme :

$(X_1 \vee \cdots \vee X_{n-1} \vee X_n) \wedge (X_1 \vee \cdots \vee X_{n-1} \vee Y_n) \wedge \cdots \wedge (Y_1 \vee \cdots \vee Y_{n-1} \vee Y_n).$

Transformations linéaires

Pour éviter les transformations exponentielles, il est possible d'appliquer des transformations en introduisant des variables supplémentaires^[1]. De ce fait, ce type de transformation ne crée plus des formules logiquement équivalentes, comme la transformation précédente, mais des transformations qui préservent la satisfiabilité de la formule originale.

La formule de l' exemple 2, par exemple, peut être réécrites en introduisant les variables $Z_1,\ldots,Z_n$.

Exemple de transformation linéaire  :

Une formule de la forme suivante :

$(X_1 \and Y_1) \or (X_2 \and Y_2) \or \dots \or (X_n \and Y_n)$

Peut être réécrite en une formule équisatisfiable

$(Z_1 \vee \cdots \vee Z_n) \wedge (\neg Z_1 \vee X_1) \wedge (\neg Z_1 \vee Y_1) \wedge \cdots \wedge (\neg Z_n \vee X_n) \wedge (\neg Z_n \vee Y_n).$

Intuitivement, dans cet exemple, les variables Z_n imposent la vérité de la i-ème conjonction de la formule originale, et imposent par les implications $Z_i \rightarrow X_i,Z_i\rightarrow Y_n$ dans le cas ou ces variables prennent la valeur vrai. Dit autrement, si Z_n est vrai, alors X_i et Y_i doivent être vrai aussi. La première clause de la transformation impose qu'au moins un des Z_i soit vrai pour que la formule soit satisfaite, donc qu'au moins une des clause de la formule originale soit vraie.

On peut aussi baser des transformations sur des clauses de types $Z_i \vee \neg X_i \vee \neg Y_i$. Ces clauses impliquent l'équivalence, $Z_i \equiv X_i \wedge Y_i$; on peut voir dans ces formules la définition de Z_i comme un alias pour la formule $X_i \wedge Y_i$.

De telles transformations permettent d'obtenir une formule en FNC dont la taille est linéaire par rapport à la taille de la formule originale^[1].

Voir aussi

• Forme normale disjonctive
• Forme normale algébrique
• Fonction booléenne
• Clause de Horn
• Calcul des propositions
• Algorithme de Quine–McCluskey
• Table de vérité
• Littéral (logique)
• Section sur les formes normales dans l'article sur le calcul des propositions

Notes et références

1. ↑ ^{a et b} (fr)Jean Betrema, « Modèles de calcul », p. chapitre 9 : Problèmes NP-complets > SAT est NP-complet > CNF est NP-complet.
   Preuve et transformation linéaire d'une formule SAT quelconque en CNF équisatisfiable.