2020-08-16
標準エラーで途中の状態を大量に出力していたが、これは debug ビルドのときのみにするようにしたら、ほんの少しだけ高速になった。(表) unit clauses の保持は、backtrack が連続したときには過去に保持していたものではうまくいかなくなることがわかった。したがって、backtrack が生じるときは毎回 unit clauses を再度探すようにした。その結果、多少以前の CDCL よりも遅くなってしまったが、途中で落ちてしまうようなケースを減らすことができた。
しかしながら、今だに落ちてしまうテストケースが存在していた(#10)。