标签：break def imp img border iter ranch ast span
位置：
E:\CNKI E-Study\localestudy\Literature\SAT求解器学习_6B1FE1DF69904FE2AEC3542DCF408574\VSIDS paper\VISDS-solvers\vsids-master-1\vsids-master-1\minisat-performance\core
代码分析
Solver.h
1 //============================================ 2 // Solver -- the main class: 3 4 class Solver { 5 public: ... 23 24 bool save_decision_trail; // Whether to save decision trail 25 bool save_learned_clauses; // Whether to save learned clauses 26 bool conflicting_vars_analysis; ... 53 void writeDecisionVar(Var next); 54 void writeLearnedClause(vec<Lit>& out_learnt); 55 void updateConflictAnalysis(Var v); 56 void updateConflictAnalysis(vec<Lit>& c); 57 58 // Track solver behavior 59 FILE* decision_trail_file; 60 FILE* learned_clauses_file; ...120 121 //XXX EXPERIMENT 122 std::vector<int> conflicting_vars_count; 123 std::vector< std::vector<double> > conflicting_vars_graph; ... 255 }; |
1 inline void Solver::writeDecisionVar(Var next) { 2 if (save_decision_trail) { 3 assert((next != var_Undef) && (next>=0) && (next<=nVars())); 4 // +1 is necessary because MiniSAT stores variables naming from 0 not 1 5 //fprintf(decision_trail_file, "%d ", next+1); 6 fprintf(decision_trail_file, "%d\n", next); 7 } 8 } 9 10 inline void Solver::writeLearnedClause(vec<Lit>& out_learnt) { 11 if (save_learned_clauses) { 12 for(int i = 0; i < out_learnt.size(); i++) 13 fprintf(learned_clauses_file, "%d ", var(out_learnt[i])); 14 fprintf(learned_clauses_file, "\n"); 15 } 16 } 17 18 inline void Solver::updateConflictAnalysis(Var v) { 19 if (conflicting_vars_analysis) { 20 // +1 at end is necessary because MiniSAT stores variables naming from 0 not 1 21 conflicting_vars_count[v] += 1; 22 } 23 } 24 25 inline void Solver::updateConflictAnalysis(vec<Lit>& c) { 26 if (conflicting_vars_analysis) { 27 int l,h; 28 //printf("asdf\n"); 29 // +1 at end is necessary because MiniSAT stores variables naming from 0 not 1 30 for(int i = 0; i < c.size()-1; i++) 31 for(int j = i + 1; j < c.size(); j++){ 32 if(var(c[i]) < var(c[j])){ 33 l = var(c[i]); 34 h = var(c[j]); 35 } 36 else{ 37 l = var(c[j]); 38 h = var(c[i]); 39 } 40 //printf("%d %d\n",l,h); 41 //XXX probably should change increment to correlate with clause size 42 conflicting_vars_graph[l][h-l-1] += 1; 43 } 44 45 } 46 } |
|
Solver.h中新增用于观察性能的代码段 |
Solver.cc
1 lbool Solver::search(int nof_conflicts) 2 { 3 assert(ok); 4 int backtrack_level; 5 int conflictC = 0; 6 vec<Lit> learnt_clause; 7 starts++; 8 9 for (;;){ 10 CRef confl = propagate(); 11 if (confl != CRef_Undef){ 12 // CONFLICT 13 conflicts++; conflictC++; 14 if (decisionLevel() == 0) return l_False; 15 16 learnt_clause.clear(); 17 analyze(confl, learnt_clause, backtrack_level); 18 cancelUntil(backtrack_level); 19 20 if (learnt_clause.size() == 1){ 21 uncheckedEnqueue(learnt_clause[0]); 22 }else{ 23 CRef cr = ca.alloc(learnt_clause, true); 24 learnts.push(cr); 25 attachClause(cr); 26 claBumpActivity(ca[cr]); 27 uncheckedEnqueue(learnt_clause[0], cr); 28 } 29 30 varDecayActivity(); 31 claDecayActivity(); 32 33 if (--learntsize_adjust_cnt == 0){ 34 learntsize_adjust_confl *= learntsize_adjust_inc; 35 learntsize_adjust_cnt = (int)learntsize_adjust_confl; 36 max_learnts *= learntsize_inc; 37 38 if (verbosity >= 1) 39 printf("| %9d | %7d %8d %8d | %8d %8d %6.0f | %6.3f %% |\n", 40 (int)conflicts, 41 (int)dec_vars - (trail_lim.size() == 0 ? trail.size() : trail_lim[0]), nClauses(), (int)clauses_literals, 42 (int)max_learnts, nLearnts(), (double)learnts_literals/nLearnts(), progressEstimate()*100); 43 } 44 45 }else{ 46 // NO CONFLICT 47 if (nof_conflicts >= 0 && conflictC >= nof_conflicts || !withinBudget()){ 48 // Reached bound on number of conflicts: 49 progress_estimate = progressEstimate(); 50 cancelUntil(0); 51 return l_Undef; } 52 53 // Simplify the set of problem clauses: 54 if (decisionLevel() == 0 && !simplify()) 55 return l_False; 56 57 if (learnts.size()-nAssigns() >= max_learnts) 58 // Reduce the set of learnt clauses: 59 reduceDB(); 60 61 Lit next = lit_Undef; 62 while (decisionLevel() < assumptions.size()){ 63 // Perform user provided assumption: 64 Lit p = assumptions[decisionLevel()]; 65 if (value(p) == l_True){ 66 // Dummy decision level: 67 newDecisionLevel(); 68 }else if (value(p) == l_False){ 69 analyzeFinal(~p, conflict); 70 return l_False; 71 }else{ 72 next = p; 73 break; 74 } 75 } 76 77 if (next == lit_Undef){ 78 // New variable decision: 79 decisions++; 80 next = pickBranchLit(); 81 82 83 if (next == lit_Undef) 84 // Model found: 85 return l_True; 86 else 87 writeDecisionVar(var(next)); 88 } 89 90 // Increase decision level and enqueue ‘next‘ 91 newDecisionLevel(); 92 uncheckedEnqueue(next); 93 } 94 } 95 } 函数writeDecisionVar(var(next))调用 |
| void Solver::analyze(CRef confl, vec& out_learnt, int& out_btlevel)
发生以下函数调用： updateConflictAnalysis(var(out_learnt[i])); updateConflictAnalysis(out_learnt); writeLearnedClause(out_learnt)； |
1 Solver::~Solver() 2 { 3 if(save_decision_trail) 4 fclose(decision_trail_file); 5 } 备注： bool save_decision_trail; // Whether to save decision trail |
最早使用cmt的minisat改进版求解器2——vsids-master-1\minisat-performance
标签：break def imp img border iter ranch ast span
原文地址：https://www.cnblogs.com/yuweng1689/p/12695078.html
