2020-12-02
状況
数独の問題を SAT 問題に還元して解くところまでやってみた。
clausesContainingLiteral というフィールドを CDCLSolver に追加することで、removeClausesContaining と removeLiteralFromClauses が実行されるときに availClauses を全部舐めるのをやめた
これのおかげで一部のテストケースで大幅な計算時間の改善が見られた（新:72b3ecb vs 旧:70265e8）。
graph-ordering-19.cnf は以前 21.28 秒だったのが 1.91 秒に
order-principle-19.cnf は以前 21.64 秒だったのが 1.90 秒に
他のテストケースでは軽微な改善が見られた。
しかしながら、total-order 系は以前として問題の難しさが上昇するにしたがって指数関数的に計算時間が増えてしまう。
数独を SAT 問題に還元してみたのが楽しかったため、他にも SAT に還元して解けるパズルはないか尋ねた。
また、ジョットクとは全然関係がないが、ipc_bot がS4様相論理の上で何かをやっている？らしいので様相論理とは何なのか尋ねた（ここで『論理学をつくる』を薦められた）。