二項決定図

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

類似のデータ構造としては、否定標準形（NNF）、ジェガルキン多項式、命題有向非巡回グラフ（PDAG）などがある。

意味

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

同型な部分グラフをすべてマージする。
2つの子ノードが同型であるノードはすべて削除する。

一般的に、BDDという用語は、ほぼ常に縮小順序付き二分決定図(文献ではROBDDと呼ばれ、順序付けと縮小の側面を強調する必要がある場合に使用されます) を指します。ROBDD の利点は、特定の関数と変数の順序に対して正準 (同型を除いて一意) であることです。 ^{[ 1 ]}この特性により、関数の等価性チェックや、関数テクノロジーマッピングなどの他の操作に役立ちます。

ルートノードから1端子へのパスは、（部分的な場合もある）変数割り当てを表し、その割り当てに対応するブール関数は真となります。パスがノードから下位（または上位）の子ノードに降りていくと、そのノードの変数には0（または1）が割り当てられます。

例

下の左図は、関数を表す二分決定木（縮約ルールは適用されていない）と真理値表を示しています。 $f(x_{1},x_{2},x_{3})$ 左側のツリーでは、関数の値は、グラフを下って終端までパスをたどることで、特定の変数割り当てに対して決定できます。下の図では、点線は下位の子へのエッジを表し、実線は上位の子へのエッジを表します。したがって、を見つけるには $f(0,1,1)$ _{x 1}から始め、点線に沿って x ₂まで進み(x ₁には0 が割り当てられているため)、次に実線を 2 つ下ります (x ₂と x ₃にはそれぞれ 1 が割り当てられているため)。これにより、ターミナル 1 に到達します。これは、次の値です。 $f(0,1,1)$ 。

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

このブール関数を記述する別の表記法は次のとおりです。 ${\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 の例図を右側に示します。これは、上の図に示されているのと同じブール式を表しています。 $(\neg x_{1}\wedge \neg x_{2}\wedge \neg x_{3})\vee (x_{1}\wedge x_{2})\vee (x_{2}\wedge x_{3})$ 低いエッジは破線、高いエッジは実線で表示され、補完エッジは始点に円で示されます。@記号が付いたノードはBDDへの参照を表し、つまり参照エッジはこのノードから始まるエッジです。

歴史

データ構造が作成された基本的なアイデアは、シャノン展開です。スイッチング関数は、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 つの概念を適用すると、集合と関係を表現するための効率的なデータ構造とアルゴリズムが得られます。^[¹⁰^]^[¹¹^]共有を複数の BDD に拡張することで、つまり 1 つのサブグラフが複数の BDD で使用されることで、共有縮小順序付き二分決定図というデータ構造が定義されます。^[²^]現在では、BDD という概念は、一般的にその特定のデータ構造を指すために使用されています。

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

アドナン・ダーウィッシュとその共同研究者たちは、BDD（ブール演算データ）がブール関数の正規形の一つであり、それぞれ異なる要件の組み合わせによって生成されることを示した。ダーウィッシュが特定したもう一つの重要な正規形は、分解可能な否定正規形（DNNF）である。

アプリケーション

BDDは、 CADソフトウェアで回路合成（論理合成）や形式検証、ネットワーク検証に広く使用されています。BDDには、フォールトツリー解析、ベイズ推論、製品構成、プライベート情報検索など、あまり知られていないアプリケーションがいくつかあります。^{[ 13 ]}^{[ 14 ]}

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

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

変数の順序付け

BDDのサイズは、表現される関数と変数の順序によって決まります。ブール関数が存在します。 $f(x_{1},\ldots ,x_{n})$ 変数の順序によっては、ノード数が最良の場合は線形（ nに関して）、最悪の場合は指数関数的になるグラフが得られることになる（例：リップルキャリー加算器）。ブール関数を考えてみよう。 $f(x_{1},\ldots ,x_{2n})=x_{1}x_{2}+x_{3}x_{4}+\cdots +x_{2n-1}x_{2n}.$ 変数順序付けを使用する $x_{1}<x_{3}<\cdots <x_{2n-1}<x_{2}<x_{4}<\cdots <x_{2n}$ BDDには $2^{n+1}$ 関数を表すノード。順序付けを使用する $x_{1}<x_{2}<x_{3}<x_{4}<\cdots <x_{2n-1}<x_{2n}$ BDDは以下から構成される。 $2n+2$ ノード。

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

変数の順序に関係なく、グラフのサイズが常に指数関数的になる関数が存在する。これは、例えば乗算関数に当てはまる。^{[ 1 ]}実際、2つの積の中間ビットを計算する関数は、 $n$ -ビット数には、より小さいOBDDがありません $2^{\lfloor n/2\rfloor }/61-4$ 頂点。^{[ 19 ]}（乗算関数が多項式サイズのOBDDを持つ場合、整数因数分解が P/polyにあることを示すことになるが、これは真であるとは知られていない。^{[ 20 ]}）もう1つの悪名高い例は、指数サイズのBDDを持つ最も単純な関数と見なされている隠れ重みビット関数である。^{[ 21 ]}

研究者たちは、BDDデータ構造の改良を提案しており、以下のような関連グラフがいくつか提案されている。

BMD（バイナリモーメント図）
ZDD（ゼロ抑制決定図）
FBDD（自由二分決定図）とは、ルートからリーフノードまでのどのパスでも、各変数を最大で1回しか読み取らない図のことです。OBDDはすべてFBDDです。
FDD（機能決定図）
MDD（多値決定図）は、決定変数が2つ以上の値をとることを可能にすることでBDDを一般化したものであり、^{[ 22 ]}
PDD（パリティ決定図）
MTBDD（マルチターミナルBDD）、
TDD（三項決定図）では、「未知」の分岐を追加することで、連続する和集合/論理和演算を遅延させ、指数関数的なサイズ増加を回避します。^{[ 23 ]}
NDD（ネットワーク決定図）

BDDに対する論理演算

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

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

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

ブール式の充足可能な割り当ての数を数えるモデルカウントは、BDD（ブール表示展開）の場合は多項式時間で実行できます。しかし、一般的な命題論理式の場合、この問題は♯P完全であり、既知の最良のアルゴリズムでも最悪の場合には指数時間が必要となります。

参考文献

1 2 Bryant, Randal E. (1986 年 8 月). "グラフベースのブール関数操作アルゴリズム" (PDF) . IEEE Transactions on Computers . C-35 (8): 677– 691. CiteSeerX 10.1.1.476.2952 . doi : 10.1109/TC.1986.1676819 . S2CID 10385726 .
1 2 Brace, Karl S.; Rudell, Richard L.; Bryant, Randal E. (1990). "Efficient Implementation of a BDD Package". Proceedings of the 27th ACM/IEEE Design Automation Conference (DAC 1990) . IEEE Computer Society Press. pp. 40–45 . doi : 10.1145/123186.123222 . ISBN 978-0-89791-363-8。
↑ Somenzi, Fabio (1999). "二分決定図" (PDF) .計算システム設計. NATO Science Series F: コンピュータおよびシステム科学. Vol. 173. IOS Press. pp. 303–366 . ISBN 978-90-5199-459-9。
↑ Jean-Christophe Madre; Jean-Paul Billon (1988). "Proving Circuit Correctness Using Formal Comparison Between Expected and Extracted Behaviour". Proceedings of the 25th ACM/IEEE Conference on Design Automation, DAC '88, Anaheim, CA, USA, June 12-15, 1988. pp. 205–210 . doi : 10.1109/DAC.1988.14759 . ISBN 0-8186-0864-1。
↑ Knuth, DE (2009). Fascicle 1: Bitwise tricks & techniques; Binary Decision Diagrams . The Art of Computer Programming . Vol. 4. Addison–Wesley. ISBN 978-0-321-58050-4。第1b巻草稿（ 2016年3月12日アーカイブ）はWayback Machineからダウンロード可能です。
↑ Lee, CY (1959). "バイナリ決定プログラムによるスイッチング回路の表現". Bell System Technical Journal . 38 (4): 985–999 . doi : 10.1002/j.1538-7305.1959.tb01585.x .
↑ Akers, Jr., Sheldon B (1978年6月). "二分決定図". IEEE Transactions on Computers . C-27 (6): 509–516 . doi : 10.1109/TC.1978.1675141 . S2CID 21028055 .
↑ Boute, Raymond T. (1976年1月). 「プログラム可能なコントローラとしてのバイナリ決定マシン」. EUROMICROニュースレター. 1 (2): 16– 22. doi : 10.1016/0303-1268(76)90033-X .
↑マムルコフ、ユ. V. (1984).非周期回路と非同期プロセスの解析(博士論文). レニングラード電気工学研究所.
↑ Bryant., Randal E. (1986). "Graph-Based Algorithms for Boolean Function Manipulation" (PDF) . IEEE Transactions on Computers . C-35 (8): 677– 691. doi : 10.1109/TC.1986.1676819 . S2CID 10385726 .
↑ Bryant, Randal E. (1992 年 9 月). "順序付き二分決定図による記号的ブール操作" . ACM Computing Surveys . 24 (3): 293– 318. doi : 10.1145/136035.136043 . S2CID 1933530 .
↑ 「スタンフォード大学専門能力開発センター」 . scpd.stanford.edu . 2014年6月4日にオリジナルからアーカイブ済み。2018年4月23日に取得。
↑ Jensen, RM (2004). "CLab: 高速でバックトラック不要の対話型製品構成のためのC++ライブラリ" .第10回制約プログラミングの原理と実践に関する国際会議議事録. Lecture Notes in Computer Science. Vol. 3258. Springer. p. 816. doi : 10.1007/978-3-540-30201-8_94 . ISBN 978-3-540-30201-8。
↑ Lipmaa, HL (2009). "データ依存計算を用いた初のCPIRプロトコル" (PDF) .国際情報セキュリティ・暗号学会議. コンピュータサイエンス講義録. 第5984巻. Springer. pp. 193–210 . doi : 10.1007/978-3-642-14423-3_14 . ISBN 978-3-642-14423-3。
↑ Whaley, John; Avots, Dzintars; Carbin, Michael; Lam, Monica S. (2005). "Using Datalog with Binary Decision Diagrams for Program Analysis" . Yi, Kwangkeun (編). Programming Languages and Systems . Lecture Notes in Computer Science. Vol. 3780. Berlin, Heidelberg: Springer. pp. 97–118 . doi : 10.1007/11575467_8 . ISBN 978-3-540-32247-4. S2CID 5223577 .
↑ Bollig, Beate; Wegener, Ingo (1996 年 9 月). "OBDD の変数順序の改善は NP 完全である". IEEE Transactions on Computers . 45 (9): 993–1002 . doi : 10.1109/12.537122 .
↑ Sieling, Detlef (2002). "OBDD最小化の非近似可能性" .Information and Computation . 172 (2): 103–138 . doi : 10.1006/inco.2001.3076 .
↑ Rice, Michael. "効率的な BDD/MDD 構築のための静的変数順序付けヒューリスティックの調査" (PDF)。
↑ Woelfel, Philipp (2005). "ユニバーサルハッシュによる整数乗算のOBDDサイズの上限" . Journal of Computer and System Sciences . 71 (4): 520– 534. CiteSeerX 10.1.1.138.6771 . doi : 10.1016/j.jcss.2005.05.004 .
↑リチャード・J・リプトン。「BDDと因数分解」。ゲーデルの失われた手紙とP=NP、2009年。
↑ Méaux, Pierrick; Seuré, Tim; Deng, Tang (2024). "The Revisited Hidden Weight Bit Function" (PDF) . IACR Cryptology ePrint Archive : 24 . 2025-06-19に取得.
↑ Miller, D. Michael; Drechsler, Rolf (1998). "多値決定図の構築について". Proceedings of the 28th IEEE International Symposium on Multiple-Valued Logic (ISMVL) . pp. 264–269 . doi : 10.1109/ISMVL.1998.679191 .
↑
- Duboc, Guillaume (2026-01-19).集合論的型を用いた動的言語の型付け：Elixirの事例（博士論文）。パリ・シテ大学。
- Valim, José (2025-12-02). "集合論的型のためのレイジー二分決定図 (BDD)" . Elixir プログラミング言語.
↑ Andersen, HR (1999). 「二分決定図入門」(PDF) .講義ノート. コペンハーゲンIT大学。
↑ Huth, Michael; Ryan, Mark (2004). Logic in computer science: modelling and reasoning about systems (2nd ed.). Cambridge University Press. pp. 380–. ISBN 978-0-52154310-1OCLC 54960031

さらに読む

Ubar, R. (1976). 「代替グラフを用いたデジタル回路のテスト生成」.タリン工科大学紀要（ロシア語）（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ソフトウェアライブラリの一覧。

[Bryant1986-1] 1 2 Bryant, Randal E. (1986 年 8 月). "グラフベースのブール関数操作アルゴリズム" (PDF) . IEEE Transactions on Computers . C-35 (8): 677– 691. CiteSeerX 10.1.1.476.2952 . doi : 10.1109/TC.1986.1676819 . S2CID 10385726 .

[Brace-2] 1 2 Brace, Karl S.; Rudell, Richard L.; Bryant, Randal E. (1990). "Efficient Implementation of a BDD Package". Proceedings of the 27th ACM/IEEE Design Automation Conference (DAC 1990) . IEEE Computer Society Press. pp. 40–45 . doi : 10.1145/123186.123222 . ISBN 978-0-89791-363-8。

[Somenzi1999-3] Somenzi, Fabio (1999). "二分決定図" (PDF) .計算システム設計. NATO Science Series F: コンピュータおよびシステム科学. Vol. 173. IOS Press. pp. 303–366 . ISBN 978-90-5199-459-9。

[MB88-4] Jean-Christophe Madre; Jean-Paul Billon (1988). "Proving Circuit Correctness Using Formal Comparison Between Expected and Extracted Behaviour". Proceedings of the 25th ACM/IEEE Conference on Design Automation, DAC '88, Anaheim, CA, USA, June 12-15, 1988. pp. 205–210 . doi : 10.1109/DAC.1988.14759 . ISBN 0-8186-0864-1。

[Knuth-5] Knuth, DE (2009). Fascicle 1: Bitwise tricks & techniques; Binary Decision Diagrams . The Art of Computer Programming . Vol. 4. Addison–Wesley. ISBN 978-0-321-58050-4。第1b巻草稿（ 2016年3月12日アーカイブ）はWayback Machineからダウンロード可能です。

[Lee-6] Lee, CY (1959). "バイナリ決定プログラムによるスイッチング回路の表現". Bell System Technical Journal . 38 (4): 985–999 . doi : 10.1002/j.1538-7305.1959.tb01585.x .

[Akers-7] Akers, Jr., Sheldon B (1978年6月). "二分決定図". IEEE Transactions on Computers . C-27 (6): 509–516 . doi : 10.1109/TC.1978.1675141 . S2CID 21028055 .

[Boute_1976-8] Boute, Raymond T. (1976年1月). 「プログラム可能なコントローラとしてのバイナリ決定マシン」. EUROMICROニュースレター. 1 (2): 16– 22. doi : 10.1016/0303-1268(76)90033-X .

[9] マムルコフ、ユ. V. (1984).非周期回路と非同期プロセスの解析(博士論文). レニングラード電気工学研究所.

[Bryant-1986-10] Bryant., Randal E. (1986). "Graph-Based Algorithms for Boolean Function Manipulation" (PDF) . IEEE Transactions on Computers . C-35 (8): 677– 691. doi : 10.1109/TC.1986.1676819 . S2CID 10385726 .

[Bryant-1992-11] Bryant, Randal E. (1992 年 9 月). "順序付き二分決定図による記号的ブール操作" . ACM Computing Surveys . 24 (3): 293– 318. doi : 10.1145/136035.136043 . S2CID 1933530 .

[Stanford-12] 「スタンフォード大学専門能力開発センター」 . scpd.stanford.edu . 2014年6月4日にオリジナルからアーカイブ済み。2018年4月23日に取得。

[Jensen-13] Jensen, RM (2004). "CLab: 高速でバックトラック不要の対話型製品構成のためのC++ライブラリ" .第10回制約プログラミングの原理と実践に関する国際会議議事録. Lecture Notes in Computer Science. Vol. 3258. Springer. p. 816. doi : 10.1007/978-3-540-30201-8_94 . ISBN 978-3-540-30201-8。

[Lipmaa-14] Lipmaa, HL (2009). "データ依存計算を用いた初のCPIRプロトコル" (PDF) .国際情報セキュリティ・暗号学会議. コンピュータサイエンス講義録. 第5984巻. Springer. pp. 193–210 . doi : 10.1007/978-3-642-14423-3_14 . ISBN 978-3-642-14423-3。

[15] Whaley, John; Avots, Dzintars; Carbin, Michael; Lam, Monica S. (2005). "Using Datalog with Binary Decision Diagrams for Program Analysis" . Yi, Kwangkeun (編). Programming Languages and Systems . Lecture Notes in Computer Science. Vol. 3780. Berlin, Heidelberg: Springer. pp. 97–118 . doi : 10.1007/11575467_8 . ISBN 978-3-540-32247-4. S2CID 5223577 .

[Bollig-16] Bollig, Beate; Wegener, Ingo (1996 年 9 月). "OBDD の変数順序の改善は NP 完全である". IEEE Transactions on Computers . 45 (9): 993–1002 . doi : 10.1109/12.537122 .

[Sieling-17] Sieling, Detlef (2002). "OBDD最小化の非近似可能性" .Information and Computation . 172 (2): 103–138 . doi : 10.1006/inco.2001.3076 .

[Rice-18] Rice, Michael. "効率的な BDD/MDD 構築のための静的変数順序付けヒューリスティックの調査" (PDF)。

[Woelfel_2005-19] Woelfel, Philipp (2005). "ユニバーサルハッシュによる整数乗算のOBDDサイズの上限" . Journal of Computer and System Sciences . 71 (4): 520– 534. CiteSeerX 10.1.1.138.6771 . doi : 10.1016/j.jcss.2005.05.004 .

[Lipton_2009-20] リチャード・J・リプトン。「BDDと因数分解」。ゲーデルの失われた手紙とP=NP、2009年。

[21] Méaux, Pierrick; Seuré, Tim; Deng, Tang (2024). "The Revisited Hidden Weight Bit Function" (PDF) . IACR Cryptology ePrint Archive : 24 . 2025-06-19に取得.

[22] Miller, D. Michael; Drechsler, Rolf (1998). "多値決定図の構築について". Proceedings of the 28th IEEE International Symposium on Multiple-Valued Logic (ISMVL) . pp. 264–269 . doi : 10.1109/ISMVL.1998.679191 .

[23] 
Duboc, Guillaume (2026-01-19).集合論的型を用いた動的言語の型付け：Elixirの事例（博士論文）。パリ・シテ大学。
Valim, José (2025-12-02). "集合論的型のためのレイジー二分決定図 (BDD)" . Elixir プログラミング言語.

[mwApc] Duboc, Guillaume (2026-01-19).集合論的型を用いた動的言語の型付け：Elixirの事例（博士論文）。パリ・シテ大学。

[mwApw] Valim, José (2025-12-02). "集合論的型のためのレイジー二分決定図 (BDD)" . Elixir プログラミング言語.

[Andersen_1999-24] Andersen, HR (1999). 「二分決定図入門」(PDF) .講義ノート. コペンハーゲンIT大学。

[Huth-25] Huth, Michael; Ryan, Mark (2004). Logic in computer science: modelling and reasoning about systems (2nd ed.). Cambridge University Press. pp. 380–. ISBN 978-0-52154310-1OCLC 54960031

[ 1 ]

[ 2 ]

[ 3 ]

[ 4 ]

[ 5 ]

[ 6 ]

[ 7 ]

これらの著者とは独立して、Yu. V. Mamrukov は、速度に依存しない回路の分析用の CAD で、「標準ブラケット形式」という名前の BDD を実現しました [ 9 ]

構造に基づく

[

[

[

[ 13 ]

[ 14 ]

[ 15 ]

[ 16 ]

[

[

[ 19 ]

[ 20 ]

[ 21 ]

[ 22 ]

[ 23 ]

[ 24 ]

[ 25 ]

意味

例