Forme normale conjonctive

Pour les articles homonymes, voir CNF.

En logique booléenne et en calcul des propositions, une formule en forme normale conjonctive ou FNC (en anglais, Conjunctive Normal Form, Clausal Normal Form ou CNF) est une conjonction de clauses, où une clause est une disjonction de littéraux. Les formules en FNC sont utilisées dans le cadre de la démonstration automatique de théorèmes ou encore dans la résolution du problème SAT (en particulier dans l'algorithme DPLL).

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 :

Cependant, les expressions suivantes ne sont pas en FNC :

Conversion en FNC équivalente

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. 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é.

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

Conversion linéaire équisatisfiable

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.

Cette transformation s'appelle parfois transformation de Tseytin (ou transformation de Tseitin^[2]).

La formule de l'exemple 2, par exemple, peut être réécrite en introduisant les variables ${\displaystyle Z_{1},\ldots ,Z_{n}}$.

Intuitivement, dans cet exemple, la variable ${\displaystyle Z_{i}}$ représente la vérité de la ${\displaystyle i}$-ème conjonction de la formule originale, et les clauses ${\displaystyle \neg Z_{i}\lor X_{i}}$et ${\displaystyle \neg Z_{i}\lor Y_{i}}$expriment la condition ${\displaystyle Z_{i}\rightarrow X_{i}\land Y_{i}}$. Dit autrement, si ${\displaystyle Z_{i}}$ est vraie, alors ${\displaystyle X_{i}}$ et ${\displaystyle Y_{i}}$ doivent être vraies aussi. La première clause de la transformation impose qu'au moins un des ${\displaystyle Z_{i}}$ soit vrai pour que la formule soit satisfaite, donc qu'au moins une des clauses de la formule originale soit vraie.

On peut aussi baser des transformations sur des clauses de type ${\displaystyle Z_{i}\vee \neg X_{i}\vee \neg Y_{i}}$. Ces clauses impliquent l'équivalence, ${\displaystyle Z_{i}\equiv X_{i}\wedge Y_{i}}$ ; on peut voir dans ces formules la définition de ${\displaystyle Z_{i}}$ comme un alias pour la formule ${\displaystyle 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].

Problème SAT

Le problème SAT est le problème algorithmique qui consiste, étant donné une formule à décider en FNC si elle est valide ou non. Le problème est NP-complet, même pour le cas particulier 3-SAT où on n'autorise que les clauses d'au plus trois littéraux. Par contre le problème avec des clauses de taille 2, 2-SAT peut-être résolu en temps polynomial.

Voir aussi

• Forme normale disjonctive
• Forme normale négative
• 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

• Portail de la logique
• Portail des mathématiques