% % $Id: report.tex 571 2008-04-20 17:31:04Z rick $ % \documentclass[12pt,a4paper]{article} \frenchspacing \usepackage[english,dutch]{babel} \selectlanguage{dutch} \usepackage{graphicx} \usepackage{url} \usepackage{multicol} \usepackage{fancybox} \usepackage{amssymb,amsmath} \usepackage{subfig} \usepackage{tikz} \usetikzlibrary{scopes} \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} \author{Rick van der Zwet\\ \texttt{}} \date{\today} \begin{document} \maketitle \section{Inleiding} De hierin besproken inhoud is een samenvatting gemaakt van pagina 86--88 en de daarin genoemde opgave 60 en 63 uit het college boek~\cite{DK2009} naar aanleiding van het vak Seminar Combinatorial Algorithms 2010~\cite{SCA2010}. \begin{figure}[htbp] \caption{fig:samenvoegen} \begin{tikzpicture}[on grid] \tikzstyle{true}=[] \tikzstyle{false}=[dashed] \tikzstyle{state}=[circle, draw] \tikzstyle{leaf}=[rectangle, draw] \begin{scope}[xshift=0cm,node distance=10mm and 10mm] \node (1) [state]{1}; \node (2) [state, below=of 1]{2}; \node (3) [state, below=of 2]{3}; \node (4) [state, below=of 3]{4}; \node (F) [leaf, below left=of 4]{$\bot$}; \node (T) [leaf, below right=of 4]{$\top$}; \path[-] (1) edge[false] (2) (1) edge[true, bend left=45] (3) (2) edge[false, bend right=45] (F) (2) edge[true] (3) (3) edge[false] (4) (3) edge[true, bend left=45] (T) (4) edge[true] (T) (4) edge[false] (F) ; \draw[left, inner sep=6mm] (1) node {$\alpha$} (2) node {$\beta$} (3) node {$\gamma$} (4) node {$\delta$} ; \end{scope} \begin{scope}[xshift=9cm,node distance=10mm and 10mm] \node (1) [state]{1}; \node (2-1) [state, below left=of 1]{2}; \node (2-2) [state, below right=of 1]{2}; \node (3) [state, below left=of 2-2]{3}; \node (4-1) [state, below left=of 3]{4}; \node (4-2) [state, below right=of 3]{4}; \node (F) [leaf, below=of 4-1]{$\bot$}; \node (T) [leaf, below=of 4-2]{$\top$}; \path[-] (1) edge[false] (2-1) (1) edge[true] (2-2) (2-1) edge[false] (3) (2-1) edge[true, bend left=70] (T) (2-2) edge[false, bend left=45] (T) (2-2) edge[true] (3) (3) edge[false] (4-1) (3) edge[true] (4-2) (4-1) edge[false] (T) (4-1) edge[false] (F) (4-2) edge[false] (T) (4-2) edge[true] (F) ; \draw[left, inner sep=4mm] (1) node {$\omega$} (2-1) node {$\chi$} (2-2) node {$\psi$} (3) node {$\varphi$} (4-1) node {$\tau$} (4-2) node {$\upsilon$} ; \end{scope} \begin{scope}[xshift=5cm,yshift=-5cm, node distance=15mm and 20mm] \node (1) [state]{1}; \node (2-1) [state, below left=of 1]{2}; \node (2-2) [state, below right=of 1]{2}; \node (3-1) [state, below left=of 2-1]{3}; \node (3-2) [state, below left=of 2-2]{3}; \node (3-3) [state, below right=of 2-2]{3}; \node (4-1) [state, below left=of 3-1]{4}; \node (4-2) [state, below=of 3-1]{4}; \node (4-3) [state, below left=of 3-2]{4}; \node (4-4) [state, below left=of 3-3]{4}; \node (4-5) [state, below right=of 3-3]{4}; \node (FT) [leaf, below=of 4-1]{}; \node (FF) [leaf, below right=of 4-2]{}; \node (TT) [leaf, below=of 4-4]{}; \node (TF) [leaf, below=of 4-5]{}; \path[-] (1) edge[false] (2-1) (1) edge[true] (2-2) (2-1) edge[false] (3-1) (2-1) edge[true] (3-2) (2-2) edge[false] (3-2) (2-2) edge[true] (3-3) (3-1) edge[false] (4-1) (3-1) edge[true] (4-2) (3-2) edge[false] (4-3) (3-2) edge[true,bend left=90] (TT) (3-3) edge[false] (4-4) (3-3) edge[true] (4-5) (4-1) edge[false] (FF) (4-1) edge[true] (FT) (4-2) edge[false] (FT) (4-2) edge[true] (FF) (4-3) edge[false] (FT) (4-3) edge[true] (TT) (4-4) edge[false] (FF) (4-4) edge[true] (TT) (4-5) edge[false] (TT) (4-5) edge[true] (TF) ; \draw[left, inner sep=6mm] (1) node {$\alpha \diamond \omega$} (2-1) node {$\beta \diamond \chi$} (2-2) node {$\gamma \diamond \psi$} (3-1) node {$\bot \diamond \varphi$} (3-2) node {$\gamma \diamond \top$} (3-3) node {$\gamma \diamond \varphi$} (4-1) node {$\bot \diamond \tau$} (4-2) node {$\bot \diamond \upsilon$} (4-3) node {$\delta \diamond \top$} (4-4) node {$\delta \diamond \tau$} (4-5) node {$\top \diamond \upsilon$} (FF) node {$\bot \diamond \bot$} (FT) node {$\bot \diamond \top$} (TF) node {$\top \diamond \bot$} (TT) node {$\top \diamond \top$} ; \end{scope} \end{tikzpicture} \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 zijn. Op het moment dat de $\diamond$ ingevuld gaat worden is het ook zaak om de bladeren (zie vergelijking~\ref{bladeren}) te vereenvoudigen.} \end{figure} \section{Introductie BDD} 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 \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 voorbeelden. \section{Samenvoegen van \BDD} \label{werking} De term voor het samenvoegen van \BDD structuren zullen we \emph{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 \diamond \alpha'$, het resultaat van de \emph{smelt} actie, de ``\emph{emulsie}'' (\emph{meld}) van $\alpha$ en $\alpha'$, is dan als volgt gedefinieerd als $\alpha$ en $\alpha'$ niet beide bladeren (\emph{sinks}) zijn: \begin{equation} \label{melt-eq} \alpha \diamond \alpha' = \left\{ \begin{array}{l l} (v, l \diamond l', h \diamond h'), & \mathrm{als~} v = v'; \\ (v, l \diamond \alpha', h \diamond \alpha'), & \mathrm{als~} v < v'; \\ (v', \alpha \diamond l', \alpha \diamond h'), & \mathrm{als~} v > v'. \\ \end{array} \right. \end{equation} Als we deze recursieve formule gebruiken op de wortels van twee \BDDs $f$ en $g$, vinden we een diagram dat het paar $(f,g)$ representeert. De oplettende lezer zal zien dan als je Formule~\ref{melt-eq} toepast op de bladeren er door samenvoegen van de bladeren ---zie bijvoorbeeld voorbeeld in Figuur~\ref{fig:samenvoegen}--- in plaats van de twee bladeren $\top$ en $\bot$, er nu vier bladeren mogelijk zijn: \begin{equation} \label{bladeren} \begin{array}{l l l l} \bot \diamond \bot, & \bot \diamond \top, & \top \diamond \bot, & \top \diamond \top\\ \end{array} \end{equation} 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 \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 \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 Hoofdstuk~\ref{voorbeeldSamenvoegen} aangescherpt. Het smelten ligt aan de basis van de daadwerkelijke synthese. Een simpele impementatie kan gemaakt worden met algoritme $R$. (a) Maak eerst een reeks van alle knopen $\alpha$ in $f$ en $\alpha'$ in $g$ met knoop $\alpha \diamond \alpha'$ in rij $\alpha$ en column $\alpha'$. (b) Vervang de bladeren (zie Formule~\ref{bladeren}) door $\bot$ en $\top$, en (c) voer het algoritme $R$\footnote{Algoritme $R$ wordt niet in deze samenvatting behandeld; zie de vak-website~\cite{SCA2010} waar het algoritme $R$ 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 hoeft te evalueren zal je uitkomen op $B(f \diamond g)$. Deze ``truc'' zorgt ervoor dat de tijd binnen de perken blijft, maar er is dan nog niets gezegd over de hoeveelheid geheugen die nodig is. Omdat er nu $B(f)B(g)$ knopen in geheugen gehouden moet wordt zal dit problemen opleveren bij kleine en grotere bomen. Om deze effici\"{e}ntie aan te pakken is algoritme $S$\footnote{Algoritme $S$ wordt niet in deze samenvatting behandeld; het boek~\cite[p.~90-92]{DK2009} gaat hier echter uitvoerig op in.} ontworpen. \section{Voorbeelden} \label{voorbeeld} \subsection{Product-groei in synthese van \BDD} \label{voorbeeldSamenvoegen} Het volgende voorbeeld is een uitwerking van opgave 60~\cite[p.~130]{DK2009} de offici\"{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 heeft (voor $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 op tweetallen knopen waarvan de \emph{HOOG} en \emph{LAAG} pointers gelijk zijn. \\ \\ 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})$ ---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})$ ---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 zien 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$. Voor een willekeurige functie $f$ met als profiel $(b_{0},\dots,b_{n})$ en quasi-profiel $(q_{0},\dots,q_{n})$ geldt dat $B(b_{0},\dots,b_{n}) \leq B(q_{0},\dots,q_{n})$. En tevens dan $(b_{0},\dots,b_{n}) \subseteq (q_{0},\dots,q_{n})$. Hieruit volgt dat een niet-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 beads van $(f,g)$ of (b) de gegenereerde reeks van een (bead,niet-bead) of (niet-bead, bead) $b_{j}(q_{j}' - b_{j}') + (q_{j} - b{j})b_{j}'$. Dit bij elkaar optellen levert op $b_{j}b_{j}' + b_{j}(q_{j}' - b_{j}') + (q_{j} - b{j})b_{j}'$. Vereenvoudigen en de sommering is oefening voor de lezer. \subsection{Som-groei in synthese van \BDD} \label{voorbeeldPlakken} Het volgende voorbeeld is een uitwerking van opgave 63~\cite[p.~131]{DK2009} de offici\"{e}le uitwerking is te vinden op \cite[p.~195]{DK2009}. De $2^{m}$-weg multiplexer $M_{m}(y_{1},\dots,y_{m};y_{m+1},\dots,y_{m+2^{m}})$ geeft bij input $y_{1},\dots,y_{m}$ de waarde van variable $y_{m+k}$ waarbij $k$ het getal is gerepresenteerd door $y_{1},\dots,y_{m}$, zie~\cite[7.1.2-(31)]{DK2009-0}. Hiermee defineren we $\oplus$ de binary operator \emph{XOR} en $n = 2m + 2^{m}$. \begin{equation} \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} Dan is $B(f) = 2^{m+2}-1 \approx 4n$, $B(g) = 2^{m+1}-2^{m} \approx 3n$ en $B(g \land f) = 2^{m+1}+2^{m-1}-1 \approx 2n^{2}$. Om aan deze reeksen te komen is het belangrijk eerst naar de profielen te kijken van $f$ en $g$ om daarna met sommering van deze tot de antwoorden te komen. Als eerste moet opgemerkt worden dat zowel $f$ als $g$ $2^m$-weg multiplexers zijn voor welke de profielen zijn $(1,2,2,\dots,2^{m-1},2^{m-1},2^m,1,1,\dots,1,2)$ respectievelijk \\ $(0,1,2,2,\dots,2^{m-1},2^{m-1},1,1,\dots,1,2)$. Dit optellen en afschatten wordt (zie ook~\cite[p.~82]{DK2009}) $B(f) = 2^{m+2} - 1 \approx 4n$ en $B(g) = 2^{m+1} - 1 \approx 3n$. \\ \\ De bereking $B(f \land g)$ (de werking van de multiplexer) wordt aanzienlijk moeilijker en zal daarom aangestipt worden. We constateren eerst dat er een unieke oplossing bestaat ---de oplossing kan aan een uniek getal gekoppeld worden namelijk de invoer--- in de vorm van $x_1 \dots x_{2m}$ als je $((x_1 \oplus x_2)(x_3 \oplus x_4) \dots (x_{2m-1} \oplus x_{2m}))_{2} = p,((x_2 \oplus x_3) \dots (x_{2m-2} \oplus x_{2m-1})x_{2m})_{2} = q$, waar $0 \leq p, q \le 2^m$ en $p=q$ dan en slechts als $x_1 = x_3 = \dots = x_{2m-1} = 0$. Dit zorgt dat het eerste deel ---het stuk voor de punt komma--- van het profiel van $f \land g$ geschreven kan worden als $(1, 2, 4,\dots, 2^{2m-2}, 2^{2m-1} - 2^{m-1})$. Het tweede deel is aanzienlijk moeilijker, het bestaat uit de sub-functies $x_{2m+j} \land \overline x_{2m+k}$ of $\overline x_{2m+j} \land x_{2m+k}$ voor $1 \leq j \le k \leq 2^m$ tezamen met de originelen $x_{2m+j}$ en $\overline x_{2m+j}$ voor $2 \leq j \leq 2^m$. Dat levert het profiel $(2^{m+1}-2, 2^{m+1}-2, 2^{m+1}-4, 2^{m+1}-6, \dots, 4, 2, 2)$ op. Beide profielen bij elkaar optellen levert op $B(f \land g) = 2^{2m+1} + 2^{m-1} -1 \approx 2n^2$. \begin{thebibliography}{} \bibitem[DK2009]{DK2009} D.E. Knuth. Bitwise Tricks \& Techniques; Binary Decision Diagrams, volume 4, Fascicle 1, of The Art of Computer Programming. Pearson Education, first edition, 2009. \bibitem[DK2009-Fas0]{DK2009-0} D.E. Knuth. Bitwise Tricks \& Techniques; Binary Decision Diagrams, volume 4, Fascicle 0, of The Art of Computer Programming. Pearson Education, first edition, 2009. \bibitem[SCA2010]{SCA2010} Lecture Seminar Combinatorial Algorithms, \url{http://www.liacs.nl/~kosters/semcom/}, W.A. (Walter) Kosters, LIACS, Spring 2010. \end{thebibliography} \end{document}