Spezialvorlesung

"Binary Decision Diagrams"

Wintersemester 2006/07

Binary Decision Diagrams (BDDs) sind eine graphische Darstellung von booleschen Funktionen. Sie werden in Programmen für den Hardwareentwurf als Datenstruktur für die Speicherung und Manipulation von booleschen Funktionen, aber auch in der Komplexitätstheorie zur Untersuchung der Ressource Speicherplatz benutzt. Aufgrund ihrer vielseitigen Anwendbarkeit werden sie inzwischen bereits in der Vorlesung DAP 2 behandelt.

Die Vorlesung beginnt mit einer Wiederholung von OBDDs (Ordered Binary Decision Diagrams). Zusätzlich werden gegenüber der Vorlesung DAP 2 weitere Verfeinerungen der Algorithmen vorgestellt und es wird untersucht, für welche Operationen es vermutlich keine effizienten Algorithmen gibt. Eine weiteres wichtiges Problem besteht darin festzustellen, welche Funktionen mit kleinen OBDDs dargestellt werden können und welche nicht.  Während es für den Nachweis, dass es kleine OBDDs für eine Funktion gibt, genügt, ein kleines OBDD anzugeben, ist der Nachweis, dass eine Funktion keine kleinen OBDDs hat, schwieriger, da man prinzipiell alle OBDDs für die Funktion betrachten muss.  Es stellt sich heraus, dass OBDDs für viele wichtige Funktionen zu groß sind. Es wird daher die Frage untersucht, ob Erweiterungen der OBDDs zu kleineren Darstellungen für diese Funktionen führen und welche Operationen auf booleschen Funktionen von den Erweiterungen unterstützt werden. Zu diesen Erweiterungen gehören Varianten mit schwächeren Anforderungen an die Variablenordnung wie auch nichtdeterministische und randomisierte Varianten von OBDDs.

Die Untersuchung von OBDDs und ihren Erweiterungen verwendet zugleich Methoden aus verschiedenen Bereichen der theoretischen Informatik. Dies sind Methoden zum Entwurf effizienter Algorithmen oder zum Beweis, dass solche Algorithmen vermutlich nicht existieren. Weiterhin wird die Kommunikationskomplexität als wichtigste Methode zum Beweis von unteren Schranken für den Ressourcenbedarf von Berechnungen behandelt. Nichtdeterministische Algorithmen sind in der Regel nicht praktikabel. Dagegen gibt es Varianten von nichtdeterministischen OBDDs, die auch in der Praxis eingesetzt werden. In der Vorlesung werden auch die Auswirkungen der theoretischen Ergebnisse auf die Praxis diskutiert.

Skript

Eine vorläufige Version des Skripts ist als PDF-Datei erhältlich.

Übungsblätter

Die Übungsblätter sind hier erhältlich.

Inhalt der Vorlesung

• 16.10.2006: Einführung und Motivation von BDDs, Zusammenhang zwischen BDDs und nichtuniformen Berechnungsmodellen, Anforderungen an Datenstrukturen für boolesche Funktionen
• 18.10.2006: Grundlagen zu OBDDs: Definition, Reduktionsregeln, Eindeutigkeit, Reduktionsalgorithmus
• 23.10.2006: Reduktion mit linearer Rechenzeit, die Abhängigkeit der OBDD-Größe von der Variablenordnung
• 25.10.2006: Der Algorithmus von Friedman und Supowit, NP-Schwere von MinSBDD
• 30.10.2006: Heuristiken für das Variablenordnungsproblem, partiell symmetrische Funktionen
• 06.11.2006: Algorithmen für die grundlegenden Operationen auf OBDDs
• 13.11.2006: Worst-Case-Beispiele für Synthese, Quantifizierung und Ersetzen durch Konstanten, die effiziente Implementierung von BDD-Paketen
• 15.11.2006: Operationen zur Veränderung der Variablenordnung, Einführung ZBDDs
  
• 20.11.2006: Struktursatz für ZBDDs, Zusammenhang zwischen ZBDD- und OBDD-Größe, Synthese, Ersetzung durch Konstanten
• 22.11.2006: OFDDs: Einführung, τ-Operator, Struktursatz, symmetrische Funktionen, die Funktionen 1-cl_n,3 und ⊕cl_n,3
• 27.11.2006: OFDDs: Erfüllbarkeit-Alle*, Synthese, Ersetzung durch Konstanten, Einführung in ⊕OBDDs
  
• 29.11.2006: ⊕OBDDs: Beispielfunktionen, Entfernen von 0-Kanten und Umdrehen der Variablenordnung*, Hinzufügen und Entfernen von Linearkombinationen, Struktursatz
• 04.12.2006: Minimierungsprobleme für ⊕OBDDs*
• 06.12.2006: Fortsetzung Minimierungsprobleme für ⊕OBDDs, Synthese und die übrigen Operationen
• 11.12.2006: Einführung nichtdeterministische und randomisierte OBDDs, Partitioned BDDs
• 13.12.2006: Ersetzen durch Konstanten bei PBDDs, Randomisierte OBDDs: Einführung, Probability Amplification, Fingerprinting
• 18.12.2006: Erfüllbarkeitstest für randomisierte OBDDs, Einführung FBDDs, Minimierung, Synthese, Arithmetisierung von Berechnungen
• 20.12.2006: Äquivalenztest von FBDDs, graphgesteuerte BDDs und Algorithmen darauf
• 08.01.2007: Transformierte BDDs*
• 10.01.2007: Untere Schranken für BDDs ohne weitere Einschränkungen, Einführung Kommunikationskomplexität
• 15.01.2007: Rechtecke, Rangmethode, Unterscheidungsmengen, Anwendung auf OBDDs
• 17.01.2007: Untere Schranke für die OBDD-Größe von HWB, nichtdeterministische Kommunikationskomplexität
• 22.01.2007: Fortsetzung nichtdeterministische Kommunikationskomplexität, untere Schranken für FBDDs für Funktionen mit der Eigenschaft k-mixed
• 24.01.2007: Untere Schranken für die Größe von FBDDs für die Funktion ⊕cl_n,3 und die charakteristischen Funktionen von Reed-Muller-Codes*, sowie für die Größe von nichtdeterministischen FBDDs für PERM.
• 29.01.2007: Untere Schranke für die Größe von PBDDs für INDEX-EQ, Beweis der Aussage NL⊆⊕L (nach S. Jukna, "Extremal Combinatorics", Springer 2001, Kap. 12.3.)
• 31.01.2007: Implizite Graphdarstellungen, PSPACE-Vollständigkeit von GAP für implizit dargestellte Graphen
• 05.02.2007: Ein impliziter Algorithmus zur Flussmaximierung
• 07.02.2007: Der Pentium-Dividierer und die Verifikation mit OBDDs (Literatur: Skript Theorie des Logikentwurfs, S. 42-46)

Für die mit * gekennzeichneten Punkte wurde in der Vorlesung zusätzliches Material verteilt.