Forme normale conjonctive

Un article de Wikipédia, l'encyclopédie libre.
Aller à : navigation, rechercher
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é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[modifier | modifier le code]

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 devant 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 :

Cependant, les expressions suivantes ne sont pas en FNC :

Contre exemples de formules en FNC :
  1. — la négation est devant la formule qui n'est pas atomique (ce n'est pas une variable)
  2. — un et est imbriqué dans un ou

Conversions en FNC[modifier | modifier le code]

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 : la formule en FNC résultante est de taille linéaire en la formule de départ et les deux formules sont équisatisfiables (mais pas logiquement équivalentes).

Conversion équivalente[modifier | modifier le code]

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 :

L'application des lois de la distributivité peut dans certain 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 :

Dont la FNC, de taille 2n, est de la forme :

Transformations linéaires[modifier | modifier le code]

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 .

Exemple de transformation linéaire :

Une formule de la forme suivante :

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

Intuitivement, dans cet exemple, la variable représente la vérité de la -ème conjonction de la formule originale, et imposent par les implications dans le cas où ces variables prennent la valeur vrai. Dit autrement, si est vrai, alors et doivent être vrai aussi. La première clause de la transformation impose qu'au moins un des 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 types . Ces clauses impliquent l'équivalence,  ; on peut voir dans ces formules la définition de comme un alias pour la formule .

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[modifier | modifier le code]

Notes et références[modifier | modifier le code]

  1. a et b (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.
  2. @incollection{tseitin1983complexity, title={On the complexity of derivation in propositional calculus}, author={Tseitin, Grigori S}, booktitle={Automation of reasoning}, pages={466--483}, year={1983}, publisher={Springer} }