Vol.2, No.2.

UNSAT log

2月の振り返り

2月はSplr-0.6シリーズのポイントリリースを2つ。 まあ大したものではないのだけど、内部的にはイオンという考え方について色々試してみた。 そして3月になってからリリースされた0.7.0で結局削除ということになりました。 これも含め0.7.0はうまくいかないアイデアを結構整理して削除するようなリリースとなりました。

イオン

非常に単純化してSAT求解過程のモデルを作るなら、無矛盾なリテラル集合を大きくしていく過程をイメージするのがいいだろう。 この集合には変数活性度が高いものから組み込まれていく。 なので、ここに含まれていない変数は大きな活性度は持っていないはずである。 逆にこの条件を満足しない変数はそれ自身がある種のブロッカーすなわち「求解の妨げとなる変数」になっていると思われるので、（導入したステージベースのvar boostingという実装で）フォーカスして集中的に解くのは意味があるのではないだろうか、 そこで求解進行状況の尺度として、後から意思決定の尺度としてこの条件を満足しない変数を調査してみた。 fixされてなくて高いエネルギー準位にいるのだからそのような変数をイオンというのは妥当なものではなかろうか。 しかし、var boostingというアイデアが全然うまくいかないので、この尺度も短期間で放棄されることになりました。 まあ、そもそも適度なリスタートがあるのなら、変数活性度だけでうまくドライブされるはずではある。

0.6.3までのまとめ

ということでSplrはLuby列によって長さが制御されるステージベースで節削減、節包摂、変数活性度減衰率、リスタート条件を変えるという問題に応じた制御パラメータの動的摂動が売りのソルバーということになった。 まあ、妥当なところだろう。 で、これは結局0.1時代のなぜかいい結果が得られていたassert数が伸びない時にはリスタートをブロックする話とさほど違わないものなのだった。 本当に0.3歩前進、0.2歩下がるという感じだ。

0.7.0リリース

3月にだいぶ食い込みましたが今日0.7.0もリリースできました。 このバージョンではrestart blocking threshold を変えるだけではなく、var decay rateも変えて変数順序の逆転が起きにくくするようにした。 restart 条件を厳しくするだけではstabilizeにならないのではなかろうか。 そして、eliminatorの設定を変えてみた。 節数や変数数を闇雲に減らすより、依存グラフが大きくならない、よい学習節を作り、将来の矛盾生成効率を上げることの方が重要のようだ。 このようなサブモジュールの調整だけで終わって0.6.4がリリースできると思ったら、最後にローカル変数のexport周りを修正したので行数的には大きな変更になり、trait 含めてexportするものがいろいろと変更されたので性能は上がってないけどマイナーバージョンあげるしかないよなあというリリースになりました。 全然ベンチマークでは性能改善してないみたいけど、UF360とかの問題では目に見えてよくなっていると思うのだけどなあ。

すいません、嘘つきました。

Splr-0.7.0をリリースできたのは上の文章を書いた3月9日ではなく12日になりました。 文章書いている時にはgolden masterはできていたつもりだったのですが、求解中に10万回を超えるほどのリスタートを行うソルバからちょうど10万回目のコンフリクトで戦略の適合を行う古いコードを削除しても問題なかろうと思ってその他のクリーンアップと合わせてコミットしてみたら、360変数3SATのベンチマークが3800秒台から5000秒台にまで遅くなってしまった。 この因果関係を見つけ、パラメータチューニングでなんとかなるのか、ならなかったらどうするのか検討するのに1日2日では対応できませんでした。 結局、3800秒台は回復できないままですが、この4日間で、

• ProgressASG の定義差し替え
• GeometricStabilizer の改訂
• ASG, LBD の閾値チューニングし直し
• select_decision_litでindex errorが発生。searchのループ作り直し

などやって4200秒まで持ち直したあたりでもうタイムアウト。 もう十分だろう＆タイムアウトだ、ということで先ほど日付が変わる直前にリリースしました。

今月の目標

先月立てた目標がなかなか達成できてないので、今月もSplrの開発をお休みして、ということは今年もSAT competitionには出せなくって、論文を読むべきなのですが、論文を読む前に圏論の勉強をしていたり、ClauseIdの一部をポインタに切り替えると性能が上がるかどうかに非常に興味が湧いてきたり。。。 いや、論文読む方が大事だって！

なんか発行日が一ヶ月遅れのような気がしてきた。内容ではなく発行月で考える方が一般的な気がする。