
\begin{slide}{Entscheidungsgraphen mit Sharing}

DAG (gerichteter kreisfreier Graph) $G=(V,E)$ heißt 
geordnetes binäres Entscheidungsdiagramm, falls:
  \begin{itemize} \itemsep 0pt \parskip 0pt
  \item $G$ hat einen Startknoten (ohne Vorgänger)
  \item die Endknoten (ohne Nachfolger) von $G$ sind $\subseteq \{0,1\}$.
  \item Struktur $s: V\setminus\{0,1\} \to V\times \Var\times V$.
  \end{itemize}
heißt \emph{geordnet}, falls Variablen auf jedem Pfad absteigen

heißt \emph{reduziert} (ROBDD), falls außerdem
  \begin{itemize} \itemsep 0pt \parskip 0pt
\item $\forall v\in V: s(v)=(l,x,r) \Rightarrow l \neq r$ (keine gleichen Kinder)
  \item $\forall v,w\in V: s(v)=s(w) \Rightarrow v = w$ (keine gleichen Knoten)
  \end{itemize}


Randal E. Bryant. 
\emph{Graph-Based Algorithms for Boolean Function Manipulation}. 
\begin{small}
IEEE Trans.Comp., C-35(8):677-691, 1986
\url{http://www.cs.cmu.edu/~bryant/pubdir/ieeetc86.pdf}
\end{small}
\end{slide}

