Conjective (forme normale)

Imaginez une serrure qui ne s’ouvre que si plusieurs contrôles réussissent. Chaque contrôle propose plusieurs possibilités : il suffit qu’une seule soit vraie. En revanche, tous les contrôles doivent être validés ensemble.

Une forme normale conjonctive organise une proposition exactement ainsi. Les possibilités regroupées par « ou » forment des clauses, puis les clauses sont reliées par « et ». Cette structure rend immédiatement visibles les conditions à satisfaire simultanément.

Une formule de logique propositionnelle est en forme normale conjonctive, abrégée FNC, lorsqu’elle est une conjonction de clauses. Une clause est une disjonction de littéraux. Un littéral est soit une variable propositionnelle, comme P, soit la négation d’une telle variable, comme ¬P. Ainsi, $(P\vee R)\wedge (\mathrm{\neg }Q\vee R)(P\; \backslash lor\; R)\; \backslash land\; (\backslash neg\; Q\; \backslash lor\; R)$ est une FNC : ses deux clauses sont reliées par « et », et chaque clause réunit ses littéraux par « ou ».

Dans le cadre classique des formules propositionnelles finies, toute formule possède une FNC logiquement équivalente. On élimine d’abord les implications éventuelles, on pousse les négations jusqu’aux variables avec les lois de De Morgan en supprimant les doubles négations, puis on distribue « ou » sur « et ». L’équivalence signifie que la formule initiale et sa FNC prennent la même valeur de vérité pour chaque attribution des variables.

La FNC est la forme duale de la forme normale disjonctive : cette dernière est un « ou » de groupes construits avec « et ». La structure en clauses convient particulièrement aux problèmes de satisfaisabilité : un solveur SAT cherche une attribution qui rend vraie chaque clause.

Prenons trois propositions : P signifie « la porte est ouverte », Q signifie « la fenêtre est ouverte » et R signifie « l’alarme est active ». On part de la formule $\mathrm{\neg }(P\vee Q)\vee R\backslash neg(P\; \backslash lor\; Q)\; \backslash lor\; R$. L’objectif est d’obtenir une FNC équivalente.

1. Appliquer la loi de De Morgan à la parenthèse : $\mathrm{\neg }(P\vee Q)\equiv \mathrm{\neg }P\wedge \mathrm{\neg }Q\backslash neg(P\; \backslash lor\; Q)\; \backslash equiv\; \backslash neg\; P\; \backslash land\; \backslash neg\; Q$.
2. Remplacer dans la formule : $(\mathrm{\neg }P\wedge \mathrm{\neg }Q)\vee R(\backslash neg\; P\; \backslash land\; \backslash neg\; Q)\; \backslash lor\; R$.
3. Distribuer « ou R » sur la conjonction : $(\mathrm{\neg }P\vee R)\wedge (\mathrm{\neg }Q\vee R)(\backslash neg\; P\; \backslash lor\; R)\; \backslash land\; (\backslash neg\; Q\; \backslash lor\; R)$.
4. Repérer les deux clauses : $\mathrm{\neg }P\vee R\backslash neg\; P\; \backslash lor\; R$ et $\mathrm{\neg }Q\vee R\backslash neg\; Q\; \backslash lor\; R$. Elles sont reliées par « et » : le résultat est bien une FNC.

Contrôle avec P vraie, Q fausse et R fausse : la formule initiale est fausse, car ¬(vrai ou faux) est faux. La FNC est également fausse : sa première clause vaut faux et sa seconde vaut vrai. La figure récapitule les deux transformations et la structure finale en clauses.

En logique formelle, la mise en FNC transforme une formule composée en une liste de contraintes lisibles clause par clause. Si l’on veut plutôt exhiber des scénarios suffisants reliés par « ou », la forme normale disjonctive est plus naturelle.

Dans un solveur SAT, chaque clause impose qu’au moins un de ses littéraux soit vrai, tandis que leur conjonction impose de satisfaire toutes les clauses. Une attribution est rejetée dès qu’elle rend une clause entière fausse.

En vérification de modèles, cette organisation encode des contraintes que l’on teste ensemble. Pour une petite formule, une conversion équivalente par distribution suffit ; pour une grande formule, un encodage avec variables auxiliaires évite souvent une explosion de taille.

Forme normale disjonctive. Elle inverse les deux niveaux : c’est une disjonction de conjonctions de littéraux. Le test est syntaxique : $(P\wedge Q)\vee (\mathrm{\neg }P\wedge R)(P\; \backslash land\; Q)\; \backslash lor\; (\backslash neg\; P\; \backslash land\; R)$ est disjonctive, tandis que $(P\vee Q)\wedge (\mathrm{\neg }P\vee R)(P\; \backslash lor\; Q)\; \backslash land\; (\backslash neg\; P\; \backslash lor\; R)$ est conjonctive.

Une simple conjonction. Relier deux sous-formules par « et » ne garantit pas une FNC. Dans $(P\leftrightarrow Q)\wedge R(P\; \backslash leftrightarrow\; Q)\; \backslash land\; R$, le premier membre contient encore une équivalence et n’est donc pas une clause formée uniquement de littéraux.

Taille de la formule. La distribution produit parfois beaucoup plus de clauses que la formule de départ. Une conversion équivalente directe peut donc devenir impraticable, même si elle est toujours possible pour une formule propositionnelle finie.

Équivalence ou simple équi-satisfaisabilité. Les encodages efficaces destinés aux solveurs introduisent parfois des variables auxiliaires. La nouvelle FNC a alors une solution exactement quand la formule initiale en a une, sans nécessairement conserver la même valeur sous toute attribution étendue.

Cas vides. Selon les conventions usuelles, la conjonction d’aucune clause représente vrai, tandis qu’une clause sans littéral représente faux. Il faut vérifier la convention du logiciel ou du texte avant d’interpréter ces deux cas dégénérés.

Parenthèses omises. Une écriture compacte peut masquer les deux niveaux de la FNC. Il faut d’abord isoler chaque clause, puis vérifier qu’elle ne contient que des littéraux reliés par « ou » et que toutes les clauses sont reliées par « et ».

Les lois de De Morgan expliquent comment une négation traverse « et » ou « ou », étape indispensable avant la distribution.

La forme normale disjonctive présente la construction duale et aide à distinguer une conjonction de clauses d’une disjonction de termes.