作者Letitiamm (Letitia)
看板EE_DSnP
标题Re: [问题] 关於 sat solver 的用法
时间Sun Jan 16 22:43:51 2011
※ 引述《ric2k1 (Ric)》之铭言：
※ 引述《TommyKSHS (汤米)》之铭言：
: 我想问的是：
: 当我们要证一个 fec pair 的时候
: 应该要 add 一个 XorCNF ( tmp, fec1, fec2 ) ？
: 然後 assume 这个 tmp 的 Var 是 true 吧？
是的， 不过请注意 sat.h 里头的 XorCNF 是要传入
(tmp, fec1, phase1, fec2, phase2) 哦!
不好意思 我想要问
这五个input是什麽
如果要证a\= b的话 （a不等於b）
fec1 = a ,
fec2 = b ,
phase1 = true;
phase2 = true;
tmp????
~~~~~~~~~~~~~~~~~~~~~~~~~~
如果要证 a\= !b 的话 (a不等於!b)
fec1 =a;
fec2 = b;
phase1 = true;
phase2 = false;
tmp????
~~~~~~~~~~~~~~~~~~~~~~~~
其实我是要问tmp要放什麽
顺便问一下
我对fec跟phase有没有误解
谢谢 ^^ 大家加油！！！！！
: 那如果证完之後
: 再 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
--
※ 发信站: 批踢踢实业坊(ptt.cc)
◆ From: 140.112.216.200