Vol.2, No.7.
亀の2021年6月
相変わらず0.10のリリースができない一ヶ月でした。 ということで今月も短信です。
問題点
色々と直してはいるのだけど、最後のピースまでは行きつかない。 transitionにおける論理バグを見つけたり、除去された変数を戻す部分を完全にRust的なコードに書き換えたり、少しづつは進展している。 監視リテラルを正しくセットしているにも関わらず単位節が無視されるという不可解なバグはchronoBTによるものではないかと思う。 これも最後まで追い詰めきれてないのだが、今のところこの方向でちょっとづつ進めていくのが正解のようだ。
これは監視リテラルが待つ対リテラルキャッシュが現在の決定レベルよりも高いレベルで充足していた時には監視リテラルの更新は行われないのだが、より高いレベルで充足リテラルが否定された場合、このリテラルをこの節は監視していないのでBCPの対象から漏れてしまうということ。 監視リテラルはその対リテラルキャッシュよりも高い決定レベルであることを保証しないとchronoBT導入は処理の妥当性を失うことになる。ようだ。
（この文章を書いていて思ったけど、監視リテラルに関しては、
- そのもの、
- 監視リテラルのリスト、
- 監視リテラルに関する構造体、
- その中のMinisatやGlucoseで言うところのblocker、 と指し示す必要のあるオブジェクトが多すぎてネーミングに苦労しているのだけど、blockerは対リテラルキャッシュと呼ぶのがよさそうだ。 英語だと Cache of Pairing Literal; CPL かな。）
これが大学の研究者なら、数ヶ月前のバグ発生の認識から一週間でここまでやってこれないと生きていけないだろうなあ。 全く能力不足だわ。
その他
Splrに初めてインタラクティブな操作関数が導入されました。 正しく動作するプログラムには全く要らない機能だけど、デバッグにこんなに苦労するなら、何が起きているのかを把握するために、節DBやassign stackを選択的に覗けるようにするのはもっと早い段階ですべきだった。 おかげで監視リテラルの時間変化がなんとなく見えるようになって、少し理解が進みました。 なんだかんだで現在Splrは11000 Line of Code。 前のリリース版から半分近くの行が書き換えられている。。。
7月の予定
そりゃもちろんバグ取り。それ以上のことは言わない。
2021-07-09:追記
どうもバグが取れたようだ。 最後に残っていた問題はcancel_until中でq_headを間違えて更新していたせいだった。 それで伝播できないリテラルが出現していたわけだ。 修正するとaes.cnfで3連続で問題なく検証できたし、SAT Competition 2019のベンチマーク、タイムアウト200秒で解けた問題も全て検証できた！ 終わった！