miniBDD を試す

miniBDD(a Minimalistic BDD Library) は、Oxford 大学において教育目的に作られた軽量のBDD(Binary Decision Diagram)ライブラリである。

miniBDD – a Minimalistic BDD Library

miniBDD is a very lightweight BDD library for teaching purposes. It's not very efficient (the nodes use too much memory), and it is missing a lot of features (e.g., dynamic variable re­ordering). The main point is that miniBDD is only about 600 lines of C++ code, and does not make use of any low-level programming. All data structures are instances of STL templates.

以下は sample code。

// sample_miniBDD
#include <iostream>

#include "miniBDD.h"

void sample(){
  miniBDD_mgr mgr;

  BDD x=mgr.Var("x");
  BDD y=mgr.Var("y");
  BDD z=mgr.Var("z");
  BDD f=(x&y&z)|(!x&!y&z);
  y.clear();
  x.clear();
  z.clear();

  mgr.DumpDot(std::cout);
  mgr.DumpTikZ(std::cout);
  mgr.DumpTable(std::cout);
}

int main(){
  sample();
}

つまり、この例では、(x&y&z)|(!x&!y&z) のBDDを作る。

これを付属の MakeFile でmake すれば良い。

// Makefile 例

CPLUSFLAGS = -g

>>
all: miniBDD.o sample_miniBDD

miniBDD.h: 
miniBDD.cpp: 

miniBDD.o: miniBDD.cpp miniBDD.inc miniBDD.h
	g++ $(CPLUSFLAGS) -c miniBDD.cpp -o miniBDD.o

sample_miniBDD.o: miniBDD.inc miniBDD.h sample_miniBDD.cpp
	g++ $(CPLUSFLAGS) -c sample_miniBDD.cpp -o sample_miniBDD.o

sample_miniBDD: miniBDD.o sample_miniBDD.o
	g++ $(CPLUSFLAGS) miniBDD.o sample_miniBDD.o -o sample_miniBDD

clean:
	rm -f miniBDD.o sample_miniBDD.o sample_miniBDD
	
miniBDD.tgz: miniBDD.cpp miniBDD.inc miniBDD.h sample_miniBDD.cpp Makefile
	tar cvfz miniBDD.tgz miniBDD.cpp miniBDD.inc \
	miniBDD.h sample_miniBDD.cpp Makefile

コンパイルされた結果、出力された実行ファイルを実行すると、tex 形式のファイルが出力される。

このtex ファイルは、tikzパッケージを使用しているので、以下をTexファイルに追加し、Texコンパイルを行えば良い。これをTexコンパイルし、dvipdfmxを通じて、PDFにするとグラフィカルなBDD表現が表示される。（dvi ファイルでは表示されないので、注意が必要。）

\usepackage[dvipdfmx]{graphicx}%
%\def\pgfsysdriver{pgfsys-dvipdfmx.def}%（graphicxパッケージを使用しない場合はこの行を有効に）
\usepackage{tikz}%（これで、pgfとpgfforが読み込まれます。）

全体としては、以下の様なTexファイルになる。

\documentclass{article}
\usepackage[dvipdfmx]{graphicx}
\usepackage{tikz}

\begin{document}
\begin{tikzpicture}[node distance=1cm]
\tikzstyle{BDDnode}=[circle,draw=black,inner sep=0pt,minimum size=5mm]
\node[] (vx) {$\mathit{x}$};
\node[xshift=0cm, BDDnode, right of=vx] (n13) {\small $13$};

\node[below of=vx] (vy) {$\mathit{y}$};
\node[xshift=0cm, BDDnode, right of=vy] (n8) {\small $8$};
\node[xshift=0cm, BDDnode, right of=n8] (n11) {\small $11$};

\node[below of=vy] (vz) {$\mathit{z}$};
\node[xshift=0cm, BDDnode, right of=vz] (n4) {\small $4$};

% terminals
\node[draw=black, style=rectangle, below of=vz, xshift=1cm] (n1) {$1$};
\node[draw=black, style=rectangle, left of=n1] (n0) {$0$};

% edges

\draw[->,dashed] (n4) -> (n0);
\draw[->] (n4) -> (n1);
\draw[->,dashed] (n8) -> (n4);
\draw[->] (n8) -> (n0);
\draw[->,dashed] (n11) -> (n0);
\draw[->] (n11) -> (n4);
\draw[->,dashed] (n13) -> (n8);
\draw[->] (n13) -> (n11);

\end{tikzpicture}
\end{document}