代码分析Maple_CM_ordUP较 Maple_LCM的改进
Posted yuweng1689
tags:
篇首语：本文由小常识网(cha138.com)小编为大家整理，主要介绍了代码分析Maple_CM_ordUP较 Maple_LCM的改进相关的知识，希望对你有一定的参考价值。
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.
代码分析：
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: %llu ", clauses_literals); 19 // if (clauses.size()> simpLimit) { 20 // printf("c too many original clauses (> %d), no original clause minimization ", 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 ", 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, "0 "); 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, "0 "); 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.2lf ", 91 // nbOriginalClauses_before, clauses.size(), nbShortening, nbShortened, avg); 92 // printf("c Original clause minimization time: %5.2lfs, number UPs: %llu ", 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=== ", 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(" %d, %d** ", trail_lim.size(), trail.size()); 107 return confl; 108 } 109 } 110 } 111 goodNbReorder++; 112 //printf(" %d, %d$$ ", trail_lim.size(), trail.size()); 113 // printf("$$$$ "); 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%d ", 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 **** "); 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 ]============================== "); 25 printf("c | Conflicts | ORIGINAL | LEARNT | Progress | "); 26 printf("c | | Vars Clauses Literals | Limit Clauses Lit/Cl | | "); 27 printf("c =============================================================================== "); 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. "); 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 =============================================================================== "); 71 72 printf("c nbReorder: %llu (%llu, %llu, %llu) with Rreorder %4.2lf at start %d ", 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.2lf ", 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, "0 "); 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 %% | ", 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 }
|
以上是关于代码分析Maple_CM_ordUP较 Maple_LCM的改进的主要内容，如果未能解决你的问题，请参考以下文章