2024-06-02 Clause pointer -> ClauseId -> ClauseIndex -> WatchLiteralIndex

[shnarazk]

いつの間にか自分のブログに投稿しなくなったのでこういうところに書くことにした。

Minisatに始まるC++でなら問題ない、２つの監視リテラルが節へのポインタを持つという実装をいかにRustにポートするかというのがRustを使ったSAT solver開発者の最初の課題だろう。
最初に直感的にmutable referenceをやめてclause idで間接参照しないといけないだろうと思ってSplrを開発してきたけども
他の方法はないか3月以降、延々と実験してきた（久しぶりに本腰を入れてSplrをいじった）。

結論：Arc<RwLock>は遅い。数割遅くなる。

ということで、最初の設計方針は間違ってなかったのだが、次にwatcher listをやめて節そのもの組み込んでポインタが要らなくする方法に興味が出た。キャッシュのヒット率に影響するという話だが、第2監視リテラルのweakly copyを持たせるのは本当に得策なのだろうか。

1. Knuthのdancing Links: 遅い。基本操作はランダムアクセスではないので、doubled-linked list上でのpropagate操作が遅い。そもそも節は削除ではなく移動するものなので、ちょっと違う気がした。
2. single linkに変えてみた。それでもpropagateが遅い。次の監視リテラルを持つ節に移動するたびにどちらの監視リテラルを使えばよいか判定しなければならないせいだろう。よいデータ構造には思えない。
3. ということで節のidを1bitシフトしてどちらのリテラルを参照しているかを1bitで追加したWatch Literal Indexを使うことにした。headの判定がif文として入ってしまうところが悔しいが、それ以外にpropagateでのtraveseでif文を多用することもなく、これがベストだろう。そもそもhashを使っているせいでいつの間にかSplrはdeterministic solverではなくなってしまっている上に、propagateで移動する節はリストの最後ではなく先頭に追加されるようになったりしたことで比較が難しいのだが、「少しは遅くなっていると思うけども許容範囲内」ではないかと思う。初めてSplrの基本構造を変える可能性が出てきた。

またこの書き換えをしている最中に、第2監視リテラルがちゃんとメインテナンスされているなら、それを見るだけで、節が充足しているかどうかの判定に使えるだけでなく、矛盾しているかどうかの判定にも使えることがわかった。そもそもそうでなければおかしい。
ただし判定に使えるのは最後のバックトラックで戻ったレベルよりも低い決定レベルで割り当てられている場合に限る。これも考えたら当然だろう。ただしこの改良はpropagationではなくconflict detectionでしか効かないので数値に現れるほどの効果ではなさそうだ。

というわけで20240524-WatchLiteralWeaverをdev-0.18.0にマージしたものかどうか悩み中です。