作者photonzero (邪心魔佛)
看板EE_DSnP
标题Re: [情报] SAT 之使用
时间Tue Jan 17 11:13:59 2012
※ 引述《ric2k1 (Ric)》之铭言：
: 虽然讲义里头应该是说明得很清楚了，但我还是翻成中文来跟大家说明一下，
: 其实是很简单用的...
: 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)
请问要给一个新的变数是什麽意思
是每次模拟就要给一个新变数吗
i.e 每次都要重新Var F=s.newVar();
: 呼叫 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: 61.228.34.151
※ 编辑: photonzero 来自: 61.228.34.151 (01/17 11:15)
1F：推 ric2k1:SAT 跟模拟没有关系吧!? 01/17 11:38
2F：→ photonzero:这李的模拟是指看是否有解能satisfy 01/17 11:50
3F：推 ric2k1:应该是说每一次要证明新的 pair 都要产生新的 SAT var 01/17 11:54
4F：→ photonzero:那可以把原本的给delete掉吗？ 01/17 11:55
5F：推 ric2k1:要 delete 原本的变数不容易，要改 sat 的 code... 01/17 12:05
6F：→ ric2k1:建议不要 01/17 12:05
7F：→ photonzero:我试过直接在XORCNF内加上^(上次结果),但会有记忆体错 01/17 12:16
8F：→ photonzero:而且错误发生在SAT内= =,为什麽直接在true false动手 01/17 12:17
9F：→ photonzero:不行勒QQ 01/17 12:17
10F：→ photonzero:教授我在最外面宣告一个Var就可以跑，但在里面就会当掉 01/17 13:15
11F：→ photonzero:而且当掉点都在SAT内，可以请问是为什麽吗，而且我FEC 01/17 13:16
12F：→ photonzero:内部有照dfs顺序 01/17 13:17