2020-08-05

状況

DPLL と CDCL で共通する部分のコードを一つにまとめた

議題

MiniSat での実装の方法を少しだけ見た

MiniSat では clause の vector をもっていて、clause が充足されたかどうかのフラグをもっている。そのなかの literal は、assign されて消えたかどうかを持っていた？

backtrack させるときに復元を適切に行わせる

データ構造が工夫されていて最小な操作でできるようになっている

=> これをやるには全体を見直す必要がある

どの literal が assign されているかを見て、それに基づいて操作すると良い

Solver#undos, trail, trail_lim, level, reason

SAT の問題で「これは成り立っていてほしい」というものを考えるため、root_level という変数が用意されている

incremental SAT …… 追加で制約がきたときに、それのための satysfi assignment を探す

1からではなく、学習節を残しているので、次回は少しだけ効率的になっている。

incremental SAT をやらないならば、cancelUntil などは不必要