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