二分決定図のソースを表示

'''二分決定図'''（にぶんけっていず、{{lang-en-short|Binary Decision Diagram, '''BDD'''}}）や'''二分決定グラフ'''（にぶんけっていグラフ）とは、[[ブール関数]]を表現するのに使われる[[有向非巡回グラフ]]である。グラフに既約していない物は二分[[決定木]]（binary decision tree）と呼ぶ。

== 概要 ==
ビット(0あるいは1)の列を入力として、最終的に1つの 0/1 を返すような関数、すなわち[[ブール関数]]は、[[閉路]]のない[[有向非巡回グラフ]]で表現できる。ノードのうちの大部分は決定ノードと呼ばれ、それぞれの決定ノードは2つの行き先、つまり2つの子ノードを持つ。決定ノードには「入力の何ビット目を読め」というラベルが与えられている。従って、与えられたブール関数の答えを得るには、指示に従って入力のビット列を読みながら、ビットが0か1かによって、分岐点ごとに2つの行き先のどちらかを選べば良い。さらに、このような決定を十分な回数行うと、2つの終端ノード、0終端あるいは1終端のどちらかに行き当たる。その場合には、どちらの終端が得られたかを、ブール関数の答えとして返す。

例えば下の左図は、ブール関数 <math>f(x_1, x_2, x_3)</math> を表す二分[[決定木]]と[[真理値表]]を示している。この[[木構造 (データ構造)|木構造]]で、引数群の値の組み合わせに対応した関数の値はグラフを上から順にたどっていけば決定できる。従って、 <math>(x_1=0, x_2=1, x_3=1)</math> の関数値は、まず <math>x_1</math> から点線(<math>x_1=0</math>)をたどって <math>x_2</math> ノードに行き、続いて実線(<math>x_2=1</math>) をたどって <math>x_3</math> へ、最後に実線(<math>x_3=1</math>)により1終端ノードにたどり着く。従って, <math>f(x_1=0, x_2=1, x_3=1)</math> の値は 1 ということになる。

{| align="center"
|-
| [[Image:BDD.png|thumb|546px|関数 <math>f(x_1, x_2, x_3) = -x_1 * -x_2 * -x_3 + x_1 * x_2 + x_2 * x_3</math> の二分決定木と真理値表]]
| [[Image:BDD_simple.svg|thumb|189px|同じ関数 f の二分決定図]]
|}

開始ノードから降りていったときに現われる変数の順序が（どの経路でも）同じである二分決定図を'''順序付き'''（ordered）'''BDD'''と呼ぶ。また、特定の規則によって簡約した二分決定図を'''既約'''（reduced）'''BDD'''と呼ぶ。左の図に示した二分決定木は、簡約することで既約な右の図へと変換される。簡約のための規則は以下のとおりである。

* あるノード<math>A</math>が子ノード<math>A_1</math>と<math>A_2</math>を持つ時、同様に<math>A_1</math>と<math>A_2</math>を子ノードに持つような、機能的に重複したノードは存在しない。
* 2つの子ノードが同じノードであるような、決定に関して意味のないノードは存在しない。

一般的に、BDDと言えば「既約な順序付き二分決定図」を指すのが普通である（既約で順序付きであることを強調する場合は Reduced Ordered Binary Decision Diagram（'''ROBDD'''）と記されることもある。なお、BDDのうち、一部のみ簡約されているものを ROBDD と呼ぶのも間違いではないが、そのようなBDDは扱いにくく、通常は２つの簡約化規則を適用してこれ以上簡約化規則を適用できない状態のROBDDを一般的に使用されるROBDD、さらに単にBDDと呼ぶのが通常である。なお、既約でも順序付きでもないBDDはUnordered BDDであるが、特にUnorderedであることに関する研究対象としてはともかく、BDDとしてのコンパクト性やROBDDの生成アルゴリズムの処理時間等の実学的観点からは、あまり重要なBDDではないといえる）。ROBDD の利点は特定の関数を最も簡単に表現している点にある。この特徴から、ブール関数を[[論理回路]]化するのに使われたり、機能の等価性の判定に使われたりする。

根のノードから1終端ノードまでの経路は、そのBDDが表現しているブール関数が真(1)となる変数群の値を経路で表している（経路上に現われない変数の真理値は関数の値に影響しない）。このとき、あるノードから HIGH （子）ノードへの経路を通る場合、そのノードに対応する変数の値が 1 であることを示し、LOW ノードの場合は 0 であることを示す。

== 歴史 ==
このデータ構造を生み出すきっかけとなった考え方は[[シャノン展開]]である。スイッチング関数（ブール関数）は、1つの変数に着目した2つの部分関数に分割できる。そのような部分関数を部分木とみなせば、これを二分決定木で表現できる。二分決定図(BDD)は、Lee （1959年）が最初に紹介し<ref>C. Y. Lee. "Representation of Switching Circuits by Binary-Decision Programs". Bell Systems Technical Journal, 38:985–999, 1959.</ref>、Akers （1978年）<ref>Sheldon B. Akers. "Binary Decision Diagrams". IEEE Transactions on Computers, C-27(6):509–516, June 1978.</ref>や Boute （1976年）<ref>Raymond T. Boute, "The Binary Decision Machine as a programmable controller". EUROMICRO Newsletter, Vol. 1(2):16-22, January 1976.</ref>でさらに研究が行われ、広まっていった。

このデータ構造を使った効率的アルゴリズムの可能性を見出したのは[[カーネギーメロン大学]]の Bryant である。彼の行った拡張は（簡約表現のための）固定変数順序の使用と（圧縮のための）部分グラフの共有である。これらを適用することで、集合や関係を表現するための効率的なデータ構造とアルゴリズムができる<ref>Randal E. Bryant. "[http://www.cs.cmu.edu/~bryant/pubdir/ieeetc86.ps Graph-Based Algorithms for Boolean Function Manipulation]". IEEE Transactions on Computers, C-35(8):677–691, 1986.</ref><ref>R. E. Bryant, "[https://www.cs.cmu.edu/~bryant/pubdir/acmcs92.ps Symbolic Boolean Manipulation with Ordered Binary Decision Diagrams"], ACM Computing Surveys, Vol. 24, No. 3 (September, 1992), pp. 293-318.</ref>。複数のBDDを共有するよう拡張することにより（1つの部分グラフを複数のBDDで利用する）、共有ROBDDというデータ構造が定義された<ref>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.</ref>。これを単に BDD と称するのが一般的となっている。

より抽象的なレベルでは、BDD は集合や関係の圧縮表現とみなすことができる。他の圧縮との違いは、具体的な操作をその圧縮表現上で行うことができ、伸張する必要がない点である。

== 変数の順序付け ==
BDDのサイズは、表現しようとする関数とその変数（引数）の順序をどうするかで決定される。BDDのサイズは変数の個数に対して、線形のオーダーから指数のオーダーまで様々である。<math>f(x_1,\ldots, x_{n})</math> というブール関数があったとき、これを二分決定図に表現する際に、根となるノードからどういう順番で変数を対応させるかによって、そのサイズは指数オーダー（2<sup>n</sup>）にも線形オーダー（n）にもなる。例えば、<math>f(x_1,\ldots, x_{2n}) = x_1x_2 + x_3x_4 + \dots + x_{2n-1}x_{2n}</math> という形式のブール関数を考える。変数の順序付けを <math>x_1 < x_3 < \dots < x_{2n-1} < x_2 < x_4 < \dots < x_{2n}</math> とすると、この関数を表現する BDD のノード数は <math>2^{n+1}</math> となる。しかし、<math>x_1 < x_2 < x_3 < x_4 < \dots < x_{2n-1} < x_{2n}</math> という順序付けにすると、ノード数は <math>2n</math> で済む。

{| align="center"
|-
| [[Image:BDD_Variable_Ordering_Bad.svg|thumb|638px|関数 f(x1, ..., x8) = x1x2 + x3x4 + x5x6 + x7x8 を悪い変数順序付けで表現した場合の BDD]]
| [[Image:BDD_Variable_Ordering_Good.svg|thumb|156px|同じ関数を良い順序付けで表現した場合]]
|}

従って、このデータ構造を実際に利用する際には変数の順序付けが非常に重要となる。最良の順序付けを見つける問題は[[NP困難]]であることが分かっている<ref>Beate Bollig, Ingo Wegener. "Improving the Variable Ordering of OBDDs Is NP-Complete". IEEE Transactions on Computers, 45(9):993––1002, September 1996.</ref>。任意の1より大きい定数 c について、最適な解の c 倍のサイズを持つOBDDを生成する順序付けを探す問題もNP困難である<ref>Detlef Sieling. "The nonapproximability of OBDD minimization." Information and Computation 172, 103-138. 2002.</ref>。ただし、最適な順序付けを探すための効率的な[[ヒューリスティック]]が存在する。<ref>{{cite web|last=Rice|first=Michael|title=A Survey of Static Variable Ordering Heuristics for Eﬃcient BDD/MDD Construction|url=http://alumni.cs.ucr.edu/~skulhari/StaticHeuristics.pdf|accessdate=2016-02-28}}</ref> (Topological Sort, MinFillなど)

変数の順序をどう変えても常に指数オーダーとなる関数（変数順序付けに依存しない関数）も存在する。例えば、[[乗算器#デジタル乗算器|二進数の乗算]]がそのような関数の例である。BDD から派生したグラフ構造として、{{仮リンク|二分モーメント図|en|Binary moment diagram}}(BMD)や{{仮リンク|ゼロサプレス型二分決定グラフ|en|Zero-suppressed decision diagram}}(ZDD)がある。

== 実装 ==
* [http://fmv.jku.at/abcd/ ABCD]: by Armin Biere
* [http://sourceforge.net/projects/buddy/ BuDDy]: by Jørn Lind-Nielsen
* [http://www-2.cs.cmu.edu/~modelcheck/bdd.html CMU BDD]: カーネギーメロン大学（ピッツバーグ）
* [http://vlsi.colorado.edu/~fabio/CUDD/ CUDD]: コロラド大学（ボールダー）
* [http://javabdd.sourceforge.net JavaBDD], Java版 BuDDy。CUDD, CAL, JDD とのインターフェイスを持つ
* [http://embedded.eecs.berkeley.edu/Research/cal_bdd/ CAL]: UCB、幅優先操作を行う。
* [http://www.rs.e-technik.tu-darmstadt.de/~sth TUD BDD]: by Stefan Höreth
* [https://bitbucket.org/vahidi/jdd JDD]: by Vahidi、Javaによる実装。BDD と ZDD をサポート
* [https://bitbucket.org/vahidi/jbdd JBDD]: by Vahidi、BuDDYおよびCUDDとのJavaインターフェイス

== 参考文献 ==
<references />
* 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.

== 関連項目 ==
* [[充足可能性問題]]
* [[データ構造]]
* [[モデル検査]]
* [[否定標準形]] (NNF)
* [[:en:Propositional directed acyclic graph]] (PDAG)
* [[基数木]]

== 外部リンク ==
* H. Andersen "[http://www.itu.dk/people/hra/bdd97.ps An Introduction to Binary Decision Diagrams]," Lecture Notes, http://www.itu.dk/people/hra/bdd97-abstract.html, October 1997.
* [http://www-alg.ist.hokudai.ac.jp/~minato/alg2006/alg2006-4.pdf アルゴリズム特論（第4回） 二分決定グラフ] 湊真一（北海道大学）

{{Normdaten}}
{{DEFAULTSORT:にふんけつていす}}
[[Category:データ構造]]
[[Category:ダイアグラム]]