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