\begin{slide}{ROBDD-Anwendungen: Modelle zählen}

typische Anwendungen von ROBDD \dots
\begin{itemize}
\item (\emph{nicht} Erfüllbarkeit, denn \dots)
\item Äquivalenz
\item Zählen von Modellen:

$|\Mod(0)|=0, |\Mod(1)|=1,$ \\
$|\Mod(l,x,r)|=|\Mod(l)|+|\Mod(r)|$
\end{itemize}

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

\end{slide}
