Vol.2, No.1.
UNSATlog
202101
あけましてSplr-0.6.0出ました。 それどころか0.6.1も0.6.2も出ました。 いやあ長かった。 その割にはむしろ圧倒的に性能劣化してしまってますが十分にベンチマークを回すだけのリソースがないんだからしょうがない。 どうでもいい「やってみたらよくなった」的な高速化は捨てる方向に舵を取ったのは長期的にはいい判断だと思いたい。
What’s Splr-0.6.0?
Splr-0.6.0の売りは、
- 依存crateの削減、
- タイムアウトを増加させれば求解数が単調に増加すること、
- 将来のためにphase, stabilize, stageという構造を土台にしたこと、
- ベンチマークの結果主導のよくわからない（理論的根拠のない）ヒューリスティックスを捨てたこと くらいだろうか。 おっと、その結果2倍くらい性能が悪くなったことも特筆しなければ。
ただし0.6.0のリリース直後に立て続けに出たpoint releaseによってまあ少しは改善しました。 0.6.1ではLBDの更新を、0.6.2では節削減のタイミングをstabilization のサイクルに合わせるようにしました（最近使用フラグをクリアする影響を除けば、はるかにゆっくり節を削減するので解けなくなることは原則としてないはず）。 遅くはなったけどだんだんよく鳴る法華の太鼓ってね。
ようこそ夏休み
夏休みが終わった！ようやく宿題できました。 やっぱりLBDはいい尺度だったんだ。ということで納得。
なんというかファイル名は2020-XX-XXでタイムスタンプは202101という収拾がつかないことになってしまった。 反省。 さてこれで去年のcompetition のproceedings 読んで、cactus plot書いて、論文読んだら新シーズンの始まり。 その前に圏論の入門を読んでしまわなければ。 巣ごもり生活に抵抗なし。
その他
大きめのSudokuに挑戦。 144x144は対応できたけど、400x400はCNFの生成でギブアップ。 ちょっと無理。
今後の予定
Splr-0.6.3がすぐにでも出せそうなのでまずはそこに集中します。 ベンチマークをすると時間を延ばしても全然求解数が増えないので、問題数を絞る代わりにタイムアウトを十分に長くした設定で何が起きているか調べている最中。 結果に結びつくかはまだまだ不明だけどUUF250の求解速度が感動的なくらい速くなっている。 ちょっと期待できるものになるのではなかろうか。