ROBDD-Anwendungen: Modelle zählen

typische Anwendungen von ROBDD ...

• (nicht Erfüllbarkeit, denn ...)
• Äquivalenz
• Zählen von Modellen:

  | Mod(0)| = 0,| Mod(1)| = 1,
  | Mod(l, x, r)| = | Mod(l )| + | Mod(r)|

diese Zahlen bottom-up dranschreiben: Linearzeit

dabei beachten, daß bei der Konstruktion evtl. Variablen verschwunden sind

Beispiel (Übung) Anzahl der Lösungen des n-Damen-Problems