大哉问，要仔细回答可能要上半学期的课... ※ 引述《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