作者BBSealion (海獅)
看板EE_DSnP
標題Re: [討論] To SAT or not to SAT?
時間Mon Jan 17 13:36:54 2011
※ 引述《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
1F：推 ric2k1:嗯! 不過 addXorCNF() 還要考慮是證 a == b or a == !b 01/17 13:59
2F：→ BBSealion:第一個是a＝＝b 第二個是a＝＝！b 不是嗎！？ 01/17 14:35
3F：推 ric2k1:對吼! 這樣子不傳 phase 進去好像比較簡單... 不過我的 01/17 14:38
4F：→ ric2k1:implementation 不想在外面檢查，所以就有傳 phase 進去， 01/17 14:38
5F：→ ric2k1:外面都是 assumeProperty(temp, true)... 01/17 14:39
6F：→ ric2k1:大家想用之前傳三個參數版本的也可以，反正 sat.h 不在 01/17 14:40
7F：→ ric2k1:MustRemove.txt 裡! 01/17 14:40
8F：推 Letitiamm:請問一下 如果沒有做optimization是不是還要 01/17 16:40
9F：→ Letitiamm:solver.assumeProperty(const,false) ?? 01/17 16:41
10F：推 ric2k1:為什麼會有 solver.assumeProperty(const,false) 啊? 01/17 16:48
11F：推 Letitiamm:誒都 我本來想說 如果我還有const gate沒有消掉 01/17 17:25
12F：→ Letitiamm:在assumeProperty的時候 是不是要也要把const gate 01/17 17:26
13F：→ Letitiamm:對應的Var 設成false?? 01/17 17:27
14F：推 ric2k1:const gate means "a gate is proven to be const 01/17 17:28
15F：→ ric2k1:or "the CONST 0" const? 01/17 17:29
16F：推 Letitiamm:恩恩恩 我是指const0 01/17 17:29
17F：→ ric2k1:如果是前者的話，可以啊! 01/17 17:30
18F：推 ric2k1:如果是後者的話，應該在建 model 時直接給他 litId = 0 就 01/17 17:30
19F：→ ric2k1:好了! 以後也不用當成 assumption (因為真的是 const) 01/17 17:31
20F：推 Letitiamm:請問老師的意思是對於const0我不用給他一個Var, 01/18 00:30
21F：→ Letitiamm:直接_gate[id]->setVar(0) 在裡面放0就好了嗎 01/18 00:31
22F：推 ric2k1:是的!! 01/18 00:38