代码分析Maple_CM_ordUP较 Maple_LCM的改进

 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\n", 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, "0\n");
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\n");
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\n",
91 //           nbOriginalClauses_before, clauses.size(), nbShortening, nbShortened, avg);
92 //    printf("c Original clause minimization time: %5.2lfs, number UPs: %llu\n",
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**\n\n", trail_lim.size(), trail.size());
107                 return confl;
108             }
109         }
110     }
111     goodNbReorder++;
112     //printf("\n%d, %d$$\n\n", trail_lim.size(), trail.size());
113     //    printf("$$$$\n\n");
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\n", 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 %d\n",
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\n",
 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\n");
 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 }