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

%
% $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{<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]
\label{voorbeeldSamenvoegen}
\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 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 \emph{BDD} is een belangrijk
\emph{BDD} algoritme~\cite[p.~86]{DK2009}. Het neemt in essentie een \emph{BDD}
functie $f$ en combineert deze met een andere \emph{BDD} functie $g$
zodanig dat er een nieuwe \emph{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
\emph{BDD}s 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 \emph{BDD}}
\label{werking}
De term voor het samenvoegen van \emph{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
Figuur~\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'' \emph{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 \emph{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 \emph{BDD} is geldig voor alle.

Door de \emph{BDD}s achter elkaar te plakken kan met maximaal $B(f)B(g)$ knopen
een \emph{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 \emph{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}

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})$\footnote{Waar er $b_{k}$ 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})$\footnote{Waar $q_{k-1}$ het aantal \circle{k} knopen in
de \emph{QDD} is.} en $(q'_{0},\dots,q'_{n})$.  

Om te laten zijn dat de gesmolten $f \diamond g$ het aantal knopen $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 naar het aantal \emph{beads}~\cite[p.~72]{DK2009} dat
mogelijkerwijs gemaakt kan worden van de functies $f$ en $g$.  

Hierbij geldt dan voor een willikeurige functie $n$ met als profiel
$(b_{0},\dots,b_{n})$ en quasi-profiel $(q_{0},\dots,q_{n})$ 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}) \setminus (b_{0},\dots,b_{n})$.

Elke bead \beta 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 \emph{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}
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}
\caption{\oplus is de binary operator \emph{XOR}}
\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~\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}