推 Letitiamm:我瞭了 謝謝老師 ^.< 01/17 01:09
First, I would like to remind you that "SAT", as its name "satisfiability"
suggests, is a "search" engine.
It search for an input assignment 'I' for a Boolean function f(X) such that
f(X = I) = 1.
So, in order to use SAT to "prove" something, say "P = 1",
we need to show that its inverse is "unsatisfiable".
That is, we will call SAT to search for "P = 0".
If "P = 0" is unsatisfiable, we prove that P is always 1.
Otherwise, it just means that P CAN BE 0, but NOT necessarily always 0 or 1.
: : 我想問的是：
: : 當我們要證一個 fec pair 的時候
: : 應該要 add 一個 XorCNF ( tmp, fec1, fec2 ) ？
: : 然後 assume 這個 tmp 的 Var 是 true 吧？
: 是的， 不過請注意 sat.h 裏頭的 XorCNF 是要傳入
: (tmp, fec1, phase1, fec2, phase2) 哦!
: 不好意思 我想要問
: 這五個input是什麼
: 如果要證a\= b的話 （a不等於b）
I assume you are asking "how to prove a != b".
In that case, we need to create a function "f = (a = b)",
and call SAT to check if "f = 1" is satisfiable.
: fec1 = a ,
: fec2 = b ,
: phase1 = true;
: phase2 = true;
: tmp????
Note that (a = b) is euqivalent to (a xnor b),
and is equivalent to (a xor !b).
The function "SatSolver::addXorCNF()" is to construct the CNF clauses for
an XOR formula. Here we have f = (a xor !b). So you need to:
(Given "SatSolver solver").
1. Var f = solver.newVar(); // create a new variable
2. solver.addXorCNF(f, a, false, b, true); // true means "inverted"
When you want to prove, you can do:
3. solver.assumeProperty(f, true);
Hope this is clear!!
You can actually refer to the example in "sat/test/satTest.cpp"
for some other information.
: ~~~~~~~~~~~~~~~~~~~~~~~~~~
: 如果要證 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