- Timestamp:
- Jul 27, 2010, 1:27:34 PM (14 years ago)
- Location:
- liacs/SCA2010/BDD
- Files:
-
- 1 added
- 1 edited
-
report.pdf (added)
-
report.tex (modified) (10 diffs)
Legend:
- Unmodified
- Added
- Removed
-
liacs/SCA2010/BDD/report.tex
r166 r167 18 18 \usetikzlibrary{positioning} 19 19 20 \newcommand*\circled[1]{% 21 \tikz[baseline=(C.base)]\node[draw,circle,inner sep=0.5pt](C) {$#1$};\! 22 } 23 \newcommand*\squared[1]{% 24 \tikz[baseline=(C.base)]\node[draw,rectangle,rounded corners,inner sep=0.5pt](C) {$#1$};\! 25 } 26 \newcommand*\BDD{\emph{BDD}} 27 \newcommand*\BDDs{\emph{BDDs}} 28 20 29 \author{Rick van der Zwet, Universiteit Leiden} 21 30 \title{BDD synthese} … … 33 42 aanleiding van het vak Seminar Combinatorial Algorithms 2010~\cite{SCA2010}. 34 43 \begin{figure}[htbp] 35 \label{voorbeeldSamenvoegen}36 44 \begin{tikzpicture}[on grid] 37 45 \tikzstyle{true}=[] … … 157 165 158 166 \end{tikzpicture} 159 \caption{Voorbeeld: twee \ emph{BDD}s die samengesmolten worden door gebruik te167 \caption{Voorbeeld: twee \BDDs die samengesmolten worden door gebruik te 160 168 maken van formule~\ref{melt-eq}. Let er wel op dat dit voorbeeld geen 161 169 ontbrekende laag van knopen heeft, waardoor knopen van alle niveaus beschikbaar … … 164 172 165 173 \section{Introductie BDD} 166 Synthese van een Binary Decision Diagram \ emph{BDD}is een belangrijk167 \ 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,174 Synthese van een Binary Decision Diagram \BDD is een belangrijk 175 \BDD algoritme~\cite[p.~86]{DK2009}. Het neemt in essentie een \BDD 176 functie $f$ en combineert deze met een andere \BDD functie $g$ 177 zodanig dat er een nieuwe \BDD ontstaat voor een nieuwe functie, 170 178 bijvoorbeeld $f \wedge g$ of $f \oplus g$. 171 179 De 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 door180 \BDDs aan de basis staat van het uitdrukken van complexe systemen door 173 181 middel van gecombineerde simpele functies. In Hoofdstuk~\ref{werking} zal deze 174 182 techniek uitgelegd worden, het zogenoemde \emph{smelten} (\emph{melding}) dat 175 183 in Hoofdstuk~\ref{voorbeeld} toegepast zal worden in een concreet voorbeelden. 176 184 177 \section{Samenvoegen van \ emph{BDD}}185 \section{Samenvoegen van \BDD} 178 186 \label{werking} 179 De term voor het samenvoegen van \ emph{BDD}structuren zullen we smelten187 De term voor het samenvoegen van \BDD structuren zullen we smelten 180 188 (\emph{melding}) noemen. Het werkt volgens de volgende principes. Men neme 181 189 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 196 204 bladeren er door samenvoegen van de bladeren ---zie bijvoorbeeld 197 Figuur~\ref{voorbeeldSamenvoegen}--- in plaats van de twee bladeren205 voorbeeld in Hoofstuk~\ref{voorbeeldSamenvoegen}--- in plaats van de twee bladeren 198 206 $\top$ en $\bot$, er nu vier bladeren mogelijk zijn: 199 207 \begin{equation} … … 203 211 \end{array} 204 212 \end{equation} 205 Om er weer een ``valide'' \ emph{BDD}van te maken zullen deze bladeren vervangen213 Om er weer een ``valide'' \BDD van te maken zullen deze bladeren vervangen 206 214 worden door het uitgerekende blad. Als bijvoorbeeld de $\diamond$ operatie 207 215 bedoelt is voor een \emph{EN} operatie, wordt de blad-rij in~\ref{bladeren} 208 vervangen door de rij $\bot, \bot, \bot, \top$. Nu is het zaak het \ emph{BDD}216 vervangen door de rij $\bot, \bot, \bot, \top$. Nu is het zaak het \BDD 209 217 te vereenvoudigen, om zo duplicaat-bladeren te snoeien (\emph{pruning}). 210 218 211 219 De kracht van deze aanpak zit hem in de generieke $\diamond$ 212 220 operatie. Het maakt niet uit welke booleaanse operatie er gebruikt wordt aan 213 het eind van de rit. De gegeneerde gesmolten \ emph{BDD}is geldig voor alle.214 215 Door de \ emph{BDD}s achter elkaar te plakken kan met maximaal $B(f)B(g)$ knopen216 een \ emph{BDD}voor $f \diamond g$ gerealiseerd worden.221 het eind van de rit. De gegeneerde gesmolten \BDD is geldig voor alle. 222 223 Door de \BDDs achter elkaar te plakken kan met maximaal $B(f)B(g)$ knopen 224 een \BDD voor $f \diamond g$ gerealiseerd worden. 217 225 Hoofdstuk~\ref{voorbeeldPlakken} is hier een voorbeeld van. In het meer algemene 218 226 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 226 234 $R$\footnote{Algoritme $R$ wordt niet in deze samenvatting behandeld; de 227 vak-website~\cite [SCA2010]heeft een referentie naar algoritme $R$228 ---\url{http://www.liacs.nl/~kosters/semcom/tomb.pdf}---welke behandeld wordt235 vak-website~\cite{SCA2010} heeft een referentie naar algoritme $R$ 236 \url{http://www.liacs.nl/~kosters/semcom/tomb.pdf} welke behandeld wordt 229 237 door Tom.} op $f \diamond g$. Op het eerste gezicht lijkt algoritme $R$ er ongeveer 230 238 $B(f)B(g)$ operaties over te doen, maar doordat je onbereikbare knopen niet … … 241 249 \section{Voorbeelden} 242 250 \label{voorbeeld} 243 \subsection{Product-groei in synthese van \ emph{BDD}}251 \subsection{Product-groei in synthese van \BDD} 244 252 \label{voorbeeldSamenvoegen} 245 253 Het volgende voorbeeld is een uitwerking van opgave 60~\cite[p.~130]{DK2009} 246 254 de offi\"{e}le uitwerking is te vinden op \cite[p~.195]{DK2009} 247 255 \\ \\ 256 Voorgaande aan de uitwerking is het belangrijk te weten wat een \emph{QDD} (aka 257 \emph{quasi-BDD}~\cite[p.~102-103]{DK2009}) is. Elke functie heeft een unieke 258 \emph{QDD} welke lijkt op een \BDD echter is de start-knoop altijd 259 \circled{1} en elke \circled{k} knoop bestaat for $k < n$ takken naar twee 260 \squared{k+1} knopen. Wat in het kort wilt zeggen dat elk pad van de 261 start-knoop naar de bladeren een lengte heeft van $n$. Om dat mogelijk te maken 262 mogen de \emph{HOOG} en \emph{LAAG} takken van een \emph{QDD} gelijk zijn. Let 263 wel op dat reductie toegepast moet worden. 264 \\ \\ 248 265 Neem aan dat $f(x_{1},\dots,x_{n})$ en $g(x_{1},\dots,x_{n})$ de respectieve 249 266 \emph{profielen} (\emph{profiles})~\cite[p.~101]{DK2009} 250 $(b_{0},\dots,b_{n})$ \footnote{Waar er $b_{k}$knopen zijn die splitsen251 op variable $f(x_{k+1})$ en $b_{n}$ het aantal bladeren is .}en267 $(b_{0},\dots,b_{n})$ ---waar $b_{k}$ met $0 \le k < n$ de knopen zijn die splitsen 268 op variable $f(x_{k+1})$ en $b_{n}$ het aantal bladeren is--- en 252 269 $(b'_{0},\dots,b_{n})$ hebben, en de respectieve \emph{quasi-profielen} 253 270 (\emph{quasi-profiles})~\cite[p.~103]{DK2009} 254 $(q_{0},\dots,q_{n})$\footnote{Waar $q_{k-1}$ het aantal \circle{k} knopen in 255 de \emph{QDD} is.} en $(q'_{0},\dots,q'_{n})$. 256 257 Om te laten zijn dat de gesmolten $f \diamond g$ het aantal knopen $B(f 258 \diamond g) \leq \sum^{n}_{j=0}(q_{j}b'_{j}+b_{j}q'_{j}-b_{j}b'_{j})$ bevat 259 moet gekeken worden naar het aantal \emph{beads}~\cite[p.~72]{DK2009} dat 271 $(q_{0},\dots,q_{n})$ ---waar $q_{k-1}$ met $0 < k < n$ het aantal \circled{k} knopen in 272 de \emph{QDD} van $f$ is--- en $(q'_{0},\dots,q'_{n})$. 273 274 Om te laten zijn dat de gesmolten $f \diamond g$ het aantal knopen 275 \begin{equation} 276 \label{eq:knopen} 277 B(f \diamond g) \leq \sum^{n}_{j=0}(q_{j}b'_{j}+b_{j}q'_{j}-b_{j}b'_{j}) 278 \end{equation} 279 bevat moet gekeken worden naar het aantal \emph{beads}~\cite[p.~72]{DK2009} dat 260 280 mogelijkerwijs gemaakt kan worden van de functies $f$ en $g$. 261 262 Hierbij geldt dan voor een willikeurige functie $n$ met als profiel 263 $(b_{0},\dots,b_{n})$ en quasi-profiel $(q_{0},\dots,q_{n})$ dat 264 $B(q_{0},\dots,q_{n}) \geq B(b_{0},\dots,b_{n})$. En tevens dan 265 $(b_{0},\dots,b_{n}) \subseteq (q_{0},\dots,q_{n})$. Hieruit volgt dat een 266 geen-bead zich bevindt in $(q_{0},\dots,q_{n}) \setminus (b_{0},\dots,b_{n})$. 267 268 Elke bead \beta van de orde $n - j$ in het geordende paar $(f,g)$ zal zich 281 Voor een willikeurige functie $n$ met als profiel $(b_{0},\dots,b_{n})$ en 282 quasi-profiel $(q_{0},\dots,q_{n})$ geldt dat $B(q_{0},\dots,q_{n}) \geq 283 B(b_{0},\dots,b_{n})$. En tevens dan $(b_{0},\dots,b_{n}) \subseteq 284 (q_{0},\dots,q_{n})$. Hieruit volgt dat een geen-bead zich bevindt in 285 $(q_{0},\dots,q_{n}) - (b_{0},\dots,b_{n})$. 286 287 Elke bead van de orde $n - j$ in het geordende paar $(f,g)$ zal zich 269 288 bevinden in een van de volgende groepen; (a) de standaard-combinatie van de 270 289 $b_{j}b_{j}'$ geordende beats van $(f,g)$ of (b) de gegenereerde reeks van een … … 276 295 lezer. 277 296 278 \subsection{Som-groei in synthese van \ emph{BDD}}297 \subsection{Som-groei in synthese van \BDD} 279 298 \label{voorbeeldPlakken} 280 299 Het volgende voorbeeld is een uitwerking van opgave 63~\cite[p.~131]{DK2009} … … 282 301 283 302 \begin{equation} 284 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}) \\ 285 en \\ 286 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} 287 \caption{\oplus is de binary operator \emph{XOR}} 303 \begin{array}{lcl} 304 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}) \\ 305 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}) \\ 306 \end{array} 307 \label{eq:opgave63} 288 308 \end{equation} 309 In Vergelijking~\ref{eq:opgave63} zijn $f$ en $g$ gedefinieerd, waarbij $\oplus$ 310 de binary operator \emph{XOR} is en $n = 2m + 2^{m}$. 289 311 290 312 Dan is $B(f) = 2^{m+2}-1 \approx 4n$, $B(g) = 2^{m+1}-2^{m} \approx 3n$ en $B(g
Note:
See TracChangeset
for help on using the changeset viewer.
