SAT ソルバー演習問題と解答

単位。\(x=F\)、\(\neg y=F\)、\(z=U\) なので、偽でないリテラルが \(z\) だけ残る。BCP は \(z=T\) を伝播する。

空 CNF は真なので SAT。空節は偽なので、それを含む CNF は UNSAT。AND の単位元は真、OR の単位元は偽である。

例えば \(a=T,b=F,c=T\)。第 1 節は \(a\) で真、第 2 節は \(c\) で真、第 3 節は \(\neg b\) と \(c\) で真。

まず \((a)\) から \(a=T\)。次に \((\neg a\lor b)\) が単位になり \(b=T\)。さらに \((\neg b\lor c)\) が単位になり \(c=T\)。衝突はない。

\(p\) は正でしか現れないので純リテラル。\(q\) も正でしか現れないので純リテラル。\(r\) は \(\neg r\) と \(r\) の両方が出るため純ではない。

\(a=T\) なら第 3 節から \(b=T\)、第 4 節から \(b=F\) が必要。矛盾。\(a=F\) なら第 1 節から \(b=T\)、第 2 節から \(b=F\) が必要。両方の \(a\) で矛盾するので UNSAT。

\(\neg(a\land b)\lor c\equiv \neg a\lor\neg b\lor c\)。したがって \((\neg a\lor\neg b\lor c)\)。

\(\neg a=F\)、\(b=F\)、\(\neg c=F\)。全リテラルが偽なので節は空になり、衝突である。

\(z\Rightarrow a\lor b\) から \((\neg z\lor a\lor b)\)。\(a\Rightarrow z\) から \((z\lor\neg a)\)。\(b\Rightarrow z\) から \((z\lor\neg b)\)。よって \((\neg z\lor a\lor b)\land(z\lor\neg a)\land(z\lor\neg b)\)。

\(z\Rightarrow a\) と \(z\Rightarrow b\) から \((\neg z\lor a)\land(\neg z\lor b)\)。\(a\land b\Rightarrow z\) から \((z\lor\neg a\lor\neg b)\)。

XOR でない 4 つの組を禁止する。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)\)。

少なくとも 1 つ：\((x_1\lor x_2\lor x_3)\)。高々 1 つ：\((\neg x_1\lor\neg x_2)\land(\neg x_1\lor\neg x_3)\land(\neg x_2\lor\neg x_3)\)。両者の AND。

各色 \(c\in\{R,G,B\}\) について \((\neg x_{u,c}\lor\neg x_{v,c})\)。具体的には \((\neg x_{u,R}\lor\neg x_{v,R})\land(\neg x_{u,G}\lor\neg x_{v,G})\land(\neg x_{u,B}\lor\neg x_{v,B})\)。

\((p_{1,1}\lor p_{1,2})\land(p_{2,1}\lor p_{2,2})\land(p_{3,1}\lor p_{3,2})\)。穴ごとの高々 1 羽制約を加えると PHP(3,2) は UNSAT になる。

基本的には同充足。補助変数を導入するため、同じ変数集合上の完全な同値式ではない。ただし、補助変数を存在量化して元変数へ射影すれば、元の式と対応する。

変数 3 個、節 2 個。節は \((x_1\lor\neg x_2)\) と \((\neg x_1\lor x_3)\)。したがって \((x_1\lor\neg x_2)\land(\neg x_1\lor x_3)\)。

\(a=T\) で第 2 節から \(c=T\)。すると第 3 節 \((\neg b\lor\neg c)\) は \((\neg b)\) になり \(b=F\)。第 1 節は \(a=T\) で満たされる。モデル \(a=T,b=F,c=T\)。

\(a=T\)：第 3 節から \(b=T\)、第 4 節から \(b=F\) で衝突。\(a=F\)：第 1 節から \(b=T\)、第 2 節から \(b=F\) で衝突。両枝が閉じるので UNSAT。

\(x\) と \(y\) は正でしか現れない。\(x=T\) と置くと前 2 節が満たされる。さらに \(y=T\) と置くと第 3 節も満たされる。したがって SAT。

\((a)\) は満たされ削除。\((\neg a\lor b\lor c)\) は \((b\lor c)\) になる。\((\neg b\lor d)\) は変わらない。残余式は \((b\lor c)\land(\neg b\lor d)\)。

各分岐で未割当変数を 1 つ決定し、同じ部分割当を無限に繰り返さない。変数数が \(n\) なら完全な割当は高々 \(2^n\) 個であり、探索木は有限。単位伝播も各変数を高々 1 回割り当てるので有限で停止する。

DPLL が SAT と返すのは、現在の部分割当がすべての節を満たす場合である。未割当変数があっても任意に拡張でき、すでに真になった節は偽に戻らない。したがって完全割当へ拡張したモデルが存在する。

DPLL は各決定変数について真枝と偽枝の両方を必要なら探索する。単位伝播は現在の部分割当に対して論理的に強制される値だけを加える。すべての枝が衝突で閉じたなら、すべての完全割当が少なくとも 1 つの節を偽にするため、モデルは存在しない。

どの順序でも完全な探索木を必要なら辿るため、正しさは変わらない。しかし早い段階で多くの単位伝播や衝突を生む変数を選ぶと枝刈りが増え、探索するノード数が大きく減る。

最後に行った未反転の決定まで戻り、その決定の反対値を試す。CDCL のように衝突解析から複数レベルを飛ぶわけではない。

現在の部分割当を拡張する任意のモデルは、その単位節を満たす必要がある。節内の他リテラルはすでに偽なので、残った \(\ell\) が真でなければならない。したがって \(\ell\) の伝播は論理的に強制される。

節は \((c)\) になるので \(c=T\) が伝播される。理由節は \((\neg a\lor\neg b\lor c)\)。含意グラフでは \(a,b\) から \(c\) へ辺が入る。

\(x\) と \(\neg x\) を消して \((A\lor B)\)。CDCL の衝突解析は、この操作を衝突節と理由節の間で繰り返す。

\(a=T\Rightarrow b=T\Rightarrow c=T\Rightarrow d=T\)。衝突節は \((\neg d\lor\neg a)\)。reason(d)=\((\neg c\lor d)\) で resolve して \((\neg c\lor\neg a)\)。reason(c)=\((\neg b\lor c)\) で \((\neg b\lor\neg a)\)。reason(b)=\((\neg a\lor b)\) で \((\neg a)\)。学習節は \((\neg a)\)。

現在レベル 8 のリテラルを除いた決定レベル集合は \(\{2,5,5\}\)。最大は 5。したがって level 5 へ backjump する。戻った後、\(p,q,r\) が偽なら \(\neg u\) が単位伝播される。

1-UIP 節は現在の決定レベルのリテラルをちょうど 1 つだけ含む。backjump 先は、それ以外のリテラルの最大決定レベルである。したがって戻った時点で他のリテラルは既に偽として残り、現在レベル由来の 1 リテラルだけが未割当になるため単位節になる。

1 個。現在レベルリテラルが 2 個以上ある間は、トレイル上で最も後ろの現在レベルリテラルをその理由節で resolve して消去する。

UNSAT。レベル 0 は仮定や決定を含まない基礎式そのものの論理帰結である。戻れる決定レベルがないので、元の CNF が矛盾している。

壊さない。restart は trail を消すが、原節と学習節は保持される。適切な分岐戦略と restart スケジュールの下で探索は継続され、学習節により同じ衝突原因を避ける。

watch されていない偽でないリテラル \(d=U\) があるので、watch を \(a\) から \(d\) へ移動できる。節は単位ではなく、伝播は起きない。

watch を移動できる代替リテラルはない。もう一方の watch \(c\) は未割当なので、節は単位になり \(c=T\) を伝播する。

偽になったリテラルは \(\neg x\) なので、\(watch[\neg x]\) を走査する。真になった \(x\) を watch している節は問題を起こさないため見る必要がない。

最近の衝突解析に関わった変数の活動度を上げ、次の決定で優先する。衝突の核心に近い変数を早く固定し、伝播や衝突を多く引き出すことが狙い。

出現する決定レベルは \(\{1,3,7\}\) なので LBD は 3。

学習節は原式の論理帰結なので、追加しても解集合を変えない。削除すると枝刈り能力は減るが、原節が残っていれば元の問題を解く探索としては正しい。実装では理由節として trail 上で参照中の節などは不用意に削除しない。

補助変数を無視し、元変数への割当だけを取り出す。Tseitin 節は補助変数が部分式の値と整合するように作られているため、元変数への射影が元の式を満たす。

NP-complete は最悪ケースの分類であり、実インスタンスが常に最悪とは限らない。CDCL は BCP、学習節、non-chronological backjump、restart、活動度ヒューリスティック、節削減によって問題構造を利用し、探索空間を大きく削る。

resolution と深い関係がある。衝突解析は衝突節と理由節の resolution 連鎖で学習節を導く。最終的に空節が導かれれば UNSAT 証明になる。

第一に、CDCL は衝突から学習節を生成して節データベースに追加する。第二に、CDCL は学習節に基づいて non-chronological backjump を行う。実装上は watched literals、restart、VSIDS なども現代 CDCL の重要な要素である。

基礎 CNF を保持したまま、一時的な仮定を追加して解ける。各呼び出し後に仮定は外せるので、節データベースや活動度、学習した情報を再利用しながら関連する複数問題を効率よく解ける。