JOI 2018/2019 春合宿講義４「充足可能性問題」

（個人用のメモにつき，解読不能です）

充足可能性問題 (SAT)
論理変数 True か False
論理式論理変数と NOT, AND, OR で出来た式
与えられた論理式 f(x, y, … , z) が True となるような x, y, … , z の割り当ては存在するか？
存在するとき：SAT（その割り当ても返す）
存在しないとき：UNSAT
例：(x || y) && (!x || z) && !y → SAT(x, y, z) = (T, F, T)
いろいろな応用
・プログラムの性質の証明，集積回路の設計支援（反例・バグをみつける）
・パズルのソルバー

SAT と反例，UNSAT と証明
満たしてほしい条件（性質を）式にする → 条件を満たす割り当てを探す
見つかれば，それは条件の反例になっている →バグ発見
SAT ソルバーの中には，UNSAT に対して証明を出力してくれるものも → 元の性質の証明になっている

CNF 形
リテラル (literal) : 論理変数 x またはその否定￢x
節 (Clause) : リテラルを OR でつないだもの
CNF (Conjunctive Normal Form, 連言標準形)：節を AND でつないだもの
すべての論理式は CNF に変換できる

一般に NP-Complete だが簡単に解ける場合も Cook-Levin の定理
論理式のクラスを制限すれば簡単に解ける場合も

Unit Propagation (UP)
節を前から見ていき，条件を明らかにする

簡単に解ける場合 2-SAT
節の長さがすべて 2 のもの
リテラルの間に辺を張ったものを Implication graph という
強連結成分内は同じ値なので，x と￢x の両方があると UNSAT
強連結成分ごとにまとめて DAG を作ると，トポロジカル順序の下から順に割り当てられるので SAT

簡単に解ける場合 Horn-SAT
￢がついている変数が 1 個以下，￢がついていない変数はいくつでも OK
Unit proragationの後，￢がついていないリテラルを満たせば OK

数独を解く

At Most One 制約：AMO(x1, x2, … , x9)
x1, x2, … , x9 のうち高々 1 つだけが True
At Least One 制約：ALO(x1, x2, … , x9) = x1 || x2 || … || x9
x1, x2, … , x9 のうち 1 つ以上が True
AMO(x1, x2, … , x9) && ALO(x1, x2, … , x9)：x1, x2, … , x9 のうち 1 つだけ True

x772 で 7 列 7 行に 2 が入っていることを表す
行と列と 3 x 3 のブロックの条件を AMO, ALO を使ってあらわす

Naïve encoding
!x1 || (!x2, !x1) || … || !x1 || !x9
!x2 || … || !x2 || !x9
…
!x8 || !x9

Product encoding
新しい変数 u1, u2, u3, v1, v2, v3
!u1 ならば (!x1, !u1) ならば (!x2, !u1) ならば !x3
!u2 と !u3 も同様
AMO(u1, u2, u3)

Commander encoding
!c(0, 8] ならば !c(0, 4], !c(0, 8] ならば !c(4, 8], !c(0, 4] && !c(4, 8]
!c(0, 4] と !c(0, 2] も同様

Bitwise encoding
新しい変数 b4, b2, b1

Sequential encoding

At-Most-k, At-least-k 制約なども
新しい変数と使う節の数はさまざま
Bitwise 追加変数 O(logN)，節 O(NlogN)
Sequential 追加変数 O(N)，節 O(N)
変数や節の数が少ないほど良いとは限らない

Dimacs format
CNFを表現する標準的なフォーマット
￢a
￢b || a
￢c || a || b || d || e
a || c || e
を以下のようにする
p cnf 5 4
-1 0
-2 1 0
-3 1 2 4 5 0
1 3 5 0

DPLL (Davis-Putnam-Logemann-Loveland Procedure)
ただの全探索
高速に探索するには，解の空間を枝刈りしなきゃいけない
→ CDCL (Conflict Driven Clause Learning)
コンフリクトを検出したときに記録しておいた割り当てた理由を元に原因をたどる
原因が分かったら解決する条件式を追加，もう一回前に戻って処理する

Watched Literals
DPLL + CDCL は Unit Propagation を多用
→ Wathed Literals 遅延データ構造の一種
リンクを張ることで考慮するリテラルを減らす

Minisat http://minisat.se/
DPLL / CDCLを実装した最も有名なソルバーの一つ
コンフリクトの解析をどこで止めるかが性能に影響する
コーディングの勉強にもなる vector, map, queueなども実装されている

その他のソルバー，問題

Look-ahead solver
分岐する前にいろいろな変数に対して割り当てと UP を行ってみて，どれぐらい式が簡単になるかを調べる
→ もっとも式を簡単にする変数を採用
変数の選択にコストがかかるが，効率よく式を簡単にできる
ソルバーによって有利・不利がある
グラフの直径や節・変数の数などによる

2-SAT に対する確率的アルゴリズム
2-SAT インスタンスに対して，
・満たされていない節 c = (x || y) をランダムにとり，
・x か y かどちらかをランダムに反転させる
期待値として O(N^2) 時間で解が見つかる
2 つの割り当ての間の距離を異なる割り当ての個数とする（ハミング距離）
ある解 z を考えたとき，ある時刻での割り当て x(t) との距離は 1 増えるか減るか
2-SAT であるので，増える期待値は 1/2 以下
[1, N] の数直線上でランダムウォークすると O(N^2) 時間程度で d(z, x(t)) = 0 に行きつく

確率的局所探索 (SLS, Stochastic Local Search)
WalkSAT：さっきのアルゴリズムの発展形
以下を解が見つかるまで繰り返す
・満たされていない節 C をランダムにとる
・確率 p で C の中のランダムなリテラルを反転させる
・確率 1 - p で C の中から反転させたときに満たされる節が最も増えるものを反転させる

Breakout
節に重みをつけて，反転させたときに満たされる節のスコアの和が最も増えるものを反転させる
スコアを改善するへんすうがなくなった時に（局所最適），満たされていない節のスコアを１増やす

変数と節の関係をグラフにすると，構造 (Local Cluster) があることが多い
ランダム生成のインスタンスとは性質が異なる

Incremental SAT solver
ある CNF 式 f に対して解いた後，節 (c1, c2, … , ck) を追加するクエリが与えられる
f' = f || c1 || c2 || … || ck
これを解く際に，もとの f を解くときに使った学習節や変数・節の重みを再利用できる
応用：ハミルトン閉路問題
グラフの全ての頂点を通る閉路を求める問題
「すべての頂点に対して入次数＝出次数＝１」という制約を満たす x_uv（u -> v の辺）の割り当てをもとめる
全ての頂点を通らない閉路があったら，これを使わないという条件を追加してまた解く
応用：SMT (Satisfiability Modulo Theories)
矛盾するものが見つかったら，このケースが出ないようにする条件を追加したf'を解く

#SAT
CNF 式 f を満たす割り当ての個数を数え上げる
MAX-SAT
すべての節を満たさなくてもいいので，満たされた節の個数を最大化する割り当てを探す
SLS（確率的局所探索）がそのまま使える
これに特化したソルバーもある
両方とも 2-SAT に限定しても NP-hard

The Chaos Within Sudoku
簡単な数独はいろんな数を試さなくてもすぐに決まるが，難しいものはいろいろ試す