Freie Universität Berlin
Fachbereich Mathematik

Das Variablenordnungsproblem für OBDDs und SBDDs

Diplomarbeit

eingereicht von Harry Preuß

Oktober 1997

Inhaltsverzeichnis

Einleitung ... 3

1 Variablenordnungen für OBDDs: Problematik und Komplexität ... 6

1.1 Motivation ... 6
1.2 OBDDs: Definitionen und Komplexität grundlegender Operationen ... 9
1.3 Die Komplexität des Variablenordnungsproblems ... 14
1.4 Heuristiken zur Lösung des Variablenordnungsproblems ... 20
1.4.1 Heuristiken zur Berechnung einer Startordnung ... 20
1.4.2 Heuristiken zur Verbesserung einer Variablenordnung ... 23

2 Blockweise Variablenordnungen für SBDDs ... 26

2.1 Die Problemstellung ... 26
2.2 SBDDs ohne komplementierte Kanten ... 29
2.3 SBDDs mit komplementierten Kanten ... 38
2.4 Beurteilung der Resultate ... 47

3 Variablenordnungsheuristiken für die formale Verifikation sequentieller Schaltwerke ... 49

3.1 Die Problemstellung ... 49
3.2 Die Variablenordnungsheuristik von Touati, Savoj, Lin, Brayton und Sangiovanni-Vincentelli ... 53
3.3 Die Variablenordnungsheuristik von Aziz, Tasiran und Brayton ... 57
3.4 Minimierung der Bewertungsfunktionen durch Simulated Annealing ... 62
3.4.1 Die Berechnung der Bewertungsfunktion von Touati ... 64
3.4.2 Die Berechnung der Bewertungsfunktion von Aziz ... 66

4 Experimentelle Resultate und Resümee ... 70

4.1 Minimierung der Bewertungsfunktionen ... 72
4.2 Minimierung des OBDD der Übergangsrelation und der erreichten Zustände ... 74
4.3 Resümee ... 77

Literaturverzeichnis ... 79

Einleitung

Für viele, auch industriell relevante Anwendungen, z.B. den Entwurf und die formale Verifikation von VLSI Schaltkreisen, benötigt man eine Datenstruktur zur Darstellung und Manipulation Boolescher Funktionen. Für diesen Zweck haben sich vor allem ordered binary decision diagrams, kurz OBDDs genannt, durchgesetzt.

Aufbauend auf frühe Arbeiten von Lee und Akers führte Bryant 1986 diese speziellen Graphen und grundlegende Algorithmen auf diesen Graphen ein. Minato, Ishiura und Yajima zeigten, wie man platzsparend mehrere OBDDs in einer Struktur speichern kann, und nannten diese Struktur shared binary decision diagram oder kurz SBDD. Außerdem führten sie OBDDs mit komplementierten Kanten ein, eine weitere Veränderung, die in manchen Fällen den Platzbedarf eines OBDD um fast die Hälfte verringert. Seitdem sind SBDDs mit oder ohne komplementierte Kanten die bevorzugte und in vielen Anwendungsbereichen erfolgreichste Datenstruktur zur Darstellung Boolescher Funktionen.

Die Größe eines OBDD oder SBDD hängt stark von der verwendeten Variablenordnung ab. Lange wurde vermutet, dass es NP-schwer ist, eine optimale Variablenordnung für ein gegebenes OBDD oder SBDD zu finden. 1993 konnten Tani, Hamaguchi und Yajima diese Vermutung für SBDDs beweisen, 1996 folgte ein Beweis von Bollig und Wegener für OBDDs.

Diese Ergebnisse rechtfertigen es, nach speziellen Klassen von Booleschen Funktionen zu suchen, für die effizient eine optimale Variablenordnung berechnet werden kann. Sauerhoff, Wegener und Werchner betrachteten Funktionen, die durch einen baumartigen Schaltkreis gegeben sind. Sie bewiesen, dass man für eine solche Funktion in linearer Zeit eine Variablenordnung berechnen kann, die sowohl für OBDDs als auch für OBDDs mit komplementierten Kanten optimal ist.

[...]