% % $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} \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} na aanleiding van het vak Seminar Combinatorial Algorithms 2010~\cite{SCA2010}. \begin{figure}[htbp] \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 \emph{BDD}s die samengesmolten worden door gebruik te maken van formule~\ref{melt-eq}. Let wel op dat dit voorbeeld geen ontbrekende laag van nodes heeft, waardoor nodes 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 \emph{BDD} is het belangrijke \emph{BDD} algoritme~\cite[pg 86]{DK2009}. Welke in essentie een \emph{BDD} functie,$f$, pakt en deze combineert met een andere \emph{BDD} functie,$g$, zodanig dat er een nieuwe \emph{BDD} ontstaat voor de 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 \emph{BDD}s aan de basis staat aan het uitdrukken van complexe systemen dmv van gecombineerde simpele functies. In sectie~\ref{werking} zal deze techniek uitgelegd worden, het zogenoemde \emph{smelten} (\emph{melding}) welke in sectie~\ref{voorbeeld} dit toegepast zal worden in een concreet voorbeelden. \section{Samenvoegen van \emph{BDD}} \label{werking} De term voor het samenvoegen \emph{BDD} structuren zullen we smelten (\emph{melding}) noemen. Er werkt volgens de volgende principes. Men neme $\alpha = (v,l,h)"$ en $\alpha' = (v',l',h')$. De $\alpha \diamond \alpha'$, de "\emph{emulsie}" (\emph{meld}) van $\alpha$ en $\alpha'$, is dan als volgt gedefinieerd als $\alpha$ ad $\alpha'$ niet beiden 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} De oplettende lezer (voor de rest, voorbeeld figuur~\ref{voorbeeldSamenvoegen}) zal zien dat je door het samenvoegen van de bladeren er 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' \emph{BDD} van te maken zullen deze bladeren vervangen worden door het uitgerekende blad. Als bijvoorbeeld de $\diamond$ operatie een $EN$ operatie was, wordt de blad-rij in~\ref{bladeren} vervangen door de rij $\bot, \bot, \bot, \top$. Nu is het zaak de \emph{BDD} te vereenvoudigen, om zo duplicaat bladeren te snoeien (\emph{pruning}). De kracht van deze aanpak zit hem in de zogenoemde generieke $\diamond$ operatie. Het maakt niet uit welke booleaanse operatie er gebruikt wordt aan het eind van de rit. De gegeneerde gesmolten \emph{BDD} is geldig voor allen. Kijkend naar de limieten moet geoordeeld worden kan hetzelfde altijd bereikt worden door in het slechte geval de \emph{BDD}s achter elkaar te plakken welke dan in dit geval $B(f)B(g)$ knopen oplevert. Voorbeeld~\ref{voorbeeldPlakken} is hier een geval van. In het meer algemene geval geldt meestal $B(f) + B(g)$. Deze grenzen worden in voorbeeld~\ref{voorbeeldSamenvoegen} aangescherpt. Het smelten ligt aan de basis van de daadwerkelijke synthese. Een simpele variant kan gemaakt worden met algoritme $R$. Maak eerst een reeks van alle knopen $\alpha$ in $B(f)$ en $\alpha'$ in $B(g)$ met knoop $\alpha \diamond \alpha'$ in rij $\alpha$ en column $\alpha'$. Vervang de bladeren (\ref{bladeren}) door $\bot$ en $\top$. En voor algoritme $R$ uit op $f \diamond g$. Op het eerste gezicht lijkt algoritme $R$ er ongeveer $B(f)B(g)$ 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 er nodig is. Omdat er nu $B(f)B(g)$ knopen in geheugen gehouden moet wordt zal dit problemen opleveren bij kleine en grotere algoritmen. Om deze efficiƫntie aan te pakken is algoritme $S$ \footnote{Algoritme $S$ wordt niet in deze samenvatting gehandeld de vak-website~\cite{SCA2010} heeft een verwijzing van de samenvatting van dit algoritme} ontworpen. \section{Voorbeelden} \label{voorbeeld} \subsection{Product groei in synthese van \emph{BDD}} \label{voorbeeldSamenvoegen} Het volgende voorbeeld is een uitwerking van opgave 60~\cite[pg. 130]{DK2009} de offi\"{e}le uitwerking is te vinden op pagina 195~\cite{DK2009} Neem aan dat $f(x_{1},dots,x_{n})$ en $g(x_{1},dots,x_{n})$ de respectieve \emph{profielen} (\emph{profiles})~\cite[pg 101]{DK2009} $(b_{0},dots,b_{n})$ en $(b'_{0},dots,b_{n})$ hebben. En de respectieve \emph{quasi-profielen} (\emph{quasi-profiles})~\cite[pg 103]{DK2009} $(q_{0},dots,q_{n})$ en $(q'_{0},dots,q'_{n})$. Om te laten zijn dat de gesmolten $f \diamond g$ het aantal knopen van $B(f \diamond g) \leq \sum^{n}_{j=0}(q_{j}b'_{j}+b_{j}q'_{j}-b_{j}b'_{j})$ bevat moet gekeken worden aan het aantal \emph{beads}~\cite[pg 72]{DK2009} dat mogelijkerwijs gemaakt kunnen worden van de functies $f$ en $g$. Elke bead van de orde $n - j$ van het geordende paar $(f,g)$ zal binnen de standaard combinatie vallen de $b_{j}b_{j}'$ geordende beats van $(f,g)$. vallen of is er eentje uit een meer speciaal gegenereerde reeks van een (bead,geen-bead) of (geen-bead, bead) $b_{j}(q_{j}' - b_{j}') + (q_{j} - b{j})b_{j}'$. Zie hierbij dat van een functie het $B(quasi-profiel) \geq B(profiel)$. En dat alle in het profiel altijd in het quasi-profiel zit. Er dus de geen-bead kan beschrijven als de rest van de quasi-profiel minus profiel. 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 \emph{BDD}} \label{voorbeeldPlakken} Het volgende voorbeeld is een uitwerking van opgave 63~\cite[pg. 131]{DK2009} de offi\"{e}le uitwerking is te vinden op pagina 195~\cite{DK2009} Laat $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})$ en $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}$. 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 'magische' 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 dan zoals $f$ als $g$ $2^m$-weg multiplexers~\cite[7.1.2-(31)]{DK2009-0} 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[pg 82]{DK2009}) $B(f) = 2^{m+2} - 1 \approx 4n$ en $B(g) = 2^{m+1} - 1 \approx 3n$ \\ \\ $B(f \land g)$ wordt aanzienlijk moeilijker. Zie dat er unieke oplossing bestaat -de oplossing kan aan een uniek getal gekoppeld worden- door $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 = 2_{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, welke 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$. Welke het profiel oplevert van $(2^{m+1}-2, 2^{m+1}-2, 2^{m+1}-4, 2^{m+1}-6, \dots, 4, 2, 2)$. Beiden profielen bij elkaar levert op $B(f \land g) = 2^{2m+1} + 2^{m-1} -1 \approx 2n^2$ \begin{thebibliography}{} \bibitem[DK2009]{DK2009} D.E. Knuth. Fascicle 1. \texttt{Bitwise Tricks \& Techniques; Binary Decision Diagrams}, volume 4 of \texttt{The Art of Computer Programming}. Pearson Education, first edition, March 2009. \bibitem[DK2009-Fas0]{DK2009-0} D.E. Knuth. Fascicle 0. \texttt{Bitwise Tricks \& Techniques; Binary Decision Diagrams}, volume 4 of \texttt{The Art of Computer Programming}. Pearson Education, first edition, March 2009. \bibitem[SCA2010]{SCA2010} Lecture Seminar Combinatorial Algorithms, \url{http://www.liacs.nl/~kosters/semcom/}, dr. W.A. (Walter) Kosters, LIACS, Spring 2010 \end{thebibliography} \end{document}