二分決定図

二分決定図 (Binary Decision Diagram, BDD) とは

二分決定図（BDD）は、ブール関数を表現するための有向非巡回グラフです。二分決定木を簡約化し、変数順序を最適化することで、データ構造の効率性を高めています。主に、論理回路の設計や機能検証の分野で利用されています。

概要

BDDは、ブール関数の入力をビット列とし、最終的に0または1の値を返す関数を表現します。グラフのノードは、決定ノードと終端ノード（0終端または1終端）から構成されます。決定ノードは、入力ビットのいずれかを読み取り、その値によって2つの子ノードへ分岐します。この分岐を繰り返すことで、最終的に終端ノードに到達し、ブール関数の結果が得られます。

例えば、ブール関数 \( f(x_1, x_2, x_3) \) を考えてみましょう。二分決定木では、入力変数の組み合わせごとにグラフを辿り、対応する関数の値を得ることができます。

例:

• - \( (x_1 = 0, x_2 = 1, x_3 = 1) \) の場合、\( x_1 \) が0なので左へ、次に\( x_2 \) が1なので右へ、最後に\( x_3 \) が1なので右へ進み、1終端ノードに到達します。

簡約化と順序付きBDD

BDDには、以下の2つの簡約規則が適用されます。

1. ノードの共有: 同じ子ノードを持つ機能的に重複したノードを共有します。
2. 不要なノードの削除: 2つの子ノードが同じノードを指すような意味のないノードを削除します。

これらの規則により、冗長なノードが削除され、グラフが簡約化されます。また、開始ノードから終端ノードまでの変数の順序がどの経路でも同じであるBDDを、順序付きBDD（Ordered BDD, OBDD）と呼びます。さらに簡約化された順序付きBDDを、既約順序付き二分決定図（Reduced Ordered Binary Decision Diagram, ROBDD）と呼びます。一般的に、BDDという場合は、ROBDDを指すことが多いです。

ROBDDの利点は、特定の関数を最も簡単に表現できる点にあります。これにより、ブール関数の論理回路化や、機能の等価性判定に利用されます。

変数の順序付け

BDDのサイズは、変数の順序付けによって大きく変化します。変数の順序によっては、ノード数が指数関数的に増加する可能性があります。例えば、\( f(x_1, ..., x_{2n}) = x_1x_2 + x_3x_4 + ... + x_{2n-1}x_{2n} \) という関数を考えたとき、変数の順序を \( x_1 < x_3 < ... < x_{2n-1} < x_2 < x_4 < ... < x_{2n} \) とすると、ノード数が \( 2^{n+1} \) になりますが、\( x_1 < x_2 < x_3 < ... < x_{2n} \) とすると \( 2n \) で済む場合があります。

最適な順序付けを見つける問題はNP困難ですが、ヒューリスティックな手法（Topological Sort, MinFillなど）を用いて効率的な順序付けを見つけることが可能です。しかし、変数の順序に関わらず常に指数オーダーになる関数も存在します（例：二進数の乗算）。

歴史

BDDの基礎となる考え方は、シャノン展開です。これは、ブール関数を一つの変数に着目した二つの部分関数に分割する手法です。Leeが1959年にこの概念を導入し、Akers（1978年）やBoute（1976年）によって研究が進められました。

Bryantは、固定変数順序の使用と部分グラフの共有によって、効率的なアルゴリズムの可能性を示しました。これにより、集合や関係を表現するための効率的なデータ構造とアルゴリズムが実現しました。

実装

BDDを実装したライブラリとしては、以下のようなものがあります。

ABCD (Armin Biere)
BuDDy (Jørn Lind-Nielsen)
CMU BDD (カーネギーメロン大学)
CUDD (コロラド大学)
JavaBDD (Java版 BuDDy)
CAL (UCB、幅優先操作)
TUD BDD (Stefan Höreth)
JDD (Vahidi、Javaによる実装)
JBDD (Vahidi、BuDDYおよびCUDDとのJavaインターフェイス)

関連事項

充足可能性問題
データ構造
モデル検査
否定標準形 (NNF)
Propositional directed acyclic graph (PDAG)
基数木

参考文献

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回） 二分決定グラフ 湊真一（北海道大学）

もう一度検索