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
modifierUne 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 :
- — la négation est devant la formule qui n'est pas atomique (ce n'est pas une variable)
- — un et est imbriqué dans un ou
Conversion en FNC équivalente
modifierToute 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.
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 :
Conversion linéaire équisatisfiable
modifierPour é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 .
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 les clauses et expriment la condition . Dit autrement, si est vraie, alors et doivent être vraies 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 type . 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].
Problème SAT
modifierLe problème SAT est le problème algorithmique qui consiste, étant donné une formule en FNC à décider si elle est satisfiable ou non. Le problème est NP-complet, même pour le cas particulier 3-SAT où on n'autorise que les clauses de trois littéraux (3-clauses). Par contre le problème avec des clauses de taille 2 (2-clauses), 2-SAT peut-être résolu en temps polynomial, il appartient donc à la classe de compléxité P.
Voir aussi
modifierNotes et références
modifier- (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, (lire en ligne).
