Summarize 一下這個問題： 1. 這是 ref prog 的一個 bug, 簡單的說，ref prog create 了一個 SAT var for const 0, 但是做錯兩件事情： (1) 它的 SAT varID != 0, 這與 SAT engine 裏頭的 const 0 (i.e. varID = 0) 並不一致。 (2) const 0 在 SAT engine 裏頭應屬 negative phase, i.e. litId = 1, 但是 const 0 在 cirMgr 是 positive phase. 2. 要解決這個問題，最簡單的方法就像是 wmin0 同學所說的， (不管 const 0 的 SAT varID != 0 這個問題) 直接在要每次證明 FEC pair 之前都加上： solver.assumeProperty(_const0->getSatVar(), false) 就可以了。 對我而言，這樣的小小缺點就是在呼叫 SAT 之前都要記得加這個 assumption, 當然，如果包成 function 應該就不會有遺漏的疑慮了。 3. 比較根本的解決辦法， <== 但這牽涉到要改 spec, 所以看看就好 (1) CirMgr 裏頭存的是 const 1, 然後把它的 SAT varID 設成 0. (2) 在 SatSolver 的 init() 以及 releaseAssumption() 的最後面都加上: _assump.push(Lit(0)); 以確保無論如何 solver 都一定會包含 const 0/1 這條 assumption. (關於這點，是因為在 solver 裏頭: value(Lit(0)) 得到的值並不是 l_True) 4. 去年沒有這個問題是因為我們去年在 circuit parse 完之後一定會做 CIROPT, 所以 DFS list 裏頭不會有 const 0. 但今年 code 把 HW6 拆開之後就沒有注意到這個問題了... ※ 引述《djshen (djshen)》之銘言： : 標題: [問題] fraig : 時間: Sun Jan 15 15:49:46 2012 : : 在sim05中 : : fraig會用0來merge其他gate : : 但是像 : : aag 4 1 0 1 3 : 8 : 6 : 2 0 8 : 4 0 8 : 6 2 4 : : cirsim -r : cirp -fec : : 1 2 3會在一起 : : 但fraig沒有作用 : : 不太懂到底要不要處理用0 merge的情況 : : -- :

※ 發信站: 批踢踢實業坊(ptt.cc) : ◆ From: 140.112.25.106 : 推 kickpp:直接接const0的aig好像不會被sat判斷成相等 01/15 16:26 : → kickpp:應該是因為這樣merge時會出問題 它是屬於input merge的case 01/15 16:27 : → kickpp:但照理說1要merge2 & 3 我的fraig會做 ref不會 01/15 16:27 : → kickpp:應該是implement不同的關係吧 01/15 16:28 : → djshen:這樣有點困擾.. 01/15 16:30 : → kickpp:但如果是第三行是2 8 9這種例子 就會被sat判斷成與const0 01/15 16:31 : → kickpp:相等 01/15 16:31 : → kickpp:這樣不會困擾吧 如果直接接const0的情況也被判斷成相等 01/15 16:32 : → kickpp:merge時還要判斷是哪種情況 反而麻煩 01/15 16:32 : 推 kickpp:另外小聲說...你的_numDecl[VARS]錯了XDDD 01/15 16:36 : 打錯而已嘛.. : ※ 編輯: djshen 來自: 140.112.25.106 (01/15 16:39) : 推 kickpp:突然發現好像不用另外判斷 那sat應該要判斷出來才對XDDDD 01/15 16:41 : → kickpp:剛剛想錯XDD 01/15 16:42 --

※ 發信站: 批踢踢實業坊(ptt.cc) ◆ From: 114.36.61.155