Accueil🇫🇷Chercher

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 ) ou faux (notée ). On désigne par l'ensemble des variables en entrée du circuit . La taille de , notée , est le nombre de ses connexions entre portes. Un circuit sur variables est associé à une fonction booléenne dont les modèles (les affectations de variables pour lesquelles la fonction vaut ) sont exactement les affectations de variables pour lesquelles la sortie du circuit est mise à (vrai). Par extension on appelle également ces affectations des modèles du circuit, on utilise pour désigner l'ensemble des modèles de .

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 () ;
  • les portes OU () ;
  • les portes NEG () à 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 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 .

Régulièrement on étend les entrées des circuits aux variables booléennes () et à leurs compléments (), 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 branchés sur les entrées d'une porte ET décomposable vérifient pour tout , autrement dit si la variable ou son complément est une entrée de , alors ni ni n'est une entrée . 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

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 et son complément . 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.

DNNF et BDD

A gauche : un nœud de décision sur la variable . À 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 et , ceux-ci sont transformés en entrées constantes ou . 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, n'appartient ni à ni à 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.

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 et permettant de représenter n'importe quelle fonction booléenne, on dit que permet des représentations plus compactes que (noté ) quand il existe une polynôme réel tel que pour chaque circuit il existe un circuit équivalent vérifiant . La relation est transitive. Il est clair que si , alors , puisque chaque dans appartient aussi à et que donc la définition précédente s'applique avec le polynôme identité.
On note quand mais que la relation inverse est fausse. C'est-à-dire que : il existe une famille (nécessairement infinie) de circuits dans et une fonction super-polynomiale (i.e., tout polynôme réel est dans , typiquement ou ) telles que pour tout et équivalent à , on a .

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

et

Les OBDD formant une sous-classe de FBDD, on a aussi 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 quand il existe un algorithme qui prend en entrée (entre autres) un circuit de et retourne le résultat de la requête sur 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 :

  • : on peut satisfaire la requête pour la classe des DNNF ;
  • : 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 , déterminer en temps polynomial (en ) s'il existe une affectation de variables satisfaisant .
VA
Test de validité
(validity check)
Étant donné un circuit , déterminer en temps polynomial (en ) si toutes les affectations de variables satisfont .
CE
Test de clause impliquée
(clausal entailment check)
Étant donnés une clause et un circuit , déterminer en temps polynomial (en ) si .
IM
Test de terme impliquant
(implicant check)
Étant donnés un terme et un circuit , déterminer en temps polynomial (en ) si .
SE
Test d'implication
(sentential entailment check)
Étant donnés deux circuits et appartenant à la même classe, déterminer en temps polynomial (en et ) si .
EQ
Test d'équivalence
(equivalence check)
Étant donnés deux circuits et appartenant à la même classe, déterminer en temps polynomial (en et ) si .
CT
Comptage des modèles
(model counting)
Étant donné un circuit , retourner en temps polynomial (en ) le nombre d'affectations de variables satisfaisant .
ME
Énumération des modèles
(model enumeration)
Étant donné un circuit , retourner en temps polynomial (en et ) toutes les affectations de variables satisfaisant .

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 () rend le test faisable en temps polynomial[2].

Soit une porte ET décomposable . Supposons pour tout , le sous-circuit retourne vrai pour une affectation des variables de . Par décomposabilité les ensembles sont deux-à-deux disjoints, donc il ressort que est une affectation cohérente des variables de — c'est-à-dire que affecte une et une seule valeur à chaque variable de — et est clairement un modèle de . 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 , pour tester l'existence de modèles d'une DNNF fonctionne récursivement selon le protocole suivant :

  • si la sortie de est une porte de type OU, , alors retourne vrai si et seulement si au moins un des retourne vrai ;
  • si la sortie de est une porte de type ET, , alors retourne vrai si et seulement si tous les retournent vrai ;
  • pour des entrées Booléennes ou , et retournent vrai ;
  • pour une entrée constante, retourne vrai et 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 et s'exécute en temps polynomial en .

Test de clause impliquée (CE)

Étant donné une clause sur les variables où chaque représente ou , on peut associer le terme à une affectation des variables de (c'est l'unique modèle de sur ).

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

implique (noté ) si et seulement si . Après conditionnement sur des deux côtés, on obtient que si . Donc pour tester on peut simplement vérifier que n'a pas de modèle. Si est une DNNF, un algorithme pour le test de clause impliquée se réduit à un appel à : retourne vrai si et seulement si retourne faux. s'exécute en temps polynomial en la taille de , laquelle est inférieure à , donc s'exécute en temps polynomial en .

Énumération des modèles (ME)

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

  • si a un modèle, on lui ajoute à ce nœud un fils correspondant à ;
  • si a un modèle, on lui ajoute à ce nœud un fils correspondant à .

À 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 , les modèles de sont alors les affectations de variables correspondant aux feuilles.

Les circuits conditionnés sont des DNNF de taille inférieure à donc tester l'existence de modèles se fait en temps polynomial avec . En tout, l'algorithme fait tests, d'où son temps d'exécution polynomial en et .

Notes et références

  1. (en) Adnan Darwiche, Pierre Marquis, « A Knowledge Compilation Map », Journal of Artificial Intelligence Research, (lire en ligne)
  2. (en) Adnan Darwiche, « Decomposable negation normal form », Journal of the ACM, (lire en ligne)
  3. (en) Stasys Jukna, Boolean Function Complexity - Advances and Frontiers., (ISBN 978-3-642-24507-7), p. 14
  4. (en) Ingo Wegener, Branching Programs and Binary Decision Diagrams, (ISBN 0-89871-458-3), Chapitre 6
  5. (en) Pierre Marquis, « Compile! », AAAI Conference on Artificial Intelligence (AAAI), (lire en ligne)
Cet article est issu de wikipedia. Text licence: CC BY-SA 4.0, Des conditions supplémentaires peuvent s’appliquer aux fichiers multimédias.