Vol.4, No.02.

Finally 0.17

このバージョンでは経験に基づく意味不明なヒューリスティックスを消しているので、 ある程度性能が悪くなって(代わりに伸び代が大きくならせたつもり)もリリースするつもりだったけどそうも行かないようだ。

sat-benchを使ったマイクロベンチマークではそこそこいいのに、 SAT competition 2021の問題だとこの4年の開発の歴史をなかったことにするような結果しか出なくてギブアップ気味だったのだけど、 この開発フェーズで導入した'two-mode reduction'のパラメータ設定がかなりシビアなことに気付いてハンドチューニングを始めたら、 一発で最高の性能が出てしまった。 two-mode reductionはcycle内のexploitation modeでは活性度が高いリテラルを含む節を総数を減らさないように節数を調整することで深い探索を邪魔しないようにして、 新たなcycleが始まるタイミングではLSD基準で総数を削減して探索方向をリセットするというものなので、 そんなにおかしなことはしていないはずなのだ (まあリリース直前まで動的な別の方針だったけど)。 ということで、ようやく0.17のリリースにこぎ着けました。

今回の目玉はコーナーケースでのバグフィックスかなあ。それとstage-cycle-segmentモデルの深化。 導入したてで色々とパラメータの定義、値におかしなところがあった。 目玉になるはずだったSLSも書いてはみたものの全然性能に結び付きませんでした。 0.17をベースにもう少し追いかけて見る気はあるけど、 昨今の電力事情を考えると3nmなM3搭載macを入手するまではベンチマークやりたくないわ。

ということでこれくらいのベースでの開発が続くでしょう。 0.18は0.99くらいになるかもしれない。