作者BBSealion (海狮)
看板EE_DSnP
标题[问题] sat证明的逻辑
时间Tue Jan 18 01:23:01 2011
我发现我sim09.aag做完後只剩508个gate耶
ref却还有13xx个，是我误砍了什麽吗？？
我做sat的逻辑是
处理完全相同的fec pair：
solver.addXorCNF(temp, fec1, false, fec2 ,false)
solver.assumeProperty(temp, true);
result1 = solver.assumpSolve();
if(result1 == false ){ merge fec1和fec2 }
处理完全相反的fec pair：
solver.addXorCNF(temp, fec1, false, fec2 ,false)
solver.assumeProperty(temp, false);
result2 = solver.assumpSolve();
if(result2 == false ){ merge fec1和fec2}
直接证明某个gate是constant 0
solver.assumeProperty( gate , true);
result3 = solver.assumpSolve();
if(result3 == false ){ 将该gate和constant 0 merge}
请问一下这样有误吗？？
--
※ 发信站: 批踢踢实业坊(ptt.cc)
◆ From: 218.168.223.109
1F：推 ric2k1:第二个是 merge (fec1, !fec2) 吗? 01/18 01:29
2F：→ BBSealion:嗯对 就是把gate直接merge 但一边会对他的fout做处理 01/18 01:33
3F：→ BBSealion:在他fout中有指回他自已的 sign要inverse 01/18 01:34
4F：→ ckmarkoh:没砍完的电路 若选择保留下不同的gate 结果就会不同 01/18 01:49
5F：→ ckmarkoh:所以要测fraig是否正确 只能用砍完是const 0的来测... 01/18 01:50
6F：→ BBSealion:没有理论上的最佳化吗？ 01/18 01:52
7F：推 ric2k1:Logic Optimization is an NP Hard problem. You cannot 01/18 01:58
8F：→ ric2k1:even know you have got the optimized solution... 01/18 01:58
9F：→ BBSealion:有道理耶！ 01/18 02:09