Vol.2, No.8.

Finally Bugs Fixed in July

ようやくバグフィックス終わった。7月に0.10.0リリースできました。

なんだったのか

Splrの開発史上最大最長の難問になった今回の不整合バグがどうやって発生したのか振り返っておきたい。現れたバグは様々だった。

• UNSAT certificateがおかしい — https://github.com/shnarazk/splr/issues/122
• 単位節が伝播を起こさない — https://github.com/shnarazk/splr/issues/119
• 割り当てられても伝播されない — https://github.com/shnarazk/splr/issues/117
• 依存グラフにより高いレベルのリテラルが出現する — https://github.com/shnarazk/splr/issues/116
• 除去リテラルを戻すとおかしい — https://github.com/shnarazk/splr/issues/115
• 依存グラフでbinary clauseでの方向が逆 — https://github.com/shnarazk/splr/issues/114

とまあ呆れるくらい様々。 もうSATソルバーとしてはほぼ壊滅状態だった。

で、これらの原因は一つではなかった。 0.10.0のリリースまでに潰したのは以下の通り。

• chronoBTの最上レベルリテラル数が1の場合はchronoBTかそうでないかに関わらず同じ処理をしなければならなかったのだが、そうなっていなかった。論文の何気ない記述に引っ張られてしまった。
• chronoBT混在環境においてcancel_untilの処理が不適切だった。割り当て順序の逆転が起きていて、正しい依存グラフが作れなくなってしまっていた。
• 単位伝播は問題ないのだが、Eliminatorやvivifierが生成する節がClauseDBに適切に登録されてなかったため、伝播に失敗する単位節が存在していた。またUNSAT certificateへの反映が不適切だった。
• 除去変数を戻すモデル拡張器があやしいようなそうでないようなわかりにくいコードだった（sliceやiteratorを使ったもっとRust的（モダン）で意味が取りやすいコードに修正した）。

どれを取っても致命的なのだが、よくもまあもっと早い段階で気づけなかったものだろうか。 おおよそ1年近くSplrはバグ持ち、それもSATソルバーを名乗れないレベルのバグ持ちだったと言うことがわかり、赤面してしまう。

After 0.10.0

というわけで無事にSplr 0.10.0をリリースしてから、正しさを壊さないようにしながら、ちょっとづつパフォーマンスチューニング中です。

まずはLuby stabilizationが全然よくないので改善中。 気づいていたけども0.10.0にはどうやっても入れる時間的な余裕はなかったので後回しにしていた。 その後、どうもモードの変更を節削減と同期を取るのが相当に効くらしいということがわかったので、そちらを採用。 aes.cnfは0.10.0だと10000秒程度掛かるのが普通なんだけど、この部分を変えてみると2000秒台になっているし、sat-benchの結果もSplrのベストにかなり近くなった。 小さな変更なのだがリリースする価値がありそうだ。 初めて使ったalgorithm2eで書くとこうなる。 Reduction, Elimination, Vivification、そしてモードスイッチ、と綺麗な流れじゃないか。

ドキュメントを更新して数日中に0.10.1としてリリースの予定です。

あとは

• 重複節の除去：どうもこれは重要のような気がするので早いところ統計データをとってみるつもり。in-processorを頻繁に起動するSplrでは無闇に重複節を発生させている可能性が捨てきれない。clause reductionの後にclause vivificationを実行するように順序を変更したことである程度は削減できているような気もするがさて？ 実際の戦略として組み込む価値があるかは未確定だけど、いくつのソルバーがこの機能のオプションを持っていたはずだし、clause.litsをhash値にマップすればそれほど計算量は高くならないのではないだろうか。

という感じでまあぼちぼちと。 それよりは

• 溜まりに溜まった論文読んで、
• proceeding読んで、
• benchmark suitを今年のものに入れ替えて、 とこれだけやれば8月は終わりです。