Operationen mit ROBDDs (Implementierung)

• dynamische Optimierung (d. h. von unten nach oben ausrechnen und Ergebnisse merken).

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

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

• alle Knoten in Hashtabelle (``hash consing''),

  garantiert Reduktion

• gemeinsames hash consing über mehrere ROBDDs ( ⇒ ``BDD base'') erlaubt Nachnutzung von Arbeit