Forme normale conjonctive

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 :

Exemples de formules en FNC :

$A\land B$
$A\lor B$
$A\!$
$(A\lor B)\land C$
$(A\lor \neg B\lor \neg C)\land (\neg D\lor E\lor F)$

Cependant, les expressions suivantes ne sont pas en FNC :

Contre exemples de formules en FNC :

$\neg (A\land B)$ — la négation $\neg$ est devant la formule $(A\land B)$ qui n'est pas atomique (ce n'est pas une variable)
$A\land (B\lor (C\land D))$ — un et est imbriqué dans un ou

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

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 certains cas faire grandir la formule de manière exponentielle.

Formule dont la FNC 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}\land Y_{1})\lor (X_{2}\land Y_{2})\lor \dots \lor (X_{n}\land Y_{n})

Dont la FNC, 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}).

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 $Z_{1},\ldots ,Z_{n}$ .

Exemple de transformation linéaire :

Une formule de la forme suivante :

(X_{1}\land Y_{1})\lor (X_{2}\land Y_{2})\lor \dots \lor (X_{n}\land 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, la variable $Z_{i}$ représente la vérité de la $i$ -ème conjonction de la formule originale, et les clauses $\neg Z_{i}\lor X_{i}$ et $\neg Z_{i}\lor Y_{i}$ expriment la condition $Z_{i}\rightarrow X_{i}\land Y_{i}$ . Dit autrement, si $Z_{i}$ est vraie, alors $X_{i}$ et $Y_{i}$ doivent être vraies 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 clauses de la formule originale soit vraie.

On peut aussi baser des transformations sur des clauses de type $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].

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

Notes et références

(fr) Jean Betrema, « Modèles de calcul », 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.
G. S. Tseitin, « On the complexity of derivation in propositional calculus », dans Automation of Reasoning, 1970 (lire en ligne)

Cet article est issu de wikipedia. Text licence: CC BY-SA 4.0, Des conditions supplémentaires peuvent s’appliquer aux fichiers multimédias.