SAT ソルバー具体例集

例 1：空 CNF は真

AND の空積なので任意の割当で真。SAT ソルバーでは、節が 0 個なら即 SAT と判定できる。

例 2：空節を含む CNF は偽

空節は OR の空和で偽。どんな割当でも空節は満たされないため UNSAT。

例 3：節の評価

\(x\) は偽、\(\neg y\) も偽、\(z\) は未割当。したがって節は単位で、\(z=T\) が強制される。

例 4：節が既に満たされた場合

他のリテラルの値に関係なく節は真。DPLL/CDCL は満たされた節から新たな伝播を行わない。

例 5：未決定節

未割当が 2 個あるので単位ではない。伝播は起きず、探索ヒューリスティックが次の決定を行う。

例 6：含意の CNF

「a ならば b」は、a が真で b が偽の場合だけ禁止する 1 節で表せる。

例 7：双方向含意

両方向の含意を AND する。等価制約はゲート符号化の基本である。

例 8：OR ゲート

CNF は \((\neg z\lor a\lor b)\land(z\lor\neg a)\land(z\lor\neg b)\)。最初の節は \(z\Rightarrow a\lor b\)、後二者は \(a\Rightarrow z\), \(b\Rightarrow z\)。

例 9：AND ゲート

CNF は \((\neg z\lor a)\land(\neg z\lor b)\land(z\lor\neg a\lor\neg b)\)。

例 10：NOT ゲート

CNF は \((\neg z\lor\neg a)\land(z\lor a)\)。これは \(z\) と \(a\) が反対値になることを表す。

例 11：XOR ゲート

CNF は \((\neg a\lor\neg b\lor\neg z)\land(a\lor b\lor\neg z)\land(a\lor\neg b\lor z)\land(\neg a\lor b\lor z)\)。4 つの禁止パターンを節にしたもの。

例 12：少なくとも 1 つ

「少なくとも 1 つ真」はそのまま 1 つの長い節になる。

例 13：高々 1 つ

例 14：ちょうど 1 つ

例 15：三角形グラフの 3 彩色

各頂点に exactly-one 色制約を置き、各辺 \((u,v)\) と色 \(c\) に対して \((\neg x_{u,c}\lor\neg x_{v,c})\) を置く。三角形は 3 色で SAT。

例 16：鳩の巣原理 PHP(3,2)

各鳩は少なくとも 1 つの穴に入る。各穴に 2 羽は入れない。3 羽を 2 穴に入れる制約は UNSAT。

例 17：Tseitin の基本

補助変数 \(u\leftrightarrow a\land b\), \(z\leftrightarrow u\lor c\) を導入し、最後に単位節 \((z)\) を加える。

例 18：入れ子 OR/AND

\(u\leftrightarrow a\lor b\), \(v\leftrightarrow c\lor d\), \(z\leftrightarrow u\land v\), \((z)\)。節数は式サイズに線形。

例 19：否定を含むゲート

\(u\leftrightarrow a\land b\), \(z\leftrightarrow\neg u\), \((z)\)。直接展開すれば \((\neg a\lor\neg b)\) だが、一般式では Tseitin が爆発を防ぐ。

例 20：分配展開の爆発回避

素朴に CNF へ分配すると節数が指数的に増える場合がある。Tseitin なら各 AND に補助変数を置き、最後を OR ゲートとして線形サイズで表せる。

例 21：同充足性と同値性の違い

Tseitin 変換は補助変数を導入するため、元変数だけで見れば同じモデル射影を持つが、全変数上で完全に同じ式ではない。重要なのは satisfiability を保存すること。

例 22：単位伝播チェーン

\((a)\) から \(a=T\)、次に \(b=T\)、次に \(c=T\)。決定なしで SAT まで進む。

例 23：即時衝突

単位伝播で \(a=T\) と \(a=F\) が同時に要求される。決定レベル 0 の衝突なので UNSAT。

例 24：純リテラル

\(a\) が正でしか現れないので、古典 DPLL では \(a=T\) と置けば \(a\) を含む節を満たせる。現代 CDCL は純リテラル規則を常用しないことが多い。

例 25：分岐後に伝播で SAT

\(a=T\) と決定すると \((\neg a\lor c)\) から \(c=T\)。さらに \((\neg b\lor\neg c)\) から \(b=F\)。全節が満たされる。

例 26：両枝衝突による UNSAT

\(a=T\) では \(b=T\) と \(b=F\) が同時に強制される。\(a=F\) でも同様。したがって UNSAT。

例 27：決定順序で探索量が変わる

先に \(y\) を決めると速い。\(y=T\) なら前 2 節は満たされ、\((\neg y\lor z)\) から \(z=T\)。変数選択は性能に直結する。

例 28：watch の初期化

任意の 2 つ、たとえば \(a,b\) を watch する。未割当ならどちらも偽でないため不変条件を満たす。

例 29：watch 移動

\(a\) が watch されていたら、未割当の \(c\) へ watch を移動できる。伝播は起きない。

例 30：watch から単位伝播

代替 watch がなく、他方の watch が \(c\) なら \(c=T\) が強制される。

例 31：watch から衝突

両 watch が偽で、代替もない。節が空になり衝突する。

例 32：理由節

節が単位になり \(b=T\) を伝播する。このとき \(b\) の reason は節 \((\neg a\lor b)\)。

例 33：線形含意からの学習

\(a=T\) と決めると \(b,c,d\) が伝播し \((\neg d\lor\neg a)\) と衝突。resolution により学習節 \((\neg a)\) を得る。

例 34：1-UIP 節

衝突節中の現在レベルリテラルが 2 個以上なら、トレイル末尾から理由節で resolution する。現在レベルリテラルが 1 個になった節が asserting clause。

例 35：backjump レベル

現在レベル 7 のリテラルは 1 個。残りの最大レベルは 4。したがって level 4 へ戻り、\(\neg u\) を単位伝播する。

例 36：決定レベル 0 衝突

レベル 0 には戻るべき決定がない。したがって式そのものが UNSAT と確定する。

例 37：restart の意味

restart は探索木を根に戻す操作だが、学習節により同じ悪い領域に入りにくくなる。完全性を壊さない。

例 38：DIMACS の 1 節

1 -3 4 0

これは節 \((x_1\lor\neg x_3\lor x_4)\) を表す。0 は節の終端。

例 39：trail entry

{ lit: x7, level: 3, reason: C42 }

割当リテラル、決定レベル、理由節を保存する。決定リテラルなら reason は null。

例 40：watch list

watch[¬x] = [C5, C18, C22]

\(x=T\) にしたとき偽になるリテラルは \(\neg x\)。その watch list だけを走査する。

例 41：VSIDS bump

衝突解析に出た変数の活動度を増やす。最近の衝突に関わる変数を優先して決定するため、探索が衝突の核心へ集中する。

例 42：LBD

この学習節の LBD は distinct decision levels の数なので 3。LBD が小さい節は複数レベルを強く結び、残す価値が高いとみなされやすい。

例 43：節削減

学習節を無制限に溜めると BCP が重くなる。活動度や LBD を使って、役に立ちにくい学習節を定期的に削除する。

例 44：phase saving

変数を再び決定するとき、前回使った極性を優先する。restart 後に近い探索状態を再構築しやすい。

例 45：incremental SAT

同じ基礎 CNF に異なる仮定リテラルを加えて何度も解く。SMT、モデル検査、最適化で重要になる。