Eigenschaften von ROBDDs

• jedes ROBDD repräsentiert eine Menge von partiellen Belegungen

  (alle Pfade von Wurzel zu 1)

  Wert [n] für Knoten mit s(n) = (l, x, r) ist ¬x∧[l]∨x∧[r].

• Erfüllbarkeit, Allgemeingültigkeit trivial
• Satz: ROBDD repräsentiert Formeln kanonisch

  (zu gegebener Formel F und Variablenordung >

  gibt es genau ein ROBDD)

  Beweis: Konstruktion aus vollständigem Entscheidungsbaum

• Größe der ROBDDS?
• effiziente Operationen? (folgende Folien)