Vol.2, No.10.

Recap

ちょっと遅れたけども9月にSplr-0.12.0リリースしました。 そして今年の研究動向をちょっとキャッチアップしました。

0.12.0

いくつかのヒューリスティックの見直しをしたらかなり性能がよくなった。 いや、depressionが解決したというのが正確かも。 また、多分、認められた研究結果とは相いれないのだろうけど、節に含まれるリテラルの活性度の最大値と節のrankから節の活性度を計算してみると、そこそこいい結果になったので、節にrewardを与えるのはやめました。 さらにVar、Clauseからフィールドを抜いてmemory footprintを抑えました。 Minisatの時代から存在するArenaは全然導入の見込みが立ってないけど、変数は半減、節も1割以上は小さくなったのでキャッシュヒット率は有意に改善したのではなかろうか。

気分よくリリースしようと（いよいよ）SAT cometition 2021の問題を使ってベンチマークしたら、またUNSAT certificateが壊れていた。 すぐにchrono-BTが原因だと分かったけど、それ以上の理由は全く検討がつかない。 しょうがないので、それと代替案の導入が目前だったのでchrono-BTを使わないことで解決させた。 ベンチマークの結果は少しだけ遅くなったけど、それでもほぼ過去最高のSplrがリリースできました。

性能が上がったことは大変望ましいんだけど、ベンチマークの検証が無視できなくらい長くなってきた。 まともなソルバだとその結果の検証にはおそらくベンチマークに要する時間と同じかそれ以上かかるみたいだ。 電気代怖い。

Trail Saving

9月に読み始めた新しめの論文に早速影響を受けてSLSを導入しないことにはいかんよなあと思いつつ、現実的に0.12で問題となったchronoBTを捨てるために喫緊の課題となったtrail savingの実装にかかりました。 これもやや苦戦中。 少しでも性能が上がるようなら0.13として早めにリリースの予定。

10月の予定

Trail saving以外には、うーん、もっと論文読まにゃ。 SAT2021で関連深そうなやつは全部読んだけどその中だと、やはりHash値を節に持たせて演算に使うのが一番面白かった。 本当は周辺の話題も拾いたい。 「proof checkerの基礎」（高速SATソルバの基礎みたいな解説記事）なんてどこかに落ちてないだろうか。 ないだろうから自分で読まにゃいかんだろうなあ。 あとASPものとかね。 ただ、読書の時間は現在Rust for Rustaceans(early access version)に取られてしまっています。 ディープすぎてのろのろペースでしか読めないわ。