Binary Decision Diagram
完全解説

1. BDD の全体像

BDD、特に Reduced Ordered Binary Decision Diagram、すなわち ROBDD は、Boolean 関数を圧縮して表す標準的な記号的データ構造である。入力変数に従って二分岐する決定木を、有向非巡回グラフ、DAG、に畳み込み、さらに冗長な節点を除去することで、しばしば真理値表よりも桁違いに小さくなる。

BDD が解いている問題

Boolean 関数は真理値表で表すと \(2^n\) 行が必要である。論理式で表すと式の構文上の冗長性が残る。BDD は同じ部分関数を共有することで、関数そのものの再利用構造を明示する。たとえば、同じ残りの条件判定が複数箇所で現れる場合、決定木では同じ部分木が繰り返されるが、BDD では 1 つの部分 DAG に共有される。

BDD の表現対象

BDD は単一の Boolean 関数だけでなく、集合、関係、遷移関係、整数制約、回路の出力、状態集合などを Boolean encoding したものも表せる。集合 \(S \subseteq \{0,1\}^n\) は特性関数 \(\chi_S\) によって BDD 化できる。

この見方により、集合演算は BDD の Boolean 演算に変換される。和集合は OR、積集合は AND、補集合は NOT、射影は存在量化に対応する。

2. 数理的基礎

2.1 Boolean 関数と代入

変数集合 \(X=\{x_0,x_1,\ldots,x_{n-1}\}\) に対し、代入は写像 \(\alpha:X\to\{0,1\}\) である。BDD の任意の根ノード \(u\) は Boolean 関数 \(F_u\) を表す。\(F_u(\alpha)\) は、根から出発して各節点の変数値を見ながら low/high 枝をたどり、到達した終端値で定義される。

2.2 コファクタ

Boolean 関数 \(f\) の変数 \(x_i\) に関する low cofactor と high cofactor を次のように定義する。

すなわち、\(x_i\) に値を固定した後に残る関数である。BDD の low 枝と high 枝は、このコファクタを直接表す。

2.3 Shannon 展開

任意の Boolean 関数は任意の変数 \(x_i\) について Shannon 展開できる。

ITE、if-then-else、を使うと、同じ式はより BDD 的に書ける。

BDD の内部節点 \((x_i, low, high)\) はまさに次の関数を表す。

2.4 決定木から BDD へ

全変数について順に分岐する完全決定木は、葉が \(2^n\) 個ある。BDD は次の 2 種類の圧縮を行う。

2.5 終端と内部節点の意味

終端 \(\bot\) は偽、終端 \(\top\) は真を表す。

内部節点 \(u\) が変数 \(x_i\) を持ち、low 子を \(l\)、high 子を \(h\) とすると、

この定義により、BDD の節点は単なるグラフの点ではなく、「その節点から下の部分関数」の代表になる。

3. BDD / OBDD / ROBDD

ROBDD の 2 つの reduction 規則

ROBDD は次の 2 規則を飽和的に適用した OBDD である。

1. 冗長節点削除: low 子と high 子が同じ節点なら、その内部節点を削除する。
2. 同型節点共有: 同じ変数 index、同じ low 子、同じ high 子を持つ節点は 1 つだけ保持する。

正規性

変数順序 \(x_{\pi(0)} \prec x_{\pi(1)} \prec \cdots \prec x_{\pi(n-1)}\) を固定する。すべての内部節点がこの順序に従い、上の 2 reduction 規則が適用された BDD では、各 Boolean 関数に対して一意な ROBDD が存在する。したがって、同じ manager 内では「根ノード ID が同じかどうか」が関数同値性の高速な判定になる。

4. 変数 index と BDD の不変条件

BDD の実装で最も誤解されやすく、かつ最も重要なのが変数 index である。index は変数順序を整数で表したものであり、ノード番号でも、作成順でも、配列中のたまたまの位置でもない。

4.1 index の定義

変数集合 \(X\) に対して、BDD manager は全順序を保持する。

これを整数で表す写像を index と呼ぶ。

たとえば変数順序が \([b,d,a,c]\) なら、\(\operatorname{idx}(b)=0\)、\(\operatorname{idx}(d)=1\)、\(\operatorname{idx}(a)=2\)、\(\operatorname{idx}(c)=3\) である。

4.2 node id、variable id、index、level の違い

4.3 OBDD の edge invariant

終端の index を \(\infty\) とみなす。内部節点 \(u\) の変数を \(\operatorname{var}(u)\)、子を \(low(u), high(u)\) とする。OBDD の合法性は次の条件で表せる。

子が終端の場合は \(\infty\) と解釈するため、常にこの不等式を満たす。この不変条件により、根から葉への任意の path では index が単調増加する。したがって同じ変数が同一 path 上に 2 回現れない。

4.4 変数が skip されること

ROBDD では、ある関数が特定の変数に依存しない場合、その変数の節点は現れない。たとえば \(f(a,b,c)=a\lor c\) は \(b\) に依存しない。変数順序が \([a,b,c]\) でも、根から葉への path は \(a\to c\) のように \(b\) を飛ばすことがある。

これは不正ではない。edge invariant は「子の index が親より大きい」ことだけを要求し、「次の index が必ず現れる」ことは要求しない。

4.5 根の index が 0 であるとは限らない

関数 \(f(x_0,x_1,x_2)=x_2\) を順序 \([x_0,x_1,x_2]\) で ROBDD 化すると、根は \(x_2\) の節点になる。\(x_0\) と \(x_1\) は関数に影響しないため削除される。よって root index は 2 になりうる。

4.6 同じグラフ形状でも index が違えば別の関数

節点構造だけを見ると同じでも、ラベルの index が異なれば意味は変わる。節点 \((i,0,1)\) は変数 \(x_i\) 自身を表す。もし \(i=0\) なら \(x_0\)、\(i=3\) なら \(x_3\) である。

したがって BDD を比較・合成・serialize する際には、node の形だけでなく、variable id と index map を同時に扱う必要がある。

4.7 「固定された index map」が正規性の前提

ROBDD の一意性は、同じ変数順序を使う場合にのみ成立する。順序 \([a,b,c]\) で作った BDD と順序 \([b,a,c]\) で作った BDD は、同じ関数を表していても根ノードが一致しない。別 manager 間のポインタ比較で同値性を判定してはいけない。

5. reduction と unique table

5.1 mk 操作

BDD 実装の中心は mk である。mk(i,l,h) は「変数 index \(i\)、low 子 \(l\)、high 子 \(h\) を持つ節点を作る」操作だが、実際には reduction を同時に行う。

mk(i, low, high):
    if low == high:
        return low
    key = (i, low, high)
    if key in unique_table:
        return unique_table[key]
    u = allocate_node(i, low, high)
    unique_table[key] = u
    return u

この一見単純な処理が、ROBDD の共有と正規化を保証する。

5.2 unique table の key

unique table の key は必ず \((index, low, high)\) でなければならない。変数名を使う場合でも、その変数名が manager 内の index map と一貫している必要がある。

5.3 computed table

unique table が「節点の一意化」を担うのに対し、computed table は「演算結果のメモ化」を担う。Apply、ITE、restrict、quantification などは再帰的に同じ部分問題を何度も解くため、computed table がないと指数的に再計算することがある。

5.4 正規性の直観的証明

固定変数順序の下で Boolean 関数 \(f\) を考える。\(f\) が定数関数なら、表現は終端 \(0\) または \(1\) だけである。定数でないなら、順序上もっとも小さい index の依存変数 \(x_i\) が一意に決まる。Shannon 展開により \(f\) は \(f_{x_i=0}\) と \(f_{x_i=1}\) で一意に決まる。帰納法でそれらの ROBDD が一意なら、\((i,low,high)\) も unique table により一意である。low と high が同じなら \(x_i\) に依存していないので削除される。したがって ROBDD は一意である。

6. BDD の構築法

6.1 真理値表からの構築

もっとも直接的な方法は、変数順序に沿って完全決定木を作り、各内部節点で mk を呼ぶ方法である。

build(level, assignment):
    if level == n:
        return terminal(f(assignment))
    x = order[level]
    assignment[x] = 0
    low = build(level + 1, assignment)
    assignment[x] = 1
    high = build(level + 1, assignment)
    remove assignment[x]
    return mk(index(x), low, high)

この方法は概念的には明快だが、最悪で \(2^n\) 個の葉を評価する。実務では、論理式や回路を構成要素ごとに BDD 化し、Apply や ITE で合成することが多い。

6.2 変数節点からの構築

変数 \(x_i\) 自身の BDD は、low が 0、high が 1 の節点である。

式 \((a\land b)\lor c\) は、まず \(BDD(a),BDD(b),BDD(c)\) を作り、Apply AND、Apply OR で合成できる。

6.3 ITE による構築

BDD の内部節点は ITE そのものであるため、あらゆる Boolean 演算は ITE から表せる。

6.4 構築時の index の役割

構築再帰の level は変数順序上の位置である。level=0 なら最上位変数、level=1 なら次の変数を分岐する。ここで使う順序が BDD の index map であり、mk に渡す index も同じ map に従う必要がある。

式の構文順、たとえば \((c\land a)\lor b\) に現れる順序は、BDD の index とは関係がない。BDD では manager が定めた順序だけが正しい順序である。

7. BDD 操作の詳細

BDD 操作は「Shannon 展開を、index の小さい変数から同期的に進める」こととして理解できる。ほとんどの操作は、top variable を選び、low/high cofactor に再帰し、最後に mk で正規化する。

7.1 top、cofactor、terminal

節点 \(u\) に対して、\(top(u)\) は \(u\) の根変数 index である。終端の top は \(\infty\) とする。

変数 index \(i\) で節点 \(u\) を分解する関数を次のように定義する。

この定義が重要である。もし \(u\) の top が \(i\) より大きいなら、\(u\) は \(x_i\) に依存していないので low/high の両方で同じ \(u\) を返す。

7.2 Apply: 二項 Boolean 演算

Apply は \(u\) と \(v\) が表す関数 \(F_u,F_v\) に、AND、OR、XOR、IMPLIES などの二項演算 \(\odot\) を適用し、\(F_u\odot F_v\) の BDD を返す。

apply(op, u, v):
    if (op, u, v) in computed_table:
        return computed_table[(op, u, v)]

    if u and v are terminals:
        return terminal(eval(op, value(u), value(v)))

    i = min(top(u), top(v))

    u0 = (top(u) == i) ? low(u)  : u
    u1 = (top(u) == i) ? high(u) : u
    v0 = (top(v) == i) ? low(v)  : v
    v1 = (top(v) == i) ? high(v) : v

    low  = apply(op, u0, v0)
    high = apply(op, u1, v1)
    r = mk(i, low, high)
    computed_table[(op, u, v)] = r
    return r

Apply の数理

\(i=\min(top(u),top(v))\) とすると、結果関数 \(r=F_u\odot F_v\) の \(x_i\) に関する cofactor は、各入力関数の cofactor に演算を適用したものになる。

最後に \(\operatorname{mk}(i,r_0,r_1)\) を呼ぶことで、\(r_0=r_1\) の場合は自動的に節点が消え、同型節点は共有される。

Apply の計算量

computed table が十分に働く場合、二項 Apply の部分問題は高々 \(|u|\cdot|v|\) 個である。ここで \(|u|\) は \(u\) から到達可能な節点数である。したがって典型的な上界は次のように書ける。

ただし、結果 BDD が大きくなる場合は、その生成自体に時間とメモリを要する。

7.3 NOT

NOT は一項演算である。単純実装では全節点をたどり、終端 0 と 1 を入れ替える。

not(u):
    if u == 0: return 1
    if u == 1: return 0
    if u in cache: return cache[u]
    r = mk(top(u), not(low(u)), not(high(u)))
    cache[u] = r
    return r

実用的な BDD パッケージでは complement edge を用いて、ポインタの 1 bit で否定を表すことが多い。この場合 \(\neg u\) は節点を作らず、補数マークを反転するだけで表せる。ただし unique table の正規化では、補数付きポインタの正規化規則が必要になる。

7.4 ITE

\(\operatorname{ITE}(f,g,h)\) は、\(f\) が真なら \(g\)、偽なら \(h\) を返す関数である。

ite(f, g, h):
    if f == 1: return g
    if f == 0: return h
    if g == h: return g
    if g == 1 and h == 0: return f

    if (f,g,h) in computed_table:
        return computed_table[(f,g,h)]

    i = min(top(f), top(g), top(h))
    low  = ite(cof(f,i,0), cof(g,i,0), cof(h,i,0))
    high = ite(cof(f,i,1), cof(g,i,1), cof(h,i,1))
    r = mk(i, low, high)
    computed_table[(f,g,h)] = r
    return r

ITE は汎用性が高く、多くの BDD パッケージで基本演算として採用される。二項 Apply は ITE で実装でき、逆に ITE は Apply と NOT で実装できる。

7.5 Restrict: 変数への値の固定

restrict は関数 \(f\) において特定の変数 \(x_i\) を値 \(b\in\{0,1\}\) に固定する。

restrict(u, i, b):
    if u is terminal: return u
    if top(u) > i:
        return u                 # u does not depend on x_i
    if top(u) == i:
        return restrict(b ? high(u) : low(u), i, b)
    low  = restrict(low(u),  i, b)
    high = restrict(high(u), i, b)
    return mk(top(u), low, high)

ここでも index が鍵である。\(top(u)>i\) なら、\(u\) の下には index \(i\) の変数は現れない。なぜなら path 上の index は単調増加するからである。したがってその節点以下は探索不要である。

7.6 Compose / Substitute: 変数を関数で置換

compose は \(f\) の変数 \(x_i\) を別の BDD \(g\) で置換する操作である。

Shannon 展開により、\(x_i\) の節点に到達したとき、low 側と high 側を \(g\) で選択すればよい。

単一変数置換は比較的単純だが、複数変数を同時置換する場合は順序と依存関係に注意が必要である。逐次置換では \(x\leftarrow y, y\leftarrow x\) のような swap が意図と異なる結果になるため、同時置換を明示的に実装する。

7.7 Existential / Universal Quantification

Boolean 関数の存在量化と全称量化は、cofactor の OR / AND で定義される。

exists(u, i):
    if u is terminal: return u
    if top(u) > i:
        return u
    if top(u) == i:
        return apply(OR, low(u), high(u))
    low  = exists(low(u), i)
    high = exists(high(u), i)
    return mk(top(u), low, high)

複数変数集合 \(S\) を量化する場合、各節点で \(top(u)\in S\) なら low/high を OR で結合し、\(top(u)\notin S\) なら同じ変数で節点を再構築する。

7.8 Relational product

記号的モデル検査では、状態集合や遷移関係を BDD で表し、次状態集合を計算する。典型的な操作が relational product である。

単純に AND を作ってから存在量化すると中間 BDD が巨大になることがある。そのため実装では andExists のように、AND と量化を再帰内で融合する。

7.9 SAT、TAUT、同値性

7.10 satisfying assignment の 1 つを取り出す

根から 1 終端に向かう path を 1 本選べば、充足代入が得られる。ただし skip された変数は don't care である。

anySat(u):
    if u == 0: fail
    if u == 1: return {}
    if high(u) != 0:
        return {var(u)=1} ∪ anySat(high(u))
    else:
        return {var(u)=0} ∪ anySat(low(u))

7.11 SatCount: 充足代入数の数え上げ

SatCount では skip された変数を正しく数える必要がある。変数数を \(n\)、節点 \(u\) を評価する現在 level を \(\ell\) とする。終端 1 に到達したら、残りの変数はすべて自由なので \(2^{n-\ell}\) 通りである。

内部節点 \(u\) の index を \(i=top(u)\) とする。\(\ell\) から \(i-1\) までの変数はこの BDD で skip されており自由である。したがって、

根の充足数は \(C(root,0)\) である。ここで \(root\) の index が 0 でなくても式は成立し、その分だけ先頭の skip 変数が \(2^{top(root)}\) 倍として数えられる。

7.12 Support

関数 \(f\) が実際に依存する変数集合を support という。BDD 上では到達可能な内部節点の変数集合として求められる。

ROBDD では冗長節点が削除されているため、到達可能内部節点に現れる変数は support に含まれる。ただし complement edge などを使う実装では、節点参照の正規化に注意する。

7.13 Variable renaming / permutation

変数 renaming は、関数 \(f(x_0,x_1,\ldots)\) の変数名を別の変数名に変える操作である。単なる node label の書き換えではない。書き換え後にも OBDD の index invariant が成り立たなければならないため、多くの場合は再帰的に再構築し、mk を通す必要がある。

特に動的 reordering を持つ manager では、variable id と current index が別概念である。renaming は variable id の対応を変える操作であり、reordering は variable id の index を変える操作である。この 2 つを混同してはいけない。

8. 操作と変数 index の関係を深掘りする

BDD の演算は「どの変数で今分岐するか」を index で決める。ここを誤ると、見た目は DAG でも、ROBDD ではなくなり、正規性・キャッシュ・同値性判定が破綻する。

8.1 Apply の top variable 選択

Apply では、入力節点 \(u,v\) の top index の小さい方を次に処理する。

この規則は、結果 BDD の根が変数順序を破らないために必要である。もし \(top(u)=3\)、\(top(v)=1\) なら、結果はまず index 1 の変数で分岐すべきであり、index 3 の変数を先に置いてはいけない。

8.2 片方だけが top variable を持つ場合

\(top(u)=i\)、\(top(v)>i\) の場合、\(v\) は \(x_i\) に依存しない。このとき cofactor は次のようになる。

つまり再帰は次の形になる。

ここで誤って \(v\) の low/high を取ろうとすると、存在しない変数分岐を強制することになり、意味が壊れる。

8.3 index が等しい場合

\(top(u)=top(v)=i\) の場合、両方を同じ変数で同期的に分解する。

この同期分解が、Shannon 展開と整合する。

8.3.1 Apply の具体的な完全トレース: 引数順ではなく index 順に分解する

変数順序を \([a,b]\)、すなわち \(idx(a)=0, idx(b)=1\) とする。\(u=b\)、\(v=a\) に対して \(u\land v\) を計算する。注意すべき点は、関数呼び出しの第 1 引数 \(u\) の top は \(b\) だが、結果の top は \(a\) でなければならないことである。

もしここで「第 1 引数の top を優先する」という誤った規則を使うと、\(b\) を \(a\) より上に置いた結果を作り、順序 \([a,b]\) の OBDD ではなくなる。Apply は交換可能な AND であっても、再帰の分解順は必ず index map に従う。

8.3.2 index invariant checker

実装中は、デバッグ用に次の検査を頻繁に走らせるとよい。これは ROBDD の完全検証ではないが、index に関する多くの破壊を検出できる。

check(u):
    visited = set()
    dfs(u):
        if u is terminal or u in visited: return
        visited.add(u)
        assert low(u)  is terminal or top(u) < top(low(u))
        assert high(u) is terminal or top(u) < top(high(u))
        assert unique_table[(top(u), low(u), high(u))] == u
        assert low(u) != high(u)          # reduced rule
        dfs(low(u))
        dfs(high(u))

この検査は「各 edge が index を増加させる」「low=high の冗長節点が残っていない」「unique table と節点実体が矛盾しない」ことを確認する。特に Apply、rename、import、dynamic reordering の直後に有効である。

8.4 終端の index は \(\infty\)

終端に変数はない。Apply で片方が終端、もう片方が内部節点なら、内部節点の top が選ばれる。

この convention により、terminal case と internal case を統一的に扱える。

8.5 「子の index が親より大きい」ことの実用的意味

edge invariant は多くの枝刈りを可能にする。たとえば restrict で \(top(u)>i\) なら、\(u\) 以下には \(x_i\) が絶対に存在しない。なぜなら、すべての子孫は \(top(u)\) よりさらに大きい index を持つからである。

同様に、quantification や support 計算でも、探している index より大きい節点に到達したら探索を打ち切れる。

8.6 unique table と index の関係

unique table の key に index を含めるのは、「この節点がどの変数で分岐しているか」が関数の意味を決めるからである。

\(i\ne j\) なら、low/high が同じでも異なる関数を表す可能性がある。特に \((i,0,1)\) は \(x_i\)、\((j,0,1)\) は \(x_j\) である。

8.7 動的 reordering と index 更新

動的 reordering では、変数の順序を変更して BDD を小さくする。ここで変わるのは variable id ではなく、variable id から index への写像である。実装には大きく 2 つの方式がある。

いずれの場合も、ユーザーが見ている「変数名」は同じでも、演算で比較される level は変わりうる。

8.8 index mismatch の典型症状

8.9 ビットベクトル変数と index

整数 \(A,B\) を bit-blast して \(A_0,A_1,\ldots,B_0,B_1,\ldots\) として扱う場合、index 設計は BDD サイズに大きく影響する。典型的には次の 2 種類がある。

BDD の index は単なる実装詳細ではなく、問題構造をどう分解するかというモデリング上の設計変数である。

9. DOT + d3-graphviz による図解

以下の図は DOT で記述され、d3-graphviz でレンダリングされる。実線が high 枝、破線が low 枝である。

節点 \(b\) の low/high が同じであれば、\(b\) で分岐しても意味がないため削除される。図では削除後の ROBDD を示す。

\(u=a\)、\(v=b\) から \(a\land b\) を作ると、index が小さい \(a\) で先に分岐し、high 側で \(b\) を評価する。

10. 対話デモ: 変数順序・restrict・存在量化

下のデモでは、同じ Boolean 関数を異なる変数順序で ROBDD 化し、節点数と形がどう変わるかを確認できる。内部では真理値表再帰と mk(index,low,high) を使っている。

11. 実装上の要点

11.1 BDD manager

BDD 実装は通常、manager と呼ばれるオブジェクトにすべての状態を閉じ込める。manager は少なくとも次を保持する。

11.2 hash-consing

hash-consing は、同じ構造の値を必ず同じオブジェクトとして共有する手法である。BDD の unique table は hash-consing そのものである。これにより、構造同一性がポインタ同一性に変換される。

11.3 参照カウントと GC

BDD 演算では大量の中間節点が生成される。不要になった節点を回収しなければ memory blow-up が起きる。典型実装では、外部から保持されている BDD root に reference count を付け、到達不能になった節点を unique table から削除する。

computed table は節点を参照するため、GC と整合するように無効化または弱参照的に扱う必要がある。GC 後に cache が解放済み節点を指すと危険である。

11.4 complement edge

complement edge は、BDD pointer の低位 bit などに否定フラグを持たせる手法である。これにより \(\neg f\) を O(1) で表せる。ただし、unique table には正規化された形で登録する必要がある。典型的には、then/high 子を regular pointer に保つなどの規則を置く。

complement edge 付き実装では、節点 ID と BDD handle が別概念になる。handle は「節点への pointer + 補数 bit」であり、同じ節点 ID でも補数 bit が違えば別関数を表す。

11.5 cache key の正規化

AND や OR のような可換演算では、cache key を \((op,\min(u,v),\max(u,v))\) に正規化すると hit 率が上がる。非可換演算、たとえば implication \(u\Rightarrow v\)、では順序を入れ替えてはいけない。

11.6 並行性

unique table と computed table は共有 mutable state であるため、マルチスレッド化ではロック、シャーディング、thread-local manager などが必要になる。manager をまたいで節点 ID を共有してはいけない。

11.7 serialization

BDD を保存する場合、少なくとも次を保存する。

1. 変数名または variable id の一覧。
2. 変数順序、つまり index map。
3. 各節点の variable id、low、high。
4. root handle。
5. complement edge を使うなら補数 bit。

index map を保存しない BDD ファイルは、別の manager で読み込んだとき別関数として解釈されうる。

12. 変数順序と BDD サイズ

BDD の最大の強みと弱みは、変数順序に敏感であることだ。良い順序では線形や多項式サイズになる関数が、悪い順序では指数サイズになることがある。

12.1 なぜ順序でサイズが変わるか

BDD は変数順序に沿って Shannon 展開を行う。早い段階で「重要な組み合わせ」を解決できる順序では、後続の部分関数が共有されやすい。逆に、相互に強く関連する変数が遠く離れると、中間の部分関数が多数に分裂し、共有が効きにくくなる。

12.2 典型例: 等式

\(n\) bit の等式 \(A=B\) を考える。

順序を \([A_0,B_0,A_1,B_1,\ldots]\) のように interleaved にすると、各 bit の比較結果をすぐ処理できる。一方で \([A_0,A_1,\ldots,A_{n-1},B_0,B_1,\ldots,B_{n-1}]\) のように grouped にすると、前半で見た \(A\) の値を後半まで区別し続ける必要があり、BDD が大きくなりやすい。

12.3 dynamic variable reordering

実用パッケージでは、BDD サイズを抑えるために動的変数順序変更を行う。代表的な heuristic は sifting である。ある変数を順序中で上下に移動し、サイズが最小になる位置を探す。これを変数ごとに繰り返す。

reordering は強力だが、計算中の cache や external reference と整合させる必要があるため、manager が一元的に制御する。

12.4 良い順序の経験則

• 論理式や回路で近く相互作用する変数を BDD 順序でも近く置く。
• 入力と出力、現在状態と次状態など、対応する bit を interleave する。
• 巨大な関係 \(R(X,Y)\) と \(S(Y,Z)\) を relational product するなら、量化される \(Y\) を局所化する。
• 変数群を group として扱い、reordering 時に group 内の相対順序を保つ。
• 最初から最適順序を当てるのではなく、構築途中の BDD サイズを観察して調整する。

12.5 順序変更の危険

順序変更後は、すべての節点が新しい index invariant を満たすように再構成される必要がある。既存の node id を単に並べ替えるだけでは不十分である。また、別順序で作られた BDD 同士を直接 Apply してはいけない。Apply は「同じ index map 上で top を比較する」ことを前提としている。

13. 応用と限界

13.1 主な応用

13.2 BDD が強い状況

BDD は、部分関数の共有が多く、良い変数順序が存在する問題に強い。等式、局所的な制約、階層的な制御論理、状態遷移の規則性が高い問題では効果を発揮しやすい。

13.3 BDD が弱い状況

関数によっては任意の変数順序で BDD が指数サイズになる。乗算器の中間 bit などは古典的に難しい例として知られる。また、良い順序を見つけること自体も難しい。BDD は万能の SAT solver ではなく、順序と構造が合わない問題ではメモリを急激に消費する。

13.4 SAT solver との関係

SAT solver は単一インスタンスの充足可能性判定に非常に強い。一方 BDD は、一度構築できれば同値性、充足数、射影、集合演算などを高速に繰り返せる。BDD は「コンパイル済みの Boolean 関数表現」として強く、SAT は「探索による判定器」として強い。

14. チートシート

14.1 基本式

14.2 実装チェックリスト

1. すべての BDD が同じ manager と同じ index map に属しているか。
2. edge invariant \(top(parent)
3. mk が low=high を削除し、unique table を使っているか。
4. Apply が min(top(...)) で top variable を選んでいるか。
5. computed table が演算名と引数を正しく key にしているか。
6. SatCount や列挙で skip 変数を考慮しているか。
7. serialize 時に variable order を保存しているか。
8. 動的 reordering 後に cache と unique table が整合しているか。

14.3 用語集

15. 参考文献

BDD の古典的・標準的な参考文献は以下である。

1. R. E. Bryant, “Graph-Based Algorithms for Boolean Function Manipulation,” IEEE Transactions on Computers, 1986.
2. R. E. Bryant, “Symbolic Boolean Manipulation with Ordered Binary-Decision Diagrams,” ACM Computing Surveys, 1992.
3. S. B. Akers, “Binary Decision Diagrams,” IEEE Transactions on Computers, 1978.
4. D. E. Knuth, The Art of Computer Programming, Volume 4, Fascicle 1: Bitwise Tricks & Techniques; Binary Decision Diagrams, Addison-Wesley, 2009.