Vol.2, No.4.

充足性判定誤りの3月

Splr-0.7シリーズのポイントリリース0.7.1をサクサク公開して、いよいよ並列化という大物に取り掛かるつもりだったのが、ベンチマークの結果の検証で論理バグが検出されて、思いも掛けない終わりのないデバッグに突入してしまいました。 なんと0.7.1でエンバグしたのではなく、0.7.0が既におかしい。 いやもしかするとそれ以前からあったのかもしれない。 SATソルバーを名乗れないものをリリースしてしまっていた！

その上このことに気づいてから1週間経ってもバグが取れない！ 時間がかかってしまう理由が簡単な問題では再現しないバグであること。 ベンチマークを走らせて検証スクリプトを走らせるとただ1問だけ不適切な充足解を生成している。 その問題は0.7.1RCで初めて解けるようになって、それ以前のソルバーではタイムアウトしてしまう問題。 なので色々なフィーチャーを切って問題を起こしているモジュールを特定しようとすると、結果が出るまで早くて数時間。 比較実験すらままならないという状況。 コミットしていないので外からは何もやってないように見えて、ずっと頭を抱えまくっていた 、Splrの開発史上ベスト3には入る問題の発生なのでした。

必要はコーディングの母ということで、いくらでも大きくなってしまうUNSAT certificationをメモリに溜め込むのではなく、リアルタイムでファイルに吐き出していくような変更も実装されました。

現状

ほぼ1週間を費やして、どうもpropagateでの監視リテラルとそのキャッシュとの整合性に起因するようだというところまで突き止めた。 これを書いている時点で、assert突っ込んで動作の等価性を確認しながら原因の証拠固め、同時に検証出来たところを最適化されたものに戻す作業を繰り返しているところ。 早いところバグなしバージョンだけでもリリースしたいところだけど地道にこのデバッグを終わらせるしか手段がない。

ここで備忘録。 assignされた変数は実は2種類ある：propagate済みのものとまだのもの。 これを区別することなくassignedの返値を使うとカタストロフが発生する。 propagate内では十分に注意すること。 なのでどうしてpropagate内のループで監視リテラルを1つだけ見つければ通常状態、つまり単位節でないのかはこれが理由。 納得して持ってきたコードではあるのだけど、あまりにも昔のことでボケてしまっていた。

4月の予定

もう、現在は「早くバグをとります」以外のことは言っても虚しいので、これでおしまい。 実はリリース直前まで行ったもの（バグも取れたのでベンチマークを取ったら、まだ充足性判定誤りが取れてなかったのでリリース直前での取り消しは既に2回）は結構いい性能だったのだけど、まあ、充足性判定誤りがあるソルバーはそもそもソルバーではない。 ああ、悔しい限り。