BDD 図解拡張レポート

visual convention

0. 図の読み方

BDD は、論理式を「変数を読む順序」と「部分関数の共有」によって圧縮した有向非巡回グラフである。円が非終端節点、四角が終端 0/1、破線が low 枝、実線が high 枝を表す。

ノードの意味。 非終端節点 \(v\) が変数 \(x_i\) を読むとき、\[F_v=(\lnot x_i\land F_{\mathrm{low}(v)})\lor(x_i\land F_{\mathrm{high}(v)}).\]

ROBDD では各根から終端への経路で index が狭義単調増加する。枝が index を飛ぶ場合、飛ばされた変数はその部分関数に対して don’t care である。

low 枝

\(F|_{x_i=0}\) への遷移。

high 枝

\(F|_{x_i=1}\) への遷移。

節点共有

同じ部分関数は同じ節点 ID になる。

construction

1. 決定木から ROBDD へ

例として \(f=\operatorname{ITE}(x_0,x_1,x_2)=(x_0\land x_1)\lor(\lnot x_0\land x_2)\) を扱う。順序は \(x_0

完全な決定木

各割当を最後まで展開した木。節点共有も冗長削除もまだ行っていない。

DOT + d3-graphviz

DOT ソースを表示

digraph FullTree {
  graph [rankdir=TB, bgcolor="transparent", margin=0.04];
  node [shape=circle, fontname="Helvetica", fontsize=12, style=filled, fillcolor="white", color="#334155"];
  edge [fontname="Helvetica", fontsize=10, arrowsize=.65, color="#475569"];
  label="完全な決定木: f = (x0 ∧ x1) ∨ (¬x0 ∧ x2)"; labelloc=t;
  r [label="x0"];
  a [label="x1"]; b [label="x1"];
  c [label="x2"]; d [label="x2"]; e [label="x2"]; f [label="x2"];
  t0a [label="0", shape=box, fillcolor="#fff1f2", color="#fb7185"];
  t1a [label="1", shape=box, fillcolor="#ecfdf5", color="#34d399"];
  t0b [label="0", shape=box, fillcolor="#fff1f2", color="#fb7185"];
  t1b [label="1", shape=box, fillcolor="#ecfdf5", color="#34d399"];
  t0c [label="0", shape=box, fillcolor="#fff1f2", color="#fb7185"];
  t1c [label="1", shape=box, fillcolor="#ecfdf5", color="#34d399"];
  t0d [label="0", shape=box, fillcolor="#fff1f2", color="#fb7185"];
  t1d [label="1", shape=box, fillcolor="#ecfdf5", color="#34d399"];
  r -> a [label="0", style=dashed]; r -> b [label="1", penwidth=1.6];
  a -> c [label="0", style=dashed]; a -> d [label="1", penwidth=1.6];
  b -> e [label="0", style=dashed]; b -> f [label="1", penwidth=1.6];
  c -> t0a [label="0", style=dashed]; c -> t1a [label="1", penwidth=1.6];
  d -> t0b [label="0", style=dashed]; d -> t1b [label="1", penwidth=1.6];
  e -> t0c [label="0", style=dashed]; e -> t0d [label="1", penwidth=1.6];
  f -> t1c [label="0", style=dashed]; f -> t1d [label="1", penwidth=1.6];
  {rank=same; a; b;} {rank=same; c; d; e; f;}
}

完全な決定木では、実際には依存しない変数も機械的に読む。次に、同じ順序を保ったまま同型部分木を共有すると OBDD になる。

順序付きだが未簡約の OBDD

同じ順序を守るが、同じ節点や冗長節点が残っている。

DOT + d3-graphviz

DOT ソースを表示

digraph OBDD_before {
  graph [rankdir=TB, bgcolor="transparent", margin=0.04];
  node [shape=circle, fontname="Helvetica", fontsize=12, style=filled, fillcolor="white", color="#334155"];
  edge [fontname="Helvetica", fontsize=10, arrowsize=.65, color="#475569"];
  label="順序付きだが未簡約の OBDD"; labelloc=t;
  x0 [label="x0\nidx=0", fillcolor="#eaf0ff", color="#1d4ed8", penwidth=2.2];
  x1a [label="x1\nidx=1"]; x1b [label="x1\nidx=1"];
  x2a [label="x2\nidx=2"]; x2b [label="x2\nidx=2"]; x2c [label="x2\nidx=2"]; x2d [label="x2\nidx=2"];
  T0 [label="0", shape=box, fillcolor="#fff1f2", color="#fb7185"]; T1 [label="1", shape=box, fillcolor="#ecfdf5", color="#34d399"];
  x0 -> x1a [label="0", style=dashed]; x0 -> x1b [label="1", penwidth=1.6];
  x1a -> x2a [label="0", style=dashed]; x1a -> x2b [label="1", penwidth=1.6];
  x1b -> x2c [label="0", style=dashed]; x1b -> x2d [label="1", penwidth=1.6];
  x2a -> T0 [label="0", style=dashed]; x2a -> T1 [label="1", penwidth=1.6];
  x2b -> T0 [label="0", style=dashed]; x2b -> T1 [label="1", penwidth=1.6];
  x2c -> T0 [label="0", style=dashed]; x2c -> T0 [label="1", penwidth=1.6];
  x2d -> T1 [label="0", style=dashed]; x2d -> T1 [label="1", penwidth=1.6];
  {rank=same; x1a; x1b;} {rank=same; x2a; x2b; x2c; x2d;} {rank=same; T0; T1;}
}

最後に、同型節点の統合と low=high 節点の削除を飽和するまで行うと ROBDD になる。

簡約後の ROBDD

root の low 側は x2、high 側は x1。飛ばされた変数はその分岐では不要。

DOT + d3-graphviz

DOT ソースを表示

digraph ROBDD_ITE {
  graph [rankdir=TB, bgcolor="transparent", margin=0.04];
  node [shape=circle, fontname="Helvetica", fontsize=12, style=filled, fillcolor="white", color="#334155"];
  edge [fontname="Helvetica", fontsize=10, arrowsize=.65, color="#475569"];
  label="ROBDD: f = ITE(x0, x1, x2)"; labelloc=t;
  x0 [label="x0\nidx=0", fillcolor="#eaf0ff", color="#1d4ed8", penwidth=2.2];
  x1 [label="x1\nidx=1"]; x2 [label="x2\nidx=2"];
  T0 [label="0", shape=box, fillcolor="#fff1f2", color="#fb7185"]; T1 [label="1", shape=box, fillcolor="#ecfdf5", color="#34d399"];
  x0 -> x2 [label="0 / skip x1", style=dashed];
  x0 -> x1 [label="1 / skip x2", penwidth=1.6];
  x1 -> T0 [label="0", style=dashed]; x1 -> T1 [label="1", penwidth=1.6];
  x2 -> T0 [label="0", style=dashed]; x2 -> T1 [label="1", penwidth=1.6];
  {rank=same; x1;} {rank=same; x2;} {rank=same; T0; T1;}
}

reduction rules

2. ROBDD を決める 2 つの簡約規則

規則 A: 同型節点の統合

同じ \((\mathrm{var},\mathrm{low},\mathrm{high})\) を持つ節点は同じ関数を表す。

規則 B: 冗長節点の削除

low と high が同じなら、その変数は関数値に影響しない。

規則 A: 同型節点の統合

unique table がこの規則を機械的に保証する。

DOT + d3-graphviz

DOT ソースを表示

digraph MergeRule {
  graph [rankdir=LR, bgcolor="transparent", margin=0.04];
  node [fontname="Helvetica", fontsize=12, style=filled, fillcolor="white", color="#334155"];
  edge [fontname="Helvetica", fontsize=10, arrowsize=.65, color="#475569"];
  label="同型節点の共有: (var, low, high) が同じなら 1 個に統合"; labelloc=t;
  subgraph cluster_before { label="統合前"; color="#cbd5e1";
    a [label="x1", shape=circle]; b [label="x1", shape=circle]; c0 [label="0", shape=box, fillcolor="#fff1f2", color="#fb7185"]; c1 [label="1", shape=box, fillcolor="#ecfdf5", color="#34d399"];
    a -> c0 [label="0", style=dashed]; a -> c1 [label="1", penwidth=1.6]; b -> c0 [label="0", style=dashed]; b -> c1 [label="1", penwidth=1.6];
  }
  subgraph cluster_after { label="統合後"; color="#cbd5e1";
    p [label="parent A", shape=ellipse, fillcolor="#f8fafc"]; q [label="parent B", shape=ellipse, fillcolor="#f8fafc"];
    x [label="x1", shape=circle, fillcolor="#eaf0ff", color="#1d4ed8"]; d0 [label="0", shape=box, fillcolor="#fff1f2", color="#fb7185"]; d1 [label="1", shape=box, fillcolor="#ecfdf5", color="#34d399"];
    p -> x; q -> x; x -> d0 [label="0", style=dashed]; x -> d1 [label="1", penwidth=1.6];
  }
}

規則 B: 冗長節点の削除

mk(var,low,high) は low=high なら子を返す。

DOT + d3-graphviz

DOT ソースを表示

digraph EliminateRule {
  graph [rankdir=LR, bgcolor="transparent", margin=0.04];
  node [fontname="Helvetica", fontsize=12, style=filled, fillcolor="white", color="#334155"];
  edge [fontname="Helvetica", fontsize=10, arrowsize=.65, color="#475569"];
  label="冗長節点の削除: low = high ならその節点は変数に依存しない"; labelloc=t;
  subgraph cluster_before { label="削除前"; color="#cbd5e1"; p [label="parent", shape=ellipse, fillcolor="#f8fafc"]; x [label="xk", shape=circle]; y [label="child", shape=ellipse, fillcolor="#f8fafc"]; p -> x; x -> y [label="0", style=dashed]; x -> y [label="1", penwidth=1.6]; }
  subgraph cluster_after { label="削除後"; color="#cbd5e1"; p2 [label="parent", shape=ellipse, fillcolor="#f8fafc"]; y2 [label="child", shape=ellipse, fillcolor="#f8fafc"]; p2 -> y2 [label="same function"]; }
}

標準性。 変数順序を固定し、2 規則を完全に適用した ROBDD は、同じ Boolean 関数に対して同型を除いて一意である。したがって同じ BDD マネージャ内では \(f\equiv g\) を root ID の比較で判定できる。

variable index

3. 変数 index と層の意味

BDD マネージャは変数を \(x_{\pi(0)},x_{\pi(1)},\dots,x_{\pi(n-1)}\) の順に並べ、各変数に index を割り当てる。非終端節点は必ず 1 つの index を持ち、根から終端へ進むと index は増加する。

\[\operatorname{idx}(v)<\operatorname{idx}(\mathrm{low}(v)),\qquad \operatorname{idx}(v)<\operatorname{idx}(\mathrm{high}(v)).\]

index を飛ばす枝

枝ラベルの skip は、中間変数が不要であることを表す。

DOT + d3-graphviz

DOT ソースを表示

digraph IndexSkip {
  graph [rankdir=TB, bgcolor="transparent", margin=0.04];
  node [fontname="Helvetica", fontsize=12, style=filled, fillcolor="white", color="#334155"];
  edge [fontname="Helvetica", fontsize=10, arrowsize=.65, color="#475569"];
  label="index と層: 枝が層を飛ぶと、その変数はその部分関数で don't care"; labelloc=t;
  x0 [label="x0\nidx=0", shape=circle, fillcolor="#eaf0ff", color="#1d4ed8", penwidth=2]; x2 [label="x2\nidx=2", shape=circle]; x4 [label="x4\nidx=4", shape=circle];
  T0 [label="0", shape=box, fillcolor="#fff1f2", color="#fb7185"]; T1 [label="1", shape=box, fillcolor="#ecfdf5", color="#34d399"];
  x0 -> x2 [label="0 / skip idx=1", style=dashed]; x0 -> x4 [label="1 / skip idx=1,2,3", penwidth=1.6]; x2 -> T0 [label="0 / skip idx=3,4", style=dashed]; x2 -> T1 [label="1 / skip idx=3,4", penwidth=1.6]; x4 -> T0 [label="0", style=dashed]; x4 -> T1 [label="1", penwidth=1.6];
  {rank=same; x2;} {rank=same; x4;} {rank=same; T0; T1;}
}

現象	意味	操作への影響
枝が index を飛ぶ	飛ばされた変数はその部分関数で don’t care	sat count では \(2^k\) を掛ける
同じ変数節点が複数ある	異なる文脈で同じ変数を読む	同じ \((var,low,high)\) なら統合
順序が違う	探索の分岐構造が違う	節点数が指数的に変化しうる

operations

4. BDD 操作の図解

4.1 Apply

二項演算 \(f\odot g\) は、2 つの BDD の節点ペア \((u,v)\) を状態とする再帰で実装する。次に読む変数は \(\min(\operatorname{idx}(u),\operatorname{idx}(v))\) で決まる。

Apply の pair recursion

computed table により同じ節点ペアを二度計算しない。

DOT + d3-graphviz

DOT ソースを表示

digraph ApplyRecursion {
  graph [rankdir=TB, bgcolor="transparent", margin=0.04];
  node [fontname="Helvetica", fontsize=12, style=filled, fillcolor="white", color="#334155"];
  edge [fontname="Helvetica", fontsize=10, arrowsize=.65, color="#475569"];
  label="Apply(f,g,⊙): pair state を根にした再帰"; labelloc=t;
  p00 [label="(u, v)\ntop = min(idx(u), idx(v))", shape=box, fillcolor="#eaf0ff", color="#1d4ed8", penwidth=2];
  p0 [label="(low(u), low(v))", shape=box]; p1 [label="(high(u), high(v))", shape=box];
  r [label="mk(top, result0, result1)", shape=ellipse, fillcolor="#ecfdf5", color="#34d399"];
  memo [label="computed table\n(u,v,op) ↦ result", shape=note, fillcolor="#fff8eb", color="#f59e0b"];
  p00 -> p0 [label="top=0 branch", style=dashed]; p00 -> p1 [label="top=1 branch", penwidth=1.6]; p0 -> r [label="result0"]; p1 -> r [label="result1"]; p00 -> memo [label="lookup / insert", style=dotted]; memo -> r [label="hitなら即返す", style=dotted];
}

Apply(op, u, v):
  if u and v are terminals: return terminal(op(value(u), value(v)))
  k  = min(level(u), level(v))
  x  = variable_at_index(k)
  u0 = low(u)  if level(u) == k else u
  u1 = high(u) if level(u) == k else u
  v0 = low(v)  if level(v) == k else v
  v1 = high(v) if level(v) == k else v
  return mk(x, Apply(op,u0,v0), Apply(op,u1,v1))

4.2 restrict と量化

restrict は対象変数の節点を該当する子で置き換える。存在量化は 2 つの余因子の OR、全称量化は AND である。

\[\exists x.F=F|_{x=0}\lor F|_{x=1},\qquad \forall x.F=F|_{x=0}\land F|_{x=1}.\]

余因子と量化

restrict は枝選択、exists/forall は Apply と組み合わせる。

DOT + d3-graphviz

DOT ソースを表示

digraph Cofactor {
  graph [rankdir=LR, bgcolor="transparent", margin=0.04];
  node [fontname="Helvetica", fontsize=12, style=filled, fillcolor="white", color="#334155"];
  edge [fontname="Helvetica", fontsize=10, arrowsize=.65, color="#475569"];
  label="restrict と existential abstraction"; labelloc=t;
  F [label="F", shape=circle, fillcolor="#eaf0ff", color="#1d4ed8", penwidth=2];
  F0 [label="F|x=0", shape=box, fillcolor="#fff1f2", color="#fb7185"]; F1 [label="F|x=1", shape=box, fillcolor="#ecfdf5", color="#34d399"];
  OR [label="OR", shape=diamond, fillcolor="#f8f5ff", color="#7c3aed"];
  Exists [label="∃x F = F|x=0 ∨ F|x=1", shape=ellipse, fillcolor="#f8fafc"]; Forall [label="∀x F = F|x=0 ∧ F|x=1", shape=ellipse, fillcolor="#f8fafc"];
  F -> F0 [label="low cofactor", style=dashed]; F -> F1 [label="high cofactor", penwidth=1.6]; F0 -> OR; F1 -> OR; OR -> Exists; F0 -> Forall [label="AND に入れる", style=dotted]; F1 -> Forall [style=dotted];
}

4.3 sat count

節点 \(u\) に到達した時点で次に期待される level を \(\ell\)、\(u\) の index を \(i\) とすると、\[\#(u,\ell)=2^{i-\ell}\{\#(low(u),i+1)+\#(high(u),i+1)\}.\]

implementation

5. unique table と computed table

unique table は標準形を保ち、computed table は操作の重複再帰を避ける。

unique table と computed table

mk と Apply の役割分担。

DOT + d3-graphviz

DOT ソースを表示

digraph UniqueComputed {
  graph [rankdir=LR, bgcolor="transparent", margin=0.04];
  node [fontname="Helvetica", fontsize=12, style=filled, fillcolor="white", color="#334155"];
  edge [fontname="Helvetica", fontsize=10, arrowsize=.65, color="#475569"];
  label="実装での 2 つの表: unique table と computed table"; labelloc=t;
  request [label="mk(var, low, high)", shape=box, fillcolor="#eaf0ff", color="#1d4ed8"];
  utable [label="unique table\n(var,low,high) ↦ node id", shape=cylinder, fillcolor="#f8fafc"];
  node_id [label="既存 id または新規 id", shape=ellipse, fillcolor="#ecfdf5", color="#34d399"];
  apply [label="Apply(op,u,v)", shape=box, fillcolor="#f8f5ff", color="#7c3aed"];
  ctable [label="computed table\n(op,u,v) ↦ result", shape=cylinder, fillcolor="#f8fafc"];
  result [label="結果 BDD root", shape=ellipse, fillcolor="#ecfdf5", color="#34d399"];
  request -> utable -> node; apply -> ctable -> result; apply -> request [label="再帰の最後に mk", style=dashed];
}

表	キー	値	目的
unique table	\((var,low,high)\)	node id	同型節点の統合
computed table	\((op,u,v)\)	result id	Apply などのメモ化
variable order table	変数名	index	top variable 判定

ordering matters

6. 変数順序で図が変わる

同じ Boolean 関数でも、変数順序が変わると共有できる部分関数が変わる。典型例は \(EQ_n=\bigwedge_i(a_i\leftrightarrow b_i)\)。

\[\text{good: }a_0

次の対話ラボで、同じ式に対して順序だけを変えて節点数と図の差を確認できる。

interactive

7. 対話ラボ: 式、変数順序、操作を変える

構築された ROBDD

root は青で強調。skip は飛ばされた index 数。

interactive

節点表

restrict / exists

操作結果

editable DOT

8. DOT 編集実験

DOT を編集して再描画する。rank、ラベル、low/high のスタイルを変えると理解しやすさが変わる。

編集結果