DOT + d3-graphviz で見る SAT ソルバー

DPLL と CDCL は、数式の上では「割当と節の操作」だが、実装上の理解はグラフとして見ると急速に深まる。このレポートでは、CNF、探索木、含意グラフ、watch list、1-UIP カット、backjump を DOT で記述し、d3-graphviz によってブラウザ上でレンダリングする。

DOT 記法d3-graphvizDPLL search treeImplication graph1-UIPWatched literals

0. このレポートの目的

SAT ソルバーの中核は、論理式そのものよりも「状態遷移」をどう管理するかにある。DPLL では探索木、CDCL では含意グラフと衝突解析が主役になる。グラフ化すると、次の対応が見える。

CNF
節とリテラルの二部グラフ。どの節がどのリテラルに依存するかを読む。

DPLL
決定を枝、単位伝播を強制遷移、衝突を葉として読む。

CDCL
トレイルをノード、理由節を有向辺、衝突を特殊ノードとして読む。

この文書は、前提として CNF を次の形に置く。

\[ F = C_1 \land C_2 \land \cdots \land C_m, \qquad C_i = \ell_{i1} \lor \ell_{i2} \lor \cdots \lor \ell_{ik_i}, \]

ここでリテラル \(\ell\) は変数 \(x\) または否定 \(\neg x\) である。割当 \(\alpha\) の下で節が単位になるとは、節中の未割当リテラルが 1 個だけで、残りがすべて偽になることである。

1. DOT と d3-graphviz

DOT は Graphviz のグラフ記述言語である。SAT ソルバーの状態を DOT で書くと、節・リテラル・割当・理由節・衝突節を視覚的なノードと辺に変換できる。

有向グラフの最小例

digraph G {
  rankdir=LR;
  a [label="decision: x1=true"];
  b [label="implied: x2=false"];
  a -> b [label="reason C3"];
}

SAT 図解で使う約束

図形	意味
角丸 box	節、または手続き上の状態
楕円	割当済みリテラル、トレイル上の代入
二重円 / 赤	衝突、矛盾、空節
太い青辺	watch、強い依存、カット対象
破線	候補、非同期的な参照、戻り先

このページでは MathJax と d3-graphviz を CDN から読み込む。ネットワークに接続していない環境では、数式やグラフが完全にはレンダリングされない場合がある。その場合でも、DOT ソースと説明文は読めるようにしてある。

2. インタラクティブ図解台

下のセレクタから図を選ぶと DOT ソースが表示され、右側に Graphviz レイアウトが描画される。DOT を編集して 再描画 すれば、SAT ソルバーの状態を自分で変形できる。

図を選択

読み込み中...

決定・watch 真 / 充足偽 / 衝突学習節

Graphviz を初期化しています。

3. CNF を二部グラフとして見る

CNF は自然に「節ノード」と「リテラルノード」の二部グラフになる。節 \(C_i\) からリテラル \(\ell\) への辺は「\(\ell\) が \(C_i\) のメンバーである」ことを表す。

例：\(F=(x_1\lor \neg x_2\lor x_3)\land(\neg x_1\lor x_4)\land(x_2\lor \neg x_3\lor \neg x_4)\)。節の充足判定は、各節ノードが少なくとも 1 つの真リテラルに接続されているかを見る問題になる。

この二部グラフ表示から、単位伝播の条件も読める。ある節に接続するリテラルのうち、偽でないものがちょうど 1 つだけなら、そのリテラルを真にしなければその節は満たせない。

4. DPLL 探索木

DPLL の探索木では、内部ノードが決定、辺が決定リテラル、各ノード内の小さな注釈がその後の単位伝播を表す。枝の先で空節が出れば衝突、すべての節が満たされれば SAT 葉になる。

要素	探索木での意味	論理的意味
根	空の割当	\(\alpha=\varnothing\)
左/右枝	変数の真/偽を試す	\(F\land x\), \(F\land \neg x\)
伝播ノード	単位節から強制された割当	\(F\models \ell\) under current partial assignment
衝突葉	ある節が空になる	現在の部分割当は拡張不能
SAT 葉	全節充足	モデル発見

DPLL は chronological backtracking を行う。すなわち衝突したら直前の未試行枝に戻る。CDCL は衝突解析で学習節を作り、衝突の本質に対応するより浅いレベルへ backjump する。

5. 単位伝播を含意グラフとして見る

単位伝播は「現在の割当が、別の割当を強制する」関係である。たとえば節 \((\neg a\lor \neg b\lor c)\) は、\(a=true\) かつ \(b=true\) の下で単位節 \((c)\) になり、\(c=true\) を強制する。

\[ a \land b \land (\neg a\lor \neg b\lor c) \quad\Longrightarrow\quad c. \]

CDCL の含意グラフでは、この強制関係を有向辺として表す。理由節 \((\neg a\lor \neg b\lor c)\) は、辺 \(a\to c\), \(b\to c\) のラベルになる。

6. 2-watched literals の動きをグラフで追う

2-watched literals は、各節につき 2 個のリテラルだけを監視し、片方が偽になったときだけ節を走査する。節全体を毎回見るのではなく、「偽になった watch を含む節」だけを調べるため、実装上の BCP が高速になる。

不変条件の典型形：非単位・非衝突の節では、少なくとも一方の watched literal が偽でないように保つ。偽になった watch を別の偽でないリテラルへ移せるなら移し、移せないなら他方の watch が単位伝播または衝突を決める。

watch ステップ

watch グラフを初期化しています。

watch 更新の判断

状況	処理	意味
偽になった watch の代替候補がある	watch を移動	節はまだ単位ではない。伝播なし。
代替候補がなく、他方の watch が未割当	他方を伝播	節が単位になった。
代替候補がなく、他方の watch も偽	衝突	節が空になった。
他方の watch が真	何もしない	節はすでに満たされている。

7. CDCL の衝突解析をグラフで見る

CDCL は DPLL に「学習」を追加する。衝突が起きたとき、含意グラフから衝突を引き起こした原因集合を切り出し、その原因を同時に再現しないような学習節を追加する。

衝突節
現在の割当で節 \(C=(\ell_1\lor\cdots\lor\ell_k)\) が偽になるとき、すべての \(\ell_i\) が偽である。したがって、現在の割当は \(\neg\ell_1\land\cdots\land\neg\ell_k\) を含む。

学習節
衝突の原因を表す割当集合 \(A=\{a_1,\ldots,a_r\}\) が同時には起きてはいけないなら、\(\neg a_1\lor\cdots\lor\neg a_r\) を学習する。

含意グラフ上では、決定ノードから衝突ノードへ向かう経路を切るカットを選ぶ。カットの「現在側」に入る割当の否定を OR したものが学習節になる。

8. 1-UIP と節学習

UIP は Unique Implication Point の略で、現在の決定レベルの決定リテラルから衝突へのすべての経路が必ず通るノードである。特に、衝突に最も近い UIP を 1-UIP と呼ぶ。実用的 CDCL は通常 1-UIP 節を学習する。

1-UIP 学習節の特徴：学習節中に現在の決定レベルのリテラルがちょうど 1 つだけ残る。そのため、backjump 後にはそのリテラルが単位伝播され、同じ衝突領域へ即座に戻ることを防ぐ。

解決操作としての衝突解析

節 \(C=(x\lor A)\) と、変数 \(x\) の理由節 \(R=(\neg x\lor B)\) から、\(x\) を消去して resolvent \((A\lor B)\) を得る。

\[ \frac{(x\lor A)\qquad(\neg x\lor B)}{A\lor B}. \]

CDCL の衝突解析では、衝突節から始め、現在の決定レベルのリテラルが 2 個以上ある限り、そのうちトレイル上で最も後ろのリテラルの理由節で resolution する。

9. backjump と restart

学習節 \(L\) に含まれるリテラルの決定レベルを見て、最大レベルを現在レベル、2 番目に大きいレベルを assertion level とする。CDCL は assertion level まで戻る。

1-UIP 節が

\[ L=(\neg u \lor \ell_{a}\lor \ell_{b}\lor \ell_{c}) \]

で、\(u\) だけが現在レベル、他が低いレベルなら、低いレベルまで戻った後に \(\ell_a,\ell_b,\ell_c\) がすべて偽であれば \(\neg u\) が単位伝播される。

restart は探索を捨てるが、学習節は捨てない。したがって restart 後の探索空間は元と同じではなく、学習節によって枝刈りされた空間になる。

10. CDCL ソルバーの構成図

実装上の CDCL は、単一の大きなループではなく、いくつかのモジュールの連携として見るとわかりやすい。

モジュール	主な状態	グラフでの表現
Trail	代入列、決定レベル、理由節	時系列ノード列
BCP	watch list、伝播キュー	節・リテラル二部グラフ上の watch 辺
Analyze	衝突節、seen フラグ、path counter	含意グラフの逆向き走査
Database	原節、学習節、活動度、LBD	節ノード集合
Branch heuristic	VSIDS などの変数活動度	未割当変数への重み付き候補辺
Restart / Reduce	restart schedule、節削減	探索木の再根化、弱い節ノードの削除

11. DOT 図を読むためのチェックリスト

DPLL 図
衝突葉までの経路が「部分割当」。分岐の兄弟は同じ変数の反対割当。単位伝播は枝ではなくノード内の強制処理として読む。

CDCL 図
衝突ノードに入る辺を逆に辿る。現在レベルのノードが複数ある限り resolution を続ける。1-UIP は衝突に最も近い支配点。

watch 図
太い青辺だけが watch。偽になったリテラルから逆向きに watch list を見る。節全体を見るのは watch 更新時だけ。

backjump 図
学習節の決定レベル集合を見る。現在レベルを除いた最大レベルが戻り先。chronological backtracking と異なり複数レベルを飛ばす。