Forme normale négative décomposable

En logique propositionnelle, dans le cadre de la compilation de connaissance, une fonction booléenne est passée d'un langage de représentation standard (par exemple une représentation CNF) vers un langage cible plus adapté pour répondre aux futures requêtes sur la fonction^[1]. Les circuits booléens en forme normale négative décomposable — plus succinctement DNNF, de l'anglais Decomposable Negation Normal Form — constituent un de ces langages cibles. Toute fonction booléenne a au moins un circuit DNNF qui lui est équivalent. Les circuits DNNF sont parmi les représentations les plus compactes des fonctions qui permettent de réaliser des tests de cohérence (ou satisfaisabilité) en temps polynomial en la taille du circuit, en contre-partie de tels circuits sont souvent plus larges que les représentations standards de la fonctions, et par un facteur exponentiel.

Définition

Concepts de base sur les circuits booléens

Les circuits considérés ont un nombre fini d'entrées et une seule sortie booléenne. Les entrées sont des variables booléennes ou des constantes vrai (notée ${\displaystyle 1}$) ou faux (notée ${\displaystyle 0}$). On désigne par ${\displaystyle var(C)}$ l'ensemble des variables en entrée du circuit ${\displaystyle C}$. La taille de ${\displaystyle C}$, notée ${\displaystyle \vert C\vert }$, est le nombre de ses connexions entre portes. Un circuit sur ${\displaystyle n}$ variables est associé à une fonction booléenne ${\displaystyle f:\{0,1\}^{n}\rightarrow \{0,1\}}$ dont les modèles (les affectations de variables pour lesquelles la fonction vaut ${\displaystyle 1}$) sont exactement les affectations de variables pour lesquelles la sortie du circuit est mise à ${\displaystyle 1}$ (vrai). Par extension on appelle également ces affectations des modèles du circuit, on utilise ${\displaystyle C^{-1}(1)}$ pour désigner l'ensemble des modèles de ${\displaystyle C}$.

Circuits NNF

Les portes utilisées par les circuits sous forme normal négative, ou NNF (de l'anglais Negation Normal Form), sont

• les portes ET (${\displaystyle \wedge }$) ;
• les portes OU (${\displaystyle \vee }$) ;
• les portes NEG (${\displaystyle \lnot }$) à une entrée.

Il n'y a pas de limite sur l'arité en sortie de ces portes. Il n'y a pas de limite sur l'arité en entrée des portes ET et OU.

Un circuit ${\displaystyle C}$ est sous forme NNF^[1] si

• le graphe orienté de ses portes est acyclique et
• les portes NEG sont uniquement appliquées sur des entrées de ${\displaystyle C}$.

Régulièrement on étend les entrées des circuits aux variables booléennes (${\displaystyle x}$) et à leurs compléments (${\displaystyle \neg x}$), de sorte qu'il n'y a plus de portes NEG dans les circuits NNF.

Circuits DNNF

Une porte ET est décomposable si les sous-circuits branchés en entrée agissent sur des ensembles distincts de variables. Formellement, les circuits ${\displaystyle C_{1},C_{2},...,C_{m}}$ branchés sur les entrées d'une porte ET décomposable vérifient ${\displaystyle var(C_{i})\cap var(C_{j})=\emptyset }$ pour tout ${\displaystyle i\neq j}$, autrement dit si la variable ${\displaystyle x}$ ou son complément est une entrée de ${\displaystyle C_{i}}$, alors ni ${\displaystyle x}$ ni ${\displaystyle \neg x}$ n'est une entrée ${\displaystyle C_{j}}$. Un circuit NNF décomposable, ou DNNF^[2] (de l'anglais Decomposable Negation Normal Form) est un circuit NNF dont toutes les portes ET sont décomposables.

A gauche : un circuit NNF dont la première porte est un ET non décomposable. À droite : un circuit DNNF représentant la même fonction booléenne.

Terminologie : circuits ou formules ?

Certaines représentations de fonctions booléennes sont désignés comme des formules, par exemple des formules DNF ou CNF, en général on évite d'employer ce terme pour les NNF. Une formule booléenne désigne un circuit booléen dont chaque porte ne peut être l'entrée que d'une seule autre porte^[3] (l'arité en sortie des portes est au plus 1). Cette condition est toujours remplie par les circuits CNF et DNF de sorte que les appellations « formules CNF » et « formules DNF » sont correctes. Cependant les NNF, et a fortiori les DNNF, ne requièrent pas de limite sur l'arité en sortie des portes, il est donc préférable de les désigner comme des circuits booléens.

Relations d'inclusion et de compacité pour les DNNF

Par définition, les DNNF forment une sous-classe des NNF, ce que l'on notera

${\displaystyle {\textsf {DNNF}}\subset {\textsf {NNF}}}$

Les DNNF englobent d'autres classes importantes de circuits, notamment les DNF (Disjunctive Normal Form, ou en français : Forme Normale Disjonctive) et certains types de BDD (Binary Decision Diagram, ou en français : Diagramme de Décision Binaires).

DNNF et DNF

Les DNF sont des DNNF à condition d'être cohérentes : c'est-à-dire qu'aucun terme ne contient à la fois une variable ${\displaystyle x}$ et son complément ${\displaystyle \neg x}$. Chaque terme cohérent d'une DNF forme une porte ET décomposable, les DNF sont donc des DNNF à deux étages : un premier étage de portes ET correspondant aux différents termes de la DNF, et un second étage composé d'une unique porte OU sur laquelle les portes ET des termes sont branchées en entrée.

${\displaystyle {\textsf {DNF}}\subset {\textsf {DNNF}}}$

DNNF et BDD

A gauche : un nœud de décision sur la variable ${\displaystyle x}$. À droite : la traduction de ce nœud en circuit.

Les diagrammes de décision binaires (BDD) ont une traduction NNF naturelle. Une méthode pour l'obtenir consiste à convertir les nœuds de décision de la BDD en circuits NNF comme indiqué sur la figure. Quand on atteint les nœuds terminaux ${\displaystyle 0}$ et ${\displaystyle 1}$, ceux-ci sont transformés en entrées constantes ${\displaystyle 0}$ ou ${\displaystyle 1}$. Comme le graphe orienté d'une BDD est acyclique et qu'aucune porte NEG n'est introduite dans la procédure sauf sur des entrées booléennes, le circuit obtenu est sous forme NNF. Si dans le cas représenté sur la figure, ${\displaystyle x}$ n'appartient ni à ${\displaystyle var(C_{0})}$ ni à ${\displaystyle var(C_{1})}$ alors le circuit pour ce nœud de décision est une DNNF.

On obtient donc des DNNF quand les BDD sont telles que chaque variable apparaît au plus une fois par chemin. Ces BDD forment la classe des FBDD^[1],[4] (Free Binary Decision Diagram). Par souci de simplicité on considère directement les FBDD comme une sous-classe des DNNF. Une sous-classe importante des FBDD sont les OBDD^[1],[4] (Ordered Binary Decision Diagram), pour lesquels l'ordre d'apparition des variables est le même pour chaque chemin. Les OBDD forment donc aussi une sous-classe de DNNF.

${\displaystyle {\textsf {OBDD}}\subset {\textsf {FBDD}}\subset {\textsf {DNNF}}}$

Relation de compacité

Différents circuits représentant une même fonction booléenne sont comparés selon leur taille (nombre de connexions entre portes). Soit deux classes des circuits ${\displaystyle {\mathcal {L}}}$ et ${\displaystyle {\mathcal {L}}'}$ permettant de représenter n'importe quelle fonction booléenne, on dit que ${\displaystyle {\mathcal {L}}}$ permet des représentations plus compactes que ${\displaystyle {\mathcal {L}}'}$ (noté ${\displaystyle {\mathcal {L}}\preceq {\mathcal {L}}'}$) quand il existe une polynôme réel ${\displaystyle p}$ tel que pour chaque circuit ${\displaystyle C'\in {\mathcal {L}}'}$ il existe un circuit équivalent ${\displaystyle C\in {\mathcal {L}}}$ vérifiant ${\displaystyle \vert C'\vert \leq p(\vert C\vert )}$. La relation ${\displaystyle \preceq }$ est transitive. Il est clair que si ${\displaystyle {\mathcal {L}}'\subset {\mathcal {L}}}$, alors ${\displaystyle {\mathcal {L}}\preceq {\mathcal {L}}'}$, puisque chaque ${\displaystyle C'}$ dans ${\displaystyle {\mathcal {L}}'}$ appartient aussi à ${\displaystyle {\mathcal {L}}}$ et que donc la définition précédente s'applique avec ${\displaystyle p}$ le polynôme identité.
On note ${\displaystyle {\mathcal {L}}\prec {\mathcal {L}}'}$ quand ${\displaystyle {\mathcal {L}}\preceq {\mathcal {L}}'}$ mais que la relation inverse est fausse. C'est-à-dire que ${\displaystyle {\mathcal {L}}'\npreceq {\mathcal {L}}}$ : il existe une famille ${\displaystyle {\mathcal {F}}}$ (nécessairement infinie) de circuits dans ${\displaystyle {\mathcal {L}}}$ et une fonction ${\displaystyle f}$ super-polynomiale (i.e., tout polynôme réel est dans ${\displaystyle o(f)}$, typiquement ${\displaystyle f(n)=\Omega (2^{n})}$ ou ${\displaystyle f(n)=\Omega (n^{\log {n}})}$) telles que pour tout ${\displaystyle C\in {\mathcal {F}}}$ et ${\displaystyle C'\in {\mathcal {L}}'}$ équivalent à ${\displaystyle C}$, on a ${\displaystyle \vert C'\vert \geq f(\vert C\vert )}$.

Les relations de compacités entre les DNNF et les classes de circuits précédemment décrites sont strictes^[1] :

${\displaystyle {\textsf {DNF}}\prec {\textsf {DNNF}}\prec {\textsf {NNF}}}$ et ${\displaystyle {\textsf {FBDD}}\prec {\textsf {DNNF}}}$

Les OBDD formant une sous-classe de FBDD, on a aussi ${\displaystyle {\textsf {OBDD}}\prec {\textsf {DNNF}}}$ par transitivité.

Requêtes sur des circuits DNNF

Faisabilité des différentes requêtes en temps polynomial

Le choix d'une classe de circuits pour représenter une fonction booléenne dépend des requêtes auxquelles la fonction sera sujette. Les requêtes peuvent être des problèmes de décision (par exemple déterminer si la fonction a un modèle) ou des tâches plus constructives (par exemple retourner la liste des modèles de la fonction). On dit que l'on satisfait une requête pour une classe de circuits ${\displaystyle {\mathcal {L}}}$ quand il existe un algorithme qui prend en entrée (entre autres) un circuit ${\displaystyle C}$ de ${\displaystyle {\mathcal {L}}}$ et retourne le résultat de la requête sur ${\displaystyle C}$ en temps polynomial.

Certaines requêtes sont systématiquement étudiées en compilation de connaissance^[1],[5]. Ces requêtes sont décrites dans le tableau suivant. Leur faisabilité pour la classe des DNNF est indiquée par un symbole en fin de ligne :

• ${\displaystyle \checkmark }$ : on peut satisfaire la requête pour la classe des DNNF ;
• ${\displaystyle \bullet }$ : on ne peut pas satisfaire la requête pour la classe des DNNF, sauf si P = NP.

Notation	Nom	Description
CO	Test de cohérence (consistency check)	Étant donné un circuit ${\displaystyle C}$, déterminer en temps polynomial (en ${\displaystyle |C|}$) s'il existe une affectation de variables satisfaisant ${\displaystyle C}$.	${\displaystyle \checkmark }$
VA	Test de validité (validity check)	Étant donné un circuit ${\displaystyle C}$, déterminer en temps polynomial (en ${\displaystyle |C|}$) si toutes les affectations de variables satisfont ${\displaystyle C}$.	${\displaystyle \bullet }$
CE	Test de clause impliquée (clausal entailment check)	Étant donnés une clause ${\displaystyle \gamma }$ et un circuit ${\displaystyle C}$, déterminer en temps polynomial (en ${\displaystyle |C|}$) si ${\displaystyle C\models \gamma }$.	${\displaystyle \checkmark }$
IM	Test de terme impliquant (implicant check)	Étant donnés un terme ${\displaystyle \tau }$ et un circuit ${\displaystyle C}$, déterminer en temps polynomial (en ${\displaystyle |C|}$) si ${\displaystyle \tau \models C}$.	${\displaystyle \bullet }$
SE	Test d'implication (sentential entailment check)	Étant donnés deux circuits ${\displaystyle C}$ et ${\displaystyle C'}$ appartenant à la même classe, déterminer en temps polynomial (en ${\displaystyle |C|}$ et ${\displaystyle \vert C'\vert }$) si ${\displaystyle C\models C'}$.	${\displaystyle \bullet }$
EQ	Test d'équivalence (equivalence check)	Étant donnés deux circuits ${\displaystyle C}$ et ${\displaystyle C'}$ appartenant à la même classe, déterminer en temps polynomial (en ${\displaystyle |C|}$ et ${\displaystyle \vert C'\vert }$) si ${\displaystyle C\equiv C'}$.	${\displaystyle \bullet }$
CT	Comptage des modèles (model counting)	Étant donné un circuit ${\displaystyle C}$, retourner en temps polynomial (en ${\displaystyle |C|}$) le nombre d'affectations de variables satisfaisant ${\displaystyle C}$.	${\displaystyle \bullet }$
ME	Énumération des modèles (model enumeration)	Étant donné un circuit ${\displaystyle C}$, retourner en temps polynomial (en ${\displaystyle |C|}$ et ${\displaystyle |C^{-1}(1)|}$) toutes les affectations de variables satisfaisant ${\displaystyle C}$.	${\displaystyle \checkmark }$

Test de cohérence (CO)

Tester l'existence d'un modèle n'est en général pas réalisable en temps polynomial pour n'importe quel circuit NNF^[1]. Dans le cas des circuits DNNF, la décomposabilité des portes ET (${\displaystyle \wedge }$) rend le test faisable en temps polynomial^[2].

Soit ${\displaystyle g}$ une porte ET décomposable ${\displaystyle g=C_{1}\wedge \dots \wedge C_{m}}$. Supposons pour tout ${\displaystyle i}$, le sous-circuit ${\displaystyle C_{i}}$ retourne vrai pour une affectation ${\displaystyle a_{i}}$ des variables de ${\displaystyle var(C_{i})}$. Par décomposabilité les ensembles ${\displaystyle var(C_{1}),\dots ,var(C_{m})}$ sont deux-à-deux disjoints, donc il ressort que ${\displaystyle a=a_{1}\wedge \dots \wedge a_{m}}$ est une affectation cohérente des variables de ${\displaystyle var(g)}$ — c'est-à-dire que ${\displaystyle a}$ affecte une et une seule valeur à chaque variable de ${\displaystyle var(g)}$ — et ${\displaystyle a}$ est clairement un modèle de ${\displaystyle g}$. Ainsi un circuit dont la racine est une porte ET décomposable admet un modèle si et seulement si tous les sous-circuits en entrée admettent un modèle, cette condition est nécessaire mais en général pas suffisante pour les portes ET non décomposables.

Un algorithme possible, que l'on note ${\displaystyle A_{\textbf {CO}}}$, pour tester l'existence de modèles d'une DNNF ${\displaystyle C}$ fonctionne récursivement selon le protocole suivant :

• si la sortie de ${\displaystyle C}$ est une porte ${\displaystyle g}$ de type OU, ${\displaystyle g=C_{1}\vee \dots \vee C_{m}}$, alors ${\displaystyle A_{\textbf {CO}}(C)}$ retourne vrai si et seulement si au moins un des ${\displaystyle A_{\textbf {CO}}(C_{i})}$ retourne vrai ;
• si la sortie de ${\displaystyle C}$ est une porte ${\displaystyle g}$ de type ET, ${\displaystyle g=C_{1}\wedge \dots \wedge C_{m}}$, alors ${\displaystyle A_{\textbf {CO}}(C)}$ retourne vrai si et seulement si tous les ${\displaystyle A_{\textbf {CO}}(C_{i})}$ retournent vrai ;
• pour des entrées Booléennes ${\displaystyle x}$ ou ${\displaystyle \neg x}$, ${\displaystyle A_{\textbf {CO}}(x)}$ et ${\displaystyle A_{\textbf {CO}}(\neg x)}$ retournent vrai ;
• pour une entrée constante, ${\displaystyle A_{\textbf {CO}}(1)}$ retourne vrai et ${\displaystyle A_{\textbf {CO}}(0)}$ retourne faux.

Chaque porte du circuit génère au plus autant d'appels récursifs que son arité en entrée, donc le nombre d'appels récursifs est en ${\displaystyle O(\vert C\vert )}$ et ${\displaystyle A_{\textbf {CO}}(C)}$ s'exécute en temps polynomial en ${\displaystyle \vert C\vert }$.

Test de clause impliquée (CE)

Étant donné une clause ${\displaystyle \gamma =l_{1}\wedge \dots \wedge l_{n}}$ sur les variables ${\displaystyle var(\gamma )=\{x_{1},\dots ,x_{n}\}}$ où chaque ${\displaystyle l_{i}}$ représente ${\displaystyle x_{i}}$ ou ${\displaystyle \neg x_{i}}$, on peut associer le terme ${\displaystyle \neg \gamma }$ à une affectation des variables de ${\displaystyle var(\gamma )}$ (c'est l'unique modèle de ${\displaystyle \neg \gamma }$ sur ${\displaystyle var(\gamma )}$).

Soit ${\displaystyle C}$ un circuit sur un sur-ensemble de ${\displaystyle var(\gamma )}$. On désigne par ${\displaystyle C\vert (\neg \gamma )}$ le circuit obtenu en remplaçant les variables d'entrée appartenant à ${\displaystyle var(\gamma )}$ par leur affectation (${\displaystyle 0}$ ou ${\displaystyle 1}$) dans ${\displaystyle \neg \gamma }$. On dit que l'on a conditionné ${\displaystyle C}$ sur ${\displaystyle \neg \gamma }$. Si ${\displaystyle C}$ est une DNNF, affecter des valeurs à certaines variables d'entrée n'impacte pas la décomposabilité des portes ET, donc ${\displaystyle C\vert (\neg \gamma )}$ est encore une DNNF dont la taille n'est pas supérieure à celle de ${\displaystyle C}$.

${\displaystyle C}$ implique ${\displaystyle \gamma }$ (noté ${\displaystyle C\models \gamma }$) si et seulement si ${\displaystyle C\equiv C\wedge \gamma }$. Après conditionnement sur ${\displaystyle \neg \gamma }$ des deux côtés, on obtient que ${\displaystyle C\models \gamma }$ si ${\displaystyle C\vert (\neg \gamma )\equiv 0}$. Donc pour tester ${\displaystyle C\models \gamma }$ on peut simplement vérifier que ${\displaystyle C\vert (\neg \gamma )}$ n'a pas de modèle. Si ${\displaystyle C}$ est une DNNF, un algorithme ${\displaystyle A_{\textbf {CE}}}$ pour le test de clause impliquée se réduit à un appel à ${\displaystyle A_{\textbf {CO}}}$ : ${\displaystyle A_{\textbf {CE}}(C,\gamma )}$ retourne vrai si et seulement si ${\displaystyle A_{\textbf {CO}}(C\vert (\neg \gamma ))}$ retourne faux. ${\displaystyle A_{\textbf {CO}}(C\vert (\neg \gamma ))}$ s'exécute en temps polynomial en la taille de ${\displaystyle C\vert (\neg \gamma )}$, laquelle est inférieure à ${\displaystyle \vert C\vert }$, donc ${\displaystyle A_{\textbf {CE}}(C,\gamma )}$ s'exécute en temps polynomial en ${\displaystyle \vert C\vert }$.

Énumération des modèles (ME)

On veut énumérer tous les modèles d'un circuit ${\displaystyle C}$ sous forme DNNF. On peut déjà tester l'existence de modèles avec le test de cohérence sur ${\displaystyle C}$. Par la suite si on détecte que ${\displaystyle C}$ a des modèles, on construit un arbre à ${\displaystyle n+1}$ niveaux dont chaque feuille (ici un nœud de niveau ${\displaystyle n}$, la racine étant le niveau ${\displaystyle 0}$) correspond à un modèle du circuit^[1]. Les nœuds de l'arbre de niveau ${\displaystyle i}$ correspondent à des affectations de variables sur ${\displaystyle \{x_{1},\dots ,x_{i}\}}$ (par convention vide pour la racine, qui est le niveau ${\displaystyle 0}$). La construction commence depuis la racine et suit la règle suivante : tant qu'il existe un nœud de niveau ${\displaystyle i<n}$ sans fils, soit ${\displaystyle a_{i}}$ l'affectation de variables correspondante :

• si ${\displaystyle C\vert (a_{i}\wedge x_{i+1})}$ a un modèle, on lui ajoute à ce nœud un fils correspondant à ${\displaystyle a_{i}\wedge x_{i+1}}$ ;
• si ${\displaystyle C\vert (a_{i}\wedge \neg x_{i+1})}$ a un modèle, on lui ajoute à ce nœud un fils correspondant à ${\displaystyle a_{i}\wedge \neg x_{i+1}}$.

À noter qu'au moins un des deux tests réussi puisqu'on sait que le circuit de départ a des modèles. La construction prend fin quand tous les chemins sont de taille ${\displaystyle n}$, les modèles de ${\displaystyle C}$ sont alors les affectations de variables correspondant aux feuilles.

Les circuits conditionnés ${\displaystyle C\vert (a_{i}\wedge x_{i+1})}$ sont des DNNF de taille inférieure à ${\displaystyle \vert C\vert }$ donc tester l'existence de modèles se fait en temps polynomial avec ${\displaystyle A_{\textbf {CO}}}$. En tout, l'algorithme fait ${\displaystyle O(n\vert C^{-1}(1)\vert )}$ tests, d'où son temps d'exécution polynomial en ${\displaystyle \vert C\vert }$ et ${\displaystyle \vert C^{-1}(1)\vert }$.

Notes et références

1. (en) Adnan Darwiche, Pierre Marquis, « A Knowledge Compilation Map », Journal of Artificial Intelligence Research,‎ 2002 (lire en ligne)
2. (en) Adnan Darwiche, « Decomposable negation normal form », Journal of the ACM,‎ 2001 (lire en ligne)
3. (en) Stasys Jukna, Boolean Function Complexity - Advances and Frontiers., 2012 (ISBN 978-3-642-24507-7), p. 14
4. (en) Ingo Wegener, Branching Programs and Binary Decision Diagrams, 2000 (ISBN 0-89871-458-3), Chapitre 6
5. (en) Pierre Marquis, « Compile! », AAAI Conference on Artificial Intelligence (AAAI),‎ 2015 (lire en ligne)