Wikipedia

二分決定図

（2分決定木から転送）

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

概要 編集

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

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

 
関数   の二分決定木と真理値表
 
同じ関数 f の二分決定図

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

  • あるノード が子ノード と を持つ時、同様に と を子ノードに持つような、機能的に重複したノードは存在しない。
  • 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年）が最初に紹介し[1]、Akers （1978年）[2]や Boute （1976年）[3]でさらに研究が行われ、広まっていった。

このデータ構造を使った効率的アルゴリズムの可能性を見出したのはカーネギーメロン大学の Bryant である。彼の行った拡張は（簡約表現のための）固定変数順序の使用と（圧縮のための）部分グラフの共有である。これらを適用することで、集合や関係を表現するための効率的なデータ構造とアルゴリズムができる[4][5]。複数のBDDを共有するよう拡張することにより（1つの部分グラフを複数のBDDで利用する）、共有ROBDDというデータ構造が定義された[6]。これを単に BDD と称するのが一般的となっている。

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

変数の順序付け 編集

BDDのサイズは、表現しようとする関数とその変数（引数）の順序をどうするかで決定される。BDDのサイズは変数の個数に対して、線形のオーダーから指数のオーダーまで様々である。  というブール関数があったとき、これを二分決定図に表現する際に、根となるノードからどういう順番で変数を対応させるかによって、そのサイズは指数オーダー（2n）にも線形オーダー（n）にもなる。例えば、  という形式のブール関数を考える。変数の順序付けを   とすると、この関数を表現する BDD のノード数は   となる。しかし、  という順序付けにすると、ノード数は   で済む。

 
関数 f(x1, ..., x8) = x1x2 + x3x4 + x5x6 + x7x8 を悪い変数順序付けで表現した場合の 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インターフェイス

参考文献 編集

  1. ^ C. Y. Lee. "Representation of Switching Circuits by Binary-Decision Programs". Bell Systems Technical Journal, 38:985–999, 1959.
  2. ^ Sheldon B. Akers. "Binary Decision Diagrams". IEEE Transactions on Computers, C-27(6):509–516, June 1978.
  3. ^ Raymond T. Boute, "The Binary Decision Machine as a programmable controller". EUROMICRO Newsletter, Vol. 1(2):16-22, January 1976.
  4. ^ Randal E. Bryant. "Graph-Based Algorithms for Boolean Function Manipulation". IEEE Transactions on Computers, C-35(8):677–691, 1986.
  5. ^ R. E. Bryant, "Symbolic Boolean Manipulation with Ordered Binary Decision Diagrams", ACM Computing Surveys, Vol. 24, No. 3 (September, 1992), pp. 293-318.
  6. ^ 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.
  7. ^ Beate Bollig, Ingo Wegener. "Improving the Variable Ordering of OBDDs Is NP-Complete". IEEE Transactions on Computers, 45(9):993––1002, September 1996.
  8. ^ Detlef Sieling. "The nonapproximability of OBDD minimization." Information and Computation 172, 103-138. 2002.
  9. ^ 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.

関連項目 編集

外部リンク 編集

「https://ja.wikipedia.org/w/index.php?title=二分決定図&oldid=95942937」から取得