Vol.2, No.9.

順調な8月

0.10のリリースから一ヶ月。この間に0.11もリリースできました。現在0.12の準備中。

0.11リリース

正しいことが売りの0.10をリリースするために、ちょっと後回しにしていた、Luby stabilizationのタイミングの調整をしました。 これは結構性能に影響するものでした。 あとはどうでもいいマイクロなチューニングの削除として、vivifierの対象節選択部を簡略化。

大物はないけど、ベンチマークの結果はそこそこ改善。 ベストではないにしろ今年リリースしたバージョンでもたらされた壊滅的な速度低下がかなり解消しました。

その他

SAT-benchをSAT Competition 2021対応にして、2018年のベンチマーク問題を削除。 2019年の問題も近々削除の予定。 というわけで、長らく愛用してきたT56.2.cnfともいよいよおさらば。 そしてKlara and the Sunを読み終わったあとは溜まりに溜まったSAT関連の論文読みモードに入りました。

さらにCaDiCaL 1.4.1をnix package化。 すぐにマージされたので、調子に乗ってKissatもパッケージングしようとしたら、なんとOS依存で挙動が変わる。 正確にはMacOSではUNSAT certificateが壊れることがある。。。。 ちょっと手が出せなくてやる気を失った。さらに言うとこういうOS依存なコーディングまでしてあるプログラムに張り合うのはちょっと戦意喪失気味になってしまいました。 まあローカル探索ソル馬を組み込むのはもう避けて通れなさそうなんだけどねえ。

いっそのことUNSAT certificate verifierの実装に舵を切ろうかしらん。。。。

9月の予定

• 論文読む, Theory and Applications of Satisfiability Testing はいつものようにSAT関係少ないからもう読むところないよ
• Local search solverは、、、大物すぎる
• binary clauseを消しちゃおうかな。これは0.13だな。
• Hash面白かった。vivificaitonまたはeliminatorの実行中だけでも実装してみようかな。

というようなことを考える一ヶ月という感じで。