Maple_CM_ordUP+, Based on Maple_LCM --Copyright (c) 2018, Chu-Min LI, Mao Luo, Fan Xiao:
implementing a clause minimisation approach and selects the conflicts to re-order the first UIPs conflict in function of the branching heuristics VSIDS and LRB.
该求解器设计 学习子句、原始子句minimization；延迟restarts；蕴含图的First UIP 冲突的选择与排序
李初民教授团队近三年研究主要脉络：
文章1：
M. Luo, C.-M. Li, F. Xiao, F. Manya, and Z. L¨u, “An effective learnt clause minimization approach for CDCL SAT solvers,” in Proceedings of IJCAI, 2017, pp. 703–711.
求解器：
|
MapleCOMSPS DRUP ——> Maple LCM 2017 ——> Maple CM 2018 且有三个变体 2016冠军（J. H. Liang） 2017年冠军 （Li，基于文章1思路改进） 2018年版本（li） |
|
|
Maple CM Dist: is Maple CM but uses a special branching heuristic called Distance for the first 50,000 conflicts; Maple CM ordUIP: is Maple CM but reorders the first UIPs implying some conflicts selected under specific conditions; Maple CM ordUIP+: is Maple CM ordUIP but selects the conflicts to re-order the first UIPs conflict in |
4.文献中有关oldUIP的部分
|
4. Blocking Restarts and Re-ordering UIPs in Maple CM ordUIP The block-restart mechanism was introduced in Glucose 2.1 [6] for postponing a restart, when the solver is estimated to be approaching a global solution using a heuristic, in order to find quickly the global solution. In Maple CM ordUIP, we push further the block-restart mechanism of Glucose. When the solver derives a conflict In addition, it constructs a complete implication graph of the conflict to collect the first UIP (Unique Implication Recall that a UIP in a decision level is a literal l such that every path from the decision literal of the level to the
Then, the solver backtracks so that all decisions in the complete implication graph are canceled, and continues the
Concretely, each time Maple_CM_ordUIP derives a conflict after the first 105 conflicts, it calls Algorithm 3 before
Restart is possible only if nbC_For_Restart is greater than 50. 当nbC_For_reOrder的值大于50次之后，才允许启动重启模式。 In other words, when the 1UIPs are re-ordered, the next restart or the next 1UIP re-ordering is possible only after the next 50 conflicts. 译文：换句话说，当1UIPs被重新排序时，只有在接下来的50个冲突之后才有可能进行下一次重启或下一次1UIP重新排序。 If unit propagation derives an empty clause C0, function unitPropagate(l) returns C0; otherwise, it returns “no conflict”. 译文：如果单元传播派生一个空子句C0，函数unitPropagate(l)返回C0;否则，返回“无冲突”。 |
  |
5. Blocking Restarts and Re-ordering UIPs in Maple CM ordUIP+
|
Maple_CM, like MapleCOMSPS_DRUP and Maple_LCM, first uses the LRB heuristic for 2500 seconds and switches to the VSIDS heuristic for the remaining run time. 首先在2500秒内使用LRB启发式，并在剩余运行时切换到VSIDS启发式。 It appears that the LRB heuristic is more powerful to solve satisfiable instances, whereas the VSIDS heuristic is more powerful to solve unsatisfiable instances. 译文：结果表明，LRB启发式在解决可满足的实例时更有效，而VSIDS启发式在解决不可满足的实例时更有效。 So, we implement Maple_CM_ordUIP+, that is Maple_CM_ordUIP but selects the conflict to re-order the 1UIPs differently in function of the branching heuristic used to derive the conflict. |
|
|
Intuitively, the first conflict is the most important in a restart, because it determines the search direction in the Maple CM ordUIP+ aims at reinforcing the capability of the VSIDS heuristic to find a global solution of the instance, by branching first on the 1UIPs implying the greatest number of literals in a restart.译文：Maple CM ordUIP+的目标是增强VSIDS启发式的能力，以找到实例的全局解决方案，方法是首先在1UIPs上分支，这意味着在重启中有最多的字量。 |
References
[1] J. H. Liang, V. Ganesh, P. Poupart, and K. Czarnecki, “Learning rate based branching heuristic for SAT solvers,” in Proceedings of SAT, 2016, pp. 123–140.[2] J. H. Liang, C. Oh, V. Ganesh, K. Czarnecki, and P. Poupart, “MapleCOMSPS, MapleCOMSPS LRB, MapleCOMSPS CHB,” in SAT Competition,2016, p. 52.
[3] M. Luo, C.-M. Li, F. Xiao, F. Manya, and Z. L¨u, “An effective learnt clause minimization approach for CDCL SAT solvers,” in Proceedings of IJCAI, 2017, pp. 703–711.
[4] G. Audemard and L. Simon, “Predicting learnt clauses quality in modern SAT solvers,” in Proceedings of IJCAI-2009, 2009, pp. 399–404.
[5] M. Moskewicz, C. Madigan, Y. Zhao, L. Zhang, and S. Malik, “Chaff:Engineering an efficient SAT solver,” in Proceedings of DAC-2001,2001.
[6] G. Audemard and L. Simon, “Refining restarts strategies for SAT and UNSAT,” in Proceedings of CP, 2012, pp. 118–126.
[7] L. Zhang, C. Madigan, M. Moskewicz, and S. Malik, “Efficient conflict driven learning in a Boolean satisfiability solver,” in Proceedings of ICCAD-2001, 2001, pp. 279–285.
代码分析：
1.新增
| 在Solver中新增的信息 |
|
vec<CRef> usedClauses; bool simplifyUsedOriginalClauses(); MyQueue<int> trailQueue; void simpleCancelUntil(int level);
bool simplifyOriginalClauses(); vec<int> pathCs; struct decision_lt { |
| Solver.cc中改进的信息 |
| // based on Maple_LCMsimpAllWithC5w+2+oriClsGoodConf20+lbd1+blockResNbTotalFix2+1e-200LRB |
| 构造函数中 |
|
, trailQueue (5000)
|
化简函数 |
1 struct clauseSize_lt { 2 ClauseAllocator& ca; 3 clauseSize_lt(ClauseAllocator& ca_) : ca(ca_) {} 4 bool operator () (CRef x, CRef y) const { return ca[x].size() > ca[y].size(); } 5 }; 6 7 #define simpLimit 100000000 8 #define tolerance 100 9 10 bool Solver::simplifyOriginalClauses() { 11 12 int last_shorten=0, nbOriginalClauses_before = clauses.size(); 13 vec<Lit> lits; 14 15 int nbShortened=0, ci, cj, nbRemoved=0, nbShortening=0; 16 17 // sort(clauses, clauseSize_lt(ca)); 18 printf("c total nb of literals: %llun", clauses_literals); 19 // if (clauses.size()> simpLimit) { 20 // printf("c too many original clauses (> %d), no original clause minimization n", 21 // simpLimit); 22 // return true; 23 // } 24 double begin_simp_time = cpuTime(); 25 for (ci = 0, cj = 0; ci < clauses.size(); ci++){ 26 CRef cr = clauses[ci]; 27 Clause& c = ca[cr]; 28 // printf("%d n", c.size()); 29 if (removed(cr)) continue; 30 // if (ci - last_shorten > tolerance) 31 // clauses[cj++] = clauses[ci]; 32 // else 33 if (s_propagations>simpLimit && ci-last_shorten>tolerance) 34 clauses[cj++] = clauses[ci]; 35 else{ 36 if (drup_file){ 37 add_oc.clear(); 38 for (int i = 0; i < c.size(); i++) add_oc.push(c[i]); } 39 40 if (simplifyLearnt(c, cr, lits)) { 41 if(drup_file && add_oc.size()!=lits.size()){ 42 #ifdef BIN_DRUP 43 binDRUP('a', lits , drup_file); 44 binDRUP('d', add_oc, drup_file); 45 #else 46 for (int i = 0; i < lits.size(); i++) 47 fprintf(drup_file, "%i ", (var(lits[i]) + 1) * (-2 * sign(lits[i]) + 1)); 48 fprintf(drup_file, "0n"); 49 50 fprintf(drup_file, "d "); 51 for (int i = 0; i < add_oc.size(); i++) 52 fprintf(drup_file, "%i ", (var(add_oc[i]) + 1) * (-2 * sign(add_oc[i]) + 1)); 53 fprintf(drup_file, "0n"); 54 #endif 55 } 56 57 nbShortening++; 58 if (lits.size() == 1){ 59 // when unit clause occur, enqueue and propagate 60 uncheckedEnqueue(lits[0]); 61 if (propagate() != CRef_Undef){ 62 ok = false; 63 return false; 64 } 65 // delete the clause memory in logic 66 c.mark(1); 67 ca.free(cr); 68 } 69 else { 70 if (c.size() > lits.size()) { 71 nbShortened++; nbRemoved += c.size() - lits.size(); last_shorten = ci; 72 } 73 detachClause(cr, true); 74 for(int i=0; i<lits.size(); i++) 75 c[i]=lits[i]; 76 c.shrink(c.size()-lits.size()); 77 attachClause(cr); 78 assert(c == ca[cr]); 79 clauses[cj++] = clauses[ci]; 80 // c.setSimplified(2); 81 } 82 } 83 } 84 } 85 clauses.shrink(ci - cj); 86 double avg; 87 if (nbShortened>0) 88 avg= ((double)nbRemoved)/nbShortened; 89 else avg=0; 90 // printf("c nbOriginalClauses before/after: %d / %d, nbShortening: %d, nbShortened: %d, avg nbLits removed: %4.2lfn", 91 // nbOriginalClauses_before, clauses.size(), nbShortening, nbShortened, avg); 92 // printf("c Original clause minimization time: %5.2lfs, number UPs: %llun", 93 // cpuTime() - begin_simp_time, s_propagations); 94 95 return true; 96 }
|
|
初始变元相关信息的函数 1 Var Solver::newVar(bool sign, bool dvar) 2 { 3 int v = nVars(); 4 watches_bin.init(mkLit(v, false)); 5 watches_bin.init(mkLit(v, true )); 6 watches .init(mkLit(v, false)); 7 watches .init(mkLit(v, true )); 8 assigns .push(l_Undef); 9 vardata .push(mkVarData(CRef_Undef, 0)); 10 activity_CHB .push(0); 11 activity_VSIDS.push(rnd_init_act ? drand(random_seed) * 0.00001 : 0); 12 13 picked.push(0); 14 conflicted.push(0); 15 almost_conflicted.push(0); 16 #ifdef ANTI_EXPLORATION 17 canceled.push(0); 18 #endif 19 20 seen .push(0); 21 seen2 .push(0); 22 polarity .push(sign); 23 decision .push(); 24 trail .capacity(v+1); 25 setDecisionVar(v, dvar); 26 27 28 pathCs .push(0); 29 var_iLevel .push(0); 30 31 return v; 32 }
|
|
分析函数改进较多 1 void Solver::analyze(CRef confl, vec<Lit>& out_learnt, int& out_btlevel, int& out_lbd) 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 int saved; 12 saved = usedClauses.size(); 13 14 do{ 15 assert(confl != CRef_Undef); // (otherwise should be UIP) 16 Clause& c = ca[confl]; 17 18 // For binary clauses, we don't rearrange literals in propagate(), so check and make sure the first is an implied lit. 19 if (p != lit_Undef && c.size() == 2 && value(c[0]) == l_False){ 20 assert(value(c[1]) == l_True); 21 Lit tmp = c[0]; 22 c[0] = c[1], c[1] = tmp; } 23 24 int lbd = computeLBD(c); 25 if (lbd < c.lbd()){ 26 if (lbd == 1) 27 c.setSimplified(0); 28 if (c.simplified() > 0) 29 c.setSimplified(c.simplified()-1); 30 if (c.learnt()) { 31 if (c.lbd() <= 30) c.removable(false); // Protect once from reduction. 32 // move confl into CORE or TIER2 if the new lbd is small enough 33 if (c.mark() != CORE){ 34 if (lbd <= core_lbd_cut){ 35 learnts_core.push(confl); 36 c.mark(CORE); 37 }else if (lbd <= 6 && c.mark() == LOCAL){ 38 // Bug: 'cr' may already be in 'learnts_tier2', e.g., if 'cr' was demoted from TIER2 39 // to LOCAL previously and if that 'cr' is not cleaned from 'learnts_tier2' yet. 40 learnts_tier2.push(confl); 41 c.mark(TIER2); } 42 } 43 } 44 c.set_lbd(lbd); 45 } 46 if (c.learnt()) { 47 if (c.mark() == TIER2) 48 c.touched() = conflicts; 49 else if (c.mark() == LOCAL) 50 claBumpActivity(c); 51 } 52 else { 53 if (c.used()==0 && c.simplified()==0) { 54 // if (c.used()==0 && c.lbd() <= lbdLimitForOriCls) { 55 usedClauses.push(confl); 56 c.setUsed(1); 57 } 58 } 59 60 for (int j = (p == lit_Undef) ? 0 : 1; j < c.size(); j++){ 61 Lit q = c[j]; 62 63 if (!seen[var(q)] && level(var(q)) > 0){ 64 if (VSIDS){ 65 varBumpActivity(var(q), .5); 66 add_tmp.push(q); 67 }else 68 conflicted[var(q)]++; 69 seen[var(q)] = 1; 70 if (level(var(q)) >= decisionLevel()){ 71 pathC++; 72 }else 73 out_learnt.push(q); 74 } 75 } 76 77 // Select next clause to look at: 78 while (!seen[var(trail[index--])]); 79 p = trail[index+1]; 80 confl = reason(var(p)); 81 seen[var(p)] = 0; 82 pathC--; 83 84 }while (pathC > 0); 85 out_learnt[0] = ~p; 86 87 // Simplify conflict clause: 88 // 89 int i, j; 90 out_learnt.copyTo(analyze_toclear); 91 if (ccmin_mode == 2){ 92 uint32_t abstract_level = 0; 93 for (i = 1; i < out_learnt.size(); i++) 94 abstract_level |= abstractLevel(var(out_learnt[i])); // (maintain an abstraction of levels involved in conflict) 95 96 for (i = j = 1; i < out_learnt.size(); i++) 97 if (reason(var(out_learnt[i])) == CRef_Undef || !litRedundant(out_learnt[i], abstract_level)) 98 out_learnt[j++] = out_learnt[i]; 99 100 }else if (ccmin_mode == 1){ 101 for (i = j = 1; i < out_learnt.size(); i++){ 102 Var x = var(out_learnt[i]); 103 104 if (reason(x) == CRef_Undef) 105 out_learnt[j++] = out_learnt[i]; 106 else{ 107 Clause& c = ca[reason(var(out_learnt[i]))]; 108 for (int k = c.size() == 2 ? 0 : 1; k < c.size(); k++) 109 if (!seen[var(c[k])] && level(var(c[k])) > 0){ 110 out_learnt[j++] = out_learnt[i]; 111 break; } 112 } 113 } 114 }else 115 i = j = out_learnt.size(); 116 117 max_literals += out_learnt.size(); 118 out_learnt.shrink(i - j); 119 tot_literals += out_learnt.size(); 120 121 out_lbd = computeLBD(out_learnt); 122 if (out_lbd <= 6 && out_learnt.size() <= 30) // Try further minimization? 123 if (binResMinimize(out_learnt)) 124 out_lbd = computeLBD(out_learnt); // Recompute LBD if minimized. 125 126 // Find correct backtrack level: 127 // 128 if (out_learnt.size() == 1) 129 out_btlevel = 0; 130 else{ 131 int max_i = 1; 132 // Find the first literal assigned at the next-highest level: 133 for (int i = 2; i < out_learnt.size(); i++) 134 if (level(var(out_learnt[i])) > level(var(out_learnt[max_i]))) 135 max_i = i; 136 // Swap-in this literal at index 1: 137 Lit p = out_learnt[max_i]; 138 out_learnt[max_i] = out_learnt[1]; 139 out_learnt[1] = p; 140 out_btlevel = level(var(p)); 141 } 142 143 if (VSIDS){ 144 for (int i = 0; i < add_tmp.size(); i++){ 145 Var v = var(add_tmp[i]); 146 if (level(v) >= out_btlevel - 1) 147 varBumpActivity(v, 1); 148 } 149 add_tmp.clear(); 150 }else{ 151 seen[var(p)] = true; 152 for(int i = out_learnt.size() - 1; i >= 0; i--){ 153 Var v = var(out_learnt[i]); 154 CRef rea = reason(v); 155 if (rea != CRef_Undef){ 156 const Clause& reaC = ca[rea]; 157 for (int i = 0; i < reaC.size(); i++){ 158 Lit l = reaC[i]; 159 if (!seen[var(l)]){ 160 seen[var(l)] = true; 161 almost_conflicted[var(l)]++; 162 analyze_toclear.push(l); } } } } } 163 164 if (out_lbd > lbdLimitForOriCls) { 165 for(int i = saved; i < usedClauses.size(); i++) 166 ca[usedClauses[i]].setUsed(0); 167 usedClauses.shrink(usedClauses.size() - saved); 168 } 169 170 for (int j = 0; j < analyze_toclear.size(); j++) seen[var(analyze_toclear[j])] = 0; // ('seen[]' is now cleared) 171 }
|
|
新增函数及信息 1 int Solver::collectFirstUIP(CRef confl){ 2 branchVars.clear(); 3 Clause& c=ca[confl]; int minLevel=decisionLevel(); 4 for(int i=0; i<c.size(); i++) { 5 Var v=var(c[i]); 6 if (level(v)>0) { 7 assert(!seen[v]); 8 seen[v]=1; 9 var_iLevel[v]=0; 10 pathCs[level(v)]++; 11 if (minLevel>level(v)) { 12 minLevel=level(v); 13 assert(minLevel>0); 14 } 15 } 16 } 17 int limit=trail_lim[minLevel-1]; //begining position of level minLevel 18 for(int i=trail.size()-1; i>=limit; i--) { 19 Lit p=trail[i]; Var v=var(p); 20 if (seen[v]) { 21 int currentDecLevel=level(v); 22 seen[v]=0; var_iLevel[v] += 1e-200; 23 if (--pathCs[currentDecLevel]==0) { 24 // v is the last var of the level directly involved in the conflict 25 branchVars.push(v); 26 } 27 else { 28 assert(reason(v) != CRef_Undef); 29 Clause& rc=ca[reason(v)]; 30 if (rc.size()==2 && value(rc[0])==l_False) { 31 // Special case for binary clauses 32 // The first one has to be SAT 33 assert(value(rc[1]) != l_False); 34 Lit tmp = rc[0]; 35 rc[0] = rc[1], rc[1] = tmp; 36 } 37 for (int j = 1; j < rc.size(); j++){ 38 Lit q = rc[j]; Var v1=var(q); 39 if (level(v1) > 0) { 40 if (minLevel>level(v1)) { 41 minLevel=level(v1); limit=trail_lim[minLevel-1]; assert(minLevel>0); 42 } 43 if (seen[v1]) { 44 // if (var_iLevel[v1]<reasonVarLevel) 45 var_iLevel[v1]+=var_iLevel[v]; //=reasonVarLevel; 46 } 47 else { 48 var_iLevel[v1]=var_iLevel[v]; //reasonVarLevel; 49 // varBumpActivity(v1); 50 seen[v1] = 1; 51 pathCs[level(v1)]++; 52 } 53 } 54 } 55 } 56 } 57 } 58 return minLevel; 59 } 60 61 void Solver::simpleCancelUntil(int level) { 62 if (decisionLevel() > level){ 63 for (int c = trail.size()-1; c >= trail_lim[level]; c--){ 64 Var x = var(trail[c]); 65 66 assigns [x] = l_Undef; 67 if (phase_saving > 1 || (phase_saving == 1) && c > trail_lim.last()) 68 polarity[x] = sign(trail[c]); 69 insertVarOrder(x); 70 } 71 qhead = trail_lim[level]; 72 trail.shrink(trail.size() - trail_lim[level]); 73 trail_lim.shrink(trail_lim.size() - level); 74 } 75 } 76 77 CRef Solver::reorderDecisions(CRef confl) { 78 int minConflictLevel; 79 80 branchVars.clear(); 81 82 minConflictLevel = collectFirstUIP(confl); 83 //printf("===%d, %d, %d=== n", trail_lim.size(), branchVars.size(), trail.size()); 84 85 // if (firstConfl) 86 // cancelUntil(0); 87 // else 88 cancelUntil(minConflictLevel-1); 89 sort(branchVars, decision_lt(var_iLevel, vardata)); 90 91 for(int i=0; i<branchVars.size(); i++) { 92 Var var=branchVars[i]; 93 // if (VSIDS) 94 //printf("%10.1lf %d || ", var_iLevel[var], vardata[var].level); 95 // else printf("%5.4lf ", activity_CHB[var]); 96 if (value(var) == l_Undef) { 97 Lit lit=mkLit(var, polarity[var]); 98 newDecisionLevel(); 99 uncheckedEnqueue(lit); 100 CRef confl = propagate(); 101 if (confl != CRef_Undef) { 102 if (trail_lim.size() < branchVars.size()) 103 normalGoodNbReorder++; 104 else 105 normalNbReorder++; 106 //printf("n%d, %d**nn", trail_lim.size(), trail.size()); 107 return confl; 108 } 109 } 110 } 111 goodNbReorder++; 112 //printf("n%d, %d$$nn", trail_lim.size(), trail.size()); 113 // printf("$$$$nn"); 114 return CRef_Undef; 115 } 116 117 double R_reorder = 1.2; 118 int reorderStart;
|
1 // Garbage Collection methods: 2 3 void Solver::relocAll(ClauseAllocator& to) 4 { 5 // All watchers: 6 // 7 // for (int i = 0; i < watches.size(); i++) 8 watches.cleanAll(); 9 watches_bin.cleanAll(); 10 for (int v = 0; v < nVars(); v++) 11 for (int s = 0; s < 2; s++){ 12 Lit p = mkLit(v, s); 13 // printf(" >>> RELOCING: %s%dn", sign(p)?"-":"", var(p)+1); 14 vec<Watcher>& ws = watches[p]; 15 for (int j = 0; j < ws.size(); j++) 16 ca.reloc(ws[j].cref, to); 17 vec<Watcher>& ws_bin = watches_bin[p]; 18 for (int j = 0; j < ws_bin.size(); j++) 19 ca.reloc(ws_bin[j].cref, to); 20 } 21 22 // All reasons: 23 // 24 for (int i = 0; i < trail.size(); i++){ 25 Var v = var(trail[i]); 26 27 if (reason(v) != CRef_Undef && (ca[reason(v)].reloced() || locked(ca[reason(v)]))) 28 ca.reloc(vardata[v].reason, to); 29 } 30 31 // All learnt: 32 // 33 for (int i = 0; i < learnts_core.size(); i++) 34 ca.reloc(learnts_core[i], to); 35 for (int i = 0; i < learnts_tier2.size(); i++) 36 ca.reloc(learnts_tier2[i], to); 37 for (int i = 0; i < learnts_local.size(); i++) 38 ca.reloc(learnts_local[i], to); 39 40 // All original: 41 // 42 int i, j; 43 for (i = j = 0; i < clauses.size(); i++) 44 if (ca[clauses[i]].mark() != 1){ 45 ca.reloc(clauses[i], to); 46 clauses[j++] = clauses[i]; } 47 clauses.shrink(i - j); 48 49 // All original used clauses 50 for (i = j = 0; i < usedClauses.size(); i++) 51 if (ca[usedClauses[i]].mark() != 1){ 52 ca.reloc(usedClauses[i], to); 53 usedClauses[j++] = usedClauses[i]; } 54 usedClauses.shrink(i - j); 55 56 // printf("c **** garbage collection done ****n"); 57 }
|
1 // NOTE: assumptions passed in member-variable 'assumptions'. 2 lbool Solver::solve_() 3 { 4 #ifdef _MSC_VER_Sleep 5 std::thread t(sleep, 2500); 6 t.detach(); 7 #else 8 signal(SIGALRM, SIGALRM_switch); 9 alarm(2500); 10 #endif 11 12 model.clear(); usedClauses.clear(); 13 conflict.clear(); 14 if (!ok) return l_False; 15 16 solves++; 17 18 max_learnts = nClauses() * learntsize_factor; 19 learntsize_adjust_confl = learntsize_adjust_start_confl; 20 learntsize_adjust_cnt = (int)learntsize_adjust_confl; 21 lbool status = l_Undef; 22 23 if (verbosity >= 1){ 24 printf("c ============================[ Search Statistics ]==============================n"); 25 printf("c | Conflicts | ORIGINAL | LEARNT | Progress |n"); 26 printf("c | | Vars Clauses Literals | Limit Clauses Lit/Cl | |n"); 27 printf("c ===============================================================================n"); 28 } 29 30 add_tmp.clear(); 31 32 if (!simplifyOriginalClauses()){ 33 #ifdef BIN_DRUP 34 if (drup_file) binDRUP_flush(drup_file); 35 #endif 36 return l_False; 37 } 38 39 VSIDS = true; 40 int init = 10000; 41 while (status == l_Undef && init > 0 /*&& withinBudget()*/) 42 status = search(init); 43 VSIDS = false; 44 // VSIDS = true; 45 // Search: 46 int curr_restarts = 0; 47 while (status == l_Undef /*&& withinBudget()*/){ 48 if (VSIDS){ 49 int weighted = INT32_MAX; 50 status = search(weighted); 51 }else{ 52 int nof_conflicts = luby(restart_inc, curr_restarts) * restart_first; 53 curr_restarts++; 54 status = search(nof_conflicts); 55 } 56 if (!VSIDS && switch_mode){ 57 VSIDS = true; 58 printf("c Switched to VSIDS.n"); 59 fflush(stdout); 60 picked.clear(); 61 conflicted.clear(); 62 almost_conflicted.clear(); 63 #ifdef ANTI_EXPLORATION 64 canceled.clear(); 65 #endif 66 } 67 } 68 69 if (verbosity >= 1) 70 printf("c ===============================================================================n"); 71 72 printf("c nbReorder: %llu (%llu, %llu, %llu) with Rreorder %4.2lf at start %dn", 73 nbReorder, normalNbReorder, normalGoodNbReorder, goodNbReorder, R_reorder, reorderStart); 74 75 #ifdef BIN_DRUP 76 if (drup_file && status == l_False) binDRUP_flush(drup_file); 77 #endif 78 79 if (status == l_True){ 80 // Extend & copy model: 81 model.growTo(nVars()); 82 for (int i = 0; i < nVars(); i++) model[i] = value(i); 83 }else if (status == l_False && conflict.size() == 0) 84 ok = false; 85 86 cancelUntil(0); 87 88 return status; 89 }
|
1 lbool Solver::search(int& nof_conflicts) 2 { 3 assert(ok); 4 int backtrack_level; 5 int lbd; 6 vec<Lit> learnt_clause; 7 bool cached = false; 8 9 bool firstConfl; 10 int conflictsForReorder; 11 conflictsForReorder=0; firstConfl=true; 12 13 starts++; 14 15 // simplify 16 // 17 if (conflicts >= curSimplify * nbconfbeforesimplify){ 18 nbSimplifyAll++; 19 // printf("c ### simplifyAll %llu on conflict : %lld and restart: %lld and nbReorder: %llu (%llu, %llu, %llu) with Rreorder %4.2lfn", 20 // nbSimplifyAll, conflicts, starts, nbReorder, normalNbReorder, normalGoodNbReorder, goodNbReorder, R_reorder); 21 if (!simplifyAll()){ 22 return l_False; 23 } 24 curSimplify = (conflicts / nbconfbeforesimplify) + 1; 25 nbconfbeforesimplify += incSimplify; 26 } 27 28 for (;;){ 29 CRef confl = propagate(); 30 31 if (confl != CRef_Undef){ 32 // CONFLICT 33 if (VSIDS){ 34 if (--timer == 0 && var_decay < 0.95) timer = 5000, var_decay += 0.01; 35 }else 36 if (step_size > min_step_size) step_size -= step_size_dec; 37 38 conflicts++; nof_conflicts--; 39 if (conflicts == 100000 && learnts_core.size() < 100) core_lbd_cut = 5; 40 if (decisionLevel() == 0) return l_False; 41 42 trailQueue.push(trail.size()); conflictsForReorder++; 43 44 // if (nbReorder < starts/100 && R_reorder > 1.1) R_reorder -= 0.01; 45 46 if (conflicts > 100000 && 47 ((VSIDS && firstConfl) || 48 (!VSIDS && conflictsForReorder > 50 && trail.size() > 2*trailQueue.avg()))) { 49 if (VSIDS) 50 lbd_queue.clear(); 51 else if (nof_conflicts < 50) nof_conflicts = 50; 52 conflictsForReorder = 0; nbReorder++; reorderStart=starts; 53 // if (nbReorder > starts/5 && R_reorder < 5) R_reorder += 0.01; 54 confl = reorderDecisions(confl); 55 firstConfl = false; 56 if (confl == CRef_Undef) 57 continue; 58 } 59 60 learnt_clause.clear(); 61 analyze(confl, learnt_clause, backtrack_level, lbd); 62 cancelUntil(backtrack_level); 63 64 lbd--; 65 if (VSIDS){ 66 cached = false; 67 conflicts_VSIDS++; 68 lbd_queue.push(lbd); 69 global_lbd_sum += (lbd > 50 ? 50 : lbd); } 70 71 if (learnt_clause.size() == 1){ 72 uncheckedEnqueue(learnt_clause[0]); 73 }else{ 74 CRef cr = ca.alloc(learnt_clause, true); 75 ca[cr].set_lbd(lbd); 76 if (lbd <= core_lbd_cut){ 77 learnts_core.push(cr); 78 ca[cr].mark(CORE); 79 }else if (lbd <= 6){ 80 learnts_tier2.push(cr); 81 ca[cr].mark(TIER2); 82 ca[cr].touched() = conflicts; 83 }else{ 84 learnts_local.push(cr); 85 claBumpActivity(ca[cr]); } 86 attachClause(cr); 87 uncheckedEnqueue(learnt_clause[0], cr); 88 } 89 if (drup_file){ 90 #ifdef BIN_DRUP 91 binDRUP('a', learnt_clause, drup_file); 92 #else 93 for (int i = 0; i < learnt_clause.size(); i++) 94 fprintf(drup_file, "%i ", (var(learnt_clause[i]) + 1) * (-2 * sign(learnt_clause[i]) + 1)); 95 fprintf(drup_file, "0n"); 96 #endif 97 } 98 99 if (VSIDS) varDecayActivity(); 100 claDecayActivity(); 101 102 /*if (--learntsize_adjust_cnt == 0){ 103 learntsize_adjust_confl *= learntsize_adjust_inc; 104 learntsize_adjust_cnt = (int)learntsize_adjust_confl; 105 max_learnts *= learntsize_inc; 106 107 if (verbosity >= 1) 108 printf("c | %9d | %7d %8d %8d | %8d %8d %6.0f | %6.3f %% |n", 109 (int)conflicts, 110 (int)dec_vars - (trail_lim.size() == 0 ? trail.size() : trail_lim[0]), nClauses(), (int)clauses_literals, 111 (int)max_learnts, nLearnts(), (double)learnts_literals/nLearnts(), progressEstimate()*100); 112 }*/ 113 114 }else{ 115 // NO CONFLICT 116 bool restart = false; 117 if (!VSIDS) 118 restart = nof_conflicts <= 0; 119 else if (!cached){ 120 restart = lbd_queue.full() && (lbd_queue.avg() * 0.8 > global_lbd_sum / conflicts_VSIDS); 121 cached = true; 122 } 123 if (restart /*|| !withinBudget()*/){ 124 lbd_queue.clear(); 125 cached = false; 126 // Reached bound on number of conflicts: 127 progress_estimate = progressEstimate(); 128 cancelUntil(0); 129 return l_Undef; } 130 131 // Simplify the set of problem clauses: 132 if (decisionLevel() == 0 && !simplify()) 133 return l_False; 134 135 if (conflicts >= next_T2_reduce){ 136 next_T2_reduce = conflicts + 10000; 137 reduceDB_Tier2(); } 138 if (conflicts >= next_L_reduce){ 139 next_L_reduce = conflicts + 15000; 140 reduceDB(); } 141 142 Lit next = lit_Undef; 143 /*while (decisionLevel() < assumptions.size()){ 144 // Perform user provided assumption: 145 Lit p = assumptions[decisionLevel()]; 146 if (value(p) == l_True){ 147 // Dummy decision level: 148 newDecisionLevel(); 149 }else if (value(p) == l_False){ 150 analyzeFinal(~p, conflict); 151 return l_False; 152 }else{ 153 next = p; 154 break; 155 } 156 } 157 158 if (next == lit_Undef)*/{ 159 // New variable decision: 160 decisions++; 161 next = pickBranchLit(); 162 163 if (next == lit_Undef) 164 // Model found: 165 return l_True; 166 } 167 168 // Increase decision level and enqueue 'next' 169 newDecisionLevel(); 170 uncheckedEnqueue(next); 171 } 172 } 173 }
|
原文链接: https://www.cnblogs.com/yuweng1689/p/13205538.html
欢迎关注
微信关注下方公众号，第一时间获取干货硬货；公众号内回复【pdf】免费获取数百本计算机经典书籍;
也有高质量的技术群，里面有嵌入式、搜广推等BAT大佬
原创文章受到原创版权保护。转载请注明出处：https://www.ccppcoding.com/archives/360187
非原创文章文中已经注明原地址，如有侵权，联系删除
关注公众号【高性能架构探索】，第一时间获取最新文章
转载文章受原作者版权保护。转载请注明原作者出处！
