2020-08-19

状況

前回までは CDCL が DPLL より遅いという問題があったが、毎回 decision variable を選ぶというバグがあったことがわかり、修正したら速くなった

「オーバーヘッドが大きい DPLL」

議題

次にやること

バグ修正、より大きなテストケースを追加する

backtrack のために Solver 全体の状態を history として持ってしまっているのを、（MiniSat などを参考にしながら）より軽い実装にする

最終的にやること

各ヒューリスティクスによる速度の差をグラフに表す

MiniSat の実装は様々なヒューリスティクスをキレイに組み合わせている

hard constraints: すべて満たす必要がある

soft constraints: できるだけ多く満たす

↑ これを多く満たせるようにする MAX SAT

CDCL と SMT ソルバの関係性について聞いた

与えられた述語論理式を命題論理式に抽象化して SAT ソルバーに解かせる

もしこの段階で UNSAT ならば、元の述語論理式も UNSAT であると確定する

もしこの段階で SAT ならば、一つの命題変数に抽象化される前の述語変数が SAT ソルバによる変数割り当てを参考にして真または偽であると仮定し、その述語論理式の充足可能性を各理論のソルバを用いて調べる

この結果、その述語論理式を満足することができたら、与えられた述語論理式は SAT である

その述語論理式を満足するようなものが見つからなかった（UNSAT）の場合は、SAT ソルバによる別の変数割り当てを探索する