BDD 演習問題と回答

\(F_v=(\lnot x_i\land F_{low})\lor(x_i\land F_{high})\)。low は \(x_i=0\)、high は \(x_i=1\) の余因子を表す。

終端 0 は恒偽関数 \(\bot\)、終端 1 は恒真関数 \(\top\)。どちらも変数に依存しない。

low 枝は \(F|_{x_i=0}\)、high 枝は \(F|_{x_i=1}\) への遷移である。

現れてはいけない。OBDD では各経路で変数 index が狭義単調増加する。

Reduced の R。同型節点の統合と冗長節点の削除が完全に適用されていることを意味する。

その枝が指す部分関数では \(x_1\) は don’t care。\(x_1=0\) と \(x_1=1\) の余因子が同じなので節点が削除され、index が飛ぶ。

\(x_0=0\) なら関数は常に 0 なので、root の low 枝は終端 0 へ行く。

\(x_0=1\) なら関数は常に 1 なので、root の high 枝は終端 1 へ行く。

root で \(x_0=0\) なら \(x_1\)、\(x_0=1\) なら \(\lnot x_2\)。したがって \(f=(\lnot x_0\land x_1)\lor(x_0\land\lnot x_2)\)。

同じ BDD マネージャ内なら同じ Boolean 関数を表す。標準性により関数同値が ID 比較で判定できる。

その変数の値に関係なく同じ部分関数へ進むため、節点が表す関数は子の関数そのものになる。

変数、low 子、high 子がすべて等しいので Shannon 展開が同一であり、表す関数が同じだから。

2 つの \(x_1\) 節点は同じ \((x_1,0,1)\) なので統合される。その後 root \(x_0\) は low も high も同じ \(x_1\) を指すため削除される。結果は \(x_1\) だけの BDD。

同値判定が root ID 比較で済むこと、同じ部分関数が自動的に共有されてメモ化とキャッシュが効くこと。

構文は違うが関数は同じなので、同じ順序で構築し簡約すれば同じ root を持つ。

節点の意味は変数と 2 つの子で完全に決まる。同じキーは同じ Shannon 展開を意味するため、正準共有に必要十分な局所情報である。

通常は前。low=high の場合は節点を作らず子を返すだけで、冗長節点を unique table に登録してはいけない。

同じ関数が複数の補辺表現を持たないよう正規化規約が必要。節点本体と edge の補フラグの扱いを一貫させる。

終端値に AND を適用し、偽なら終端 0、真なら終端 1 を返す。

出力 BDD でも変数順序を守るため、2 入力のうち次に現れる最小 index の変数を読む。

両方の分岐で同じ節点として使う。つまり \(u_0=u_1=u\)。その節点は現在変数に依存しない。

\((op,u,v)\) から結果 root への対応をメモ化する。単項操作では \((op,u,parameter)\) などを使う。

root は \(x_0\)。low は 0、high は \(x_1\)。\(x_1\) の low は 0、high は 1。

恒偽なので終端 0 になる。

low と high に NOT を再帰適用し、同じ変数で \(mk(var,not(low),not(high))\) を呼ぶ。終端では 0 と 1 を入れ替える。

\(ITE(c,t,e)=(c\land t)\lor(\lnot c\land e)\)。専用三項 Apply として実装するとキャッシュ効率がよい。

対象変数 \(x\) の節点に到達したら low 子を採用する。対象変数より index が大きい節点に来たら、その部分 BDD には \(x\) がないのでそのまま返す。

low/high が同じなら削除し、既存の同型節点があれば共有するため。mk を通さないと ROBDD の簡約性が壊れる。

\(\exists x.F=F|_{x=0}\lor F|_{x=1}\)。

\(\forall x.F=F|_{x=0}\land F|_{x=1}\)。

\((0\land y)\lor(1\land y)=0\lor y=y\)。

\((0\oplus y)\lor(1\oplus y)=y\lor\lnot y=1\)。

\((0\oplus y)\land(1\oplus y)=y\land\lnot y=0\)。

飛ばされた 2 変数は任意なので \(2^2=4\) 個の割当を表す。

同じ部分関数を共有し、スキップ変数を \(2^k\) の係数としてまとめて数えるため。

飛ばされた変数を don’t care として扱う。展開するなら全組合せ、圧縮表示なら * を使う。

BDD の全経路で変数を読む順番を定める全順序。実装では各変数に整数 index を割り当てる。

rankdir=TB の図では通常、index が小さい変数ほど上に現れる。

\(a_0

\(a_0

セレクタを読めば必要なデータ入力が 1 本に絞られ、他のデータ変数が don’t care になる。

\(v\) の部分関数は現在の変数に依存していないから。

良い順序は問題依存で、悪い順序では節点数が指数的に増えるため。sifting などで実行中に改善する。

単にラベルを変えると順序制約と標準性が壊れる。reordering は BDD を構造的に作り直しながら行う。

変数数 \(n\)。現在 level から \(n\) までの未読変数が自由なので \(2^k\) を掛ける。

root から到達可能な全 BDD に出てこないなら不要。特定枝で出てこないだけなら、その分岐で不要という意味。

節点配列、unique table、computed table、変数順序表。実装によって参照カウントや GC 情報も持つ。

終端判定が高速になり、false/true の表現が一貫する。

中間操作で一時節点が多く作られるため、参照されなくなった節点を回収しないとメモリが増え続ける。

古い節点 ID や回収済み節点を指すエントリが残り、メモリを圧迫する。GC 時の無効化やサイズ制限が必要。

変数数が多く、経路が長い場合。Apply では 2 つの BDD の depth に依存する。

マネージャには他の関数や過去の中間節点が残る。対象関数のサイズは root から到達できる節点だけで測る。

制約全体の BDD を構築し、root が終端 0 なら充足不能、そうでなければ充足可能。

状態集合や遷移関係を Boolean 関数として表し、到達可能状態計算や像計算を BDD 操作で行う。

AND と存在量化を BDD 上で行うことで、巨大な真理値表を明示せずに関係合成を計算できる。

整数乗算の中央ビットなどは任意の変数順序で指数的な BDD サイズを持つ典型例。

BDD は Boolean 関数一般の標準表現。ZDD は疎な集合族に特化し、high が 0 の節点を削除するゼロ抑制規則を使う。

固定順序の ROBDD は標準形なので、同値判定、モデル数え上げ、量化が構造的に扱いやすい。