我把startVerify和addBoundCkt的部份寫完了
跑了a.dofile的結果和ref program完全一樣 (我還沒做dump 但應該… 沒差吧XDD)
但是跑Traffic.dofile的時候 在證p2 0的時候 MiniSAT就炸裂了
我說的炸裂是
(MiniSat Core 2.2 : #Vars = 97710329, #Clauses = 167696187, Solves = 14, Time
= 45.69)
我是覺得它徹底沒救了… 果然下一秒它就abort了
不過的確我看到了老師上課說的learnt clause爆炸性成長的現象XD (一開始#vars = 9)
但為什麼ref program是秒殺 我的卻炸掉QQ
拜託高手指點… 謝謝！