二分決定図
出典: フリー百科事典『ウィキペディア(Wikipedia)』
二分決定図(にぶんけっていず、Binary Decision Diagram、BDD)とは、ブール関数を表現するのに使われるデータ構造である。二分決定グラフあるいは(基本的には二分木のような構造であることから)二分決定木と呼ぶこともある。
目次 |
[編集] 概要
ブール関数は、1つの出発点がある、有向で非環状のグラフで表現できる。2つの終端ノード(0終端と1終端)以外のノードは決定ノードであり、決定ノードにはブーリアン変数が1つ対応していて、2つの子ノードを持つ。2つの子ノードは、ブーリアンの値が0の場合の HIGH ノードと1の場合の LOW ノードである。根のノードから降りていったときに現われる変数の順序が(どの経路でも)同じである二分決定図を「順序付き; ordered」BDDと呼ぶ。また、次の規則に従って簡約化した二分決定図を「既約; reduced」BDDと呼ぶ。
- 任意の同型的(isomorphic)なサブグラフをマージする。
- 2つの子ノードが同型的である任意のノードを省略する。
一般的に、BDDと言えば「既約な順序付き二分決定図」を指すのが普通である(既約で順序付きであることを強調する場合は ROBDD と記されることもある)。ROBDD の利点は特定の関数を最も簡単に表現している点にある。この特徴から、ブール関数を論理回路化するのに使われたり、機能の等価性の判定に使われたりする。
根のノードから1終端ノードまでの経路は、そのBDDが表現しているブール関数が真(1)となる変数群の値を経路で表している(経路上に現われない変数の真理値は関数の値に影響しない)。このとき、あるノードから HIGH (子)ノードへの経路を通る場合、そのノードに対応する変数の値が 1 であることを示し、LOW ノードの場合は 0 であることを示す。
[編集] 例
下の左図は、ブール関数 f(x1, x2, x3) を表す(簡約化していない)二分決定木と真理値表を示している。この木構造で、引数群の値の組み合わせに対応した関数の値はグラフを上から終端まで所定の変数の値に従って辿っていけば決定される。下図において、点線のエッジ(枝)は LOW(子)ノードへのエッジを表し、実線のエッジは HIGH(子)ノードへのエッジを表す。従って、例えば (x1=0, x2=1, x3=1) の場合の関数値を求めるには、まず x1 から点線をたどって x2 ノードに行き、その後は実線を2回たどる。そうすると、1終端にたどり着き、f (x1=0, x2=1, x3=1) の値は 1 ということになる。
左図の二分決定木は、上述の2つの簡約化規則に従って簡約化することで既約な順序付き二分決定図へと変換される(下の右図参照)。
[編集] 歴史
このデータ構造を生み出すきっかけとなった考え方はシャノン展開である。スイッチング関数(ブール関数)は、1つの変数に着目した2つの部分関数に分割できる。そのような部分関数を部分木とみなせば、これを二分決定木で表現できる。二分決定図(BDD)は、Lee (1959年)が最初に紹介し[1]、Akers (1978年)[2]や Boute (1976年)[3]でさらに研究が行われ、広まっていった。
このデータ構造を使った効率的アルゴリズムの可能性を見出したのはカーネギーメロン大学の Bryant である。彼の行った拡張は(簡約表現のための)固定変数順序の使用と(圧縮のための)部分グラフの共有である。これらを適用することで、集合や関係を表現するための効率的なデータ構造とアルゴリズムができる[4][5]。複数のBDDを共有するよう拡張することにより(1つの部分グラフを複数のBDDで利用する)、共有ROBDDというデータ構造が定義された[6]。これを単に BDD と称するのが一般的となっている。
より抽象的なレベルでは、BDD は集合や関係の圧縮表現とみなすことができる。他の圧縮との違いは、具体的な操作をその圧縮表現上で行うことができ、伸張する必要がない点である。
[編集] 変数の順序付け
BDDのサイズは、表現しようとする関数とその変数(引数)の順序をどうするかで決定される。BDDのサイズは変数の個数に対して、線形のオーダーから指数のオーダーまで様々である。 というブール関数があったとき、これを二分決定図に表現する際に、根となるノードからどういう順番で変数を対応させるかによって、そのサイズは指数オーダー(2n)にも線形オーダー(n)にもなる。例えば、 という形式のブール関数を考える。変数の順序付けを とすると、この関数を表現する BDD のノード数は 2n + 1 となる。しかし、 という順序付けにすると、ノード数は 2n で済む。
従って、このデータ構造を実際に利用する際には変数の順序付けが非常に重要となる。最良の順序付けを見つける問題はNP困難であることが分かっている[7]。任意の1より大きい定数 c について、最適な解の c 倍のサイズを持つOBDDを生成する順序付けを探す問題もNP困難である[8]。ただし、最適な順序付けを探すための効率的なヒューリスティックが存在する。
変数の順序をどう変えても常に指数オーダーとなる関数(変数順序付けに依存しない関数)も存在する。例えば、二進数の乗算がそのような関数の例である。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 と ZBDD 操作をサポート
- 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.
- 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 "An Introduction to Binary Decision Diagrams," Lecture Notes, http://www.itu.dk/people/hra/bdd97-abstract.html, October 1997.
- アルゴリズム特論(第4回) 二分決定グラフ 湊真一(北海道大学)