作者ric2k1 (Ric)
看板EE_DSnP
標題Re: [請益] 在sat merge
時間Tue Jan 17 02:39:21 2012
: 請問一下
: 做sat的時候如果把gate merge掉了
: 那麼原本建立的var id之間的關係要如何處理呢
: 例如const0要merge aig 4
: aig 4被砍掉之後是用assumeProperty來處理aig 4的var id嗎?
電路上就用與 strash 相同的方法來 merge 兩個 gates,
被 merge 的 gate 我是只有 delete 掉它本身，沒有去管它的 transitive fanins,
所以有可能會造成 floating cells, 反正 fraig 完再呼叫 cirsweep 就好了。
至於是不是証完一個 FEC pair UNSAT 就馬上 merge，
我是沒有啦! 因為改了 netlist 之後就改 FEC groups, 以及 DFS list,
這樣有點得不償失。
不過完全不 merge (等到証完再 merge) 其實也不好，
就找個 balance 囉!
另外就是在 SAT 方面，
當兩個 gates 被證明是相等的時候，
SAT engine 會 learn 起來這件事情，
所以除非你 reset solver, 否則後來的 assumpSolve 都會有這樣的資訊。
這叫做 "incremental SAT"，如果你沒有用的話保證你會証很慢，
因為前面証的後面沒有用到，那相當於證明的 cone 越來越大...
p.s. 其實 SAT 證明過程還有 learn 到很多東西，他都有記下來。
: --
:
※ 發信站: 批踢踢實業坊(ptt.cc)
: ◆ From: 111.249.189.38
: → victoret:個人是沒有重新接...反正一樣的就是一樣。 01/16 13:11
: → victoret:我是說 SAT 裡的東西...不過不知道重新接會不會比較快？ 01/16 13:12
: → victoret:因為目前還沒重接拆...sim12 崩潰...但是也不確定接了速 01/16 13:12
: → victoret:度上有沒有幫助 @@ 01/16 13:13
: 推 ntueesuevan:sim12崩潰+1 01/16 15:49
: → wmin0:我的做法是每次把solver reset 重接... 01/16 18:55
: 推 victoret:請問要重接一定要 reset 嗎？還是有什麼指令可以直接重設 01/16 21:34
: → victoret:某個 gate 的 fanin？ 01/16 21:34
: → wmin0:召喚教授... 01/16 21:45
每次 solver reset 的話之前 learn 的東西就都不見了，
通常是不好...
--
※ 發信站: 批踢踢實業坊(ptt.cc)
◆ From: 114.36.61.155
1F：→ djshen:sat.h裡面寫 for incremental proof, use assumeSolve 01/17 02:50
2F：→ djshen:可是他又clear 所以assumpSolve才是incremental proof? 01/17 02:51
3F：→ ric2k1:clear() 只有清掉 assumption 而已，之前的 proof mode 01/17 03:08
4F：→ ric2k1:以及 learned info 都不會被清掉。 01/17 03:08
5F：→ djshen:我眼花了 根本就沒有assumeSolve= = 打錯字無誤 01/17 03:16
6F：→ djshen:sat 68行 01/17 03:16