Operationen mit ROBDDs

binäre boolesche Operation f mathend000#:

• auf Blättern 0,1 Wert ausrechnen
• auf Knoten mit gleichen Variablen: gemeins. Fallunterscheidung
• auf Knoten mit versch. Variablen: Fallunterscheidung in kleinerer Variablen

der Trick ist: dynamische Optimierung (d. h. von unten nach oben ausrechnen und Ergebnisse merken).

ergibt Laufzeit für f (s, t) mathend000# von O(| s|⋅| t|) mathend000#.

⇒ mathend000# worst-case-Laufzeit für Konstruktion eines ROBDD zu einer Formel: exponentiell