Re: [情报] SAT 之使用 XDucka PTT批踢踢实业坊

Re: [情报] SAT 之使用

楼主: 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变很慢吗@@?

作者: yan12125 (姥姥) 2013-01-14 19:21:00

老师是说删clause要改sat的code 无解...

继续阅读

[问题] SatSolver Aborted() 已解决david942j [问题]segmentation fault在SatSolver内发生(已解决)taldehyde Re: [公告] Final Project Updatesric2k1 Re: [问题] Ref的小问题ric2k1 [问题] Ref的小问题mikechen25 Re: [问题] FECric2k1 [问题] FECXDucka [心得] src/sat/test/Makefiletaldehyde [问题] Updating by SAT???yan12125 [闲聊] PTT 就要步上 M$N 的后尘了吗?ric2k1