Changeset 164
- Timestamp:
- Jul 27, 2010, 10:04:48 AM (14 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
liacs/SCA2010/BDD/report.tex
r139 r164 30 30 \section{Inleiding} 31 31 De hierin besproken inhoud is een samenvatting gemaakt van pagina 86--88 en de 32 daarin genoemde opgave 60 en 63 uit het college boek~\cite{DK2009} na 32 daarin genoemde opgave 60 en 63 uit het college boek~\cite{DK2009} naar 33 33 aanleiding van het vak Seminar Combinatorial Algorithms 2010~\cite{SCA2010}. 34 34 \begin{figure}[htbp] 35 \label{voorbeeldSamenvoegen} 35 36 \begin{tikzpicture}[on grid] 36 37 \tikzstyle{true}=[] … … 157 158 \end{tikzpicture} 158 159 \caption{Voorbeeld: twee \emph{BDD}s die samengesmolten worden door gebruik te 159 maken van formule~\ref{melt-eq}. Let wel op dat dit voorbeeld geen ontbrekende160 laag van nodes heeft, waardoor nodes van alle niveaus beschikbaar zijn. Op het 161 moment dat de $\diamond$ ingevuld gaat worden is het ook zaak om de bladeren 162 (zie vergelijking~\ref{bladeren}) te vereenvoudigen} \end{figure}160 maken van formule~\ref{melt-eq}. Let er wel op dat dit voorbeeld geen 161 ontbrekende laag van knopen heeft, waardoor knopen van alle niveaus beschikbaar 162 zijn. Op het moment dat de $\diamond$ ingevuld gaat worden is het ook zaak om 163 de bladeren (zie vergelijking~\ref{bladeren}) te vereenvoudigen} \end{figure} 163 164 164 165 \section{Introductie BDD} 165 Synthese van een Binary Decision Diagram \emph{BDD} is het belangrijke166 \emph{BDD} algoritme~\cite[p g 86]{DK2009}. Welkein essentie een \emph{BDD}167 functie ,$f$, pakt en deze combineert met een andere \emph{BDD} functie,$g$,168 zodanig dat er een nieuwe \emph{BDD} ontstaat voor de nieuwe functie.169 Bijvoorbeeld $f \wedge g$ of $f \oplus g$.166 Synthese van een Binary Decision Diagram \emph{BDD} is een belangrijk 167 \emph{BDD} algoritme~\cite[p.~86]{DK2009}. Het neemt in essentie een \emph{BDD} 168 functie $f$ en combineert deze met een andere \emph{BDD} functie $g$ 169 zodanig dat er een nieuwe \emph{BDD} ontstaat voor een nieuwe functie, 170 bijvoorbeeld $f \wedge g$ of $f \oplus g$. 170 171 De reden dat dit zo belangrijk is komt met het feit dat het combineren van 171 \emph{BDD}s aan de basis staat aan het uitdrukken van complexe systemen dmv van172 gecombineerde simpele functies. In sectie~\ref{werking} zal deze techniek 173 uitgelegd worden, het zogenoemde \emph{smelten} (\emph{melding}) welke in 174 sectie~\ref{voorbeeld} dittoegepast zal worden in een concreet voorbeelden.172 \emph{BDD}s aan de basis staat van het uitdrukken van complexe systemen door 173 middel van gecombineerde simpele functies. In Hoofdstuk~\ref{werking} zal deze 174 techniek uitgelegd worden, het zogenoemde \emph{smelten} (\emph{melding}) dat 175 in Hoofdstuk~\ref{voorbeeld} toegepast zal worden in een concreet voorbeelden. 175 176 176 177 \section{Samenvoegen van \emph{BDD}} 177 178 \label{werking} 178 De term voor het samenvoegen \emph{BDD} structuren zullen we smelten 179 (\emph{melding}) noemen. Er werkt volgens de volgende principes. Men neme 180 $\alpha = (v,l,h)"$ en $\alpha' = (v',l',h')$. De $\alpha \diamond \alpha'$, de 181 "\emph{emulsie}" (\emph{meld}) van $\alpha$ en $\alpha'$, is dan als volgt 182 gedefinieerd als $\alpha$ ad $\alpha'$ niet beiden bladeren (\emph{sinks}) zijn: 179 De term voor het samenvoegen van \emph{BDD} structuren zullen we smelten 180 (\emph{melding}) noemen. Het werkt volgens de volgende principes. Men neme 181 twee knopen $\alpha = (v,l,h)$ en $\alpha' = (v',l',h')$. De knoop $\alpha 182 \diamond \alpha'$, de ``\emph{emulsie}'' (\emph{meld}) van $\alpha$ en 183 $\alpha'$, is dan als volgt gedefinieerd als $\alpha$ en $\alpha'$ niet beiden 184 bladeren (\emph{sinks}) zijn: 183 185 \begin{equation} 184 186 \label{melt-eq} 185 187 \alpha \diamond \alpha' = \left\{ 186 188 \begin{array}{l l} 187 (v, l \diamond l' ), h \diamond h'), & \mathrm{als~} v = v'; \\188 (v, l \diamond \alpha' ), h \diamond \alpha'), & \mathrm{als~} v < v'; \\189 (v, \alpha \diamond l' ), \alpha \diamond h'), & \mathrm{als~} v > v'. \\189 (v, l \diamond l', h \diamond h'), & \mathrm{als~} v = v'; \\ 190 (v, l \diamond \alpha', h \diamond \alpha'), & \mathrm{als~} v < v'; \\ 191 (v, \alpha \diamond l', \alpha \diamond h'), & \mathrm{als~} v > v'. \\ 190 192 \end{array} \right. 191 193 \end{equation} 192 194 193 De oplettende lezer (voor de rest, voorbeeld figuur~\ref{voorbeeldSamenvoegen}) zal 194 zien dat je door het samenvoegen van de bladeren er in plaats van de twee bladeren 195 De oplettende lezer zal zien dan als je Formule~\ref{melt-eq} toepast op de 196 bladeren er door samenvoegen van de bladeren ---zie bijvoorbeeld 197 Figuur~\ref{voorbeeldSamenvoegen}--- in plaats van de twee bladeren 195 198 $\top$ en $\bot$, er nu vier bladeren mogelijk zijn: 196 199 \begin{equation} … … 200 203 \end{array} 201 204 \end{equation} 202 Om er weer een 'valide' \emph{BDD} van te maken zullen deze bladeren vervangen203 worden door het uitgerekende blad. Als bijvoorbeeldde $\diamond$ operatie een204 $EN$ operatie was, wordt de blad-rij in~\ref{bladeren} vervangen door de rij205 $\bot, \bot, \bot, \top$. Nu is het zaak de\emph{BDD} te vereenvoudigen, om zo206 duplicaat 207 208 De kracht van deze aanpak zit hem in de zogenoemdegenerieke $\diamond$205 Om er weer een ``valide'' \emph{BDD} van te maken zullen deze bladeren vervangen 206 worden door het uitgerekende blad. Door bijvoorbeeld voor de $\diamond$ operatie een 207 \emph{EN} operatie te nemen, wordt de blad-rij in~\ref{bladeren} vervangen door de rij 208 $\bot, \bot, \bot, \top$. Nu is het zaak het \emph{BDD} te vereenvoudigen, om zo 209 duplicaat-bladeren te snoeien (\emph{pruning}). 210 211 De kracht van deze aanpak zit hem in de generieke $\diamond$ 209 212 operatie. Het maakt niet uit welke booleaanse operatie er gebruikt wordt aan 210 het eind van de rit. De gegeneerde gesmolten \emph{BDD} is geldig voor alle n.213 het eind van de rit. De gegeneerde gesmolten \emph{BDD} is geldig voor alle. 211 214 212 215 Kijkend naar de limieten moet geoordeeld worden kan hetzelfde altijd bereikt … … 304 307 305 308 \begin{thebibliography}{} 306 \bibitem[DK2009]{DK2009} D.E. Knuth. Fascicle 1. \texttt{Bitwise Tricks \&307 Techniques; Binary Decision Diagrams}, volume 4 of \texttt{The Art of Computer 308 P rogramming}. Pearson Education, first edition, March2009.309 \bibitem[DK2009-Fas0]{DK2009-0} D.E. Knuth. Fascicle 0. \texttt{Bitwise Tricks \&310 Techniques; Binary Decision Diagrams}, volume 4 of \texttt{The Art of Computer311 Programming }. Pearson Education, first edition, March2009.309 \bibitem[DK2009]{DK2009} D.E. Knuth. Bitwise Tricks \& Techniques; Binary 310 Decision Diagrams, volume 4, Fascicle 1, of The Art of Computer Programming. 311 Pearson Education, first edition, 2009. 312 \bibitem[DK2009-Fas0]{DK2009-0} D.E. Knuth. Bitwise Tricks \& Techniques; 313 Binary Decision Diagrams, volume 4, Fascicle 0, of The Art of Computer 314 Programming. Pearson Education, first edition, 2009. 312 315 \bibitem[SCA2010]{SCA2010} Lecture Seminar Combinatorial Algorithms, 313 \url{http://www.liacs.nl/~kosters/semcom/}, dr.W.A. (Walter) Kosters, LIACS,314 Spring 2010 316 \url{http://www.liacs.nl/~kosters/semcom/}, W.A. (Walter) Kosters, LIACS, 317 Spring 2010. 315 318 316 319 \end{thebibliography}
Note:
See TracChangeset
for help on using the changeset viewer.