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