大哉問，要仔細回答可能要上半學期的課... ※ 引述《puerpuella (柏亨)》之銘言： : 看不太懂sat engine是要怎麼用.. : 是要一開始就把整個電路每個gate建出來，simulate找出FEC pairs後再證明， : 還是對每一個FEC pair都把子電路建出來，證完再刪掉建下一個? Simulation 的複雜度基本上是 linear to the circuit size x num of patterns. 所以要 simulate 成千上萬個 patterns 還算是快。 電路裡的 signal pairs 有 N 平方對， simulation 可以用來將 non-EQ (non-equivalent) pairs 找出來， 剩下的就是可能的 EQ pairs (FEC). SAT solver 是用來檢查一個 Boolean function F 是否為 satisfiable， 也就是說可否找到一組 variable assignment 使得 F = 1. 所以如果我們將 FEC pair (a, b) 加個 xor gate, 也就是說讓 F = a xor b, 再用 SAT 去解 F = 1， 如果 SAT 告訴你無解 (UNSAT) 的話你就可以確定 a 一定永遠等於 b, 反之，你可以找到一組 assignment 去見證 a != b, 而你也可以用這組 assignment 來看看它是否可以見證其他 FEC pair 為 non-EQ 不過，SAT in general 是 NP complete 的問題， 也就是說，它的複雜度可以跟電路大小成 exponential 的關係。 總而言之，我們不希望給他太多 FEC pair 讓他解太久， 所以跑 simulation 的用意就是希望把一些 non-EQ 的 pairs 盡量找出來， 但是有些 singla pairs 要用 simulation 來證實是 non-EQ 的機率太低了， 所以很可能 simulation 跑老半天也無法 distinguish 出來， 這時就不如交給 SAT 去證明比較好。 請注意 SAT solver 有它自己的 data structure， 通常是以 CNF (conjunctive normal form; i.e. product of sum) 來表示， 裏頭最主要的 DS 就是 "clause", "variable", 以及 "literal". 後兩者與 AIG 的定義相似，而前者泛指 literals 的 disjunctions， 像是 "(a + !b + c)", 或是 "(!a)" 等等。 而一個 SAT 的問題 (called "proof model") 就是以一堆 clauses conjunct 起來的。 >> 以上為介紹，以下回答你的問題: 實際的做法應該是: Construct circuit; // AIGER file to circuit graph Strash; // Weed out structurally EQ signals Simulate; // Collect potential FEC pairs Initialize SAT engine; // init(); assign Var ID for each gate for_each(Pair p, FEC_pairs) 將 p 的 子電路對應的 CNF formula 建出來； // use "addAigCNF()" Release assumption; 將新的要證的 FEC pair logic (i.e. a xor b) 的 CNF 加入 as assumption; Call assumeSolve(); 處理證完的結果; // simplify 電路 or gather counter-example continue for the next pair : 另外我搞不懂sat裡面的assume和assert要怎麼分別? : 每個直接xor起來再assert和分別assume值求解感覺效果一樣 這牽涉到 SAT 內部的實作， 簡而言之，現在的 SAT solver 為了使的效率提高， 通常會在解的過程加入各式各樣的學習機制， 比方說他在搜尋 assignment 的時候很可能會發現搜尋的方向錯誤， 這時學習機制就會將錯誤的原因找出來，加入搜尋的條件， 讓 SAT engine 以後不要再犯相同的錯誤。 而這種學習的結果通常對於一個電路而言是永遠成立的， 也就是說在證明一個 (例如) FEC pair 時所學到的所有東西 在證明下一個 FEC pair 時還是適用，這叫做 "incremental SAT solving"。 因此，"assume" 系列的 functions 就是要用來做 "incremental SAT" 的， 我們一次將一個 FEC pair 的 "a xor b" 加入 proof model 當作是 assumption， 證完之後再將 assumption release，然後繼續下一個 FEC pair， 這樣所有的 learned informaion 都可以 carry over， 提升整體效能。 而 assert 是用來做 one-time proof 的。 --

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