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

%

% $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{<hvdzwet@liacs.nl>}}

\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}