"Binaere Entscheidungsgraphen 001.ps.gz" - читать интересную книгу автора

Universit"at Trier Fachbereich IV - Informatik

Christoph Meinel:

Bin"areEntscheidungsgraphen

Vorlesungsskript Sommersemester 1997

Inhaltsverzeichnis 1 Boolesche Algebra 1

1.1 Notationen . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 1 1.2 Boolesche Algebra . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 2

1.2.1 Algebraische Strukturen . . . . . . . . . . . . . . . . . . . . . . . . 2 1.2.2 Posets . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 2 1.2.3 Verb"ande . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 3 1.2.4 Boolesche Algebra . . . . . . . . . . . . . . . . . . . . . . . . . . . 4 1.2.5 Beispiele und Eigenschaften Boolescher Algebren . . . . . . . . . . 5 1.3 Boolesche Funktionen . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 5 1.4 Tabellendarstellung . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 7 1.5 Shannon'scher Entwicklungssatz . . . . . . . . . . . . . . . . . . . . . . . . 7 1.6 Boolesche Formeln . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 9 1.7 Partielle Boolesche Funktionen . . . . . . . . . . . . . . . . . . . . . . . . . 11

2 OBDDs - Datenstruktur f"ur Schaltfunktionen 13

2.1 Einf"uhrung . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 13

2.1.1 Beispiele . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 13 2.1.2 OBDDs f"ur wichtige Funktionen . . . . . . . . . . . . . . . . . . . . 14 2.1.3 Konstruktion von OBDDs . . . . . . . . . . . . . . . . . . . . . . . 15 2.1.4 Reduzierte OBDDs . . . . . . . . . . . . . . . . . . . . . . . . . . . 16 2.1.5 Weitere Eigenschaften . . . . . . . . . . . . . . . . . . . . . . . . . 17 2.1.6 Einfluss der Variablenordnung . . . . . . . . . . . . . . . . . . . . . 17 2.1.7 Praktische Arbeit mit OBDDs . . . . . . . . . . . . . . . . . . . . . 19 2.1.8 Darstellung partieller Funktionen . . . . . . . . . . . . . . . . . . . 20 2.2 Grundlegende Datenstruktur und Algorithmen . . . . . . . . . . . . . . . . 21

2.2.1 Datenstruktur der OBDDs . . . . . . . . . . . . . . . . . . . . . . . 21

1

2.3 ite-Synthesealgorithmus f"ur OBDDs . . . . . . . . . . . . . . . . . . . . . 23

2.3.1 OBDD-Konstruktion durch "Symbolische Simulation" . . . . . . . . 23 2.3.2 Kompositionsalgorithmus f"ur OBDDs . . . . . . . . . . . . . . . . . 23 2.3.3 Implementierung der Unique-Tabelle . . . . . . . . . . . . . . . . . 24 2.3.4 Implementierung der Computed-Tabelle . . . . . . . . . . . . . . . 24 2.3.5 Pseudocode f"ur den ite-Algorithmus . . . . . . . . . . . . . . . . . . 25 2.3.6 Komplexit"atsanalyse . . . . . . . . . . . . . . . . . . . . . . . . . . 26 2.3.7 Nutzen komplementierter Kanten . . . . . . . . . . . . . . . . . . . 26 2.3.8 Nutzen der Computed-Tabelle . . . . . . . . . . . . . . . . . . . . . 27 2.3.9 Memory Management . . . . . . . . . . . . . . . . . . . . . . . . . . 29

3 Grundlegende OBDD-basierte Algorithmen 31

3.1 Implikationstest . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 3.2 Erf"ullbarkeitsproblem . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32

3.2.1 Finden erf"ullender Belegung . . . . . . . . . . . . . . . . . . . . . . 33 3.2.2 Zahl der erf"ullenden Belegungen . . . . . . . . . . . . . . . . . . . . 34 3.2.3 Finde billigste erf"ullende Belegung . . . . . . . . . . . . . . . . . . 35 3.3 Komposition von Funktionen . . . . . . . . . . . . . . . . . . . . . . . . . . 35 3.4 Quantifizierung . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 3.5 Berechnung verallgemeinerter Kofaktoren . . . . . . . . . . . . . . . . . . . 37

3.5.1 Orthogonale Entwicklung von Schaltfunktionen . . . . . . . . . . . 37 3.5.2 Constrain Operator . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 3.5.3 Restrict Operator . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 3.6 Mengenoperationen und Relationen . . . . . . . . . . . . . . . . . . . . . . 44

4 Optimierung der Variablenordnung 47