Diagramme de décision binaire
Un article de Wikipédia, l'encyclopédie libre.
 |
Cet article est une ébauche concernant l’informatique.
Vous pouvez partager vos connaissances en l’améliorant. (Comment ?).
|
Un diagramme de décision binaire (BDD pour 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 nœuds de décisions, et deux nœuds terminaux appelés 0-terminal et 1-terminal. Chaque nœud de décision est étiqueté par une variable booléenne et a deux nœuds fils, appelés fils bas et fils haut. L'arête d'un nœud à un fils bas (resp. haut) représente l'affectation de la variable à 0 (resp. 1). Un tel BBD est appelé « ordonné » si toutes les variables apparaissent dans le même ordre sur tous les chemins depuis la racine vers les nœuds terminaux. Il est appelé « réduit » si le graphe est réduit selon deux règles :
- – tous les sous-graphes isomorphes ont une représentation unique ;
- – tous les nœuds 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 ordonné réduit (ROBDD pour Reduced Ordered Binary Decision Diagram). L'avantage d'un ROBDD est qu'il est canonique (unique) pour une fonction booléenne donnée. Cette propriété le rend utile, par exemple, pour la vérification d'équivalence fonctionnelle (qui se traduit par l'égalité des ROBDD associés, laquelle peut être évaluée en temps constant).
Un chemin de la racine au nœud 1-terminal représente une affectation de variable (partielle ou pas) pour laquelle la fonction booléenne représentée est vraie. Quand le chemin descend d'un nœud vers un fils bas (resp. fils haut), on affecte à la variable représentée par ce nœud la valeur 0 (resp. 1).
Les diagrammes de décision binaires sont très utilisés par les programmes de conception assistée par ordinateur (CAD) pour générer des circuits (synthèse logique), et dans la vérification formelle.
