Binäres Entscheidungsdiagramm

Grundidee und Definition

Ein binäres Entscheidungsdiagramm (BED; englisch: binary decision diagram, BDD) ist eine Datenstruktur zur Darstellung Boolescher Funktionen. Boolesche Funktionen verarbeiten Variablen mit den möglichen Werten 0 oder 1 beziehungsweise Falsch oder Wahr und liefern wieder einen solchen Wert. BEDs werden vor allem in der Hardwaresynthese und Hardwareverifikation eingesetzt.

Ein BED kann als Flussdiagramm zur Auswertung einer Booleschen Funktion f(x₁, …, xₙ) verstanden werden. Nacheinander wird der Wert von Variablen abgefragt. Für jede Variable gibt es zwei Entscheidungsmöglichkeiten: Wahr oder Falsch. Beide führen über unterschiedliche Kanten in Teilbereiche des Diagramms. Schließlich erreicht man ein Blatt, dessen Wert der Funktionswert für die gewählte Variablenbelegung ist. Irrelevante Fragen werden ausgelassen und gleiche Teildiagramme zusammengelegt, sodass die Darstellung weitestgehend komprimiert ist.

Formal ist ein BED ein azyklischer, gerichteter Graph G = (V, E) mit einer Wurzel. Jeder Knoten v aus V ist entweder ein Blatt oder ein innerer Knoten. Blätter besitzen keine ausgehenden Kanten und sind mit einem Wert aus {0, 1} beschriftet. Jeder innere Knoten besitzt genau zwei ausgehende Kanten: die niedrig-Kante und die hoch-Kante. Ihre Endpunkte heißen niedrig(v) beziehungsweise hoch(v). Außerdem ist jeder innere Knoten mit einer Variablen xᵢ beschriftet.

Ein BED heißt geordnet (OBDD), wenn die Variablen auf allen von der Wurzel ausgehenden Pfaden in derselben Reihenfolge auftreten. Es heißt reduziert (RBDD), wenn zwei Regeln erschöpfend angewendet wurden: Je zwei isomorphe Teilgraphen werden zu einem verschmolzen, und Knoten, deren beide Endpunkte identisch sind, werden durch Überbrückung eliminiert.

Der Begriff BED schließt im Allgemeinen bereits Variablenordnung und Reduktion ein. Bei fester Variablenordnung existiert für jede Boolesche Funktion genau ein reduziertes, geordnetes BED. Es handelt sich damit um eine kanonische Darstellung der Booleschen Funktion (Bryant, 1986).

Berechnung der dargestellten Funktion

Die durch ein BED dargestellte Boolesche Funktion lässt sich mit der Shannon-Zerlegung berechnen. Für einen Knoten v sei fᵥ die von ihm dargestellte Funktion.

• Ist v ein Blatt, dann ist fᵥ gleich dem Wert, mit dem das Blatt beschriftet ist.
• Ist v ein innerer Knoten mit der Beschriftung xᵢ, dann gilt: fᵥ(x) = xᵢ fₕₒcₕ(v)(x) ∨ x̄ᵢ fₙᵢₑdᵣᵢg(v)(x).

Dabei bezeichnet ∨ die Disjunktion (ODER), und x̄ᵢ die Negation von xᵢ. Ist xᵢ = 1, wird die hoch-Funktion ausgewertet; ist xᵢ = 0, wird die niedrig-Funktion ausgewertet.

Beispiel mit der Variablenordnung x₁ < x₃ < x₂

Das im Artikel dargestellte BED ist ein freies, geordnetes und reduziertes binäres Entscheidungsdiagramm. Die niedrig-Kante wird gestrichelt, die hoch-Kante durchgezogen dargestellt. Die verwendete Variablenordnung lautet x₁ < x₃ < x₂.

Die Teilfunktionen werden schrittweise berechnet:

• Für den x₂-Knoten gilt: f₁(x₁, x₂, x₃) = 0 · x₂ ∨ 1 · x̄₂ = x̄₂.
• Für den linken x₃-Knoten gilt: f₂(x₁, x₂, x₃) = f₁ · x₃ ∨ 1 · x̄₃ = x̄₂x₃ ∨ x̄₃.
• Für den rechten x₃-Knoten gilt: f₃(x₁, x₂, x₃) = 0 · x₃ ∨ f₁ · x̄₃ = x̄₂ x̄₃.
• Für den x₁-Knoten gilt: f₄(x₁, x₂, x₃) = f₂ · x₁ ∨ f₃ · x̄₁ = x₁x̄₂x₃ ∨ x₁x̄₃ ∨ x̄₁x̄₂x̄₃.

Eine konkrete Belegung wird direkt ausgewertet, indem man dem zu ihr gehörenden Pfad von der Wurzel bis zu einem Blatt folgt. Für (x₁, x₂, x₃) = (0, 1, 1) startet man am x₁-Knoten. Weil x₁ = 0 ist, folgt man der niedrig-Kante und erreicht einen x₃-Knoten. Da x₃ = 1 gilt, folgt man der hoch-Kante und erreicht das Blatt mit der Beschriftung 0. Daher ist f(0, 1, 1) = 0.

Bedeutung der Variablenordnung

Die Struktur und die Anzahl der Knoten eines geordneten und reduzierten BEDs hängen bei vielen Funktionen stark von der gewählten Variablenordnung ab. Schon eine ungünstige Reihenfolge kann das Diagramm deutlich vergrößern.

Betrachtet wird die Boolesche Funktion f(x₁, …, x₂ₙ) = x₁x₂ ∨ x₃x₄ ∨ … ∨ x₂ₙ₋₁x₂ₙ. Bei der Variablenordnung x₁ < x₃ < … < x₂ₙ₋₁ < x₂ < x₄ < … < x₂ₙ benötigt das BED mehr als 2ⁿ Knoten. Bei der Reihenfolge x₁ < x₂ < x₃ < x₄ < … < x₂ₙ₋₁ < x₂ₙ genügen dagegen 2n Knoten.

Es gibt außerdem Funktionen, die unabhängig von der Variablenordnung exponentiell viele Knoten in der Zahl der Variablen benötigen. Dazu gehört auch die wichtige Funktion der Multiplikation. Deshalb wurden zahlreiche Varianten von BEDs entwickelt, darunter Kronecker Functional Decision Diagrams, Binary Moment Diagrams und Edge-valued Binary Decision Diagrams.

Operationen und Implementierungen

Zu den grundlegenden Operationen, die normalerweise von Implementierungen bereitgestellt werden, gehören die Booleschen Verknüpfungen Konjunktion (AND), Disjunktion (OR) und Negation (NOT).

Die Negation entsteht, indem das 0-Blatt und das 1-Blatt vertauscht werden. Andere zweistellige Boolesche Operationen werden meist auf den ternären ITE-Operator zurückgeführt. ITE steht für if-then-else und ist definiert als ITE(f, g, h) = (f ∧ g) ∨ (¬f ∧ h). Ist f gleich 1, liefert ITE den Funktionswert von g; andernfalls den von h. Damit gilt:

• f ∧ g = ITE(f, g, 0)
• f ∨ g = ITE(f, 1, g)
• ¬f = ITE(f, 0, 1)

Alle 16 binären Booleschen Operationen lassen sich mit dem ITE-Operator ausdrücken. Daher genügt grundsätzlich eine Implementierung von ITE.

Weitere wichtige Operationen sind der Gleichheitstest zweier dargestellter Funktionen, der Erfüllbarkeitstest und die Berechnung der Anzahl erfüllender Belegungen. Werden gleiche Funktionen immer nur durch denselben Knoten dargestellt, können beim Gleichheitstest einfach die Zeiger auf die Knoten verglichen werden. Gleiche Zeiger bedeuten gleiche Funktionen und umgekehrt; die Laufzeit ist dann konstant, also O(1). Erfüllbarkeit bedeutet, dass es eine Variablenbelegung gibt, für die die Funktion den Wert 1 annimmt. Sie kann durch den Vergleich des BEDs mit dem 0-Blatt geprüft werden. Die Anzahl erfüllender Belegungen lässt sich durch Traversieren des BEDs in Linearzeit berechnen.

Im Artikel genannte Implementierungen sind CMU BDD, CUDD, CrocoPat, JINC und BuDDy. CMU BDD stammt von der Carnegie Mellon University in Pittsburgh, CUDD von der University of Colorado in Boulder, CrocoPat ist ein BDD-Paket mit Interpreter für relationales Programmieren der University of California in Berkeley, JINC eine parallele C++-Bibliothek der Universität Bonn und BuDDy eine in C geschriebene BDD-Bibliothek mit C++-Interface.