Version sans JavaScript, en lecture seule : les ateliers, les quiz et l’exécution du code n’y sont pas. Version complète · Catalogue · Se connecter

Support de cours · chapitre 3

Formes normales

Ramener toute formule à une forme standard, conjonction de clauses ou disjonction de conjonctions, et ce que ça coûte.

Pourquoi une forme normale

Une même idée s'écrit de mille façons : $p \to q$, $\lnot p \lor q$, $\lnot q \to \lnot p$, $\lnot(p \land \lnot q)$ sont équivalentes. Pour comparer deux formules, les simplifier, ou les donner à un programme, on les ramène à une forme normale : une écriture standard, construite avec $\lnot$, $\land$ et $\lor$ seulement, et dans un ordre imposé.

Les deux formes de ce chapitre sont celles qu'utilisent les outils : la forme normale conjonctive est l'entrée des solveurs SAT (chapitre 4) et de la résolution (chapitre 5).

Le vocabulaire

  • Un littéral est une variable ou sa négation : $p$, $\lnot q$.
  • Une clause est une disjonction de littéraux : $p \lor \lnot q \lor r$. Un seul littéral est une clause ; la clause vide, sans littéral, vaut $\bot$.
  • Un monôme est une conjonction de littéraux : $p \land \lnot q \land r$.

Une formule est en :

  • forme normale conjonctive (FNC) si c'est une conjonction de clauses : $(p \lor q) \land (\lnot p \lor r) \land \lnot q$ ;
  • forme normale disjonctive (FND) si c'est une disjonction de monômes : $(p \land q) \lor (\lnot p \land r) \lor \lnot q$.

Moyen mnémotechnique : dans une FNC, le connecteur principal est la conjonction.

Mettre en forme normale par calcul

Trois étapes

  1. Éliminer $\leftrightarrow$ et $\to$ : $A \leftrightarrow B \equiv (A \to B) \land (B \to A)$, puis $A \to B \equiv \lnot A \lor B$.
  2. Faire descendre les négations jusqu'aux variables, avec De Morgan et la double négation. On obtient la forme normale négative : les $\lnot$ ne portent plus que sur des variables.
  3. Distribuer :
  4. pour une FNC, $\lor$ sur $\land$ : $A \lor (B \land C) \equiv (A \lor B) \land (A \lor C)$ ;
  5. pour une FND, $\land$ sur $\lor$ : $A \land (B \lor C) \equiv (A \land B) \lor (A \land C)$.

On termine en simplifiant : une clause qui contient $p$ et $\lnot p$ vaut $\top$ et disparaît d'une FNC ; un monôme qui contient $p$ et $\lnot p$ vaut $\bot$ et disparaît d'une FND ; l'absorption retire une clause qui en contient une autre.

Mettre en forme normale par la table de vérité

Chaque ligne de la table est décrite par un monôme : la ligne $p = 1, q = 0$ est décrite par $p \land \lnot q$, vrai sur cette ligne et nulle part ailleurs.

  • FND : la disjonction des monômes des lignes où la formule vaut 1.
  • FNC : la conjonction des négations des lignes où la formule vaut 0. La négation du monôme $p \land \lnot q$ est la clause $\lnot p \lor q$.

Cette méthode prouve que toute formule a une FND et une FNC : il suffit de lire sa table. Elle a un défaut : la table a $2^n$ lignes.

Ce que ça coûte

La distribution peut faire exploser la taille. La formule

$$(p_1 \land q_1) \lor (p_2 \land q_2) \lor \cdots \lor (p_n \land q_n)$$

est une FND de $2n$ littéraux. Sa FNC choisit un littéral dans chaque parenthèse, de toutes les façons possibles : elle a $2^n$ clauses. Pour $n = 30$, plus d'un milliard.

On ne cherche donc pas une FNC équivalente quand elle est trop grosse : les solveurs utilisent une FNC équisatisfiable (satisfiable si et seulement si la formule de départ l'est), obtenue en ajoutant de nouvelles variables, qui reste de taille linéaire. C'est la transformation de Tseitin, hors programme ici.

Ce que ça prouve : trois connecteurs suffisent

Comme toute formule a une FND, toute table de vérité s'écrit avec $\lnot$, $\land$ et $\lor$ seulement. On dit que $\{\lnot, \land, \lor\}$ est un ensemble fonctionnellement complet.

On peut descendre plus bas : $A \lor B \equiv \lnot(\lnot A \land \lnot B)$, donc $\{\lnot, \land\}$ suffit. Et un seul connecteur suffit, le « non-et » ($p \uparrow q$, vrai sauf quand $p$ et $q$ le sont) : $\lnot p \equiv p \uparrow p$. C'est pourquoi un circuit électronique peut être entièrement construit de portes NAND.

« Exactement un parmi $n$ »

Contrainte fréquente en modélisation : exactement une des propositions $p_1, \ldots, p_n$ est vraie. On l'écrit en FNC comme la conjonction de deux contraintes :

  • au moins un : la clause $p_1 \lor p_2 \lor \cdots \lor p_n$ ;
  • au plus un : pour chaque paire, $\lnot p_i \lor \lnot p_j$.

Pour trois propositions : $(p \lor q \lor r) \land (\lnot p \lor \lnot q) \land (\lnot p \lor \lnot r) \land (\lnot q \lor \lnot r)$.