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.
Exemple de diagramme de décision binaire.

En informatique, un graphe de décision binaire ou 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, ou des questionnaires binaires. On utilise les BDD pour représenter des ensembles ou des relations de manière compacte / compressée.

Description[modifier | modifier le code]

Base[modifier | modifier le code]

On peut représenter une décision booléenne par un nœud porteur de la question, dont sont issues 2 arcs, l'un marqué 1 pour oui/vrai, l'autre marqué 0 pour non/faux.

Soit f(x, y, .... ) une fonction booléenne. D'après Shannon, .

Une fonction booléenne peut donc être représentée par un graphe étiqueté sans circuit avec

  • un sommet initial ou racine,
  • deux nœuds terminaux nommés 0 et 1,
  • chaque nœud non-terminal, étiqueté par une variable booléenne et muni de deux arcs sortants, l'un étant marqué 0 et l'autre 1.

Un chemin de la racine au terminal 1 représente une affectation de variables (partielle ou pas) pour laquelle la fonction booléenne f représentée est vraie (et la fonction complémentaire f' fausse).

Un chemin de la racine au terminal 0 représente une affectation de variables (partielle ou pas) pour laquelle la fonction booléenne f est fausse (et la complémentaire f' vraie).

Quand le chemin descend d'un nœud par un arc noté 0 (resp. 1), on affecte à la variable représentée par ce nœud la valeur 0 (resp. 1)[1].

Ordonné / Réduit[modifier | modifier le code]

Un tel graphe ou 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 :

  • aux sous-graphes isomorphes on associe une représentation unique ;
  • tous les nœuds dont les deux fils mènent au même successeur sont éliminés.

Dans son usage courant, le terme diagramme de décision binaire se réfère généralement à 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).

Utilisations[modifier | modifier le code]

Les diagrammes de décision binaires sont utilisés par les programmes de conception assistée par ordinateur (CAO / 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]

Bibliographie[modifier | modifier le code]

Liens externes[modifier | modifier le code]

(en) Edmund M. Clarke, Jr., « Model Checking - Binary Decision Diagrams » [PDF]

Pravossoudovitch S., Représentation et Synthèse des Systèmes Logiques, Ch. 3, Graphes de décision binaire [1] [PDF]