Vol.1, No.5.

Splr-0.4.1リリースの5月

今月たてたissue及びブランチは以下の通り：

• No restart for LR and Stabilization
• 20200514-incremental
• 20200524-handle
• 20200502-new-select
• 20200503-litpointer-on-0.3.1
• 20200509-new-rephrase
• 20200510-restart-for-lr
• 20200514-incremental
• 20200516-no-restart
• 20200518-tuning
• 20200524-dead
• 20200524-handle

Splr-0.4.0以降の分をまとめると

• incremental SATソルバの実装
• stabilizationの解釈と変数選択機構の実装
• リスタートの必要性

といったところ。順番に振り返っていきましょう（ここは大友良英氏の口調でお願いします）。

Incremental SATソルバ

初めて他の人から反応をもらったので、考えていなかったインクリメンタルな求解機構、およびWASM環境下でコンパイル可能、実行可能への変更の実現をしました。 インクリメンタルSATソルバを実現するのに大きな問題となったのは、実はeliminatorが非可逆的な変換をしていることです。 まあ当たり前なんだけど（正しい）ソルバの処理過程は論理式の等価変換なので、ソルバが停止した状態でassignとcdbが保持している情報は実行前の与式と論理的に等価なはずです。 だから、求められた解の否定を加えて求解し直すだけでインクリメンタルソルバになるはず。 ところがeliminatorは非可逆的な変換（具体的には変数削除処理においてモデル拡張時に必要としない節が完全に削除されてしまう）をやっているので、このナイーブなアイデアはプリプロセッサを含めて考えるとうまくいきません。 論文や他の実装を見ずに対応策（削除されていた節を新たなリストに保存し、次の求解開始前にcdbに戻すという処理）を思いついたのでやってみました。 かなり網羅的なテストでうまく行っているので多分これでいいのでしょう。

結局、次の求解開始前に呼び出すAPIとしてresetを, 変数、節、割り当てをそれぞれ追加するAPIを SatSolverIF に追加して完成です。 高レベルなIFとしてイテレータも追加したので、

for ans in Certificate::try_from(...).unwrap().iter() { ... }

と書くだけで全解探索処理ができるのはなかなかいいな。

またWASM環境に対応しました。 要はstructoptとタイマ機能を条件付きコンパイルの対象にすればいいのだろうと思い、structoptとlibcをoption扱いに変更して作業終了。 のつもりだったけど、実はコンパイルできるのだけれども std::time が実行中に対応していないエラーを吐き出しているのに気づくのに一週間掛かってしまいました。

この件に対応して（結局自分で確認する羽目になってしまった）0.4.1をリリースしました。 ちなみにWASMだとSplrのコードは140KBくらい。 Darwin上のexecutableと比べて意外に小さいというべきか、そっちが異常に大きいというべきか（C++で書かれたGlucoseやCaDiCaLと比べてRust製Splrは一桁くらい大きいからなあ）。

この修正によってstructoptなどがオプション扱いに格下げされてしまったので、Splrをインストールするには

cargo install —force —path . —features cli

とすることが必要になったけど、まあこれくらいなら許容範囲でしょう（Splrは一義的にはライブラリではなくexecutableパッケージなのだ）。 ここまでできたら、ステップ実行でアニメーションを実現する機能もいつか作りたいものだなあ。 continuationかyieldあたりでsearchの中断できないかな。

Stabilizationの解釈と変数選択機能の実装

Splr-0.4.0はそんなに悪くない性能なのだけど色々と新しく追加した機能に見合った性能向上がみられたかというとそれほど肯定的なものではありません。 世間的にいいということになっているアイデアがそれほどうまく動いていないなあと思って見直してみると、0.4.0はStabilizationの導入が大きな売りのはずだけど実はリスタートの抑制をしてないじゃん！ と言うことでもう一度設定を変えながらベンチマークをやり直し。 これが些細な修正ごとにベンチマークを走らせることが必要でえらい時間がかかってしまったけど、結局0.4.1で生き残ったのは、Stabilizingモードでのベスト割当てのリフェーズだけで、やはりリスタートの抑制はしない方がいいということになりました。 0.4.0と0.4.1の間の変更点は（アカデミック的には）ほとんどなくて、search関数が性能悪化をもたらさない範囲で合理的な流れに変更されたくらいです。

リスタートの必要性

一体何度目なのかわからないけど、リスタートの必要性も再検討しました ➡️https://shnarazk.github.io/2020/2020-05-20-LR-needs-something/

• StabilizationはSAT問題に対してうまくいくという話でこれはわかる。
• 逆にUNSAT問題にはリスタートが必要と昔から言われている（これもわかる）。
• どちらの問題かわからないから（そしてlong tailに捕まらないように)両方を切り替えながらやろう。
• 一方LRは矛盾発生率を最適化しようとする。矛盾を頻発させればUNSAT問題は効率よく解けないだろうか？
• VSIDSは何をやっているのかわからない。もしかしたら矛盾回避率の最適化かもしれない。矛盾を回避していたらSAT問題が効率よく解けないだろうか？➡️https://shnarazk.github.io/2020/2020-05-19-two-heuristics/

このあたりの整理は必要ではないかと。

出てきた（極端な）アイデアの一つがexploit&exploreのバランスが取れればリスタートはいらないというもので、いくつかの例ではうまくいくのだけどSAT race2019レベルのベンチマーク設定だとよくないので放棄せざるを得ませんでした。 ただ極端な設定の割にはそれほど悪くないのよねえ。

ここまで極端なことを考えないものとして、VSIDSとLRを(stabilizationモードに合わせて）定期的に切り替えるという混合戦略もやってみたけどダメでした。 今年のcompetition前にもう一度検討する時間は取れないだろうなあ。お蔵入りかな。なにかあればnoteを更新することにします。

おわりに

現在Splrは去年competitionにエントリーしてもそんなに恥ずかしくないところまで来ている。

間違った解も出てないし、本当にエントリーを考えようと思っているのだけど、改良するにはせいぜい後一ヶ月。 うーん、何ができるのか戦略的に考えなければ。 勝負の6月だ。