2020-09-23

メモ

CDCL はresolution proof をつくっているともいえる

UNSAT なら矛盾が導出される → resolution proof という、論理体系における矛盾を探していることになる

pigeon hole などだと DAG が大きくなって、UNSAT のときの証明の木が大きくなってしまう

random k-sat であれば、節と変数の比が 4.3 で難しくなる、のような……

→ 一見簡単そうに見えても、問題のサイズだけで難しさが決まるわけではない

原因となった clause が返ってきてる？

↑これを導出するための clause の情報が保持されていたはず

incremental SAT だと clause が増えていく

MiniSat の Solver#solve だと assumption が与えられている

与えられた assumption によって解くのを高速にしようとしている？