Résumé
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. 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. C'est une structure de donnée considérée comme compacte, en comparaison par exemple aux arbres de décision. Les diagrammes de décision binaire sont utilisés dans le model checking symbolique de CTL. thumb|Exemple de diagramme de décision binaire. Un diagramme de décision binaire (BDD) est un graphe acyclique, comme montré dans la figure ci-contre. Il est composé de nœuds non terminaux porteurs de questions, aussi nommés nœuds de décision (dans l'exemple, il s'agit des ) et d'au plus deux nœuds terminaux étiquetés par et . Chaque nœud non terminal a deux successeurs, l'un par un arc marqué pour 'oui/vrai' et l'autre par un arc marqué pour 'non/faux'. Un diagramme de décision binaire possède un seul sommet initial ou racine (dans l'exemple, il s'agit du nœud ). Un chemin de la racine à un nœud terminal représente une affectation de variables (partielle ou pas) : on affecte à la variable qui étiquette un nœud la valeur ou selon qu'on a pris l'arc sortant marqué par ou . Un BDD représente une fonction booléenne . Un chemin de la racine au terminal 1 représente une affectation de variables (partielle ou pas) pour laquelle la fonction booléenne représentée est vraie. Un exemple d'assignation de variables pour laquelle la fonction est vraie est . Si on considère un chemin de la racine au terminal , alors celui-ci représente une assignation de variables pour laquelle la fonction est fausse. Un exemple d'une assignation partielle dans ce cas est , dans ce cas, et quelle que soit la valeur de , la fonction est fausse.
À propos de ce résultat
Cette page est générée automatiquement et peut contenir des informations qui ne sont pas correctes, complètes, à jour ou pertinentes par rapport à votre recherche. Il en va de même pour toutes les autres pages de ce site. Veillez à vérifier les informations auprès des sources officielles de l'EPFL.