Binäres Entscheidungsdiagramm

In der Informatik ist ein binäres Entscheidungsdiagramm ( BDD ) oder verzweigtes Programm eine Datenstruktur zur Darstellung einer booleschen Funktion . Abstrakter betrachtet, lassen sich BDDs als komprimierte Repräsentation von Mengen oder Relationen verstehen . Im Gegensatz zu anderen komprimierten Repräsentationen werden Operationen direkt auf der komprimierten Repräsentation ausgeführt, also ohne Dekomprimierung.

Ähnliche Datenstrukturen sind die Negationsnormalform (NNF), Zhegalkin-Polynome und propositionale gerichtete azyklische Graphen (PDAG).

Eine Boolesche Funktion lässt sich als gerichteter, azyklischer Graph mit Wurzel darstellen , der aus mehreren Entscheidungsknoten und zwei Endknoten besteht. Die beiden Endknoten sind mit 0 (FALSCH) und 1 (WAHR) beschriftet. Jeder Entscheidungsknoten ist mit einer Booleschen Variable beschriftet und hat zwei Kindknoten, den sogenannten unteren und den oberen Kindknoten. Die Kante von einem Knoten zu einem unteren (oder oberen) Kindknoten repräsentiert die Zuweisung des Wertes FALSCH (bzw. WAHR) an die Variable . Ein solches BDD wird als „geordnet“ bezeichnet, wenn verschiedene Variablen auf allen Pfaden von der Wurzel in derselben Reihenfolge vorkommen. Ein BDD heißt „reduziert“, wenn die folgenden beiden Regeln auf seinen Graphen angewendet wurden: ${\displaystyle u}$${\displaystyle x_{i}}$${\displaystyle u}$${\displaystyle x_{i}}$

• Verschmelze alle isomorphen Teilgraphen.
• Entferne alle Knoten, deren zwei Kinder isomorph sind.

Im allgemeinen Sprachgebrauch bezeichnet der Begriff BDD fast immer ein reduziertes geordnetes binäres Entscheidungsdiagramm ( ROBDD , in der Literatur verwendet, wenn die Aspekte der Ordnung und Reduktion betont werden sollen). Der Vorteil eines ROBDD liegt darin, dass es für eine bestimmte Funktions- und Variablenordnung kanonisch (bis auf Isomorphie eindeutig) ist. ^{[ 1 ]} Diese Eigenschaft macht es nützlich für die Prüfung funktionaler Äquivalenz und andere Operationen wie das Mapping funktionaler Technologien.

Ein Pfad vom Wurzelknoten zum 1-Terminal repräsentiert eine (möglicherweise partielle) Variablenzuweisung, für die die entsprechende boolesche Funktion wahr ist. Beim Abstieg des Pfades zu einem niedrigeren (oder höheren) Kindknoten wird dessen Variable auf 0 (bzw. 1) gesetzt.

Die linke Abbildung unten zeigt einen binären Entscheidungsbaum (ohne Reduktionsregeln) und eine Wahrheitstabelle , die jeweils die Funktion darstellen . Im linken Baum lässt sich der Funktionswert für eine gegebene Variablenbelegung bestimmen, indem man einem Pfad im Graphen zu einem Endknoten folgt. In den Abbildungen unten stellen gestrichelte Linien Kanten zu einem Kind mit niedrigem Wert dar, durchgezogene Linien hingegen Kanten zu einem Kind mit hohem Wert. Um also den Funktionswert zu finden , beginnt man bei x₁ _, folgt der gestrichelten Linie zu x₂ ₍ da _x₁ den Wert 0 hat) und anschließend den beiden durchgezogenen Linien (da x₂ _und x₃ _jeweils den Wert 1 haben). Dies führt zum Endknoten 1, der den Funktionswert angibt . ${\displaystyle f(x_{1},x_{2},x_{3})}$${\displaystyle f(0,1,1)}$${\displaystyle f(0,1,1)}$

Der binäre Entscheidungsbaum in der linken Abbildung kann durch maximale Reduktion gemäß den beiden Reduktionsregeln in ein binäres Entscheidungsdiagramm umgewandelt werden. Das resultierende BDD ist in der rechten Abbildung dargestellt.

Eine weitere Notation zum Schreiben dieser Booleschen Funktion ist . ${\displaystyle {\overline {x}}_{1}{\overline {x}}_{2}{\overline {x}}_{3}+x_{1}x_{2}+x_{2}x_{3}}$

Ein ROBDD lässt sich noch kompakter darstellen, indem man komplementäre Kanten, auch Komplementverbindungen genannt, verwendet . ^{[ 2 ] [ 3 ]} Das resultierende BDD wird manchmal auch als typisiertes BDD ^{[ 4 ]} oder signiertes BDD bezeichnet . Komplementäre Kanten entstehen, indem man Kanten niedriger Ordnung als komplementär oder nicht komplementär annotiert. Eine komplementäre Kante verweist auf die Negation der Booleschen Funktion, die dem Knoten entspricht, auf den die Kante zeigt (die Boolesche Funktion, die durch das BDD mit diesem Knoten als Wurzel repräsentiert wird). Kanten höherer Ordnung werden nicht komplementiert, um sicherzustellen, dass die resultierende BDD-Darstellung eine kanonische Form ist. In dieser Darstellung haben BDDs aus den unten erläuterten Gründen nur einen einzigen Blattknoten.

Zwei Vorteile der Verwendung komplementärer Kanten bei der Darstellung von BDDs sind:

• Die Berechnung der Negation eines BDD benötigt konstante Zeit.
• Der Speicherplatzbedarf (d. h. der benötigte Arbeitsspeicher) wird reduziert (um höchstens den Faktor 2).

^{Knuth [ 5 ]} vertritt jedoch die gegenteilige Ansicht:

Obwohl solche Verknüpfungen von allen gängigen BDD-Paketen verwendet werden, sind sie nur bedingt empfehlenswert, da die Computerprogramme dadurch deutlich komplexer werden. Die Speichereinsparung ist in der Regel vernachlässigbar und beträgt maximal den Faktor 2; zudem zeigen die Experimente des Autors nur geringe Laufzeitvorteile.

In dieser Darstellung ist ein Verweis auf ein BDD eine (möglicherweise komplementierte) Kante, die auf die Wurzel des BDD verweist. Dies steht im Gegensatz zu einem Verweis auf ein BDD in der Darstellung ohne komplementierte Kanten, der dem Wurzelknoten des BDD entspricht. Der Grund, warum ein Verweis in dieser Darstellung eine Kante sein muss, liegt darin, dass für jede boolesche Funktion die Funktion selbst und ihre Negation durch eine Kante zur Wurzel eines BDD und eine komplementierte Kante zur Wurzel desselben BDD repräsentiert werden. Daher benötigt die Negation konstante Zeit. Dies erklärt auch, warum ein einzelner Blattknoten ausreicht: FALSCH wird durch eine komplementierte Kante repräsentiert, die auf den Blattknoten verweist, und WAHR durch eine normale Kante (d. h. nicht komplementiert), die auf den Blattknoten verweist.

Nehmen wir beispielsweise an, eine boolesche Funktion wird durch ein BDD mit komplementären Kanten dargestellt. Um den Wert der booleschen Funktion für eine gegebene Belegung der Variablen mit booleschen Werten zu ermitteln, beginnen wir an der Referenzkante, die auf die Wurzel des BDD zeigt, und folgen dem Pfad, der durch die gegebenen Variablenwerte definiert ist (einer niedrigen Kante, wenn die Variable, die einen Knoten kennzeichnet, den Wert FALSE hat, und einer hohen Kante, wenn die Variable, die einen Knoten kennzeichnet, den Wert TRUE hat), bis wir den Blattknoten erreichen. Auf diesem Pfad zählen wir die durchlaufenen komplementären Kanten. Wenn wir beim Erreichen des Blattknotens eine ungerade Anzahl komplementärer Kanten durchlaufen haben, ist der Wert der booleschen Funktion für die gegebene Variablenbelegung FALSE; andernfalls (wenn wir eine gerade Anzahl komplementärer Kanten durchlaufen haben) ist der Wert der booleschen Funktion für die gegebene Variablenbelegung TRUE.

Rechts ist ein Beispieldiagramm eines BDD in dieser Darstellung abgebildet. Es repräsentiert denselben booleschen Ausdruck wie die obigen Diagramme. Niedrige Kanten sind gestrichelt, hohe Kanten durchgezogen, und komplementäre Kanten werden durch einen Kreis an ihrem Ursprung gekennzeichnet. Der Knoten mit dem @-Symbol stellt die Referenz zum BDD dar; die Referenzkante ist also die Kante, die von diesem Knoten ausgeht. ${\displaystyle (\neg x_{1}\wedge \neg x_{2}\wedge \neg x_{3})\vee (x_{1}\wedge x_{2})\vee (x_{2}\wedge x_{3})}$

Die grundlegende Idee, auf der die Datenstruktur basiert, ist die Shannon-Entwicklung . Eine Schaltfunktion wird durch die Zuweisung einer Variablen in zwei Teilfunktionen (Kofaktoren) aufgeteilt (vgl. Wenn-Dann-Sonst-Normalform ). Betrachtet man eine solche Teilfunktion als Teilbaum, lässt sie sich durch einen binären Entscheidungsbaum darstellen . Binäre Entscheidungsdiagramme (BDDs) wurden von C. Y. Lee ^{[ 6 ] eingeführt und von Sheldon B. Akers [ 7 ]} und Raymond T. Boute ^{[ 8 ]} weiterentwickelt und bekannt gemacht . Unabhängig von diesen Autoren realisierte Yu. V. Mamrukov ein BDD unter dem Namen „kanonische Klammerform“ in einem CAD-System zur Analyse geschwindigkeitsunabhängiger Schaltungen ^{[ 9 ]} . Das volle Potenzial effizienter Algorithmen auf Basis dieser Datenstruktur wurde von Randal Bryant an der Carnegie Mellon University untersucht . Seine wichtigsten Erweiterungen bestanden in der Verwendung einer festen Variablenreihenfolge (für die kanonische Darstellung) und gemeinsam genutzter Teilgraphen (zur Komprimierung). Die Anwendung dieser beiden Konzepte führt zu einer effizienten Datenstruktur und Algorithmen zur Darstellung von Mengen und Relationen. ^{[ 10 ] [ 11 ]} Durch die Erweiterung der gemeinsamen Nutzung auf mehrere BDDs, d. h. ein Teilgraph wird von mehreren BDDs verwendet, wird die Datenstruktur Shared Reduced Ordered Binary Decision Diagram (SDRDD) definiert. ^{[ 2 ]} Der Begriff BDD wird heute allgemein für diese spezielle Datenstruktur verwendet.

In seinem Video-Vortrag „ Spaß mit binären Entscheidungsdiagrammen (BDDs)“ bezeichnet Donald Knuth BDDs als „eine der wenigen wirklich grundlegenden Datenstrukturen, die in den letzten fünfundzwanzig Jahren entwickelt wurden“ und erwähnt, dass Bryants Arbeit von 1986 einige Zeit lang zu den meistzitierten Arbeiten in der Informatik gehörte. ^{[ 12 ]}

Adnan Darwiche und seine Mitarbeiter haben gezeigt, dass BDDs eine von mehreren Normalformen für Boolesche Funktionen darstellen, die jeweils durch eine unterschiedliche Kombination von Anforderungen induziert werden. Eine weitere wichtige Normalform, die Darwiche identifiziert hat, ist die zerlegbare Negationsnormalform (DNNF).

BDDs werden in CAD -Software zur Schaltungssynthese ( Logiksynthese ) sowie zur formalen und Netzwerkverifikation umfassend eingesetzt . Es gibt einige weniger bekannte Anwendungen von BDDs, darunter Fehlerbaumanalyse , Bayes'sche Inferenz, Produktkonfiguration und private Informationssuche . ^{[ 13 ] [ 14 ]}

Jedes beliebige BDD (auch wenn es nicht reduziert oder geordnet ist) lässt sich direkt in Hardware implementieren, indem jeder Knoten durch einen 2-zu-1- Multiplexer ersetzt wird; jeder Multiplexer kann direkt mit einer 4-LUT in einem FPGA realisiert werden . Die Umwandlung eines beliebigen Netzwerks von Logikgattern in ein BDD ist hingegen nicht so einfach (anders als beim UND-Inverter-Graphen ).

BDDs wurden in effizienten Datalog- Interpretern eingesetzt. ^{[ 15 ]}

Die Größe des BDD wird sowohl durch die dargestellte Funktion als auch durch die gewählte Variablenreihenfolge bestimmt. Es gibt Boolesche Funktionen, deren Anzahl an Knoten je nach Variablenreihenfolge bestenfalls linear (in  n ) und schlimmstenfalls exponentiell ist (z. B. ein Ripple-Carry-Addierer ). Betrachten wir die Boolesche Funktion . Bei der Variablenreihenfolge benötigt das BDD Knoten, um die Funktion darzustellen. Bei der Reihenfolge besteht das BDD aus Knoten. ${\displaystyle f(x_{1},\ldots ,x_{n})}$${\displaystyle f(x_{1},\ldots ,x_{2n})=x_{1}x_{2}+x_{3}x_{4}+\cdots +x_{2n-1}x_{2n}.}$${\displaystyle x_{1}<x_{3}<\cdots <x_{2n-1}<x_{2}<x_{4}<\cdots <x_{2n}}$${\displaystyle 2^{n+1}}$${\displaystyle x_{1}<x_{2}<x_{3}<x_{4}<\cdots <x_{2n-1}<x_{2n}}$${\displaystyle 2n+2}$

Bei der praktischen Anwendung dieser Datenstruktur ist die Variablenreihenfolge von entscheidender Bedeutung. Das Problem, die optimale Variablenreihenfolge zu finden, ist NP-schwer . ^{[ 16 ]} Für jede Konstante c  > 1 ist es sogar NP-schwer, eine Variablenreihenfolge zu berechnen, die zu einer OBDD führt, deren Größe höchstens c -mal größer ist als die einer optimalen. ^{[ 17 ]} Es existieren jedoch effiziente Heuristiken zur Lösung dieses Problems. ^{[ 18 ]}

Es gibt Funktionen, deren Graphgröße stets exponentiell ist – unabhängig von der Variablenreihenfolge. Dies gilt beispielsweise für die Multiplikationsfunktion. ^{[ 1 ]} Tatsächlich besitzt die Funktion, die das mittlere Bit des Produkts zweier n-Bit-Zahlen berechnet, kein OBDD, das kleiner als n Knoten ist. ^{[ 19 ]} (Hätte die Multiplikationsfunktion OBDDs polynomieller Größe, würde dies zeigen, dass die Faktorisierung ganzer Zahlen in P/poly liegt , was jedoch nicht bekannt ist. ^{[ 20 ]} ) Ein weiteres bekanntes Beispiel ist die Funktion mit versteckten Gewichten, die als einfachste Funktion mit einem BDD exponentieller Größe gilt. ^{[ 21 ]}${\displaystyle n}$${\displaystyle 2^{\lfloor n/2\rfloor }/61-4}$

Forscher haben Verbesserungen an der BDD-Datenstruktur vorgeschlagen, die zu einer Reihe verwandter Graphen geführt haben, wie zum Beispiel:

• BMD ( Binärmomentdiagramme ),
• ZDD ( Zero-Suppressed Decision Diagrams ),
• Bei FBDD ( Free Binary Decision Diagrams ) liest jeder Pfad von der Wurzel zu einem Blattknoten jede Variable höchstens einmal. Jedes OBDD (Object-Based Decision Diagram) ist ein FBDD.
• FDD ( funktionale Entscheidungsdiagramme ),
• MDD ( Mehrwertige Entscheidungsdiagramme ), die BDDs verallgemeinern, indem sie Entscheidungsvariablen erlauben, mehr als zwei Werte anzunehmen, ^{[ 22 ].}
• PDD ( Paritätsentscheidungsdiagramme ),
• MTBDD (Multiple-Terminal BDDs),
• TDD ( ternäre Entscheidungsdiagramme ), bei dem ein "unbekannter" Zweig hinzugefügt wird, um aufeinanderfolgende Vereinigungs-/Disjunktionsoperationen verzögert auszuführen und so ein exponentielles Größenwachstum zu vermeiden. ^{[ 23 ]}
• NDD ( Netzwerkentscheidungsdiagramme ),

Viele logische Operationen auf BDDs können durch Graphmanipulationsalgorithmen mit polynomieller Laufzeit implementiert werden: ^{[ 24 ] : 20}

• Verbindung
• Disjunktion
• Negation

Die mehrmalige Wiederholung dieser Operationen, beispielsweise die Bildung der Konjunktion oder Disjunktion einer Menge von BDDs, kann im schlimmsten Fall zu einem exponentiell großen BDD führen. Dies liegt daran, dass jede der vorhergehenden Operationen für zwei BDDs ein BDD mit einer Größe proportional zum Produkt der Größen der BDDs erzeugen kann, und folglich kann die Größe für mehrere BDDs exponentiell mit der Anzahl der Operationen wachsen. Die Reihenfolge der Variablen muss daher erneut überdacht werden; eine für (einige) der BDDs sinnvolle Reihenfolge ist möglicherweise nicht optimal für das Ergebnis der Operation. Da die Konstruktion des BDD einer Booleschen Funktion das NP-vollständige Problem der Booleschen Erfüllbarkeit und das co-NP-vollständige Tautologieproblem löst , kann die Konstruktion des BDD exponentiell in der Größe der Booleschen Formel dauern, selbst wenn das resultierende BDD klein ist.

Die Berechnung existentieller Abstraktion über mehrere Variablen reduzierter BDDs ist NP-vollständig. ^{[ 25 ]}

Das Zählen von Modellen, also das Ermitteln der Anzahl erfüllender Belegungen einer Booleschen Formel, ist für BDDs in Polynomialzeit möglich. Für allgemeine Aussagenlogik ist das Problem ♯P -vollständig, und die besten bekannten Algorithmen benötigen im schlechtesten Fall exponentielle Laufzeit.

• Boolesche Erfüllbarkeitsproblem , das kanonische NP-vollständige Berechnungsproblem
• L/poly , eine Komplexitätsklasse , die strikt die Menge der Probleme mit BDDs polynomieller Größe enthält.
• Modellprüfung
• Radixbaum
• Satz von Barrington
• Hardwarebeschleunigung
• Karnaugh-Diagramm , eine Methode zur Vereinfachung von Ausdrücken der Booleschen Algebra
• Nullunterdrücktes Entscheidungsdiagramm
• Algebraisches Entscheidungsdiagramm , eine Verallgemeinerung von BDDs von zweielementigen auf beliebige endliche Mengen
• Satzentscheidungsdiagramm , eine Verallgemeinerung von OBDDs
• Einflussdiagramm

• Ubar, R. (1976). „Testgenerierung für digitale Schaltungen mittels alternativer Graphen“. Tagungsband der Technischen Universität Tallinn (in Russisch) (409). Tallinn, Estland: 75–81 .
• Meinel, C.; Theobald, T. (2012) [1998]. Algorithmen und Datenstrukturen im VLSI-Design: OBDD – Grundlagen und Anwendungen (PDF) . Springer. ISBN 978-3-642-58940-9DieDas vollständige Lehrbuch steht zum Download bereit.
• Ebendt, Rüdiger; Fey, Görschwin; Drechsler, Rolf (2005). Erweiterte BDD-Optimierung . Springer. ISBN 978-0-387-25453-1Die
• Becker, Bernd; Drechsler, Rolf (1998). Binäre Entscheidungsdiagramme: Theorie und Implementierung . Springer. ISBN 978-1-4419-5047-5Die

• Spaß mit binären Entscheidungsdiagrammen (BDDs) , Vortrag von Donald Knuth
• Liste von BDD-Softwarebibliotheken für verschiedene Programmiersprachen.