\begin{slide}{Eigenschaften von ROBDDs}

  \begin{itemize}\itemsep 2pt \parskip 2pt
  \item 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
    $\neg x\wedge [l] \vee x\wedge [r]$.

  \item Erfüllbarkeit, Allgemeingültigkeit trivial
  \item Satz: ROBDD repräsentiert Formeln \emph{kanonisch}

    (zu gegebener Formel $F$ und Variablenordung $>$ 

    gibt es genau ein ROBDD)

    Beweis: Konstruktion aus vollständigem Entscheidungsbaum
  \item Größe  der ROBDDS?
  \item effiziente Operationen? (folgende Folien)
  \end{itemize}

\end{slide}
