Changeset 127 for liacs/SCA2010/BDD/report.tex

Timestamp:

Jun 20, 2010, 7:11:59 PM (14 years ago)

Author:

Rick van der Zwet

Message:

DK _really_ likes his math

File:

• liacs/SCA2010/BDD/report.tex (modified) (1 diff)

liacs/SCA2010/BDD/report.tex

@@ -25 +25 @@
 
 \section{Inleiding}
-Samenvoegen van een Binary Decision Diagram \emph{BDD} is het meest belangrijke
+Samenvoegen van een Binary Decision Diagram \emph{BDD} is het belangrijke
 \emph{BDD} algoritme~\cite[pp 86]{DK2009}. Welke in essentie een \emph{BDD}
 functie,$f$, pakt en deze combineert met een andere \emph{BDD} functie,$g$,
 zodanig dat er een nieuwe \emph{BDD} ontstaat voor de nieuwe functie.
-In sectie~\ref{werking} zal deze techniek uitgelegd worden, welke in
-sectie~\ref{voorbeeld} dit toegepast zal worden als concreet voorbeeld.
+Bijvoorbeeld $f \wedge g$ of $f \oplus g$.
+De reden dat dit zo belangrijk is komt met het feit dat het combineren van
+\emph{BDD}s aan de basis staat aan het uitdrukken van complexe systemen dmv van
+gecombineerde simpele functies. In sectie~\ref{werking} zal deze techniek
+uitgelegd worden, welke in sectie~\ref{voorbeeld} dit toegepast zal worden in een
+concreet voorbeeld.
 
 \section{Samenvoegen}
 \label{werking}
-XXX: TODO
+De term voor het samenvoegen \emph{BDD} structuren zullen we smelten
+(\emph{melding}) noemen. Er werkt volgens de volgende principies.  Men neme
+$\alpha = (v,l,h)"$ en $\alpha' = (v',l',h')$. De $\alpha \diamond \alpha'$, de
+"\emph{emulsie}" (\emph{meld}) van $\alpha$ en $\alpha'$, is dan als volgt
+gedefineerd als $\alpha$ ad $\alpha'$ niet beiden bladeren (\emph{sinks}) zijn:
+\begin{equation}
+\alpha \diamond \alpha' = \left\{
+\begin{array}{l l}
+(v, l \diamond \l'), h \diamond h'), & \mathrm{if~} v = v'; \\
+(v, l \diamond \alpha'), h \diamond \alpha'), & \mathrm{if~} v < v'; \\
+(v, \alpha \diamond l'), \alpha \diamond h'), & \mathrm{if~} v > v'. \\
+\end{array} \right.
+\end{equation}
+ 
 
 \section{Voorbeeld}