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

Timestamp:

Jun 20, 2010, 7:53:35 PM (14 years ago)

Author:

Rick van der Zwet

Message:

Work in process we are getting somewhere...

File:

• liacs/SCA2010/BDD/report.tex (modified) (3 diffs)

liacs/SCA2010/BDD/report.tex

@@ -25 +25 @@
 
 \section{Inleiding}
-Samenvoegen van een Binary Decision Diagram \emph{BDD} is het belangrijke
+Synthese 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$,
@@ -33 +33 @@
 \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.
+uitgelegd worden, het zogenoemde \emph{smelten} (\emph{melding}) welke in
+sectie~\ref{voorbeeld} dit toegepast zal worden in een concreet voorbeeld.
 
-\section{Samenvoegen}
+\section{Samenvoegen van \emph{BDD}}
 \label{werking}
 De term voor het samenvoegen \emph{BDD} structuren zullen we smelten
@@ -51 +51 @@
 \end{array} \right.
 \end{equation}
- 
 
-\section{Voorbeeld}
+De oplettende lezer (voor de rest, voorbeeld figuur~\ref{voorbeeldSamenvoegen}) zal
+zien dat je door het samenvoegen van de bladeren er in plaats van de twee bladeren
+$\top$ en $\bot$, er nu vier bladeren mogelijk zijn:
+\begin{equation}
+\label{bladeren}
+\begin{array}{l l l l}
+\bot \diamond \bot, & \bot \diamond \top, & \top \diamond \bot, & \top \diamond \top\\
+\end{array}
+\end{equation}
+Om er weer een 'valide' \emph{BDD} van te maken zullen deze bladeren vervangen
+worden door het uitgerekende blad. Als bijvoorbeeld de $\diamond$ operatie een
+$EN$ operatie was, wordt de bladrij in~\ref{bladeren} vervangen door de rij
+$\bot, \bot, \bot, \top$. Nu is het zaak de \emph{BDD} te vereenvoudigen, om zo
+duplicaat bladeren te snoeien (\emph{pruning}).
+
+De kracht van deze aanpak zit hem in de zogenoemde generieke $\diamond$
+operatie. Het maakt niet uit welke booleaanse operatie er gebruikt wordt aan
+het eind van de rit. De gegeneerde gesmolten \emph{BDD} is geldig voor allen.
+
+Kijkend naar de limieten kan hetzelfde altijd bereikt worden door in het
+slechte geval de \emph{BDD}s achter elkaar te plakken welke dan in dit geval
+$B(f)B(g)$ knopen oplevert. Voorbeeld~\ref{voorbeeldPlakken} is hier een geval
+van. In het meer algemene geval $B(f) + B(g)$
+XXX: TODO 
+
+\section{Voorbeelden}
+\label{voorbeeld}
+\label{voorbeeldSamenvoegen}
 XXX: TODO
-\label{voorbeeld}
+\label{voorbeeldPlakken}
 
 \begin{thebibliography}{}