我把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
拜托高手指点… 谢谢！