二分決定図
二分決定図（にぶんけっていず、英: Binary Decision Diagram, BDD）や二分決定グラフ（にぶんけっていグラフ）とは、ブール関数を表現するのに使われる有向非巡回グラフである。グラフに既約していない物は二分決定木（binary decision tree）と呼ぶ。
概要
ビット(0あるいは1)の列を入力として、最終的に1つの 0/1 を返すような関数、すなわちブール関数は、閉路のない有向非巡回グラフで表現できる。ノードのうちの大部分は決定ノードと呼ばれ、それぞれの決定ノードは2つの行き先、つまり2つの子ノードを持つ。決定ノードには「入力の何ビット目を読め」というラベルが与えられている。従って、与えられたブール関数の答えを得るには、指示に従って入力のビット列を読みながら、ビットが0か1かによって、分岐点ごとに2つの行き先のどちらかを選べば良い。さらに、このような決定を十分な回数行うと、2つの終端ノード、0終端あるいは1終端のどちらかに行き当たる。その場合には、どちらの終端が得られたかを、ブール関数の答えとして返す。
例えば下の左図は、ブール関数 
開始ノードから降りていったときに現われる変数の順序が（どの経路でも）同じである二分決定図を順序付き（ordered）BDDと呼ぶ。また、特定の規則によって簡約した二分決定図を既約（reduced）BDDと呼ぶ。左の図に示した二分決定木は、簡約することで既約な右の図へと変換される。簡約のための規則は以下のとおりである。
- あるノード
従って、このデータ構造を実際に利用する際には変数の順序付けが非常に重要となる。最良の順序付けを見つける問題はNP困難であることが分かっている[7]。任意の1より大きい定数 c について、最適な解の c 倍のサイズを持つOBDDを生成する順序付けを探す問題もNP困難である[8]。ただし、最適な順序付けを探すための効率的なヒューリスティックが存在する。[9] (Topological Sort, MinFillなど)
変数の順序をどう変えても常に指数オーダーとなる関数（変数順序付けに依存しない関数）も存在する。例えば、二進数の乗算がそのような関数の例である。BDD から派生したグラフ構造として、二分モーメント図(BMD)やゼロサプレス型二分決定グラフ(ZDD)がある。
実装
- ABCD: by Armin Biere
- BuDDy: by Jørn Lind-Nielsen
- CMU BDD: カーネギーメロン大学（ピッツバーグ）
- CUDD: コロラド大学（ボールダー）
- JavaBDD, Java版 BuDDy。CUDD, CAL, JDD とのインターフェイスを持つ
- CAL: UCB、幅優先操作を行う。
- TUD BDD: by Stefan Höreth
- JDD: by Vahidi、Javaによる実装。BDD と ZDD をサポート
- JBDD: by Vahidi、BuDDYおよびCUDDとのJavaインターフェイス
参考文献
- ^ C. Y. Lee. "Representation of Switching Circuits by Binary-Decision Programs". Bell Systems Technical Journal, 38:985–999, 1959.
- ^ Sheldon B. Akers. "Binary Decision Diagrams". IEEE Transactions on Computers, C-27(6):509–516, June 1978.
- ^ Raymond T. Boute, "The Binary Decision Machine as a programmable controller". EUROMICRO Newsletter, Vol. 1(2):16-22, January 1976.
- ^ Randal E. Bryant. "Graph-Based Algorithms for Boolean Function Manipulation". IEEE Transactions on Computers, C-35(8):677–691, 1986.
- ^ R. E. Bryant, "Symbolic Boolean Manipulation with Ordered Binary Decision Diagrams", ACM Computing Surveys, Vol. 24, No. 3 (September, 1992), pp. 293-318.
- ^ Karl S. Brace, Richard L. Rudell and Randal E. Bryant. "Efficient Implementation of a BDD Package". In Proceedings of the 27th ACM/IEEE Design Automation Conference (DAC 1990), pages 40–45. IEEE Computer Society Press, 1990.
- ^ Beate Bollig, Ingo Wegener. "Improving the Variable Ordering of OBDDs Is NP-Complete". IEEE Transactions on Computers, 45(9):993––1002, September 1996.
- ^ Detlef Sieling. "The nonapproximability of OBDD minimization." Information and Computation 172, 103-138. 2002.
- ^ Rice, Michael. “A Survey of Static Variable Ordering Heuristics for Efficient BDD/MDD Construction”. 2016年2月28日閲覧。
- Ch. Meinel, T. Theobald, "Algorithms and Data Structures in VLSI-Design: OBDD - Foundations and Applications", Springer-Verlag, Berlin, Heidelberg, New York, 1998.
- R. Ubar, "Test Generation for Digital Circuits Using Alternative Graphs (in Russian)", in Proc. Tallinn Technical University, 1976, No.409, Tallinn Technical University, Tallinn, Estonia, pp.75-81.
関連項目
外部リンク
- H. Andersen "An Introduction to Binary Decision Diagrams," Lecture Notes, http://www.itu.dk/people/hra/bdd97-abstract.html, October 1997.
- アルゴリズム特論（第4回） 二分決定グラフ 湊真一（北海道大学）
