Vol.2, No.11.

Recap

10月はSplrを2回もリリースできました。 Githubの新しいproject機能で進捗管理を始めたので、それを見ながらどういう進展があったのか振り返っていきます。

Splr-0.13

目玉は問題が多かったchrono-BTを捨ててtrail savingを実装したこと。 実際にはまだコードとしては残っているけどchrono-BTはもうサポートしないでしょう。 Chrono-BTはUNSAT certificationのバグがどうやっても取れなかった。 Splrでのpropagateの非決定性に由来する論理バグに少しだけ悩まされ、結局論文にあった3つの改良点の最初の項目（saving over multiple conflicts）は結局放棄することになった。 というわけでいくつかの妥協を重ねることにはなったものの論理バグをおそらく持ち込まずに実装できたと思う。 そしてそこそこの効果は出たようだ。 めでたし。

他の変更点はUNSAT certificateのファイル出力をまめ書きするようにしたこと。 ただfile lockをよくわかってないのでまとめ書きで速くなったかどうかは不明。 いつか考えねば。

Splr-0.14

ついで0.14ではbinary clauseに対するpropagationを高速化するためbinary linkをHashMapだけに入れるのをやめてリスト構造とHashMapを併用する形に変更。 その結果HashMapに対するiterationがなくなって決定性が復活しました！これは意外に大きな副産物。 デバッグがすごくやりやすくなった。 binary clauseはそれ以外の節とかなり違う実装になってきたのでもうclauseではなく(directional) linkとしか思えなくなってきたので識別子としてclauseという語句を使うやめてbinary_linkという名前で書き直し。 もはやclause eliminator（のループ）さえ対応したらbinary clauseは存在しなくなるところまできました（実際Clause DBの中にBinary Link DBがあるような形になっている）。 ただ実際に変更を始める論理エラーが噴出しそうなので0.14が終わってからのfuture workとして一旦棚上げしておこう。 関連してwatch listをHashMapで実装するためのコード、featureも削除した。

オリジナルのアイデアとしてbinary linkで繋がった依存グラフの中間ノードに報酬を与える必要はないのではなかろうかと考えてsuppress_reason_chainというfeatureを実装してみた。 しかし実験結果は否定的だったので削除した。 特にbinary clauseが多い問題で悪化が激しいようなので、やはりもらうべき報酬をもらい損ねた変数が出てくるようだ。 binary clauseが少なければそもそも圧縮する必要性が軽減されるのでアイデアとしては袋小路だろう。

さらに細かい修正としては、節削減時に特別に残すための条件を次のステップで実行されるvivificationで選択されるものということにした。これまで使っていた節長だとか活性度だとかLBDだとかは全部無視。 この手の尺度は実験繰り返さないと選択する根拠が得られず、時間だけが過ぎてしまいがちなのだ。 そもそも本来のvivification target選択条件は2回以上LBDが2以上減少したことなのだが、1減少を3回繰り返したものはどうしてダメなのかよくわからない。 あまり論理的ではないような気がしたのでvivification前のrankからどれだけ減ったかで判断することにした。 そこで各節がrankを二つ保存する必要が出てきた。 Clauseのmemory footprintを増やしたくなかったのでプログラム全体で一つのデータ型にまとめていた各種フラグFlagを変数用と節用に分割してそれぞれ8bitで保持するようにして場所を確保。 rankは16bitとなり、多分、多分大丈夫だろう（節長が6万を超える。あるだろうか？）。 こうなってくると24bit整数とか56bit整数とかが欲しいなあ。 結構大胆な変更だけまあ許せる実験結果になったので、採用。 またコンフリクトの原因と変数割り当ての理由は同じ形式で表現できるはずなのにConflictContextとAssignReasonという二つの型を使っていたので、ConflictContextはAssignReasonを内包する形で定義し直し。

アルゴリズム以外の変更としてはfeature configurationの違いを吸収するため関数内でマクロをいくつも定義して関数本体では余計な分岐が見えないようなスタイルを採用。 関数そのものはさらに長くなるけど、フローが追いやすくなったので、もっと早い段階で検討すべきだった。 パラメータチューニングとしてvar elimination/clause subsumptionに時間をかけ過ぎ（リテラルから節へのマッピングデータを作るのが重すぎ）なのでin-processorの実行回数を節数に応じて減らすことにした。

そして開発中にrustc 1.56がリリースされたのでRust 2021 Editionに移行しました。 と言ってもTryFromをimportしなくなっただけかも。

最後の最後に余計なフィールドやメソッドを削除しつつ、大事なfeaturesの設定変えてもコンパイルできるように変更し、そしてLitをNonZeroU32に変更して、2021年11月01日にリリース（なんとなくキリがいい感じ）。 結構なメンテナンスが入って広範な修正になったので、diffがかなり大きなものになってしまいました。

SAT Competition 2021 benchmarkの結果はほんのちょっとだけ0.13より遅くなったけどまあ誤差範囲内と強弁できるかもといった感じ。 なので0.14はほぼSplr史上最強のSplrなのだ。 めでたし。

11月の予定

論文読むさ。 _Rust for Rustaceans_は後100ページ程なので多分時間を作れるでしょう。

気が向いたらbinary clauseを完全抹消して0.15。 その後（どちらかといえば遠い将来のイメージだが）はSLSをキャッチアップだ！