作者ric2k1 (Ric)
看板EE_DSnP
标题Re: [问题] sat
时间Sun Jan 16 00:34:07 2011
※ 引述《Letitiamm (Letitia)》之铭言：
: 请问一下
: 在fraig的时候
: 应该是把每个fec都丢进去看他是否有解
: 有解 则不再是fec
: 无解 则merge起来
: 那最後不是应该没有fec了吗
: 我跑ref的时候
: read sim12.aag
: simulate pattern.12
: 最後在fraig
: 然後还是有3组fec存在
那三组是在 fraig 之後变成 unused，我的 fraig 只操作在 DFS list 里面，
而我也会三不五时的 update 一下 DFS list.
你 run 的可能不是最新版本的 ref prog.
我记得最新版本我在 fraig 完後就把 FEC 都清掉了...
其实为了 fraig 的 performance, 你可以考虑不用每个 FEC pair 都证,
否则 complexity 是 O(N^2) * O(SAT).
有些 FEC pair 就算没证也会被其他的 FEC pair 所包含住,
所以就算没证最後 optimized 的 ciruict 还是一样的.
: ～～～～～～～～～～～～～～～～～
: 第二个问题
: 如果没做optimization可以做fraig吗
: 如果可以 是不是把const gate那个assumption成false就好了？
可以啊!
我前面好像有回文，对於 simulate 後 value = all 0's or all 1's 的 gates,
我是 assume false/true 去证的.
--
※ 发信站: 批踢踢实业坊(ptt.cc)
◆ From: 114.36.62.203
1F：推 Letitiamm:所以fraig之後 应该要都没有FEC吗？？ 01/16 00:37
2F：→ Letitiamm:还有CIRsat 是不是就是fraig 只是 不一定要做完？？？ 01/16 00:38
3F：→ ric2k1:fraig 之後还有没有 FEC 要看你的 implementation, 如我前 01/16 00:41
4F：→ ric2k1:面所述，我不会去测大家 fraig 之後的 FEC...(都不会一样吧 01/16 00:42
5F：→ ric2k1:CIRsat 是用来设定 SAT 的 effort limit, 01/16 00:42
6F：→ ric2k1:有些FEC pair 可能会很难证, 你花很多力气去证它可能对最後 01/16 00:43
7F：→ ric2k1:的 circuit optimization 并没有甚麽影响，所以不如早点 01/16 00:44
8F：→ ric2k1:放弃, 继续去证别的 pairs. 01/16 00:44
9F：→ ric2k1:不过你可能要了解 SAT 的一些基本原理才会知道怎麽调 SAT 01/16 00:45
10F：→ ric2k1:的 effort limit... 既然是 bonus, 我就不提示了... 01/16 00:45
11F：推 Letitiamm:喔喔喔 谢谢老师 01/16 00:55