Entscheidungsgraphen mit Sharing

DAG (gerichteter kreisfreier Graph) G = (V, E) heißt geordnetes binäres Entscheidungsdiagramm, falls:

• G hat einen Startknoten (ohne Vorgänger)
• die Endknoten (ohne Nachfolger) von G sind ⊆{0, 1}.
• Struktur s : V $\setminus$ {0, 1}→V×Var×V.

heißt geordnet, falls Variablen auf jedem Pfad absteigen

heißt reduziert (ROBDD), falls außerdem

• ∀v∈V : s(v) = (l, x, r)⇒l≠r (keine gleichen Kinder)
• ∀v, w∈V : s(v) = s(w)⇒v = w (keine gleichen Knoten)

Randal E. Bryant. Graph-Based Algorithms for Boolean Function Manipulation. IEEE Trans.Comp., C-35(8):677-691, 1986 http://www.cs.cmu.edu/~bryant/pubdir/ieeetc86.pdf