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

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

Some more corrections we are almost at the end

File size: 13.0 KB
Line 
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\usepackage{subfig}
16\usepackage{tikz}
17\usetikzlibrary{scopes}
18\usetikzlibrary{positioning}
19
20\author{Rick van der Zwet, Universiteit Leiden}
21\title{BDD synthese}
22\author{Rick van der Zwet\\
23 \texttt{<hvdzwet@liacs.nl>}}
24\date{\today}
25
26\begin{document}
27
28\maketitle
29
30\section{Inleiding}
31De hierin besproken inhoud is een samenvatting gemaakt van pagina 86--88 en de
32daarin genoemde opgave 60 en 63 uit het college boek~\cite{DK2009} naar
33aanleiding van het vak Seminar Combinatorial Algorithms 2010~\cite{SCA2010}.
34\begin{figure}[htbp]
35\label{voorbeeldSamenvoegen}
36\begin{tikzpicture}[on grid]
37\tikzstyle{true}=[]
38\tikzstyle{false}=[dashed]
39\tikzstyle{state}=[circle, draw]
40\tikzstyle{leaf}=[rectangle, draw]
41\begin{scope}[xshift=0cm,node distance=10mm and 10mm]
42\node (1) [state]{1};
43\node (2) [state, below=of 1]{2};
44\node (3) [state, below=of 2]{3};
45\node (4) [state, below=of 3]{4};
46\node (F) [leaf, below left=of 4]{$\bot$};
47\node (T) [leaf, below right=of 4]{$\top$};
48\path[-]
49(1) edge[false] (2)
50(1) edge[true, bend left=45] (3)
51(2) edge[false, bend right=45] (F)
52(2) edge[true] (3)
53(3) edge[false] (4)
54(3) edge[true, bend left=45] (T)
55(4) edge[true] (T)
56(4) edge[false] (F)
57;
58\draw[left, inner sep=6mm]
59(1) node {$\alpha$}
60(2) node {$\beta$}
61(3) node {$\gamma$}
62(4) node {$\delta$}
63;
64\end{scope}
65
66\begin{scope}[xshift=9cm,node distance=10mm and 10mm]
67\node (1) [state]{1};
68\node (2-1) [state, below left=of 1]{2};
69\node (2-2) [state, below right=of 1]{2};
70\node (3) [state, below left=of 2-2]{3};
71\node (4-1) [state, below left=of 3]{4};
72\node (4-2) [state, below right=of 3]{4};
73\node (F) [leaf, below=of 4-1]{$\bot$};
74\node (T) [leaf, below=of 4-2]{$\top$};
75\path[-]
76(1) edge[false] (2-1)
77(1) edge[true] (2-2)
78(2-1) edge[false] (3)
79(2-1) edge[true, bend left=70] (T)
80(2-2) edge[false, bend left=45] (T)
81(2-2) edge[true] (3)
82(3) edge[false] (4-1)
83(3) edge[true] (4-2)
84(4-1) edge[false] (T)
85(4-1) edge[false] (F)
86(4-2) edge[false] (T)
87(4-2) edge[true] (F)
88;
89\draw[left, inner sep=4mm]
90(1) node {$\omega$}
91(2-1) node {$\chi$}
92(2-2) node {$\psi$}
93(3) node {$\varphi$}
94(4-1) node {$\tau$}
95(4-2) node {$\upsilon$}
96;
97\end{scope}
98
99\begin{scope}[xshift=5cm,yshift=-5cm, node distance=15mm and 20mm]
100\node (1) [state]{1};
101\node (2-1) [state, below left=of 1]{2};
102\node (2-2) [state, below right=of 1]{2};
103\node (3-1) [state, below left=of 2-1]{3};
104\node (3-2) [state, below left=of 2-2]{3};
105\node (3-3) [state, below right=of 2-2]{3};
106\node (4-1) [state, below left=of 3-1]{4};
107\node (4-2) [state, below=of 3-1]{4};
108\node (4-3) [state, below left=of 3-2]{4};
109\node (4-4) [state, below left=of 3-3]{4};
110\node (4-5) [state, below right=of 3-3]{4};
111\node (FT) [leaf, below=of 4-1]{};
112\node (FF) [leaf, below right=of 4-2]{};
113\node (TT) [leaf, below=of 4-4]{};
114\node (TF) [leaf, below=of 4-5]{};
115\path[-]
116(1) edge[false] (2-1)
117(1) edge[true] (2-2)
118(2-1) edge[false] (3-1)
119(2-1) edge[true] (3-2)
120(2-2) edge[false] (3-2)
121(2-2) edge[true] (3-3)
122(3-1) edge[false] (4-1)
123(3-1) edge[true] (4-2)
124(3-2) edge[false] (4-3)
125(3-2) edge[true,bend left=90] (TT)
126(3-3) edge[false] (4-4)
127(3-3) edge[true] (4-5)
128(4-1) edge[false] (FF)
129(4-1) edge[true] (FT)
130(4-2) edge[false] (FT)
131(4-2) edge[true] (FF)
132(4-3) edge[false] (FT)
133(4-3) edge[true] (TT)
134(4-4) edge[false] (FF)
135(4-4) edge[true] (TT)
136(4-5) edge[false] (TT)
137(4-5) edge[true] (TF)
138;
139\draw[left, inner sep=6mm]
140(1) node {$\alpha \diamond \omega$}
141(2-1) node {$\beta \diamond \chi$}
142(2-2) node {$\gamma \diamond \psi$}
143(3-1) node {$\bot \diamond \varphi$}
144(3-2) node {$\gamma \diamond \top$}
145(3-3) node {$\gamma \diamond \varphi$}
146(4-1) node {$\bot \diamond \tau$}
147(4-2) node {$\bot \diamond \upsilon$}
148(4-3) node {$\delta \diamond \top$}
149(4-4) node {$\delta \diamond \tau$}
150(4-5) node {$\top \diamond \upsilon$}
151(FF) node {$\bot \diamond \bot$}
152(FT) node {$\bot \diamond \top$}
153(TF) node {$\top \diamond \bot$}
154(TT) node {$\top \diamond \top$}
155;
156\end{scope}
157
158\end{tikzpicture}
159\caption{Voorbeeld: twee \emph{BDD}s die samengesmolten worden door gebruik te
160maken van formule~\ref{melt-eq}. Let er wel op dat dit voorbeeld geen
161ontbrekende laag van knopen heeft, waardoor knopen van alle niveaus beschikbaar
162zijn. Op het moment dat de $\diamond$ ingevuld gaat worden is het ook zaak om
163de bladeren (zie vergelijking~\ref{bladeren}) te vereenvoudigen} \end{figure}
164
165\section{Introductie BDD}
166Synthese 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}
168functie $f$ en combineert deze met een andere \emph{BDD} functie $g$
169zodanig dat er een nieuwe \emph{BDD} ontstaat voor een nieuwe functie,
170bijvoorbeeld $f \wedge g$ of $f \oplus g$.
171De reden dat dit zo belangrijk is komt met het feit dat het combineren van
172\emph{BDD}s aan de basis staat van het uitdrukken van complexe systemen door
173middel van gecombineerde simpele functies. In Hoofdstuk~\ref{werking} zal deze
174techniek uitgelegd worden, het zogenoemde \emph{smelten} (\emph{melding}) dat
175in Hoofdstuk~\ref{voorbeeld} toegepast zal worden in een concreet voorbeelden.
176
177\section{Samenvoegen van \emph{BDD}}
178\label{werking}
179De term voor het samenvoegen van \emph{BDD} structuren zullen we smelten
180(\emph{melding}) noemen. Het werkt volgens de volgende principes. Men neme
181twee 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
184bladeren (\emph{sinks}) zijn:
185\begin{equation}
186\label{melt-eq}
187\alpha \diamond \alpha' = \left\{
188\begin{array}{l l}
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'. \\
192\end{array} \right.
193\end{equation}
194
195De oplettende lezer zal zien dan als je Formule~\ref{melt-eq} toepast op de
196bladeren er door samenvoegen van de bladeren ---zie bijvoorbeeld
197Figuur~\ref{voorbeeldSamenvoegen}--- in plaats van de twee bladeren
198$\top$ en $\bot$, er nu vier bladeren mogelijk zijn:
199\begin{equation}
200\label{bladeren}
201\begin{array}{l l l l}
202\bot \diamond \bot, & \bot \diamond \top, & \top \diamond \bot, & \top \diamond \top\\
203\end{array}
204\end{equation}
205Om er weer een ``valide'' \emph{BDD} van te maken zullen deze bladeren vervangen
206worden door het uitgerekende blad. Als bijvoorbeeld de $\diamond$ operatie
207bedoelt is voor een \emph{EN} operatie, wordt de blad-rij in~\ref{bladeren}
208vervangen door de rij $\bot, \bot, \bot, \top$. Nu is het zaak het \emph{BDD}
209te vereenvoudigen, om zo duplicaat-bladeren te snoeien (\emph{pruning}).
210
211De kracht van deze aanpak zit hem in de generieke $\diamond$
212operatie. Het maakt niet uit welke booleaanse operatie er gebruikt wordt aan
213het eind van de rit. De gegeneerde gesmolten \emph{BDD} is geldig voor alle.
214
215Door de \emph{BDD}s achter elkaar te plakken kan met maximaal $B(f)B(g)$ knopen
216een \emph{BDD} voor $f \diamond g$ gerealiseerd worden.
217Hoofdstuk~\ref{voorbeeldPlakken} is hier een voorbeeld van. In het meer algemene
218geval geldt meestal $B(f) + B(g)$ als bovengrens. Deze grenzen worden in
219Hoofdstuk~\ref{voorbeeldSamenvoegen} aangescherpt.
220
221Het smelten ligt aan de basis van de daadwerkelijke synthese. Een simpele
222impementatie kan gemaakt worden met algoritme $R$. (a) Maak eerst een reeks van
223alle knopen $\alpha$ in $f$ en $\alpha'$ in $g$ met knoop $\alpha
224\diamond \alpha'$ in rij $\alpha$ en column $\alpha'$. (b) Vervang de bladeren
225(zie Formule~\ref{bladeren}) door $\bot$ en $\top$, en (c) voer het algoritme
226$R$\footnote{Algoritme $R$ wordt niet in deze samenvatting behandeld; de
227vak-website~\cite[SCA2010] heeft een referentie naar algoritme $R$
228---\url{http://www.liacs.nl/~kosters/semcom/tomb.pdf}--- welke behandeld wordt
229door Tom.} op $f \diamond g$. Op het eerste gezicht lijkt algoritme $R$ er ongeveer
230$B(f)B(g)$ operaties over te doen, maar doordat je onbereikbare knopen niet
231hoeft te evalueren zal je uitkomen op $B(f \diamond g)$.
232
233Deze ``truc'' zorgt ervoor dat de tijd binnen de perken blijft, maar er is dan
234nog niets gezegd over de hoeveelheid geheugen die nodig is. Omdat er nu
235$B(f)B(g)$ knopen in geheugen gehouden moet wordt zal dit problemen opleveren
236bij kleine en grotere bomen. Om deze effici\"{e}ntie aan te pakken is
237algoritme $S$\footnote{Algoritme $S$ wordt niet in deze samenvatting behandeld;
238het boek~\cite[p.~90-92]{DK2009} gaat hier echter uitvoerig op in.} ontworpen.
239
240
241\section{Voorbeelden}
242\label{voorbeeld}
243\subsection{Product groei in synthese van \emph{BDD}}
244\label{voorbeeldSamenvoegen}
245Het volgende voorbeeld is een uitwerking van opgave 60~\cite[p.~130]{DK2009}
246de offi\"{e}le uitwerking is te vinden op \cite[p~.195]{DK2009}
247
248Neem aan dat $f(x_{1},\dots,x_{n})$ en $g(x_{1},\dots,x_{n})$ de respectieve
249\emph{profielen} (\emph{profiles})~\cite[p.~101]{DK2009} $(b_{0},\dots,b_{n})$ en
250$(b'_{0},\dots,b_{n})$ hebben, en de respectieve \emph{quasi-profielen}
251(\emph{quasi-profiles})~\cite[p.~103]{DK2009} $(q_{0},\dots,q_{n})$ en
252$(q'_{0},\dots,q'_{n})$. Om te laten zijn dat de gesmolten $f \diamond g$ het
253aantal knopen $B(f \diamond g) \leq
254\sum^{n}_{j=0}(q_{j}b'_{j}+b_{j}q'_{j}-b_{j}b'_{j})$ bevat moet gekeken worden
255naar het aantal \emph{beads}~\cite[p.~72]{DK2009} dat mogelijkerwijs gemaakt
256kan worden van de functies $f$ en $g$.
257
258Hierbij geldt dan voor een willikeurige functie $n$ met als profiel
259$(b_{0},\dots,b_{n})$ en quasi-profiel $(q_{0},\dots,q_{n})$ dat
260$B(q_{0},\dots,q_{n}) \geq B(b_{0},\dots,b_{n})$. En tevens dan
261$(b_{0},\dots,b_{n}) \subseteq (q_{0},\dots,q_{n})$. Hieruit volgt dat een
262geen-bead zich bevindt in $(q_{0},\dots,q_{n}) \setminus (b_{0},\dots,b_{n})$.
263
264Elke bead \beta van de orde $n - j$ in het geordende paar $(f,g)$ zal zich
265bevinden in een van de volgende groepen; (a) de standaard-combinatie van de
266$b_{j}b_{j}'$ geordende beats van $(f,g)$ of (b) de gegenereerde reeks van een
267(bead,geen-bead) of (geen-bead, bead) $b_{j}(q_{j}' - b_{j}') + (q_{j} -
268b{j})b_{j}'$.
269
270Dit bij elkaar optellen levert op $b_{j}b_{j}' + b_{j}(q_{j}' - b_{j}') +
271(q_{j} - b{j})b_{j}'$. Vereenvoudigen en de sommering is oefening voor de
272lezer.
273
274\subsection{Som groei in synthese van \emph{BDD}}
275\label{voorbeeldPlakken}
276Het volgende voorbeeld is een uitwerking van opgave 63~\cite[pg. 131]{DK2009}
277de offi\"{e}le uitwerking is te vinden op pagina 195~\cite{DK2009}
278
279Laat $f(x_{1},\dots,x_{n}) = M_{m}(x_{1} \oplus x_{2},x_{3} \oplus
280x_{4},\dots,x_{2m-1} \oplus x_{2m};x_{2m+1},\dots,x_{n})$ en $g(x_{1},\dots,x_{n}) =
281M_{m}(x_{2} \oplus x_{3},\dots,x_{2m-2} \oplus x_{2m-1},x_{2m};\overline
282x_{2m+1},\dots,\overline x_{n})$ waar $n = 2m + 2^{m}$.
283
284Dan is $B(f) = 2^{m+2}-1 \approx 4n$, $B(g) = 2^{m+1}-2^{m} \approx 3n$ en $B(g
285\land f) = 2^{m+1}+2^{m-1}-1 \approx 2n^{2}$. Om aan deze 'magische' reeksen te
286komen is het belangrijk eerst naar de profielen te kijken van $f$ en $g$ om
287daarna met sommering van deze tot de antwoorden te komen. Als eerste moet
288opgemerkt worden dan zoals $f$ als $g$ $2^m$-weg
289multiplexers~\cite[7.1.2-(31)]{DK2009-0} zijn voor welke de profielen zijn
290$(1,2,2,\dots,2^{m-1},2^{m-1},2^m,1,1,\dots,1.2)$ respectievelijk
291$(0,1,2,2,\dots,2^{m-1},2^{m-1},1,1,\dots,1,2$. Dit optellen en afschatten wordt
292(zie ook~\cite[pg 82]{DK2009}) $B(f) = 2^{m+2} - 1 \approx 4n$ en $B(g) =
2932^{m+1} - 1 \approx 3n$ \\
294\\
295$B(f \land g)$ wordt aanzienlijk moeilijker. Zie dat er unieke oplossing
296bestaat -de oplossing kan aan een uniek getal gekoppeld worden- door $x_1 \dots
297x_{2m}$ als je $((x_1 \oplus x_2)(x_3 \oplus x_4) \dots (x_{2m-1} \oplus
298x_{2m}))_{2} = p,((x_2 \oplus x_3) \dots (x_{2m-2} \oplus x_{2m-1})x_{2m})_{2}
299= q$. waar $0 \leq p, q \le 2^m$ en $p=q$ dan en slechts als $x_1 = x_3 = \dots
300= 2_{2m-1} = 0$. Dit zorgt dat het eerste deel -het stuk voor de punt
301komma- van het profiel van $f \land g$ geschreven kan worden als $(1, 2, 4,\dots,
3022^{2m-2}, 2^{2m-1} - 2^{m-1}$.
303Het tweede deel is aanzienlijk moeilijker, welke bestaat uit de sub-functies
304$x_{2m+j} \land \overline x_{2m+k}$ of $\overline x_{2m+j} \land x_{2m+k}$ voor
305$1 \leq j \le k \leq 2^m$ tezamen met de originelen $x_{2m+j}$ en $\overline
306x_{2m+j}$ voor $2 \leq j \leq 2^m$. Welke het profiel oplevert van $(2^{m+1}-2,
3072^{m+1}-2, 2^{m+1}-4, 2^{m+1}-6, \dots, 4, 2, 2)$.
308Beiden profielen bij elkaar levert op $B(f \land g) = 2^{2m+1} + 2^{m-1} -1 \approx 2n^2$
309
310
311
312
313
314\begin{thebibliography}{}
315\bibitem[DK2009]{DK2009} D.E. Knuth. Bitwise Tricks \& Techniques; Binary
316Decision Diagrams, volume 4, Fascicle 1, of The Art of Computer Programming.
317Pearson Education, first edition, 2009.
318\bibitem[DK2009-Fas0]{DK2009-0} D.E. Knuth. Bitwise Tricks \& Techniques;
319Binary Decision Diagrams, volume 4, Fascicle 0, of The Art of Computer
320Programming. Pearson Education, first edition, 2009.
321\bibitem[SCA2010]{SCA2010} Lecture Seminar Combinatorial Algorithms,
322\url{http://www.liacs.nl/~kosters/semcom/}, W.A. (Walter) Kosters, LIACS,
323Spring 2010.
324
325\end{thebibliography}
326\end{document}
Note: See TracBrowser for help on using the repository browser.