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

%
% $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]
\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 een concreet voorbeelden.

\section{Samenvoegen van \BDD}
\label{werking}
De term voor het samenvoegen van \BDD structuren zullen we 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'$, de ``\emph{emulsie}'' (\emph{meld}) van $\alpha$ en
$\alpha'$, is dan als volgt gedefinieerd als $\alpha$ en $\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 zal zien dan als je Formule~\ref{melt-eq} toepast op de
bladeren er door samenvoegen van de bladeren ---zie bijvoorbeeld
voorbeeld in Hoofstuk~\ref{voorbeeldSamenvoegen}--- 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; de
vak-website~\cite{SCA2010} heeft een referentie naar algoritme $R$ 
\url{http://www.liacs.nl/~kosters/semcom/tomb.pdf} welke 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 offi\"{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 bestaat for $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. 
\\ \\
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 zijn 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 willikeurige functie $n$ met als profiel $(b_{0},\dots,b_{n})$ en
quasi-profiel $(q_{0},\dots,q_{n})$ geldt dat $B(q_{0},\dots,q_{n}) \geq
B(b_{0},\dots,b_{n})$. En tevens dan $(b_{0},\dots,b_{n}) \subseteq
(q_{0},\dots,q_{n})$. Hieruit volgt dat een geen-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 beats van $(f,g)$ of (b) de gegenereerde reeks van een
(bead,geen-bead) of (geen-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 offi\"{e}le uitwerking is te vinden op \cite[p.~195]{DK2009}.

\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}
In Vergelijking~\ref{eq:opgave63} zijn $f$ en $g$ gedefinieerd, waarbij $\oplus$
de binary operator \emph{XOR} is en $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 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~\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[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)$ wordt aanzienlijk moeilijker. We constateren eerst
dat er een unieke oplossing bestaat ---de oplossing kan aan een uniek getal
gekoppeld worden---
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
= 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, 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}