2020-08-15

1UIP を取得しているはずが、毎回 decision variable を取得していたというバグがあった（#7）ので、これを #8 で修正した。その結果、今まで DPLL よりも遅かった CDCL が、大きなケースについてはとても高速に動作するようになった。（表）

これは、$ cnfgen op n で生成されたテストケースを CDCL にぶっこんだ結果である。i7-8700K を搭載した自分の PC 上で、WSL2 によって走る Ubuntu 20.04.1 LTS にて実行している。（これを書いている今も実行中で、op20 までとりあえず動かしてみる予定）

code:csv

testcase,result,seconds

op1,UNSAT,0.000000

op2,UNSAT,0.000060

op3,UNSAT,0.000210

op4,UNSAT,0.001111

op5,UNSAT,0.005183

op6,UNSAT,0.017123

op7,UNSAT,0.038007

op8,UNSAT,0.097430

op9,UNSAT,0.269762

op10,UNSAT,0.764436

op11,UNSAT,2.124796

op12,UNSAT,5.949236

op13,UNSAT,15.051116

op14,UNSAT,39.671842

op15,UNSAT,104.641070

op16,UNSAT,269.683591

op17,UNSAT,692.437665

op18,UNSAT,1744.956638

op19,UNSAT,4430.133510

op20,UNSAT,10426.387543

また、https://github.com/okayu1230z/NumberPlaceSolver/blob/master/toi_001.cnf は 1.156318 秒で解くことができた。このリポジトリで clasp という SAT ソルバーが利用されていたので試しに op20 を解かせてみたところ、1.009s で解かれてしまった（これは自分のソルバの 1万分の1 しか時間がかかっていない）。

2020-08-16 につづく

#diary