作者XDucka (Duck)
看板EE_DSnP
标题Re: [情报] SAT 之使用
时间Mon Jan 14 16:32:19 2013
: 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变很慢吗@@?
--
※ 发信站: 批踢踢实业坊(ptt.cc)
◆ From: 140.112.25.107
顺便问一个问题 fraig完 留下来的float gate是规定不能删(留给cirsweep)吗
我顺手把他删掉了现在有点懒得改回来= =a
※ 编辑: XDucka 来自: 140.112.25.107 (01/14 19:10)
1F：推 yan12125:老师是说删clause要改sat的code 无解... 01/14 19:21