2020-06-03
状況
DPLL のデバッグができた（完）
CNFgen で作ったテストケースで自動テストするようにした https://gyazo.com/04e801c03e0408e9fe67ee505bc4985b
ただ、その変数割り当てが本当に valid かどうかはまだやってない（まあ多分大丈夫だと思うが、多分大丈夫は多分大丈夫じゃない場合があるのでこわい。ちゃんと検証するべき）
議題
A. CNF の探索が深すぎると Stack Overflow になったりする可能性があるので、可能ならそのようにすべきだが、いかんせん DPLL はそれが効くほど現実的に十分高速に問題を解けるわけではないので……。CDCL 実装時はそのようにすると良い。
CDCL
様々な heuristics なやつを実装して、性能比較をしている
x: 解けた問題の数
y: かかった CPU time
"CDCL" ってなってるのは CDCL を実装したやつ
マイナスから始まるやつらは、その heuristics を無効にしたもの
Restart という手法があって、これは学習節は保持したまま変数割り当てを初期化するものらしい。この Restart をいつやると効果的なのかを機械学習で決定しようとしたらしい（探索の深さなどを参考にしていつ Restart するかを決めたりはしていたらしい）
CDCL の理論的な説明
（この文書とともに CDCL の説明をしていただいた）
conflict clause (この辺まだしっかりわかっていない。メモを転記しただけ)
$ S = (\Delta, \Gamma, D)が、Unit Propagation で矛盾 (1-consistent) とわかったとき、
$ \Delta \land \lnot \alpha \vdash_1 \textrm{false}
例:
$ \alpha = \lnot x \lor \lnot y
$ \implies \Delta \vdash_1 \alpha
$ \Leftrightarrow \Delta \land \lnot \alpha \vdash_1 \textrm{false}がいえる。
$ \implies S \vdash_1 \lnot\lnot x, \lnot\lnot y
$ x, yがそれぞれ真であると決め打ったら矛盾が出てきて、ここで $ \alphaはその原因で、$ \alphaは$ \Deltaから導かれるものであるから、$ \Deltaに$ \alphaを学習節として加えたら、$ \alphaを原因とした矛盾が今後起きなくなる。
次回までにやりたいこと
これらを読む
ある程度親しみのある文書を読むことで基礎知識を取り入れていきたいので
CDCL の理論的説明を厳密に追いたいので（assertion level について見たりしたい。上で書いた conflict clause の話もちゃんと自分で追う必要がある）
実装寄りの情報も気になる
これからの方向性?
↑みたいに、様々なものを実装して性能比較をする