Diagramme de décision binaire
Un article de Wikipédia, l'encyclopédie libre.
 |
Cet article est une ébauche à compléter concernant l'informatique, vous pouvez partager vos connaissances en le modifiant. |
Un diagramme de décision binaire (BDD, binary decision diagram en anglais), comme une forme normale niée ou un graphe orienté acyclique propositionnel, est une structure de données utilisée pour représenter des fonctions booléennes. Une fonction booléenne peut être représentée par un graphe orienté acyclique avec une racine consistant en noeuds de décisions, et deux noeuds terminaux appelés 0-terminal et 1-terminal. Chaque noeud de décision et étiqueté par une variable booléenne et a deux noeuds fils, appelés fils bas et fils haut. L'arête d'un noeud à un fils bas (resp. haut) représente l'assignation de la variable à 0 (resp. 1). Un tel BBD est appelé "ordonné" si différentes variables apparaissent dans le même ordre sur tous les chemins depuis la racine. Il est appelé "réduit" si le graphe est réduit selon deux règles:
- Tous les sous-graphes isomorphes sont fusionné
- Tous les noeuds dont les deux fils sont isomorphes sont éliminés
Dans son usage courant, le terme diagramme de décision binaire réfère pratiquement tout le temps à un diagramme de décision binaire d'ordre réduit (ROBDD, reduced ordered dinary decision diagram, terme utilisé quand l'ordre et la réduction doivent être mis en avant). L'avantage d'un ROBDD est qu'il est canonique (unique) pour une fonctionnalité particulière. Cette propriété le rend utile pour la vérification d'équivalence fonctionnelle par exemple.
Un chemin de la racine au noeud 1-terminal représente une assignation de variable (partielle ou pas) pour laquelle la fonction booléenne représentée est vraie. Quand le chemin descend d'un noeud vers un fils bas (resp. fils haut), on assigne à la variable représentée par ce noeud la valeur 0 (resp. 1).
Les arbres de décision binaires sont très utilisés par les programmes de CAD (Conception assistée par ordinateur) pour générer des circuits (synthèse logique), et dans la vérification formelle.
