3.Cadical-代码解读restart.cpp

Posted 2020-12-18 yuweng1689

restart.cpp定义了internal类型的几个成员函数：

bool Internal::stabilizing ()

bool Internal::restarting ()

int Internal::reuse_trail ()

void Internal::restart ()

---

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 }

 

---

 

score.cpp

score.hpp

实际上CaDiCal中相同标识.hpp和.cpp之间没有直接的联系。此处的两个问价都与score有关，但不是通常hpp和cpp的关系。

score.cpp	1 #include "internal.hpp" 2 3 namespace CaDiCaL { 4 5 // This initializes variables on the binary ‘scores‘ heap also with 6 // smallest variable index first (thus picked first) and larger indices at 7 // the end. 8 // 这将初始化二进制“分数”堆上的变量，最小的变量索引在前面(因此首先被选中)，较大的索引在最后。 9 void Internal::init_scores (int old_max_var, int new_max_var) { 10 LOG ("initializing EVSIDS scores from %d to %d", 11 old_max_var + 1, new_max_var); 12 for (int i = old_max_var; i < new_max_var; i++) 13 scores.push_back (i + 1); 14 } 15 16 // Shuffle the EVSIDS heap. 17 18 void Internal::shuffle_scores () { 19 if (!opts.shuffle) return; 20 if (!opts.shufflescores) return; 21 assert (!level); 22 stats.shuffled++; 23 LOG ("shuffling scores"); 24 vector<int> shuffle; 25 if (opts.shufflerandom){ 26 scores.erase (); 27 for (int idx = max_var; idx; idx--) 28 shuffle.push_back (idx); 29 Random random (opts.seed); // global seed 30 random += stats.shuffled; // different every time 31 for (int i = 0; i <= max_var-2; i++) { 32 const int j = random.pick_int (i, max_var-1); 33 swap (shuffle[i], shuffle[j]); 34 } 35 } else { 36 while (!scores.empty ()) { 37 int idx = scores.front (); 38 (void) scores.pop_front (); 39 shuffle.push_back (idx); 40 } 41 } 42 score_inc = 0; 43 for (const auto & idx : shuffle) { 44 stab[idx] = score_inc++; 45 scores.push_back (idx); 46 } 47 } 48 49 }
score.hpp	1 #ifndef _score_hpp_INCLUDED 2 #define _score_hpp_INCLUDED 3 4 namespace CaDiCaL { 5 6 struct score_smaller { 7 Internal * internal; 8 score_smaller (Internal * i) : internal (i) { } 9 bool operator () (unsigned a, unsigned b); 10 }; 11 12 typedef heap<score_smaller> ScoreSchedule; 13 14 } 15 16 #endif