年末から1月中旬までのSATソルバー開発記録unsatlogです。ひたすら再検討。同じところをグルグル回っているようなもので、今回も特に進展なしでした。
インパクトのあるタイトルなので読んでみたが、残念なことに系統的ソルバーではなく統計的ソルバーの話。ランダムウォーク的な精錬過程において極性の分散がすごくいい尺度になるという話。論文には全く系統的ソルバーへの言及がないのはうまくいかなかったからだろうか。すごくわかる気がする。以前phaseを数ビットに拡張する話があったのでEMA→偏差に替えるのはいいかもしれない。
と思ってSplrで実装実験したが、意外に結果が出ないもんだ。偏差が大きいものを優先するのはいいと思うのだが結果が出ない。偏差総和でearly restartをかけるのもありそうだが手をつけてない。
さらにこの考えから派生して変数ごとの矛盾の頻度(frequency of conflict; FOC)から現在の「問題」の難しさを判定してリスタートをかける方法に変化していった。が、こちらも結果が出なかった。やはり過去の履歴から将来の予測をするのは大変に難しい（マルコフ的な未来予測が可能ならNP完全ではないか）。さて、ではなぜLBDによるリスタートはうまくいくのだろう。問題の難しさではなく得られた知識そのものの評価だからだろうか。知識の有効性のマルコフ性？疑問だ。
どうしてdeep searchが必要なのかずっと疑問だったが、これはリスタートパラメータの動的チューニングをしているせいかもしれない。固定パラメータだとリスタートもブロックも起きない長いスパンが観測される。Splrは皮相的にパラメータの値を変えて無理矢理リスタートを起こしているのでそのような「リスタート停滞期間」を潰していた。そもそも探索のよさの評価を動的に変えていいものだろうか？筋が悪かったかも。評価を変えるのではなく感受性のスケールを変えるだけがいいのかもしれない。また、時間軸方向の利得最大化がLuby列ならこれはdeep searchの代わりになるかもと思ったがよく検討していない。
でかなりよさそうなものでベンチマークしてみたがやっぱり圧倒的な差が付いてしまう。なんでこのdeep search はこんなにいいのだ？また半年ほど悩む事になりそうだ。
今回の目玉。リリースノートではSplr-0.2.1は修正CHBを使っていることになっているけど、改めて論文と見比べてみると随分違う。これをCHBと言っていいものだろうか。リリースノートを修正しなければいけないかも。という事で論文を見ながら再実装してみた。
何度も実装ミスを繰り返しながら論文に忠実にCHB、その延長のLRBを実装して、deep searchなしでマイクロベンチマークでは若干の性能劣化で済むようになったが、UNSAT問題が全然解けない。そしてベンチマークではどうやっても論文のようないい結果が出なかった。deep searchを抜いたのが悪かったのかCHB の実装が悪いのか？
また、LRBはCHBにReason Side Rate(RSR)とlocality extensionのアイデアを追加したもの。全部組み合わせた場合が一番いいことになっているのだけど、それらに関する実験結果が（またもや）それを支持しない。locality extensionの計算コストはバカにならないんじゃないか？これは遅延評価でいいんじゃないか、splr-0.2.1がやっているような。。。
ということでほぼ一ヶ月検討した結果、0.2.1の実装はやはりCHBの一種であり（何といってもEMA的なdecayを掛けているし）、それなりに同じ効果を既に得られているという結論を出さざるを得ない。locality extensionは自然に実装されている。RSRの判断はまだついてない。
この手のヒューリスティックの検討に疲れたので軽いアイデアとしてpropagate中の未矛盾変数探索において最初に見つかったリテラルではなく、活性度が一番高いリテラル変数を選ぶ手法を思いついたのだが（活性度が高い変数は早く試されるので矛盾距離は短くなるはず）、これもうまくいかない。なぜ？探索コストの増大では説明できないことが起きている。このアイデアギブアップすべきかもう少し検討すべきか？
ということで引き続き結論を出すことが求められているのは：
やりたいことは
といったところだろうか。なんか全然進まない。