Diagramme de décision binaire

Un article de Wikipédia, l'encyclopédie libre.
Aller à : navigation, rechercher
Page d'aide sur l'homonymie Pour les articles homonymes, voir BDD.
Ce modèle est-il pertinent ? Cliquez pour en voir d'autres.
Cet article ne cite pas suffisamment ses sources (décembre 2010).

Si vous disposez d'ouvrages ou d'articles de référence ou si vous connaissez des sites web de qualité traitant du thème abordé ici, merci de compléter l'article en donnant les références utiles à sa vérifiabilité et en les liant à la section « Notes et références » (modifier l'article, comment ajouter mes sources ?).

Exemple de diagramme de décision binaire

En informatique, un diagramme de décision binaire ou BDD pour Binary Decision Diagram en anglais) est une structure de données utilisée pour représenter des fonctions booléennes. On utilise les BDD pour représenter des ensembles ou des relations de manière compacte / compressée.

Description[modifier | modifier le code]

Définition basique[modifier | modifier le code]

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 chemin de la racine au nœud 1-terminal représente une affectation de variables (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)[1].

Ordonné et réduit[modifier | modifier le code]

Un tel BDD est « 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 « 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[1]. 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). Université Paris-Est Créteil

Utilisations[modifier | modifier le code]

Les diagrammes de décision binaires sont 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[1]. c'est une structure de donnée considérée comme compacte, en comparaison par exemple aux arbres de décision.

Notes et références[modifier | modifier le code]

  1. a, b et c Catalin Dima, « Langages de spécification – cours 4 : Diagrammes de décision binaire(BDD) », sur Université Paris-Est Créteil Val-de-Marne

Bibliographie[modifier | modifier le code]

Liens externes[modifier | modifier le code]

Model Checking - Binary Decision Diagrams