最早使用cmt的minisat改进版求解器3——vsids-master-1countbridgemvsids

Posted 2021-03-01 yuweng1689

位置：

E:CNKI E-StudylocalestudyLiteratureSAT求解器学习_6B1FE1DF69904FE2AEC3542DCF408574VSIDS paperVISDS-solversvsids-master-1vsids-master-1countbridgemvsidscore

代码解读

---

 

Solver.h

1 class Solver { ...100 101 // Statistics: (read-only member variable) 102 // 103 uint64_t solves, starts, decisions, bridge_decisions, rnd_decisions, propagations, conflicts, backjumps; 104 uint64_t dec_vars, clauses_literals, learnts_literals, max_literals, tot_literals; 105 uint64_t learnt_clause_vars, bridge_learnt_clause_vars, cag_vars, bridge_cag_vars; ... 178 179 vec<bool> bridges; ... 239 };

 

Solver.cpp

1 Solver::Solver() : ... 33 , learnt_clause_vars (0) 34 , bridge_learnt_clause_vars(0) 35 , cag_vars (0) 36 , bridge_cag_vars (0) ...54 {}

1 void Solver::analyze(CRef confl, vec<Lit>& out_learnt, int& out_btlevel) 2 { 3 int pathC = 0; 4 Lit p = lit_Undef; 5 6 // Generate conflict clause: 7 // 8 out_learnt.push(); // (leave room for the asserting literal) 9 int index = trail.size() - 1; 10 11 do{ 12 assert(confl != CRef_Undef); // (otherwise should be UIP) 13 Clause& c = ca[confl]; 14 15 if (c.learnt()) 16 claBumpActivity(c); 17 18 for (int j = (p == lit_Undef) ? 0 : 1; j < c.size(); j++){ 19 Lit q = c[j]; 20 21 if (!seen[var(q)] && level(var(q)) > 0){ 22 varBumpActivity(var(q)); 23 if (bridges[var(q)]) { 24 bridge_cag_vars++; 25 } 26 cag_vars++; 27 seen[var(q)] = 1; 28 if (level(var(q)) >= decisionLevel()) 29 pathC++; 30 else 31 out_learnt.push(q); 32 } 33 } 34 35 // Select next clause to look at: 36 while (!seen[var(trail[index--])]); 37 p = trail[index+1]; 38 confl = reason(var(p)); 39 seen[var(p)] = 0; 40 pathC--; 41 42 }while (pathC > 0); 43 out_learnt[0] = ~p; 44 45 // Simplify conflict clause: 46 // 47 int i, j; 48 out_learnt.copyTo(analyze_toclear); 49 if (ccmin_mode == 2){ 50 uint32_t abstract_level = 0; 51 for (i = 1; i < out_learnt.size(); i++) 52 abstract_level |= abstractLevel(var(out_learnt[i])); // (maintain an abstraction of levels involved in conflict) 53 54 for (i = j = 1; i < out_learnt.size(); i++) 55 if (reason(var(out_learnt[i])) == CRef_Undef || !litRedundant(out_learnt[i], abstract_level)) 56 out_learnt[j++] = out_learnt[i]; 57 58 }else if (ccmin_mode == 1){ 59 for (i = j = 1; i < out_learnt.size(); i++){ 60 Var x = var(out_learnt[i]); 61 62 if (reason(x) == CRef_Undef) 63 out_learnt[j++] = out_learnt[i]; 64 else{ 65 Clause& c = ca[reason(var(out_learnt[i]))]; 66 for (int k = 1; k < c.size(); k++) 67 if (!seen[var(c[k])] && level(var(c[k])) > 0){ 68 out_learnt[j++] = out_learnt[i]; 69 break; } 70 } 71 } 72 }else 73 i = j = out_learnt.size(); 74 75 max_literals += out_learnt.size(); 76 out_learnt.shrink(i - j); 77 tot_literals += out_learnt.size(); 78 79 // Find correct backtrack level: 80 // 81 if (out_learnt.size() == 1) 82 out_btlevel = 0; 83 else{ 84 int max_i = 1; 85 // Find the first literal assigned at the next-highest level: 86 for (int i = 2; i < out_learnt.size(); i++) 87 if (level(var(out_learnt[i])) > level(var(out_learnt[max_i]))) 88 max_i = i; 89 // Swap-in this literal at index 1: 90 Lit p = out_learnt[max_i]; 91 out_learnt[max_i] = out_learnt[1]; 92 out_learnt[1] = p; 93 out_btlevel = level(var(p)); 94 } 95 96 for (int i = 0; i < out_learnt.size(); i++) { 97 Var v = var(out_learnt[i]); 98 if (bridges[v]) { 99 bridge_learnt_clause_vars++; 100 } 101 learnt_clause_vars++; 102 } 103 104 for (int j = 0; j < analyze_toclear.size(); j++) seen[var(analyze_toclear[j])] = 0; // (‘seen[]‘ is now cleared) 105 } void Solver::analyze(CRef confl, vec& out_learnt, int& out_btlevel)  关注分析函数中的新增统计量：learnt_clause_vars, bridge_learnt_clause_vars, cag_vars, bridge_cag_vars;

1 lbool Solver::solve_() 2 { 3 if (!opt_cmty_file) 4 fprintf(stderr, "missing community file "), exit(1); 5 FILE* cmty_file = fopen(opt_cmty_file, "r"); 6 if (cmty_file == NULL) 7 fprintf(stderr, "could not open file %s ", (const char*) opt_cmty_file), exit(1); 8 9 vec<int> cmtys (nVars()); 10 int v; 11 int cmty; 12 while (fscanf(cmty_file, "%d %d ", &v, &cmty) == 2) { 13 cmtys[v] = cmty; 14 } 15 for (int i = 0; i < nClauses(); i++) { 16 Clause& c = ca[clauses[i]]; 17 if (c.size() > 0) { 18 for (int j = 0; j < c.size(); j++) { 19 Var varJ = var(c[j]); 20 for (int k = j + 1; k < c.size(); k++) { 21 Var varK = var(c[k]); 22 if (cmtys[varJ] != cmtys[varK]) { 23 bridges[varJ] = true; 24 bridges[varK] = true; 25 } 26 } 27 } 28 } 29 } 30 int nBridges = 0; 31 for (int i = 0; i < bridges.size(); i++) { 32 if (bridges[i]) nBridges++; 33 } 34 35 printf("Bridges : %d ", nBridges); 36 printf("Variables : %d ", nVars()); 37 38 fclose(cmty_file); 39 40 model.clear(); 41 conflict.clear(); 42 if (!ok) return l_False; 43 44 solves++; 45 46 max_learnts = nClauses() * learntsize_factor; 47 learntsize_adjust_confl = learntsize_adjust_start_confl; 48 learntsize_adjust_cnt = (int)learntsize_adjust_confl; 49 lbool status = l_Undef; 50 51 if (verbosity >= 1){ 52 printf("============================[ Search Statistics ]============================== "); 53 printf("| Conflicts | ORIGINAL | LEARNT | Progress | "); 54 printf("| | Vars Clauses Literals | Limit Clauses Lit/Cl | | "); 55 printf("=============================================================================== "); 56 } 57 58 // Search: 59 int curr_restarts = 0; 60 while (status == l_Undef){ 61 double rest_base = luby_restart ? luby(restart_inc, curr_restarts) : pow(restart_inc, curr_restarts); 62 status = search(rest_base * restart_first); 63 if (!withinBudget()) break; 64 curr_restarts++; 65 } 66 67 if (verbosity >= 1) 68 printf("========================================================== "); 69 70 71 if (status == l_True){ 72 // Extend & copy model: 73 model.growTo(nVars()); 74 for (int i = 0; i < nVars(); i++) model[i] = value(i); 75 }else if (status == l_False && conflict.size() == 0) 76 ok = false; 77 78 cancelUntil(0); 79 return status; 80 } 重点关注：cmtys     cmty_file    bridges