最終発表会/スライドに入れたいこと
流れ
1. 動機
2. SAT の説明
具体的な入力と出力を掲載
応用例を並べる
数独に着目、エンコード前とその後を掲載
SAT の問題を解くことは難しい(NP 完全である)
多項式時間アルゴリズムがあるかどうかがそもそもわかっていないが、おそらくない(P ≠ NP)
「ナイーブな方法として真理値表を書くことができるが、それでは全くかなわない」
💭9x9 の数独の問題を解かせてみたら DPLL でもほぼ一瞬で解けてしまった
4x4 だと $ 4^3 = 64 個の変数が必要なので、考えられる真偽値の組み合わせは $ 2^{64} \approx 10^{19} 通り。
コンピュータが一秒に $ 10^9 通りを検証できたとしても、全くの工夫がないので最悪でも $ 10^{10} 秒 \approx 316 年かかってしまう
⚠️ 「これぐらいの数独のサイズでも、真理値表を書いていては全然間に合わない!」
SAT の応用ではどれぐらいの大きさの問題を解くのか
最先端のソルバーはこれぐらいの規模の問題を扱える(SAT Competition のページより)
3. SAT ソルバーの代表的なアルゴリズム
DPLL の拡張が CDCL で、これが代表的なものである
DPLL の拡張として節の学習を追加することで探索の効率化が進んだ
これが非常に効果的だった(実行時間のグラフを出す)
SAT Competition で優勝している主要なソルバーに搭載されるアルゴリズム
これの動作原理が複雑であり、解説も少ないので「可視化」に意味がある
他にもアルゴリズムはある
確率的な(survey inspired decimation)
SAT の問題を多項式で表し、多項式用の最適化アルゴリズムで解を探索(FourierSAT)
4. DPLL の説明
DPLL には単位伝播と空節の処理がある
単位節があると内側のリテラルが
Appendix
CNF の単純化