推 yan12125:老師是說刪clause要改sat的code 無解... 01/14 19:21
: 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)