Changeset 167 for liacs/SCA2010/BDD

Timestamp:

Jul 27, 2010, 1:27:34 PM (14 years ago)

Author:

Rick van der Zwet

Message:

Paper ready for next delivery

Location:

liacs/SCA2010/BDD

Files:

• report.pdf (added)
• report.tex (modified) (10 diffs)

liacs/SCA2010/BDD/report.tex

@@ -18 +18 @@
 \usetikzlibrary{positioning}
 
+\newcommand*\circled[1]{%
+  \tikz[baseline=(C.base)]\node[draw,circle,inner sep=0.5pt](C) {$#1$};\!
+}
+\newcommand*\squared[1]{%
+  \tikz[baseline=(C.base)]\node[draw,rectangle,rounded corners,inner sep=0.5pt](C) {$#1$};\!
+}
+\newcommand*\BDD{\emph{BDD}}
+\newcommand*\BDDs{\emph{BDDs}}
+
 \author{Rick van der Zwet, Universiteit Leiden}
 \title{BDD synthese}
@@ -33 +42 @@
 aanleiding van het vak Seminar Combinatorial Algorithms 2010~\cite{SCA2010}. 
 \begin{figure}[htbp]
-\label{voorbeeldSamenvoegen}
 \begin{tikzpicture}[on grid]
 \tikzstyle{true}=[]
@@ -157 +165 @@
 
 \end{tikzpicture}
-\caption{Voorbeeld: twee \emph{BDD}s die samengesmolten worden door gebruik te
+\caption{Voorbeeld: twee \BDDs die samengesmolten worden door gebruik te
 maken van formule~\ref{melt-eq}. Let er wel op dat dit voorbeeld geen
 ontbrekende laag van knopen heeft, waardoor knopen van alle niveaus beschikbaar
@@ -164 +172 @@
 
 \section{Introductie BDD}
-Synthese van een Binary Decision Diagram \emph{BDD} is een belangrijk
-\emph{BDD} algoritme~\cite[p.~86]{DK2009}. Het neemt in essentie een \emph{BDD}
-functie $f$ en combineert deze met een andere \emph{BDD} functie $g$
-zodanig dat er een nieuwe \emph{BDD} ontstaat voor een nieuwe functie,
+Synthese van een Binary Decision Diagram \BDD is een belangrijk
+\BDD algoritme~\cite[p.~86]{DK2009}. Het neemt in essentie een \BDD
+functie $f$ en combineert deze met een andere \BDD functie $g$
+zodanig dat er een nieuwe \BDD ontstaat voor een nieuwe functie,
 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 van het uitdrukken van complexe systemen door
+\BDDs aan de basis staat van het uitdrukken van complexe systemen door
 middel van gecombineerde simpele functies. In Hoofdstuk~\ref{werking} zal deze
 techniek uitgelegd worden, het zogenoemde \emph{smelten} (\emph{melding}) dat 
 in Hoofdstuk~\ref{voorbeeld} toegepast zal worden in een concreet voorbeelden.
 
-\section{Samenvoegen van \emph{BDD}}
+\section{Samenvoegen van \BDD}
 \label{werking}
-De term voor het samenvoegen van \emph{BDD} structuren zullen we smelten
+De term voor het samenvoegen van \BDD structuren zullen we smelten
 (\emph{melding}) noemen. Het werkt volgens de volgende principes.  Men neme
 twee knopen $\alpha = (v,l,h)$ en $\alpha' = (v',l',h')$. De knoop $\alpha
@@ -195 +203 @@
 De oplettende lezer zal zien dan als je Formule~\ref{melt-eq} toepast op de
 bladeren er door samenvoegen van de bladeren ---zie bijvoorbeeld
-Figuur~\ref{voorbeeldSamenvoegen}--- in plaats van de twee bladeren
+voorbeeld in Hoofstuk~\ref{voorbeeldSamenvoegen}--- in plaats van de twee bladeren
 $\top$ en $\bot$, er nu vier bladeren mogelijk zijn:
 \begin{equation}
@@ -203 +211 @@
 \end{array}
 \end{equation}
-Om er weer een ``valide'' \emph{BDD} van te maken zullen deze bladeren vervangen
+Om er weer een ``valide'' \BDD van te maken zullen deze bladeren vervangen
 worden door het uitgerekende blad. Als bijvoorbeeld de $\diamond$ operatie
 bedoelt is voor een \emph{EN} operatie, wordt de blad-rij in~\ref{bladeren}
-vervangen door de rij $\bot, \bot, \bot, \top$. Nu is het zaak het \emph{BDD}
+vervangen door de rij $\bot, \bot, \bot, \top$. Nu is het zaak het \BDD
 te vereenvoudigen, om zo duplicaat-bladeren te snoeien (\emph{pruning}).
 
 De kracht van deze aanpak zit hem in de 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 alle.
-
-Door de \emph{BDD}s achter elkaar te plakken kan met maximaal $B(f)B(g)$ knopen
-een \emph{BDD} voor $f \diamond g$ gerealiseerd worden.
+het eind van de rit. De gegeneerde gesmolten \BDD is geldig voor alle.
+
+Door de \BDDs achter elkaar te plakken kan met maximaal $B(f)B(g)$ knopen
+een \BDD voor $f \diamond g$ gerealiseerd worden.
 Hoofdstuk~\ref{voorbeeldPlakken} is hier een voorbeeld van. In het meer algemene
 geval geldt meestal $B(f) + B(g)$ als bovengrens.  Deze grenzen worden in
@@ -225 +233 @@
 (zie Formule~\ref{bladeren}) door $\bot$ en $\top$, en (c) voer het algoritme
 $R$\footnote{Algoritme $R$ wordt niet in deze samenvatting behandeld; de
-vak-website~\cite[SCA2010] heeft een referentie naar algoritme $R$ 
----\url{http://www.liacs.nl/~kosters/semcom/tomb.pdf}--- welke behandeld wordt
+vak-website~\cite{SCA2010} heeft een referentie naar algoritme $R$ 
+\url{http://www.liacs.nl/~kosters/semcom/tomb.pdf} welke behandeld wordt
 door Tom.} op $f \diamond g$. Op het eerste gezicht lijkt algoritme $R$ er ongeveer
 $B(f)B(g)$ operaties over te doen, maar doordat je onbereikbare knopen niet
@@ -241 +249 @@
 \section{Voorbeelden}
 \label{voorbeeld}
-\subsection{Product-groei in synthese van \emph{BDD}}
+\subsection{Product-groei in synthese van \BDD}
 \label{voorbeeldSamenvoegen}
 Het volgende voorbeeld is een uitwerking van opgave 60~\cite[p.~130]{DK2009}
 de offi\"{e}le uitwerking is te vinden op \cite[p~.195]{DK2009}
-
+\\ \\
+Voorgaande aan de uitwerking is het belangrijk te weten wat een \emph{QDD} (aka
+\emph{quasi-BDD}~\cite[p.~102-103]{DK2009}) is. Elke functie heeft een unieke
+\emph{QDD} welke lijkt op een \BDD echter is de start-knoop altijd
+\circled{1} en elke \circled{k} knoop bestaat for $k < n$ takken naar twee
+\squared{k+1} knopen. Wat in het kort wilt zeggen dat elk pad van de
+start-knoop naar de bladeren een lengte heeft van $n$. Om dat mogelijk te maken
+mogen de \emph{HOOG} en \emph{LAAG} takken van een \emph{QDD} gelijk zijn. Let
+wel op dat reductie toegepast moet worden. 
+\\ \\
 Neem aan dat $f(x_{1},\dots,x_{n})$ en $g(x_{1},\dots,x_{n})$ de respectieve
 \emph{profielen} (\emph{profiles})~\cite[p.~101]{DK2009}
-$(b_{0},\dots,b_{n})$\footnote{Waar er $b_{k}$ knopen zijn die splitsen
-op variable $f(x_{k+1})$ en $b_{n}$ het aantal bladeren is.} en
+$(b_{0},\dots,b_{n})$ ---waar $b_{k}$ met $0 \le k < n$ de knopen zijn die splitsen
+op variable $f(x_{k+1})$ en $b_{n}$ het aantal bladeren is--- en
 $(b'_{0},\dots,b_{n})$ hebben, en de respectieve \emph{quasi-profielen}
 (\emph{quasi-profiles})~\cite[p.~103]{DK2009}
-$(q_{0},\dots,q_{n})$\footnote{Waar $q_{k-1}$ het aantal \circle{k} knopen in
-de \emph{QDD} is.} en $(q'_{0},\dots,q'_{n})$.  
-
-Om te laten zijn dat de gesmolten $f \diamond g$ het aantal knopen $B(f
-\diamond g) \leq \sum^{n}_{j=0}(q_{j}b'_{j}+b_{j}q'_{j}-b_{j}b'_{j})$ bevat
-moet gekeken worden naar het aantal \emph{beads}~\cite[p.~72]{DK2009} dat
+$(q_{0},\dots,q_{n})$ ---waar $q_{k-1}$ met $0 < k < n$ het aantal \circled{k} knopen in
+de \emph{QDD} van $f$ is--- en $(q'_{0},\dots,q'_{n})$.  
+
+Om te laten zijn dat de gesmolten $f \diamond g$ het aantal knopen
+\begin{equation}
+\label{eq:knopen}
+B(f \diamond g) \leq \sum^{n}_{j=0}(q_{j}b'_{j}+b_{j}q'_{j}-b_{j}b'_{j})
+\end{equation} 
+bevat moet gekeken worden naar het aantal \emph{beads}~\cite[p.~72]{DK2009} dat
 mogelijkerwijs gemaakt kan worden van de functies $f$ en $g$.  
-
-Hierbij geldt dan voor een willikeurige functie $n$ met als profiel
-$(b_{0},\dots,b_{n})$ en quasi-profiel $(q_{0},\dots,q_{n})$ dat
-$B(q_{0},\dots,q_{n}) \geq B(b_{0},\dots,b_{n})$. En tevens dan
-$(b_{0},\dots,b_{n}) \subseteq (q_{0},\dots,q_{n})$. Hieruit volgt dat een
-geen-bead zich bevindt in $(q_{0},\dots,q_{n}) \setminus (b_{0},\dots,b_{n})$.
-
-Elke bead \beta van de orde $n - j$ in het geordende paar $(f,g)$ zal zich
+Voor een willikeurige functie $n$ met als profiel $(b_{0},\dots,b_{n})$ en
+quasi-profiel $(q_{0},\dots,q_{n})$ geldt dat $B(q_{0},\dots,q_{n}) \geq
+B(b_{0},\dots,b_{n})$. En tevens dan $(b_{0},\dots,b_{n}) \subseteq
+(q_{0},\dots,q_{n})$. Hieruit volgt dat een geen-bead zich bevindt in
+$(q_{0},\dots,q_{n}) - (b_{0},\dots,b_{n})$.
+
+Elke bead van de orde $n - j$ in het geordende paar $(f,g)$ zal zich
 bevinden in een van de volgende groepen; (a) de standaard-combinatie van de
 $b_{j}b_{j}'$ geordende beats van $(f,g)$ of (b) de gegenereerde reeks van een
@@ -276 +295 @@
 lezer.
 
-\subsection{Som-groei in synthese van \emph{BDD}}
+\subsection{Som-groei in synthese van \BDD}
 \label{voorbeeldPlakken}
 Het volgende voorbeeld is een uitwerking van opgave 63~\cite[p.~131]{DK2009}
@@ -282 +301 @@
 
 \begin{equation}
-f(x_{1},\dots,x_{n}) = M_{m}(x_{1} \oplus x_{2},x_{3} \oplus x_{4},\dots,x_{2m-1} \oplus x_{2m};x_{2m+1},\dots,x_{n}) \\
-en \\
-g(x_{1},\dots,x_{n}) = M_{m}(x_{2} \oplus x_{3},\dots,x_{2m-2} \oplus x_{2m-1},x_{2m};\overline x_{2m+1},\dots,\overline x_{n})$ waar $n = 2m + 2^{m}
-\caption{\oplus is de binary operator \emph{XOR}}
+\begin{array}{lcl}
+f(x_{1},\dots,x_{n}) & = & M_{m}(x_{1} \oplus x_{2},x_{3} \oplus x_{4},\dots,x_{2m-1} \oplus x_{2m};x_{2m+1},\dots,x_{n}) \\
+g(x_{1},\dots,x_{n}) & = & M_{m}(x_{2} \oplus x_{3},\dots,x_{2m-2} \oplus x_{2m-1},x_{2m};\overline x_{2m+1},\dots,\overline x_{n}) \\
+\end{array}
+\label{eq:opgave63}
 \end{equation}
+In Vergelijking~\ref{eq:opgave63} zijn $f$ en $g$ gedefinieerd, waarbij $\oplus$
+de binary operator \emph{XOR} is en $n = 2m + 2^{m}$.
 
 Dan is $B(f) = 2^{m+2}-1 \approx 4n$, $B(g) = 2^{m+1}-2^{m} \approx 3n$ en $B(g