新型コロナウィルスで世間は大変なことになっているけど、確定申告以外はコツコツとSplrの開発を続ける日々。第３号です。
ようやくChoroBTのバグが取れてSplr-0.3.1がリリースできました。いつものベンチマーク設定においても、どうも一つは多く解けるような感じ。そしてこれによって事実上、deep searchモードの引退になりました。開発は一つ階段を登った感じ。ただベンチマークの結果はそれほどよくない。SAT Competitionに出しても参加賞がもらえる程度だなあ。ということで引き続き0.3.2の開発を開始しました。0.3.1ではなんとGlucose流のヒューリスティック選択が有効に働いていない（設定していない項目があった）ので、その修正を始めたら、またこれが時間を取る作業で、ほぼ毎日ベンチマークを取る羽目に。さらにその途中で、タイムアウトした問題からもデータを取らないと効率が上がらないという全く当たり前のことに気付いて、SAT-benchと連携して結果の検証、対象問題の限定などのテストベッドの強化も色々とやっている最中。やはり問題がカテゴリに分割できると、それに集中したベンチマークが実行できるので大変に捗ります。
ということで3月になってからSAT Competitionへの参加を考えた開発になってきた。今年こそは参加したい。なんと言っても5000秒のタイムアウトで実行したベンチマークが一体どういうことになるのか、こういう機会がなければ決して拝めないからなあ。参加することが開発につながるはず。ということでベンチマークを何度も実行しながら修正を繰り返して煮詰まってきたので適当なところで0.3.2のリリースをしようと思ったのだけど、念のためにCadicalの性能を測ってみることにしたら、愕然、数倍（ちょっと開発者の立場で大袈裟な言い方をすると桁違い）の求解数だった。これはとっとといろいろな方面に散らばったdev-0.3.2ブランチのコードをmasterにマージして、全く新しいコードの開発というか移植を始めた方がよさそうだったので、0.3.2も特に目玉はないけどもリリースすることにしました。コアサイズで変数活性度のdecay rateを変えるという趣向以外はせいぜい内部構造のリファクタリング（リスタートが第6のモジュールになったのが大きな変更）がメインのリリース。
これからの開発ですが、短期的にはむしろベンチマーク環境のSAT-benchの機能改善が重要になってきたので、cadical対応を進めて何が差を生み出しているのかを真剣に検討することにしました。もしかすると当分はcadicalのコードリーディングになるかも。ということで次号に続く。