Vol.2, No.3.
UNSATlog
Splr-0.7.1リリースのはずが
前号を出したのが12日でそれから2週間足らずなので、Splr-0.7.1をリリースしたことしか書くことないよなあと思っていたら、リリース前のルーチンワークのベンチマークの検証中にエラーが発見されてしまった。
まさか、UNSAT問題をSATと答えるなんて！ それも、原因モジュールの同定に数時間かかることになってしまって、半日経っても何が問題なのかすら判明できていない有様。 ちょっとこのバグはキツい。リリースは（楽観的にみて）1週間ほど延期になりそうだ。
という以上の内容だけでvol.3を出して、Splr-0.7.1のリリースのタイミングで次の号を出し、そこで UNSAT logの号数を実暦に合わせよう。ああ、それだけが楽しみ。
2021-04-02
やっと、やっと、原因の節が特定できそう。watchが適切なリテラルを持ってない。 多分shrink, shortenでのリテラル削除に監視リテラルが追従してないようだ。
$ splr aes.cnf
aes.cnf 501284,2928183 |time: 5.21
#conflict: 0, #decision: 0, #propagate: 221128
Assignment|#rem: 34160, #ass: 221128, #elm: 245996, prg%: 93.1855
Clause|Remv: 0, LBD2: 0, Binc: 2472979, Perm: 4073761
Restart|#BLK: 0, #RST: 0, trgr: 1, peak: 1
LBD|avrg: 0.0000, trnd: NaN, depG: 0.0000, /dpc: 0.00
Conflict|tASG: NaN, cLvl: 0.00, bLvl: 0.00, /ppc: 0.00
misc|elim: 1, #sub: 87499, core: 501284, /cpr: 0.00
unreachable core: 24650
[src/cdb/db.rs:958]
(l, w.blocker, w.c, &c.lits)
= ( L151359, L158797, Cid3949122, [ L151358, L149809, L151175 ])
この結果を出すのに実行時間は3時間越え。 原因を正確につきとめようと細かくチェックを入れたら10時間経ってもコアサイズが31000を下回らなかった。 今日中に塞げるだろうか。
2021-04-03
塞げたような気がする。 まだ結論が出てないので「気がする」としか書きようがないのが、とにかく検証中。 バグによって偶然解けたことになってしまった問題なので、何時間かかっても解き、さらにそれが無謬であることを証明しなければならない。 計算が終わるまでじっと我慢しなくては。
ダメだった。この結果を出すのに7時間。Splr開発史上ベスト3に入る難問。
$ splr -t 50000 -c aes.cnf
aes.cnf 501284,2928183 |time: 24585.10
#conflict: 16888219, #decision: 31352807, #propagate: 5559560810
Assignment|#rem: 8797, #ass: 243789, #elm: 248698, prg%: 98.2451
Clause|Remv: 798625, LBD2: 24841, Binc: 2484735, Perm: 8987095
Restart|#BLK: 7868, #RST: 8946, trgr: 1, peak: 128
LBD|avrg: 7.0407, trnd: 0.3329, depG: 4.9266, /dpc: 1.62
Conflict|tASG: 0.0247, cLvl: 313.07, bLvl: 311.69, /ppc: 23.16
misc|elim: 28, #sub: 101678, core: 0, /cpr: 1676.43
Result|file: ./ans_aes.cnf
s SATISFIABLE: aes.cnf
2021-04-05
バグ取れた！
- Eliminator でwatchを適切に更新してなかったため、
propagateが単位節に気づかないことがあった。 ClauseDB::strengthenでbiclauseになった節のLEARNTフラグを落としてなかっため、設定次第でreduce_dbが回収してしまっていた。
ということらしい。以下の通り、4時間掛かって検証できた。
[04-05T15:48:54]$ splr -c -t 300000 aes.cnf
aes.cnf 501284,2928183 |time: 13814.37
#conflict: 25313304, #decision: 50455202, #propagate: 4858368671
Assignment|#rem: 8700, #ass: 243745, #elm: 248839, prg%: 98.2645
Clause|Remv: 549214, LBD2: 43074, Binc: 2485952, Perm: 4429040
Restart|#BLK: 9997, #RST: 13738, trgr: 8, peak: 128
LBD|avrg: 2.6736, trnd: 0.3569, depG: 4.7183, /dpc: 1.01
Conflict|tASG: 1.0058, cLvl: 9.60, bLvl: 8.36, /ppc: 10.11
misc|elim: 52, #sub: 102614, core: 4, /cpr: 282.31
Result|file: ./ans_aes.cnf
Certificate|file: proof.drat
s UNSATISFIABLE: aes.cnf
[04-05T19:39:15]$ gratgen aes.cnf proof.drat -o proof.grat
c sizeof(cdb_t) = 4
c sizeof(cdb_t*) = 8
c Using RAT run heuristics
c Parsing formula ... 4035ms
c Parsing proof (ASCII format) ... 907366ms
c Forward pass ... 41143ms
c Starting Backward pass
c Single threaded mode
c Waiting for aux-threads ...done
c Lemmas processed by threads: 3649502 mdev: 0
c Finished Backward pass: 305584ms
c Writing combined proof ... 17723ms
s VERIFIED
c Timing statistics (ms)
c Parsing: 911402
c Checking: 347424
c * bwd: 305584
c Writing: 17723
c Overall: 1277911
c * vrf: 1260188
c Lemma statistics
c RUP lemmas: 3649502
c RAT lemmas: 0
c RAT run heuristics: 0
c Total lemmas: 3649502
c Size statistics (bytes)
c Number of clauses: 33358889
c Clause DB size: 6030820484
c Item list: 986114048
c Pivots store: 134217728
[04-05T20:39:29]$ gratchk unsat aes.cnf proof.grat
c Reading cnf
c Reading proof
c Done
c Verifying unsat
s VERIFIED UNSAT
[T20:55:04]$
ただ時々、SATになっちゃうことがあるんだなあ。あるいは実行時間が大きく変動したりとか。 今のSplrに非決定性はないので、ハードウェアエラーくらいしか理由が思いつかない。。。