作者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