Vol.1, No.7.

UNSATlog

今月のキーワード

Debugging Vivification
Restricted Stabilization
Maximum LBD of Dependency Graph
Duplicated Bin-clause Checking
Change of Restart Point

Vivification update

先月、実装終わったつもりだったvivification。本当に効果あるのかどうかベンチマークを走らせているはずなんだけども、他のアイデアが出てきたりして、なかなかコードがフィックスしない。そして7月も下旬になってから実はエラーを出していたことが判明しました。Splrでは決定による含意での割り当てはエラーを返さないのが原因なので、割り当てチェックを走らせることで対応します（これでいいはず）。

節の重複検査

その修正中のダンプを見ていてvivifyされて短くなった節が同じ節であることが意外に多いことに気づいたので、binclauseの時に限りbin_watcherを使って重複検査をするように修正。eliminaterも同様の検査を追加。watcherを一本たどるだけなのでコストは低いはず。まあ効果の程は不明だけど問題ないでしょう。

Fixed or Solved -> Asserted

vivificationに関する論文では、単位学習節によって割り当てが確定することをassertと読んでいたので、これまで使っていたsolvedという語をassertedに変更することにしました。うーん、そういうwordingは頭になかった。

Restart revised

vivificationとstabilizationを混ぜたチューニング中に突然閃いたのだけど、stabilizationが必要なのは、必要なんだけどもLBDが大きいので捨てられる学習節を救うためなので、そもそもLBDが大きくても捨てなければいいんじゃないだろうか？そのためのいろいろなアイデアがあったわけなんだけども、要るか要らないかを、履歴を基に判定すれば難しいことはないんじゃないでしょうか。要るか要らないかの判定はめちゃくちゃ簡単で、矛盾解析中に使った節のLBDの統計値と比較すればいいだけ。ということで「依存グラフ中の最大LBD」のEMAを保持するようにして、これで獲得学習節のLBDのEMAを比較する手法を実装してみた。ただし節は実行中にLBDが段々と減少するよなぁとか色々と考えることはあるので、現在チューニング、ベンチマーク中です。

節サイズ4バイト減

その話に関して、もしかしてLBDの初期値も保存した方がいいのだろうか、footprintを増やしたくはないなあと思ったけど、rankにusizeを取るのは妥当だろうか？ 6万レベルもあれば十分じゃない？というわけでrankは8Byteから2Byteへと激減しました。flagと合わせて4Byteも減りました。

リスタートIF作り替え

SplrはGlucose以来の矛盾が発生した時に実行されるforce_restartと矛盾が発生しなかった時に実行されるblock_restartの2関数を使って動的リスタートを実現していましたが、これもやっぱり議論の余地がある。きっちりデータ残していれば判定は矛盾発生時の1箇所だけでいいんじゃなかろうか。そして関数を2つ用意する必要ないんじゃないか。思考実験では問題なさそうなので、まる1年は変更していなかった部分を変更してみました。restarterは各所でSolverEventを受け取り、判断は矛盾発生・対応後の1箇所。これでいいのでは。

Rephase to the best

stabilization中に最良（部分）割り当てに戻ってくるのはいいけど、多く問題で早々にいい割り当てが出てしまった後、まったくその割り当てを超えられないという経過を辿ることが多いようだ。割当量が同じでも後から見つかった方が制約がきつい中での部分解なのでこちらを優先した方がよさそうだし、そうするとわずかに最良に届かなかったとしても後から見つかった部分解は考慮に足るのではなかろうか。というわけで最良割り当ての判定に使っている最大割り当て数も腐らせることにしました（正しく腐れているかどうか検証待ち。）。

Stabilizationのバリエーション

何も考えずにstabilizationの持続期間を増やしていくと（それは必要なことであることは十分わかるんだけど）、あまりにもリスタート回数が減ってしまうので、何かトンネルされることはできないだろうか。ということで思いついたのが現在のfocal pointから大きくずれなかったらリスタートを許してもいいんじゃなかろうかというアイデア。これまではrephase、リスタートの完全抑制の２種類の方法を使っていたけど、これを

同じような割り当て列に戻ってきそうな場合はリスタートを許容（その後rephaseするかどうかは現在検討中）
そうでなければリスタートを抑制

に変えてもよさそうに思える。さらに言えば

stabilization中はこの制御法でdeep search（やはりrestartを止めるのはどうだろうかという疑問に戻ってきてしまう）
そうでなければ浅い矛盾を見つけるため従来法

としてもいいかもしれない。どちらがいいのかはLearning Rateのわかりやすい矛盾発生頻度の最大化に対する寄与の度合いとして、これがまたmulti-armed bandid問題なのか？？？うーむ、やること多すぎ。ということでアイデア豊作な一ヶ月でした。

おわりに

おまけにもう一つ。今年のSATの国際会議の予稿集がいつものようにSpringerのLNCSとして刊行されているんだけど、論文単位だとただでダウンロードできますよ。（あれ、これって期間限定でいつものことだっけ？いつも出遅れていただけだっけ？）というわけで論文も豊作でした。そして、来月までにはSAT Competition 2020の分析をしなければ。