作者ric2k1 (Ric)
看板EE_DSnP
標題Re: [問題] 關於 sat solver 的用法
時間Sun Jan 16 17:11:01 2011
※ 引述《TommyKSHS (湯米)》之銘言：
: 我想問的是：
: 當我們要證一個 fec pair 的時候
: 應該要 add 一個 XorCNF ( tmp, fec1, fec2 ) ？
: 然後 assume 這個 tmp 的 Var 是 true 吧？
是的， 不過請注意 sat.h 裏頭的 XorCNF 是要傳入
(tmp, fec1, phase1, fec2, phase2) 哦!
: 那如果證完之後
: 再 assumeRelease
: 要證下一對 pair 時，上次 add 的 xorCNF 會影響到下一次證明的結果嗎？
不會影響到下一次證明的正確性，
相反的，這次證明所 "learn" 到的 information (embedded in SAT codes)
還可以幫助以後的證明。
不過 learn 太多有時會有反效果 (performance 而言)，
但這些都已經被 SAT engine 內部 take care 了，
你們可以不用管。
--
※ 發信站: 批踢踢實業坊(ptt.cc)
◆ From: 114.36.62.203
1F：推 TommyKSHS:阿阿 囧 我用的是舊的 sat.h .... 01/16 17:14
2F：→ TommyKSHS:謝謝老師！ XD 01/16 17:14
3F：推 michael0728n:推~學太多有反效果是想太多喔怎麼跟人有點像XDDDDD 01/16 17:34
4F：→ ric2k1:對啊! SAT engine 會 periodically 把一下 learned info 01/16 17:36
5F：→ ric2k1:丟掉... 留下一些比較有用的 01/16 17:36
6F：推 TommyKSHS:咦 我在 ceiba 作業區新載下來的 fraig.tgz 裡的 sat.h 01/16 18:36
7F：→ TommyKSHS:的 addXorCNF 只有三個參數耶…和老師這篇文說的不同@@ 01/16 18:37
8F：→ ric2k1:咦... 莫非我忘記 copy 了... anyway, 請先用 2997 篇 01/16 18:40
9F：→ ric2k1:我來重新上傳一下... 01/16 18:40
10F：推 ggegge:原本的三個變數的版本就可以用了 01/16 22:00
11F：→ ggegge:只要注意要證明是=1 還是=0 01/16 22:00
12F：→ ric2k1:嗯嗯, 不過這樣外面 opt flow 還得記得 proof value... 01/16 22:04
13F：推 TommyKSHS:我只是想說和新的 ref code 一樣比較心安 XD 01/16 22:04
14F：→ ric2k1:大家如果想要自行修改 sat 裡面的東西，請自便! 01/16 22:05