Vol.1, No.8.
8月の目玉
Splr-0.5.0をリリースしました。表立ってはclause vilification の導入です。一方裏ではリスタートの尺度がオリジナルなものへ変更されました。これは今のところ充分な評価ができてないのでChangelogではundocumentedで済ませたという代物。宿題です。
Glucose-4.1との比較
前回, Glucoseと比べて全然遅いという話をしましたが、0.5.0はタイムアウトを100秒に設定するとoutperformできるようになりました。結構早い段階でこの成果は出ていたのですが、タイムアウトを500秒に伸ばすと100秒での求解数が10近くも落ちてしまうため、本当にいいのかどうかなんとも言えない。これはSplrがタイムアウト時間を考慮して{pre, in}-processorのタイムスロットを決めているため、ある時間で解ける問題がそれより長いタイムアウト設定で解ける保証がないことから生じた問題なので、本質的には仕方ないとしか言いようがありません。一方でこれはprocessorに与える時間に関するヒューリスティックスに改善の余地があることを示しているようにも思え、ついついその試行錯誤に時間を掛けてしまったせいでリリースが一ヶ月は延びる羽目になってしまいました。適当なところで打ち切ってパラメータチューニングは0.5.1にしようと思ったのですが、これまたパラメータチューニングで済むかどうか、やってみないことにはなんとも。 で結局タイムアウト500秒域では多分Glucoseを上回ることはないでしょう。やっぱりなんか根本のところで王道を外しているようにしか見えない。
リスタートについて
Clause vivificationとリフレーズの探求が0.5.0の主たる変更点ですが、後者を色々と試していて、特に一体Stableはどういう時に必要とされるのかを考えていて、結局オリジナルな尺度をリスタートモジュールに導入することになってしまいました。
- 学習節のLBDが大きくてもそれがリテラル断定(assertionの訳です）への道のりの途中ならそれを許容してもいいだろう。つまり非常に頻繁に活性度の更新が起きているリテラルが存在する間は（それは今大きな問題になっている重要なリテラルなのでその解決を優先するため）リスタートを抑制してもいいんじゃなかろうか。
- 学習節のLBDの良さはその相対地で決まるのではなく、矛盾解析に使われるかどうかで決まるのではなかろうか。直近の傾向が矛盾解析中に出てきた最大LSBのEMAより大きければそれはリスタートに値するのでは。
なんだかどちらもよさそうに思えて、実際実験結果もこれを棄却できてなさそうなので試しに入れてみました。
9月の抱負
生活が忙しくなって、さらに体力減少中なのでペースは落ちるだろうけど、processorのもうちょっとよい実行契機を見つけたい。これだけやって0.5.1を出したいものです。そしてSC2020に更新しなければ。