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