\begin{slide}{Operationen mit ROBDDs (Plan)}

binäre boolesche Operation $f(n_1,n_2)$:

mit $s(n_i)=(l_i,x_i,r_i)$


\begin{itemize}
\item auf Blättern 0,1 Wert ausrechnen
\item auf Knoten mit gleichen Variablen $(x_1=x=x_2)$

  $f(n_1,n_2)= f(\neg x\wedge l_1\vee x\wedge r_1,
                \neg x\wedge l_2\vee x\wedge r_2)
            = \neg x\wedge(f(l_1,l_2))
            \vee x\wedge (f(r_1,r_2))$



\item auf Knoten mit versch. Variablen $(x_1>x_2)$

  $f(n_1,n_2)= f(\neg x\wedge l_1\vee x\wedge r_1,n_2)
  = \neg x\wedge(f(l_1,n_2))\vee x\wedge(f(r_1,n_2)).$

\end{itemize}
\end{slide}

\begin{slide}{Operationen mit ROBDDs (Implementierung)}

  \begin{itemize}
  \item 
dynamische Optimierung 
(d. h. von unten nach oben ausrechnen und Ergebnisse merken).

ergibt Laufzeit für $f(s,t)$ von $O(|s|\cdot|t|)$.

$\Rightarrow$ worst-case-Laufzeit für Konstruktion 
eines ROBDD zu einer Formel: exponentiell

\item
  alle Knoten in Hashtabelle (``hash consing''), 

  garantiert Reduktion

\item
  gemeinsames hash consing über mehrere ROBDDs
  ($\Rightarrow$ ``BDD base'') erlaubt Nachnutzung von Arbeit

  \end{itemize}

\end{slide}
