Re: [情報] SAT 之使用

看板EE_DSnP作者photonzero (邪心魔佛)時間12年前 (2012/01/17 11:14)推噓3(3推 0噓 9→)

留言12則, 2人參與討論串2/3 (看更多)

※ 引述《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)

推

ric2k1

01/17 11:38, , 1^F

01/17 11:38, 1^F

→

photonzero

01/17 11:50, , 2^F

01/17 11:50, 2^F

推

ric2k1

01/17 11:54, , 3^F

01/17 11:54, 3^F