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