作者ric2k1 (Ric)
看板EE_DSnP
标题[情报] SAT 之使用
时间Sat Jan 14 22:26:40 2012
虽然讲义里头应该是说明得很清楚了，但我还是翻成中文来跟大家说明一下，
其实是很简单用的...
1. Create 一个 SatSolver 的 object, 并且呼叫 initialize().
2. 在证明任何 FEC pair 之前，请先建立整个 circuit 的 SAT model,
也就是说: (1) 每个 gate (含 PIs) 要对应到一个 SAT Var (solver.newVar()),
(2) 呼叫 solver.addAigCNF() 去建立每个 AIG gate 对应的 CNF，
这些 CNF clauses 会存在 solver 中。
3. 针对某个要证明的 FEC pair "F == XOR(f, g)", (<= 要给 F 一个新的 SAT Var)
呼叫 solver.addXorCNF() 去建立对应的 CNF clauses.
4. 呼叫 "solver.assumeProperty(F_var)" 以及 solver.assumpSolve()
来看看 F == XOR(f, g) 是否可以 satisfied.
5. 如果 UNSAT (solve() return false), 则 f alywas = g, => 可以merge.
如果 SAT (solver() return true), 则可以根据 circuit 的 PIs 所对应的
SAT vars 去抓到 SAT assignment (呼叫 getValue()),
然後等一下可以利用这些 assignment (pattern) 去 simulate.
6. 下次要再证明别的 pair 时只要把 assumption release,
再重复 3 ~ 5 就可以了! 不用重建电路的 proof model.
--
※ 发信站: 批踢踢实业坊(ptt.cc)
◆ From: 114.36.54.233
1F：→ ric2k1:补充一下，如果你的电路改掉了，circuit 的 proof model 01/14 22:29
2F：推 happ6:请问一下在步骤2的时候,po有要建立SAT Var吗？ 01/14 22:29
3F：→ ric2k1:可能就要重建罗! 不能只是 release assumption 哦! 01/14 22:30
4F：→ ric2k1:PO 如果会在 FEC pairs 里头理论上是要啦! 不过也可以让 01/14 22:31
5F：→ ric2k1:PO 的 SAT var 等於 po->fanin[0] 的 SAT var 01/14 22:31
6F：推 happ6:谢谢教授 01/14 22:32
7F：推 ntueesuevan:请问我们找的FEC pairs不是不用包含po吗？ 01/14 22:58
8F：→ ric2k1:所以我说 "如果"... 01/14 23:12
9F：→ ric2k1:更正一下，我删掉 gates 时并没有重新 create proof model 01/15 00:12
10F：→ ric2k1:不过这边要小心，不要拿到 garbage 来证... 01/15 00:12