1 #include "internal.hpp"
  2 
  3 namespace CaDiCaL {
  4 
  5 // As observed by Chanseok Oh and implemented in MapleSAT solvers too,
  6 // various mostly satisfiable instances benefit from long quiet phases
 
  7 // with less or almost no restarts.  We implement this idea by prohibiting
  8 // the Glucose style restart scheme in a geometric fashion, which is very
  9 // similar to how originally restarts were scheduled in MiniSAT and earlier
 10 // solvers.  We start with say 1e3 = 1000 (opts.stabilizeinit) conflicts of
 
 11 // Glucose restarts.  Then in a "stabilizing" phase we disable these
 12 // until 1e4 = 2000 conflicts (if 'opts.stabilizefactor' is '200' percent)
 13 // have passed. After that we switch back to regular Glucose style restarts
 14 // until again 2 times more conflicts than the previous limit are reached.
 15
 
 // Actually, in the latest version we still restarts during stabilization
 16 // but only in a reluctant doubling scheme with a rather high interval.

正如Chanseok Oh所觀察到的，並且在MapleSAT求解器中實現的那樣，各種最容易滿足的例項從長時間的靜默階段中獲益，
無需或幾乎無需重新啟動。為了實現這個想法，我們以幾何方式禁止了葡萄糖式重啟方案，
這與最初在MiniSAT和早期求解器中安排重啟的方式非常相似。
我們開始說1e3 = 1000(選項。穩定init)衝突的葡萄糖重新開始。
然後在“穩定”階段我們禁用這些，直到1e4 = 2000衝突(如果選擇的話)。穩定因素是' 200% ')已經通過。
之後，我們又回到正常的葡萄糖模式，直到再次發生比之前的極限多2倍的衝突。
實際上，在最新版本中，我們仍然在穩定期間重新啟動，但只是在一個相當高間隔的勉強加倍方案。

 17 
 18 bool Internal::stabilizing () {
 19   if (!opts.stabilize) return false;
 20   if (stable && opts.stabilizeonly) return true;
 21   if (stats.conflicts >= lim.stabilize) {
 22     report (stable ? ']' : '}');
 23     if (stable) STOP (stable);
 24     else        STOP (unstable);
 25     stable = !stable;
 26     if (stable) stats.stabphases++;
 27     PHASE ("stabilizing", stats.stabphases,
 28       "reached stabilization limit %" PRId64 " after %" PRId64 " conflicts",
 29       lim.stabilize, stats.conflicts);
 30     inc.stabilize *= opts.stabilizefactor*1e-2;
 31     if (inc.stabilize > opts.stabilizemaxint)
 32       inc.stabilize = opts.stabilizemaxint;
 33     lim.stabilize = stats.conflicts + inc.stabilize;
 34     if (lim.stabilize <= stats.conflicts)
 35       lim.stabilize = stats.conflicts + 1;
 36     swap_averages ();
 37     PHASE ("stabilizing", stats.stabphases,
 38       "new stabilization limit %" PRId64 " at conflicts interval %" PRId64 "",
 39       lim.stabilize, inc.stabilize);
 40     report (stable ? '[' : '{');
 41     if (stable) START (stable);
 42     else        START (unstable);
 43   }
 44   return stable;
 45 }
 46 
 47 // Restarts are scheduled by a variant of the Glucose scheme as presented in
 48 // our POS'15 paper using exponential moving averages.  There is a slow
 49 // moving average of the average recent glucose level of learned clauses as
 50 // well as a fast moving average of those glues.  If the end of a base
 51 // restart conflict interval has passed and the fast moving average is above
 52 // a certain margin over the slow moving average then we restart.
     重新啟動計劃的葡萄糖方案的一個變體，在我們的POS'15論文使用指數移動平均。
     有一個學習過的子句近期平均葡萄糖水平的緩慢移動平均值，以及這些膠水的快速移動平均值。
     如果基線重新啟動衝突間隔已經結束，並且快速移動平均線高於慢速移動平均線的一定範圍，
     那麼我們將重新啟動。
 53 
 54 bool Internal::restarting () {
 55   if (!opts.restart) return false;
 56   if ((size_t) level < assumptions.size () + 2) return false;
 57   if (stabilizing ()) return reluctant;
 58   if (stats.conflicts <= lim.restart) return false;
 59   double f = averages.current.glue.fast;
 60   double margin = (100.0 + opts.restartmargin)/100.0;
 61   double s = averages.current.glue.slow, l = margin * s;
 62   LOG ("EMA glue slow %.2f fast %.2f limit %.2f", s, f, l);
 63   return l <= f;
 64 }
 65 
 66 // This is Marijn's reuse trail idea.  Instead of always backtracking to the
 67 // top we figure out which decisions will be made again anyhow and only
 68 // backtrack to the level of the last such decision or to the top if no such
 69 // decision exists top (in which case we do not reuse any level).
 70 
    這是Marijn的再利用路線。我們不總是回溯到頂層，而是找出將再次做出哪些決策，
    並且只回溯到上一個此類決策的級別，或者在頂層不存在此類決策的情況下回溯到頂層
    (在這種情況下，我們不重用任何級別)。
 71 int Internal::reuse_trail () {
 72   if (!opts.restartreusetrail) return assumptions.size ();
 73   int decision = next_decision_variable ();
 74   assert (1 <= decision);
 75   int res = assumptions.size ();
 76   if (use_scores ()) {
 77     while (res < level &&
 78            score_smaller (this)(decision, abs (control[res+1].decision)))
 79       res++;
 80   } else {
 81     int64_t limit = bumped (decision);
 82     while (res < level && bumped (control[res+1].decision) > limit)
 83       res++;
 84   }
 85   int reused = res - assumptions.size ();
 86   if (reused > 0) {
 87     stats.reused++;
 88     stats.reusedlevels += reused;
 89     if (stable) stats.reusedstable++;
 90   }
 91   return res;
 92 }
 93 
 94 void Internal::restart () {
 95   START (restart);
 96   stats.restarts++;
 97   stats.restartlevels += level;
 98   if (stable) stats.restartstable++;
 99   LOG ("restart %" PRId64 "", stats.restarts);
100   backtrack (reuse_trail ());
101 
102   lim.restart = stats.conflicts + opts.restartint;
103   LOG ("new restart limit at %" PRId64 " conflicts", lim.restart);
104 
105   report ('R', 2);
106   STOP (restart);
107 }
108 
109 }