0. このレポートの使い方
各カードは 1 つの Boolean 関数、推奨変数順序、その順序での ROBDD 図を示す。root は青、low 枝は破線、high 枝は実線である。
1. 具体例カタログ
定数 0
全ての割当で偽。ROBDD は終端 0 だけになる。
定数 1
全ての割当で真。ROBDD は終端 1 だけになる。
リテラル
最小の非終端節点。low が 0、high が 1。
否定リテラル
low が 1、high が 0。
2 変数 AND
x0=0 で即 0 へ行くため x1 を読まない。
2 変数 OR
x0=1 で即 1。短絡評価に似た形。
NAND
AND の終端を反転した形。
含意
x0=0 で常に真、x0=1 のとき x1 を見る。
2 変数 XOR
両方の分岐で x1 が現れるが low/high の向きが反転する。
2 変数同値
XOR の否定。
if-then-else
BDD の Shannon 展開そのものを表す典型例。
3 変数多数決
2 個以上が真なら真。
3 変数 exactly-one
カウンタ制約の最小例。
4 変数 at-most-one
一度 1 を見た後は、残りがすべて 0 でなければならない。
4 変数 at-least-two
しきい値関数。残り変数数による枝刈りが起きる。
4 変数 exactly-two
個数制約 BDD は「これまでの 1 の数」を状態として共有する。
3 変数 parity
各 level で偶奇状態が 2 つずつ残る。
5 変数 parity
順序によらず線形サイズだが、毎層 2 状態を持つ。
one-hot 4
exactly-one の 4 変数版。
3 変数全同値
000 と 111 だけが真。
入れ子条件
x0 の分岐で読む変数集合が大きく変わる。
4-to-1 MUX
セレクタを先に読むと小さい。データを先に読むと膨らみやすい。
2-bit equality / interleaved
対応するビットを隣接させる良い順序。
2-bit equality / grouped
同じ関数だが、先に A 全体を読んでから B を読む順序。
3-bit equality / interleaved
等価性は各ビットペアを処理して共有できる。
2-bit less-than
MSB で決まらない場合だけ LSB を読む。
2-bit less-or-equal
比較器は辞書式の短絡が BDD に現れる。
半加算器 sum
XOR と同じ。
半加算器 carry
AND と同じ。
全加算器 carry
3 変数多数決。
全加算器 sum
3 変数 parity。
矛盾 CNF
すべての割当を排除するため終端 0。SAT 判定が root=0 で終わる。
Horn 制約
含意チェーン x0⇒x1⇒x2。
小さな到達可能性
1 から 3 へ直接行くか、1→2→3 で行く。
2 並列パス信頼性
共有パスがない単純なネットワーク信頼性。
アクセス制御
admin=1 の枝が終端 1 に飛ぶ。
隣接競合なし
パスグラフ上の独立集合制約。
資源 1 個だけ選択
one-hot 5。状態は「まだ 1 を見ていない」「すでに 1 を見た」に近い。
ペア積和
対応ペアを隣接させると部分関数が早く確定する。
共通因子の共有
x0=0 で即 0、x0=1 で OR に移る。
2. 順序比較ラボ
例を選び、複数の順序で ROBDD の節点数を比較する。変数数が 6 以下なら全順列を試せる。
3. 真理値表ラボ
BDD は真理値表を圧縮したものとも見なせる。以下では選択した例の真理値表と充足割当の割合を表示する。
4. パターン別の読み方
短絡型
AND、OR、含意、比較器では、一部の枝が早く終端に落ちる。
状態共有型
parity、個数制約、one-hot では「ここまでの状態」が共有される。
対応ペア型
等価性や \(x_i y_i\) の積和は、対応変数を近くに置くと小さい。
セレクタ型
マルチプレクサはセレクタを先に読むと、選ばれるデータ線だけに絞れる。