二分決定図

コンピュータサイエンスにおいて、二分決定図( BDD ) または分岐プログラムは、ブール関数を表すために使用されるデータ構造です。より抽象的なレベルでは、BDD はセットまたは関係の圧縮表現と考えることができます。他の圧縮表現とは異なり、操作は圧縮表現に対して直接、つまり解凍なしで実行されます。

同様のデータ構造には、否定正規形(NNF)、Zhegalkin 多項式、命題有向非巡回グラフ(PDAG)などがあります。

ブール関数は、ルート付き有向非巡回グラフ として表すことができます。これは、複数の (決定) ノードと 2 つの終端ノードで構成されます。2 つの終端ノードには、0 (FALSE) と 1 (TRUE) のラベルが付けられます。各 (決定) ノードには、ブール変数 のラベルが付けられ、low child と high child と呼ばれる 2 つの子ノードがあります。ノードから low (または high) 子へのエッジは、それぞれ値 FALSE (または TRUE) を変数に割り当てることを表します。このようなBDD は、ルートからのすべてのパスで異なる変数が同じ順序で出現する場合、「順序付き」と呼ばれます。次の 2 つのルールがグラフに適用されている場合、BDD は「簡約済み」であると言われます。 ${\displaystyle u}$${\displaystyle x_{i}}$${\displaystyle u}$${\displaystyle x_{i}}$

• 同型サブグラフをマージします。
• 2 つの子が同型であるノードをすべて削除します。

一般的な用法では、 BDDという用語はほとんどの場合、Reduced Ordered Binary Decision Diagram (文献ではROBDDと呼ばれ、順序付けと削減の側面を強調する必要がある場合に使用されます) を指します。ROBDD の利点は、特定の関数と変数の順序に対して標準的 (同型性まで一意) であることです。 ^[1]この特性により、ROBDD は機能的等価性チェックや機能的テクノロジ マッピングなどの操作に役立ちます。

ルート ノードから 1 ターミナルへのパスは、表現されるブール関数が true となる (部分的な場合もある) 変数割り当てを表します。パスがノードから下位 (または上位) の子に降りていくと、そのノードの変数にはそれぞれ 0 (または 1) が割り当てられます。

下の左の図は、バイナリ決定木（削減規則は適用されない）と真理値表を示しており、それぞれが関数 を表しています。 左側のツリーでは、グラフを末端までたどるパスをたどることで、特定の変数割り当てに対する関数 の値を決定できます。 下の図では、点線は下位の子へのエッジを表し、実線は上位の子へのエッジを表しています。 したがって、 を見つけるには、 x ₁から始めて、点線を下って x ₂まで移動し（x ₁には0 への割り当てがあるため）、次に 2 本の実線を下って移動します（x ₂と x ₃にはそれぞれ 1 への割り当てがあるため）。 これにより、末端 1 に到達し、これが の値です。 ${\displaystyle f(x_{1},x_{2},x_{3})}$${\displaystyle f(0,1,1)}$${\displaystyle f(0,1,1)}$

左の図の二分決定木は、2 つの削減規則に従って最大限に削減することで二分決定図に変換できます。結果として得られるBDD は右の図に示されています。

このブール関数を記述するための別の表記法は です。 ${\displaystyle {\overline {x}}_{1}{\overline {x}}_{2}{\overline {x}}_{3}+x_{1}x_{2}+x_{2}x_{3}}$

ROBDDは、補完リンクとも呼ばれる補完エッジを使用して、さらにコンパクトに表現できます。^{[2] [3]}結果として得られるBDDは、型付きBDD ^[4]または符号付きBDDと呼ばれることもあります。補完エッジは、低エッジを補完されているかどうかに注釈を付けることで形成されます。エッジが補完されている場合、それはエッジが指すノードに対応するブール関数の否定を参照します（そのノードをルートとするBDDによって表されるブール関数）。結果として得られるBDD表現が標準形式であることを保証するために、高エッジは補完されません。この表現では、以下に説明する理由により、BDDには単一のリーフノードがあります。

BDD を表現するときに補完エッジを使用する利点は 2 つあります。

• BDDの否定を計算するには一定の時間がかかる
• スペース使用量（つまり必要なメモリ）が削減される（最大2分の1）

しかし、クヌース^[5]はそうではないと主張している。

このようなリンクはすべての主要な BDD パッケージで使用されていますが、コンピュータ プログラムがはるかに複雑になるため、推奨することは困難です。メモリの節約は通常無視できるほど小さく、2 倍を超えることはありません。さらに、著者の実験では、実行時間の増加はほとんど見られませんでした。

この表現における BDD への参照は、BDD のルートを指す (おそらく補完された)「エッジ」です。これは、補完されたエッジを使用しない表現 (BDD のルート ノード) における BDD への参照とは対照的です。この表現における参照がエッジである必要がある理由は、各ブール関数について、関数とその否定が BDD のルートへのエッジと、同じ BDD のルートへの補完されたエッジによって表されるためです。これが、否定に一定の時間がかかる理由です。また、単一のリーフ ノードで十分である理由も説明できます。FALSE はリーフ ノードを指す補完されたエッジによって表され、TRUE はリーフ ノードを指す通常のエッジ (つまり、補完されていないエッジ) によって表されます。

たとえば、ブール関数が、補完エッジを使用して表現された BDD で表現されているとします。変数への (ブール) 値の特定の割り当てに対するブール関数の値を見つけるには、BDD のルートを指す参照エッジから開始し、特定の変数値によって定義されるパス (ノードのラベルとなる変数が FALSE の場合はロー エッジをたどり、ノードのラベルとなる変数が TRUE の場合はハイ エッジをたどります) を、リーフ ノードに到達するまでたどります。このパスをたどりながら、補完エッジをいくつ通過したかをカウントします。リーフ ノードに到達したときに補完エッジを奇数個通過した場合、特定の変数割り当てに対するブール関数の値は FALSE になります。そうでない場合 (補完エッジを偶数個通過した場合)、特定の変数割り当てに対するブール関数の値は TRUE になります。

この表現による BDD の例の図が右側に示されており、上の図に示されているのと同じブール式、つまり を表しています。低いエッジは破線、高いエッジは実線、補完エッジはソースに円で示されます。@ 記号の付いたノードは BDD への参照を表します。つまり、参照エッジはこのノードから始まるエッジです。 ${\displaystyle (\neg x_{1}\wedge \neg x_{2}\wedge \neg x_{3})\vee (x_{1}\wedge x_{2})\vee (x_{2}\wedge x_{3})}$

データ構造が作成された基本的なアイデアは、シャノン展開です。スイッチング関数は、 1つの変数を割り当てることによって2つのサブ関数（コファクター）に分割されます（if-then-else標準形式を参照）。このようなサブ関数をサブツリーと見なすと、バイナリ決定木で表すことができます。バイナリ決定図（BDD）は、CY Leeによって導入され、^{[6] Sheldon B. Akers [7]}とRaymond T. Bouteによってさらに研究され、知られるようになりました。 ^[8]これらの著者とは独立して、Yu. V. Mamrukovは、速度に依存しない回路の解析のために、CADで「標準ブラケット形式」という名前のBDDを実現しました。^[9]データ構造に基づく効率的なアルゴリズムの完全な可能性は、カーネギーメロン大学のRandal Bryantによって調査されました。彼の主要な拡張は、固定変数順序付け（標準表現用）と共有サブグラフ（圧縮用）を使用することでした。これら2つの概念を適用することで、集合と関係を表現するための効率的なデータ構造とアルゴリズムが生まれます。^{[10] [11]}共有を複数のBDDに拡張することで、つまり1つのサブグラフを複数のBDDで使用することで、データ構造Shared Reduced Ordered Binary Decision Diagramが定義されます。^[2]現在、BDDという概念は、一般的にその特定のデータ構造を指すために使用されます。

ドナルド・クヌースはビデオ講義「二分決定図（BDD）を楽しむ」の中で、^[12] BDDを「過去25年間に登場した数少ない本当に基本的なデータ構造の1つ」と呼び、ブライアントの1986年の論文がしばらくの間、コンピュータサイエンスで最も引用された論文の1つであったと述べています。

Adnan Darwiche 氏とその協力者は、BDD がブール関数の複数の正規形の 1 つであり、それぞれが異なる要件の組み合わせによって誘導されることを示しました。Darwiche 氏が特定したもう 1 つの重要な正規形は、分解可能否定正規形 (DNNF) です。

BDDは、回路を合成するCADソフトウェア（論理合成）や形式検証で広く使用されています。BDDのあまり知られていない応用としては、フォールトツリー分析、ベイズ推論、製品構成、個人情報検索などがあります。^{[13] [14] [要出典]}

任意の BDD (縮小または順序付けされていない場合でも) は、各ノードを 2 対 1マルチプレクサに置き換えることでハードウェアで直接実装できます。各マルチプレクサは、 FPGA内の 4-LUT で直接実装できます。任意の論理ゲートのネットワークから BDD に変換するのはそれほど簡単ではありません^{[引用が必要]} ( AND インバータ グラフとは異なります)。

BDDは効率的なDatalogインタープリタに適用されている。^[15]

BDD のサイズは、表現される関数と、選択された変数の順序の両方によって決まります。変数の順序によっては、グラフのノード数が最良の場合は線形 (  nの場合)、最悪の場合は指数関数的 (たとえば、リップル キャリー加算器) になるブール関数が存在します。ブール関数を考えてみましょう。変数の順序を使用すると、BDD は関数を表現するためにノードを必要とします。順序を使用すると、BDD はノードで構成されます。 ${\displaystyle f(x_{1},\ldots ,x_{n})}$${\displaystyle f(x_{1},\ldots ,x_{2n})=x_{1}x_{2}+x_{3}x_{4}+\cdots +x_{2n-1}x_{2n}.}$${\displaystyle x_{1}<x_{3}<\cdots <x_{2n-1}<x_{2}<x_{4}<\cdots <x_{2n}}$${\displaystyle 2^{n+1}}$${\displaystyle x_{1}<x_{2}<x_{3}<x_{4}<\cdots <x_{2n-1}<x_{2n}}$${\displaystyle 2n+2}$

このデータ構造を実際に適用する場合、変数の順序に注意することが極めて重要です。最適な変数の順序を見つける問題はNP困難です。^[16]定数c > 1に対して、最適なサイズよりも最大でc倍大きい サイズのOBDDを生成する変数の順序を計算することさえNP困難です。 ^[17]しかし、この問題に対処するための効率的なヒューリスティックが存在します。^[18]

グラフのサイズが常に指数関数的である関数があり、これは変数の順序とは無関係である。これは例えば乗算関数に当てはまる。^[1]実際、2つの ビット数の積の中央のビットを計算する関数には、頂点よりも小さいOBDDはない。 ^{[19] （乗算関数に多項式サイズのOBDDがあれば、}整数因数分解がP/polyであることが示されるが、これが真かどうかはわかっていない。^[20]） ${\displaystyle n}$${\displaystyle 2^{\lfloor n/2\rfloor }/61-4}$

研究者は、BDD データ構造を改良して、BMD (バイナリ モーメント ダイアグラム)、ZDD (ゼロ サプレス決定ダイアグラム)、FBDD (自由バイナリ決定ダイアグラム)、FDD (機能決定ダイアグラム)、PDD (パリティ決定ダイアグラム)、MTBDD (多重端末 BDD) などの関連グラフをいくつか提案しています。

BDD上の多くの論理演算は多項式時間グラフ操作アルゴリズムによって実装できる: ^{[21] : 20}

• 接続詞
• 分離
• 否定

しかし、これらの操作を複数回繰り返すと、たとえば BDD のセットの論理積または論理和を形成すると、最悪の場合、BDD が指数関数的に大きくなる可能性があります。これは、2 つの BDD に対する前述の操作のいずれかにより、BDD のサイズの積に比例するサイズの BDD が生成されることがあり、その結果、複数の BDD ではサイズが操作の数に対して指数関数的になる可能性があるためです。変数の順序付けは改めて検討する必要があります。BDD のセット (の一部) に適した順序付けが、操作の結果に適した順序付けとは限りません。また、ブール関数の BDD を構築すると、NP 完全なブール充足問題と NP 完全な共存トートロジー問題が解決されるため、結果の BDD が小さい場合でも、BDD の構築にはブール式のサイズが指数関数的に増加する時間がかかります。

縮小BDDの複数の変数にわたる存在抽象化を計算することはNP完全である。^[22]

モデルカウント、つまりブール式の充足割り当ての数をカウントすることは、BDD では多項式時間で実行できます。一般的な命題式の場合、問題は♯P完全であり、最もよく知られているアルゴリズムでは最悪の場合、指数時間が必要です。

• ブール充足可能性問題、標準的なNP完全 計算問題
• L/poly、多項式サイズのBDDの問題の集合を厳密に含む複雑性クラス^[要出典]
• モデルチェック
• 基数木
• バリントンの定理
• ハードウェアアクセラレーション
• カルノー図、ブール代数式を簡略化する手法
• ゼロ抑制決定図
• 代数的決定図、2要素から任意の有限集合へのBDDの一般化
• 文決定図、OBDD の一般化
• 影響図

• Ubar, R. (1976). 「代替グラフを使用したデジタル回路のテスト生成」Proc. Tallinn Technical University (ロシア語) (409). タリン、エストニア: 75–81.
• Meinel, C.; Theobald, T. (2012) [1998]. VLSI設計におけるアルゴリズムとデータ構造: OBDD – 基礎と応用(PDF) . Springer. ISBN 978-3-642-58940-9。完全な教科書をダウンロードできます。
• エベント、リュディガー。フェイ、ゲルシュウィン。ロルフ・ドレクスラー (2005)。高度な BDD 最適化。スプリンガー。ISBN 978-0-387-25453-1。
• ベッカー、ベルント。ロルフ・ドレクスラー (1998)。二分決定図: 理論と実装。スプリンガー。ISBN 978-1-4419-5047-5。

ウィキメディア・コモンズには、二分決定図に関連するメディアがあります。

• 二分決定図 (BDD) を楽しむ、ドナルド・クヌースによる講義
• いくつかのプログラミング言語用の BDD ソフトウェア ライブラリのリスト。