source: liacs/SCA2010/BDD/report.tex@ 128

Last change on this file since 128 was 128, checked in by Rick van der Zwet, 14 years ago

Work in process we are getting somewhere...

File size: 3.5 KB
RevLine 
[2]1%
2% $Id: report.tex 571 2008-04-20 17:31:04Z rick $
3%
4
5\documentclass[12pt,a4paper]{article}
6
7\frenchspacing
8\usepackage[english,dutch]{babel}
9\selectlanguage{dutch}
10\usepackage{graphicx}
11\usepackage{url}
12\usepackage{multicol}
13\usepackage{fancybox}
14\usepackage{amssymb,amsmath}
15
16\author{Rick van der Zwet, Universiteit Leiden}
[126]17\title{BDD synthese}
[2]18\author{Rick van der Zwet\\
[126]19 \texttt{<hvdzwet@liacs.nl>}}
[2]20\date{\today}
21
22\begin{document}
23
24\maketitle
25
26\section{Inleiding}
[128]27Synthese van een Binary Decision Diagram \emph{BDD} is het belangrijke
[126]28\emph{BDD} algoritme~\cite[pp 86]{DK2009}. Welke in essentie een \emph{BDD}
29functie,$f$, pakt en deze combineert met een andere \emph{BDD} functie,$g$,
30zodanig dat er een nieuwe \emph{BDD} ontstaat voor de nieuwe functie.
[127]31Bijvoorbeeld $f \wedge g$ of $f \oplus g$.
32De reden dat dit zo belangrijk is komt met het feit dat het combineren van
33\emph{BDD}s aan de basis staat aan het uitdrukken van complexe systemen dmv van
34gecombineerde simpele functies. In sectie~\ref{werking} zal deze techniek
[128]35uitgelegd worden, het zogenoemde \emph{smelten} (\emph{melding}) welke in
36sectie~\ref{voorbeeld} dit toegepast zal worden in een concreet voorbeeld.
[126]37
[128]38\section{Samenvoegen van \emph{BDD}}
[126]39\label{werking}
[127]40De term voor het samenvoegen \emph{BDD} structuren zullen we smelten
41(\emph{melding}) noemen. Er werkt volgens de volgende principies. Men neme
42$\alpha = (v,l,h)"$ en $\alpha' = (v',l',h')$. De $\alpha \diamond \alpha'$, de
43"\emph{emulsie}" (\emph{meld}) van $\alpha$ en $\alpha'$, is dan als volgt
44gedefineerd als $\alpha$ ad $\alpha'$ niet beiden bladeren (\emph{sinks}) zijn:
45\begin{equation}
46\alpha \diamond \alpha' = \left\{
47\begin{array}{l l}
48(v, l \diamond \l'), h \diamond h'), & \mathrm{if~} v = v'; \\
49(v, l \diamond \alpha'), h \diamond \alpha'), & \mathrm{if~} v < v'; \\
50(v, \alpha \diamond l'), \alpha \diamond h'), & \mathrm{if~} v > v'. \\
51\end{array} \right.
52\end{equation}
[126]53
[128]54De oplettende lezer (voor de rest, voorbeeld figuur~\ref{voorbeeldSamenvoegen}) zal
55zien dat je door het samenvoegen van de bladeren er in plaats van de twee bladeren
56$\top$ en $\bot$, er nu vier bladeren mogelijk zijn:
57\begin{equation}
58\label{bladeren}
59\begin{array}{l l l l}
60\bot \diamond \bot, & \bot \diamond \top, & \top \diamond \bot, & \top \diamond \top\\
61\end{array}
62\end{equation}
63Om er weer een 'valide' \emph{BDD} van te maken zullen deze bladeren vervangen
64worden door het uitgerekende blad. Als bijvoorbeeld de $\diamond$ operatie een
65$EN$ operatie was, wordt de bladrij in~\ref{bladeren} vervangen door de rij
66$\bot, \bot, \bot, \top$. Nu is het zaak de \emph{BDD} te vereenvoudigen, om zo
67duplicaat bladeren te snoeien (\emph{pruning}).
68
69De kracht van deze aanpak zit hem in de zogenoemde generieke $\diamond$
70operatie. Het maakt niet uit welke booleaanse operatie er gebruikt wordt aan
71het eind van de rit. De gegeneerde gesmolten \emph{BDD} is geldig voor allen.
72
73Kijkend naar de limieten kan hetzelfde altijd bereikt worden door in het
74slechte geval de \emph{BDD}s achter elkaar te plakken welke dan in dit geval
75$B(f)B(g)$ knopen oplevert. Voorbeeld~\ref{voorbeeldPlakken} is hier een geval
76van. In het meer algemene geval $B(f) + B(g)$
77XXX: TODO
78
79\section{Voorbeelden}
80\label{voorbeeld}
81\label{voorbeeldSamenvoegen}
[126]82XXX: TODO
[128]83\label{voorbeeldPlakken}
[126]84
85\begin{thebibliography}{}
86\bibitem[DK2009]{DK2009} D.E. Knuth. Fascicle 1. \texttt{Bitwise Tricks \&
87Techniques; Binary Decision Diagrams}, volume 4 of \texttt{The Art of Computer
88Programming}. Pearson Education, first edition, March 2009.
[2]89\end{thebibliography}
90\end{document}
Note: See TracBrowser for help on using the repository browser.