Re: [討論] To SAT or not to SAT?

[BBSealion (海獅)]

※ 引述《ric2k1 (Ric)》之銘言：
: 提醒一下，免得有人做錯:
: 使用 SAT 時是要得到 UNSAT (i.e. assumeSolve() return false) 才能化簡電路哦!
: 如果你的到的是 SAT，你只能拿它產生的 assignment (by int getValue(Var v))
: 去 refine 你的 FEC groups (by more simulations)!!

所以大概是

完全相同的fec檢驗：
solver.addXorCNF(temp, fec1, false,fec2 ,false)
solver.assumeProperty(temp, true);
result1 = solver.assumpSolve();
if(result1 == false ){ merge }

完全相反的fec檢驗：
solver.addXorCNF(temp, fec1, false,fec2 ,false)
solver.assumeProperty(temp, false);
result2 = solver.assumpSolve();
if(result2 == false ){ merge }

是這樣嗎？

--
※ 發信站: 批踢踢實業坊(ptt.cc) 
◆ From: 218.168.223.109
推 ric2k1:嗯! 不過 addXorCNF() 還要考慮是證 a == b or a == !b
→ BBSealion:第一個是a＝＝b 第二個是a＝＝！b 不是嗎！？
推 ric2k1:對吼! 這樣子不傳 phase 進去好像比較簡單... 不過我的
→ ric2k1:implementation 不想在外面檢查，所以就有傳 phase 進去，
→ ric2k1:外面都是 assumeProperty(temp, true)...
→ ric2k1:大家想用之前傳三個參數版本的也可以，反正 sat.h 不在
→ ric2k1:MustRemove.txt 裡!
推 Letitiamm:請問一下 如果沒有做optimization是不是還要
→ Letitiamm:solver.assumeProperty(const,false)  ??
推 ric2k1:為什麼會有 solver.assumeProperty(const,false) 啊?
推 Letitiamm:誒都  我本來想說  如果我還有const gate沒有消掉
→ Letitiamm:在assumeProperty的時候  是不是要也要把const gate
→ Letitiamm:對應的Var 設成false??
推 ric2k1:const gate means "a gate is proven to be const
→ ric2k1:or "the CONST 0" const?
推 Letitiamm:恩恩恩 我是指const0
→ ric2k1:如果是前者的話，可以啊!
推 ric2k1:如果是後者的話，應該在建 model 時直接給他 litId = 0 就
→ ric2k1:好了! 以後也不用當成 assumption (因為真的是 const)
推 Letitiamm:請問老師的意思是對於const0我不用給他一個Var,
→ Letitiamm:直接_gate[id]->setVar(0)  在裡面放0就好了嗎
推 ric2k1:是的!!