Vol.1, No.2.
はじめに
今期のビッグイベントはなんと言ってもSplr-0.3.0のリリース。めでたい。
Splr-0.3.0リリース
三ヶ月の開発期間を経て2月10日にようやくSplr-0.3.0をリリースすることができました。その更新内容から大事な部分を拾ってみると、
- 変数選択機構を最新のLearnt Rate based Branching with Reson Side Rewardingに基づくものに変更したこと。なお更新の単位は矛盾ではなく割当てから未割り当てまでで考えることにした。これは単なるアイデア。
- タイムアウト用のスレッドを導入してEliminatorを残り時間を考えて自発的に中断するようにしたこと。こうしないと大きな問題では何時間でも変数除去をやっていたようだ。
- 変数活性度の減衰率が意外に重要だということがわかったのでやや小さめにしたこと。これは小さくする、すなわち学習による更新が稀にしか起きなくすることで、結局リスタート時に大きな変化を生じさせなくする効果があり、それはつまりdeep searchモードでリスタート発生を抑えようとしたのと同じような効果があるらしいことがわかったから。このパラメータだけで求解数が大きく違う。またdeep searchの理解が少し進んだので、deep saerchの重みを減らした（期間の減少、定期的な通常モードへの復帰、クールダウン期間の減少など）。
- あとは標準的なtraitを様々導入したこと。サブモジュール間のインターフェイスが変わったので0.2.2ではなく0.3.0にナンバリング。
これで6000行のプログラムの2000行ほどが更新されることになったし、質的にも結構大きな修正だった。多分この文章以外にはどこにも書かないだろうけど、上記強調部分は眼から鱗の出来事だった。
ChronoBTの試み
前回から0.2.2の目玉として考えてきたChronoBTの実装は論文をちゃんと読んでみると、バックトラック時の再割り当ての手間を省くのは主目的ではなく、バックトラックコストが少ない学習節の作成から得られるむしろ副作用のようなものであることがわかった。ということでこれまでの安直な実装を目指していたブランチは全て見当外れ。0.3.0のリリース後に論文見ながら一からやり直すことになった。これが0.3.1の主目標になるでしょう。
ベンチマーク変更
ベンチマークをSAT Competition 2018ものからSAT RACE 2019に変更しました。過去のデータが使えなくなるのは大きいので延び延びになっていたけどようやく重い腰をあげた。下図が去年の公式データの結果のカクタスプロット（2つほどなんか変なデータがあったので除去が必要だった）。やはり500秒くらいで既にある程度の傾向は見て取れる。現実的な到達目標にしようと思う。これなら並列実行すれば今の環境でも1日掛からないくらいで1回のベンチマークを終わらせることができるし。
さて、ここに（並列実行の影響補正用の適当なスケーリングありで）Splr-0.3.0でやってみた結果を追加してみると、絶望するほどじゃないじゃん。少なくとも下位グループの中位には位置づけできそうな感じだ。
あとはChronoBTを導入することで、どこまで伸ばすことができるか。期待しよう。
さらにJupyter labを導入しました。まあ慣れてしまえばいいことでRもPythonも同じようなもんだな。Pythonでプログラミングするつもりはないけど、まあ21世紀のPostScriptのようなもんだろう、図形表示言語という意味で。Rustカーネルも入れてみたけど、使いところがないなあ。
結び
さあChronoBTの実装だ！下位グループから脱却できるかなあ。