Vol.1, No.4.

0.3.3まだまだ

非常事態宣言が発出されて外を出歩かなくなってしまったのでカバーに使えるような写真のストックがなくなっ てきました。プログラミングの時間は増えてそれなりに進展あり。

CaDiCaLにおける重要技術の絞り込み

CaDiCaLの何がいいのかを調べるためsat-benchでオプションを切り替えながら3SATを実行してみました。詳細な結果はImportance of modern techniques in SAT solvers に書きました。

結論として、今のSplrにないものをまとめると、

• walk — ランダムウォークしてるんだ。
• stabilize — モードを切り替えて'deep searc'hのようなことをやっているようだ。
• rephase — なんだこれは？

といったところ。なのでこれらの理解・検討を始めることにしました。

Issue 1: propagation pointerの導入

その前にもっと低レベルな実装上の改善を発見。propagate関数内の最適化として、節ごとに監視リテラルを見つけるのにどこまでリテラルを辿ったかを覚えておいて次回の新監視リテラル探索時の無駄な検査を減らすというものがある。CaDiCaLのコメントでは、節ごとに4バイト増えるとあるので導入するのはリテラルへのポインタ（インデックス）だけのはず。簡単な変更なので導入してみた。確かに速くなりそうなのだが全然計算量の差が現れない。なんだかよく分からなくて一旦お手上げ。その後、CaDiCaLのソース中の別のコメントを読んで理解した。当初はバックトラック時にどこから探せばよいかを計算する（クリアする）ようにしていたが、もっと簡単に前回の検出インデックスからサイクリックに一周辿ればいいだけだった。この方針で実装し直してみると、この1年くらいで最大の高速化が実現できたようだ。

言われてみればなぜこんな簡単なことを思いつかなかったのだろうと反省しきり。監視リテラル対のような実装レベルでの改良はまだまだあったのだなあ。この時点で0.3.3をリリースする価値がでた。

Issue 2: Stabilizationの導入

ヒューリスティックレベルの高速化技法に話を戻します。ランダムウォークの導入は僕にとって全くの新技術なので後回しにして分かりやすそうなstabilizationに手をつけることにしました。どうも最良の割り当てを（部分的に？）再利用する枠組みのよう。コメントを読むと等比数列的にリスタートを止めているようなのでdeep search系の技術のようだ。とても簡単なのでProgressEvaluatorとして実装してみた。

しかし、うーん、これまた微妙な結果。ついでにstabilizephaseにも手を出してみたけど同じく微妙。3SAT UF250では全然改善の兆しは見られないし、ベンチマーク問題で解ける問題のカテゴリが広がりそうなんだけどもそうも家なさそう。ずっとパラメータチューニングをやっているけども、なぜこんなに微妙なのだろうか。現在苦戦中です。

さて、stabilizing modeを持ち込むとvar decayなんかのパラメータも再調整した方がいいかも。exploreとexploitの両方を一つのパラメータでカバーしなくてよくなるはずだよなあ。うーん、マルチエージェント化すべきだろうか。。。

NixOSでのCaDiCaLのパッケージング🎉

余談だけど、すごくいい結果を出しているのでCaDiCaLをnixOSに取り込んでもらえるようにpull requestを投げてみました。大量に修正が必要だったけど取り込んでもらえました。リリースが遅れている20.03には入っています。ちなみにArch LinuxではAURに入っている。ということでNixOSコントリビューターデビューです。そのうちgratgenとgratchk-smlのpull requestも作ってみよう。

今後の展望

現在開発ブランチで3000行近いdiffになっているのでせめてdev-0.3.3にマージしたいのだけど性能が上がらぬことにはどうしようもない。せめて劣化しないところまで早急に持っていきたいと思う。最終的にはpropagation pointerのおかげで次バージョンのリリースは実験の結果待ちまで来たので時間の問題。ただし大改造が（また）入ったので0.4シリーズにしようと思う。 ひと段落ついたら、stabilizeは二つのソルバーを切り替える実装にすべきだと今強く思っているので、bidirectional searchのようなコンテキスト切り替えを可能にするフレームワーク、モジュラリティの導入がやりたい。その上でいろいろ実験したいと思っている。しかしそうすると今年のSAT Cometition 2020にも間に合わなさそうな。うーん頭痛い。