at Sat Competition 2020

まともなSAT solverなら250変数の3-SATなんて1秒程度で解け、その求解速度なんてなんの尺度にもならないものだろう。 なので最近のSplrの開発は360変数の3-SATをマイクロベンチマークに使っている。 最近はまあ「そこそこ待ち遠しくない時間」でSAT問題、UNSAT問題どちらも解けるようになってきていた。 で、やっとSAT competition 2021での問題をつまみ食いし始めたのだけど、ある問題に衝撃を受けてしまった。

それはSATな320変数3-SAT問題170058143.cnf。解けて当然だと思ってたのだが、5000秒タイムアウトで解けない。 色々設定変えて、やっと解けたらこんな感じ：

$ splr ~/Library/SAT/SC20/170058143.cnf
170058143.cnf                                      320,1120 |time:  1574.08
 #conflict:    6289871, #decision:      7955609, #propagate:      306206577
  Assignment|#rem:      320, #ass:        0, #elm:        0, prg%:   0.0000
      Clause|Remv:   195608, LBD2:    78093, Binc:    18750, Perm:    19871
     Restart|#BLK:        1, #RST:    24004, trgr:        2, peak:       64
         LBD|avrg:  14.0921, trnd:   0.9422, depG:   3.3053, /dpc:     1.08
    Conflict|tASG:   0.9536, cLvl:    18.99, bLvl:    17.84, /ppc:    46.90
        misc|elim:        5, #sub:        0, core:        0, /cpr:   227.20
      Result|file: ./ans_170058143.cnf
s SATISFIABLE: /Users/nash/Library/SAT/SC20/170058143.cnf

部分解には至らずに、たまたま解を見つけたということか！

なんというか、どうしたもんか。すげーな。

2021-03-17

散発的網羅的なclause vivificationを試してみたのだが、否定的だ。

2021-03-18

big-bang initializationが効いた。それでもvivificationは必要のようだ。

いや、実際にはvivifierはなんの貢献もしていないので、活性度の「かき混ぜ」が鍵かもしれない。 なので、定期的に下駄を履かせてみると、、、、

ここまでのまとめ

• big-bang initialization必要。とりあえず初期値0.4。
• clause vivification必要。ただしこいつはpurgeもshrinkもしないので効果は変数活性度のかき混ぜのだけと思われる。
• 頭が重たいLuby stabilization必要。文字通りの三角形なやつではダメ。