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 }
