楼主:
XDucka (Duck)
2013-01-14 16:32:19: 3. 针对某个要证明的 FEC pair "F == XOR(f, g)", (<= 要给 F 一个新的 SAT Var)
: 呼叫 solver.addXorCNF() 去建立对应的 CNF clauses.
请问一下如果生成了一堆 newVar F 在 CNF里面
release assumptions的时候感觉不会把F 移掉 (会吗@@?)
那到时候solver的CNF最后面就有一堆(f1)(f2)(f3)...这样样的clause
这样不是会让solver变很慢吗@@?