: 推 puerpuella:剛剛測試sim08,不過為什麼fraig完strash會刪掉gate? 01/12 23:48 : → puerpuella:可以strash掉的不是會出現在FEC pairs裡面？ 01/12 23:48 : : 推 puerpuella:抱歉可能沒有說清楚..我的意思是跑了讓fraig跑完之後， 01/13 09:09 : → puerpuella:我下strash指令，又有gates被merge掉，可是這些被merge 01/13 09:09 : → puerpuella:的gate不是應該會出現在FEC pair中而被SAT證明? 01/13 09:10 這問題其實有點 tricky... 我觀察到的情況是: 某個 FEC group, for example, [38] 100, 200, 300, 400, 500, 600, 700, 800... 比較特別的是這個 group simulatoin 之後的值是 all 0's, 這種情況很有可能會發生在像是大 AND gates, 它們 output = 1 的機率極低， 而且 simulation 其實對它們沒有甚麼鑑別力。 所以我 ref prog 的作法並不是去檢查 N^2 個 FEC pairs, 而是去檢查每一個 gate 是否等於 constant 0 (i.e. 去解 SAT(g = 1)). 如果是的話, 我就用 const 0 去 replace 它, 反之如果不是的話，產生出來的 counter example 就足以證明 g != 0, Either way g 都會被從這個 FEC group 拿掉。 但是被拿掉的 gates 並不保證他們原來不會相等， 因此會有 fraig 做完之後再 strash, 甚至是再 fraig, 仍然會有新的可以 merge 的 pairs. BTW, fraig 的 runtime 以及 optimization result 是個 trade off, 大家行有餘力可以試試看如何 balance, 或是試試看做幾次很快的 fraig, 看可不可以達到 runtime 以及 optimization 都比單次比較昂貴的演算法好? (目前版本的 ref prog 還很陽春...) 歡迎分享心得!! --

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