最早使用cmt的minisat改进版求解器4——vsids-master-1\adaptvsids

1  int lbd_val = lbd(learnt_clause);       //计算新增学习子句的lbd值
2  lbd_ema = lbd_ema_decay * lbd_ema + (1 - lbd_ema_decay) * lbd_val;//整体LBD的移动平均值
3  if (lbd_val >= lbd_ema) {               //第一种情况
4      decays++;                           //正常普通衰减模式使用次数计数
5      varDecayActivity(var_decay);        //正常模式下var_decay为0.85，变元活跃度碰撞增加较快
6  } else {                                //第二种情况：学习子句lbd低于移动平均
7      thresh_decays++;                    // 学习子句lbd低于移动平均lbd时，单独计数
8      varDecayActivity(var_thresh_decay); //var_thresh_decay为0.95，变元活跃度碰撞增加较慢
9  }

  1 class Solver {
  ...
102     // Statistics: (read-only member variable)
103     //
104     uint64_t solves, starts, decisions, rnd_decisions, propagations, conflicts, backjumps, decays, thresh_decays;
105     uint64_t dec_vars, clauses_literals, learnts_literals, max_literals, tot_literals;
106 
107...
180     long double         lbd_ema;
181     long double         lbd_ema_decay;
...
200     vec<bool>           lbd_seen;
...
207     int      lbd(vec<Lit>& c);
...
243 };

 1 inline int Solver::lbd(vec<Lit>& c) {
 2     int lbd = 0;
 3     for (int i = 0; i < c.size(); i++) {
 4         int lvl = level(var(c[i]));
 5         if (!lbd_seen[lvl]) {
 6             lbd_seen[lvl] = true;
 7             lbd++;
 8         }
 9     }
10     for (int i = 0; i < c.size(); i++) {
11         int lvl = level(var(c[i]));
12         lbd_seen[lvl] = false;
13     }
14     return lbd;
15 }

36 static DoubleOption  opt_lbd_ema_decay 
(_cat, "lbd-ema-decay",    "The lbd decay factor", 0.95,DoubleRange(0, false, 1, false));

 1 Solver::Solver() :
...50   , lbd_ema            (0)
51   , lbd_ema_decay      (opt_lbd_ema_decay)  //取值0.95
52 {}

  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             backjumps += decisionLevel() - backtrack_level;
 19             cancelUntil(backtrack_level);
 20 
 21             if (learnt_clause.size() == 1){
 22                 uncheckedEnqueue(learnt_clause[0]);
 23             }else{
 24                 CRef cr = ca.alloc(learnt_clause, true);
 25                 learnts.push(cr);
 26                 attachClause(cr);
 27                 claBumpActivity(ca[cr]);
 28                 uncheckedEnqueue(learnt_clause[0], cr);
 29             }
 30 
 31             int lbd_val = lbd(learnt_clause);
 32             lbd_ema = lbd_ema_decay * lbd_ema + (1 - lbd_ema_decay) * lbd_val;
 33             if (lbd_val >= lbd_ema) {
 34                 decays++;
 35                 varDecayActivity(var_decay);  //超出移动平均值，正常碰撞衰减因子0.85，活跃度增加块。
 36             } else {
 37                 thresh_decays++;
 38                 varDecayActivity(var_thresh_decay);  //在移动平均值范围内，衰减因子0.99，活跃度增加慢。
 39             }
 40             claDecayActivity();
 41 
 42             if (--learntsize_adjust_cnt == 0){
 43                 learntsize_adjust_confl *= learntsize_adjust_inc;
 44                 learntsize_adjust_cnt    = (int)learntsize_adjust_confl;
 45                 max_learnts             *= learntsize_inc;
 46 
 47                 if (verbosity >= 1)
 48                   ...
 52             }
 53 
 54         }else{
 55             // NO CONFLICT
 56             if (nof_conflicts >= 0 && conflictC >= nof_conflicts || !withinBudget()){
 57                 // Reached bound on number of conflicts:
 58                 progress_estimate = progressEstimate();
 59                 cancelUntil(0);
 60                 return l_Undef; }
 61 
 62             // Simplify the set of problem clauses:
 63             if (decisionLevel() == 0 && !simplify())
 64                 return l_False;
 65 
 66             if (learnts.size()-nAssigns() >= max_learnts)
 67                 // Reduce the set of learnt clauses:
 68                 reduceDB();
 69 
 70             Lit next = lit_Undef;
 71             while (decisionLevel() < assumptions.size()){
 72                 // Perform user provided assumption:
 73                 Lit p = assumptions[decisionLevel()];
 74                 if (value(p) == l_True){
 75                     // Dummy decision level:
 76                     newDecisionLevel();
 77                 }else if (value(p) == l_False){
 78                     analyzeFinal(~p, conflict);
 79                     return l_False;
 80                 }else{
 81                     next = p;
 82                     break;
 83                 }
 84             }
 85 
 86             if (next == lit_Undef){
 87                 // New variable decision:
 88                 decisions++;
 89                 next = pickBranchLit();
 90 
 91                 if (next == lit_Undef)
 92                     // Model found:
 93                     return l_True;
 94             }
 95 
 96             // Increase decision level and enqueue ‘next‘
 97             newDecisionLevel();
 98             uncheckedEnqueue(next);
 99         }
100     }
101 }