すっかり遅くなってしまった。あちこち怪我したせいで色々と時間をとられてしまいました。9月はパラメータチューニングだけやって0.5.2をリリースするつもりだったのだけど、実行時間に対して求解可能問題が単調に増えるソルバにしたくてやっている最中にまた脱線してしまいました。ということで特に成果なし。強いて言うなら、
StructOpts
への依存を削除。オブジェクトサイズがほぼ半減した!さらにlibc
への依存も実は std::time::{Duration, Instant} で代替できたのでこれも削除。今やSplrが依存するのはbitflags
だけ!
つい昨日気づいたけどリスタート延期の判断を矛盾発生時まで遅延させるのは筋が悪い。タイミングを逸している。作り直すべき。9月に散々試したいろいろなstabilizationの実験結果は全て放棄することになりました。まあ、リスタートに関するオリジナルの尺度は捨ててもいいかなと思っていたところではある。しかし、何を使っても実はベンチマークの設定が超短期間ならあまり意味がなくて、十分に線形に求解数が伸びていくことの方が大事なんだろう。これを実践するにはリソースがなさすぎ。
これまではchronoBTの理解ができていない箇所をうまいこと避けるような実装になっていたけど、レアケースでは無限ループに陥っていたことが判明。矛盾レベルのリテラルが一つしか含まれない矛盾節に対するバックトラックの処理を正しく実装し直した。
もしかしてと思ってリテラル監視節リストをVecDequeにしてみたりBinaryHeapにしてみたりしました。stabilizationと同じ効果があるのではと思ったのだけど、全般的にはむしろ性能悪化の傾向。計算量多すぎ。そもそもSplrのカクタスプロットが早い段階から悪化するのはやはり計算量のレベルの問題だろうか。
他に何かあったかな? 思い出したら追加します。
sudoku25が5000秒以内に解けなかったのが大変ショックなのでした。