[問題] sat證明的邏輯

[BBSealion (海獅)]

我發現我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
推 ric2k1:第二個是 merge (fec1, !fec2) 嗎?
→ BBSealion:嗯對  就是把gate直接merge 但一邊會對他的fout做處理
→ BBSealion:在他fout中有指回他自已的 sign要inverse
→ ckmarkoh:沒砍完的電路 若選擇保留下不同的gate 結果就會不同
→ ckmarkoh:所以要測fraig是否正確 只能用砍完是const 0的來測...
→ BBSealion:沒有理論上的最佳化嗎？
推 ric2k1:Logic Optimization is an NP Hard problem. You cannot
→ ric2k1:even know you have got the optimized solution...
→ BBSealion:有道理耶！