1 //
2 // Copyright (c) 2006-2017 Benjamin Kaufmann
3 //
4 // This file is part of Clasp. See http://www.cs.uni-potsdam.de/clasp/
5 //
6 // Permission is hereby granted, free of charge, to any person obtaining a copy
7 // of this software and associated documentation files (the "Software"), to
8 // deal in the Software without restriction, including without limitation the
9 // rights to use, copy, modify, merge, publish, distribute, sublicense, and/or
10 // sell copies of the Software, and to permit persons to whom the Software is
11 // furnished to do so, subject to the following conditions:
12 //
13 // The above copyright notice and this permission notice shall be included in
14 // all copies or substantial portions of the Software.
15 //
16 // THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
17 // IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
18 // FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
19 // AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
20 // LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING
21 // FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS
22 // IN THE SOFTWARE.
23 //
24 #include <clasp/heuristics.h>
25 #include <clasp/clause.h>
26 #include <potassco/basic_types.h>
27 #include <algorithm>
28 #include <limits>
29 #include <cstdlib>
30 #include <string>
31 #include <utility>
32 #include <cmath>
33 namespace Clasp {
34 /////////////////////////////////////////////////////////////////////////////////////////
35 // Lookback selection strategies
36 /////////////////////////////////////////////////////////////////////////////////////////
momsScore(const Solver & s,Var v)37 uint32 momsScore(const Solver& s, Var v) {
38 uint32 sc;
39 if (s.sharedContext()->numBinary()) {
40 uint32 s1 = s.estimateBCP(posLit(v), 0) - 1;
41 uint32 s2 = s.estimateBCP(negLit(v), 0) - 1;
42 sc = ((s1 * s2)<<10) + (s1 + s2);
43 }
44 else {
45 // problem does not contain binary constraints - fall back to counting watches
46 uint32 s1 = s.numWatches(posLit(v));
47 uint32 s2 = s.numWatches(negLit(v));
48 sc = ((s1 * s2)<<10) + (s1 + s2);
49 }
50 return sc;
51 }
addOther(TypeSet & t,uint32 other)52 static void addOther(TypeSet& t, uint32 other) {
53 if (other != HeuParams::other_no) { t.addSet(Constraint_t::Loop); }
54 if (other == HeuParams::other_all) { t.addSet(Constraint_t::Other); }
55 }
56 /////////////////////////////////////////////////////////////////////////////////////////
57 // Berkmin selection strategy
58 /////////////////////////////////////////////////////////////////////////////////////////
59 #define BERK_NUM_CANDIDATES 5
60 #define BERK_CACHE_GROW 2.0
61 #define BERK_MAX_MOMS_VARS 9999
62 #define BERK_MAX_MOMS_DECS 50
63 #define BERK_MAX_DECAY 65534
64
ClaspBerkmin(const HeuParams & params)65 ClaspBerkmin::ClaspBerkmin(const HeuParams& params)
66 : topConflict_(UINT32_MAX)
67 , topOther_(UINT32_MAX)
68 , front_(1)
69 , cacheSize_(5)
70 , numVsids_(0) {
71 ClaspBerkmin::setConfig(params);
72 }
73
setConfig(const HeuParams & params)74 void ClaspBerkmin::setConfig(const HeuParams& params) {
75 maxBerkmin_ = params.param == 0 ? UINT32_MAX : params.param;
76 order_.nant = params.nant != 0;
77 order_.huang = params.huang != 0;
78 order_.resScore = params.score == HeuParams::score_auto ? static_cast<uint32>(HeuParams::score_multi_set) : params.score;
79 addOther(types_ = TypeSet(), params.other);
80 if (params.moms) { types_.addSet(Constraint_t::Static); }
81 }
82
getMostActiveFreeVar(const Solver & s)83 Var ClaspBerkmin::getMostActiveFreeVar(const Solver& s) {
84 ++numVsids_;
85 // first: check for a cache hit
86 for (Pos end = cache_.end(); cacheFront_ != end; ++cacheFront_) {
87 if (s.value(*cacheFront_) == value_free) {
88 return *cacheFront_;
89 }
90 }
91 // Second: cache miss - refill cache with most active vars
92 if (!cache_.empty() && cacheSize_ < s.numFreeVars()/10) {
93 cacheSize_ = static_cast<uint32>( (cacheSize_*BERK_CACHE_GROW) + .5 );
94 }
95 cache_.clear();
96 Order::Compare comp(&order_);
97 // Pre: At least one unassigned var!
98 for (; s.value( front_ ) != value_free; ++front_) {;}
99 Var v = front_;
100 LitVec::size_type cs = std::min(cacheSize_, s.numFreeVars());
101 for (;;) { // add first cs free variables to cache
102 cache_.push_back(v);
103 std::push_heap(cache_.begin(), cache_.end(), comp);
104 if (cache_.size() == cs) break;
105 while ( s.value(++v) != value_free ) {;} // skip over assigned vars
106 }
107 for (v = (cs == cacheSize_ ? v+1 : s.numVars()+1); v <= s.numVars(); ++v) {
108 // replace vars with low activity
109 if (s.value(v) == value_free && comp(v, cache_[0])) {
110 std::pop_heap(cache_.begin(), cache_.end(), comp);
111 cache_.back() = v;
112 std::push_heap(cache_.begin(), cache_.end(), comp);
113 }
114 }
115 std::sort_heap(cache_.begin(), cache_.end(), comp);
116 return *(cacheFront_ = cache_.begin());
117 }
118
getTopMoms(const Solver & s)119 Var ClaspBerkmin::getTopMoms(const Solver& s) {
120 // Pre: At least one unassigned var!
121 for (; s.value( front_ ) != value_free; ++front_) {;}
122 Var var = front_;
123 uint32 ms = momsScore(s, var);
124 uint32 ls = 0;
125 for (Var v = var+1; v <= s.numProblemVars(); ++v) {
126 if (s.value(v) == value_free && (ls = momsScore(s, v)) > ms) {
127 var = v;
128 ms = ls;
129 }
130 }
131 if (++numVsids_ >= BERK_MAX_MOMS_DECS || ms < 2) {
132 // Scores are not relevant or too many moms-based decisions
133 // - disable MOMS
134 hasActivities(true);
135 }
136 return var;
137 }
138
startInit(const Solver & s)139 void ClaspBerkmin::startInit(const Solver& s) {
140 if (order_.score.empty()) {
141 rng_.srand(s.rng.seed());
142 }
143 order_.score.resize(s.numVars()+1);
144 initHuang(order_.huang);
145
146 cache_.clear();
147 cacheSize_ = 5;
148 cacheFront_ = cache_.end();
149
150 freeLits_.clear();
151 freeOtherLits_.clear();
152 topConflict_ = topOther_ = (uint32)-1;
153
154 front_ = 1;
155 numVsids_ = 0;
156 }
157
endInit(Solver & s)158 void ClaspBerkmin::endInit(Solver& s) {
159 if (initHuang()) {
160 const bool clearScore = types_.inSet(Constraint_t::Static);
161 // initialize preferred values of vars
162 cache_.clear();
163 for (Var v = 1; v <= s.numVars(); ++v) {
164 order_.decayedScore(v);
165 if (order_.occ(v) != 0 && s.pref(v).get(ValueSet::saved_value) == value_free) {
166 s.setPref(v, ValueSet::saved_value, order_.occ(v) > 0 ? value_true : value_false);
167 }
168 if (clearScore) order_.score[v] = HScore(order_.decay);
169 else cache_.push_back(v);
170 }
171 initHuang(false);
172 }
173 if (!types_.inSet(Constraint_t::Static) || s.numFreeVars() > BERK_MAX_MOMS_VARS) {
174 hasActivities(true);
175 }
176 std::stable_sort(cache_.begin(), cache_.end(), Order::Compare(&order_));
177 cacheFront_ = cache_.begin();
178 }
179
updateVar(const Solver & s,Var v,uint32 n)180 void ClaspBerkmin::updateVar(const Solver& s, Var v, uint32 n) {
181 if (s.validVar(v)) { growVecTo(order_.score, v+n); }
182 front_ = 1;
183 cache_.clear();
184 cacheFront_ = cache_.end();
185 }
186
newConstraint(const Solver & s,const Literal * first,LitVec::size_type size,ConstraintType t)187 void ClaspBerkmin::newConstraint(const Solver& s, const Literal* first, LitVec::size_type size, ConstraintType t) {
188 if (t == Constraint_t::Conflict) { hasActivities(true); }
189 if ((t == Constraint_t::Conflict && order_.resScore == HeuParams::score_min)
190 || (t == Constraint_t::Static && order_.huang)) {
191 for (const Literal* x = first, *end = first+size; x != end; ++x) {
192 order_.inc(*x, s.varInfo(x->var()).nant());
193 }
194 }
195 if (t != Constraint_t::Static && !order_.huang) {
196 for (const Literal* x = first, *end = first+size; x != end; ++x) { order_.incOcc(*x); }
197 }
198 }
199
updateReason(const Solver & s,const LitVec & lits,Literal r)200 void ClaspBerkmin::updateReason(const Solver& s, const LitVec& lits, Literal r) {
201 if (order_.resScore > HeuParams::score_min) {
202 const bool ms = order_.resScore == HeuParams::score_multi_set;
203 for (LitVec::size_type i = 0, e = lits.size(); i != e; ++i) {
204 if (ms || !s.seen(lits[i])) { order_.inc(~lits[i], s.varInfo(lits[i].var()).nant()); }
205 }
206 }
207 if ((order_.resScore & 1u) != 0 && !isSentinel(r)) {
208 order_.inc(r, s.varInfo(r.var()).nant());
209 }
210 }
211
bump(const Solver & s,const WeightLitVec & lits,double adj)212 bool ClaspBerkmin::bump(const Solver& s, const WeightLitVec& lits, double adj) {
213 for (WeightLitVec::const_iterator it = lits.begin(), end = lits.end(); it != end; ++it) {
214 if (!order_.nant || s.varInfo(it->first.var()).nant()) {
215 uint32 xf = order_.decayedScore(it->first.var()) + static_cast<weight_t>(it->second*adj);
216 order_.score[it->first.var()].act = (uint16)std::min(xf, UINT32_MAX>>16);
217 }
218 }
219 return true;
220 }
221
undoUntil(const Solver &,LitVec::size_type)222 void ClaspBerkmin::undoUntil(const Solver&, LitVec::size_type) {
223 topConflict_ = topOther_ = static_cast<uint32>(-1);
224 front_ = 1;
225 cache_.clear();
226 cacheFront_ = cache_.end();
227 if (cacheSize_ > 5 && numVsids_ > 0 && (numVsids_*3) < cacheSize_) {
228 cacheSize_ = static_cast<uint32>(cacheSize_/BERK_CACHE_GROW);
229 }
230 numVsids_ = 0;
231 }
232
hasTopUnsat(Solver & s)233 bool ClaspBerkmin::hasTopUnsat(Solver& s) {
234 topConflict_ = std::min(s.numLearntConstraints(), topConflict_);
235 topOther_ = std::min(s.numLearntConstraints(), topOther_);
236 assert(topConflict_ <= topOther_);
237 freeOtherLits_.clear();
238 freeLits_.clear();
239 TypeSet ts = types_;
240 if (ts.m > 1) {
241 while (topOther_ > topConflict_) {
242 if (s.getLearnt(topOther_-1).isOpen(s, ts, freeLits_) != 0) {
243 freeLits_.swap(freeOtherLits_);
244 ts.m = 0;
245 break;
246 }
247 --topOther_;
248 freeLits_.clear();
249 }
250 }
251 ts.addSet(Constraint_t::Conflict);
252 uint32 stopAt = topConflict_ < maxBerkmin_ ? 0 : topConflict_ - maxBerkmin_;
253 while (topConflict_ != stopAt) {
254 uint32 x = s.getLearnt(topConflict_-1).isOpen(s, ts, freeLits_);
255 if (x != 0) {
256 if (x == Constraint_t::Conflict) { break; }
257 topOther_ = topConflict_;
258 freeLits_.swap(freeOtherLits_);
259 ts.m = 0;
260 ts.addSet(Constraint_t::Conflict);
261 }
262 --topConflict_;
263 freeLits_.clear();
264 }
265 if (freeOtherLits_.empty()) topOther_ = topConflict_;
266 if (freeLits_.empty()) freeOtherLits_.swap(freeLits_);
267 return !freeLits_.empty();
268 }
269
doSelect(Solver & s)270 Literal ClaspBerkmin::doSelect(Solver& s) {
271 const uint32 decayMask = order_.huang ? 127 : 511;
272 if ( ((s.stats.choices + 1)&decayMask) == 0 ) {
273 if ((order_.decay += (1+!order_.huang)) == BERK_MAX_DECAY) {
274 order_.resetDecay();
275 }
276 }
277 if (hasTopUnsat(s)) { // Berkmin based decision
278 assert(!freeLits_.empty());
279 Literal x = selectRange(s, &freeLits_[0], &freeLits_[0]+freeLits_.size());
280 return selectLiteral(s, x.var(), false);
281 }
282 else if (hasActivities()) { // Vsids based decision
283 return selectLiteral(s, getMostActiveFreeVar(s), true);
284 }
285 else { // Moms based decision
286 return selectLiteral(s, getTopMoms(s), true);
287 }
288 }
289
selectRange(Solver & s,const Literal * first,const Literal * last)290 Literal ClaspBerkmin::selectRange(Solver& s, const Literal* first, const Literal* last) {
291 Literal candidates[BERK_NUM_CANDIDATES];
292 candidates[0] = *first;
293 uint32 c = 1;
294 uint32 ms = static_cast<uint32>(-1);
295 uint32 ls = 0;
296 for (++first; first != last; ++first) {
297 Var v = first->var();
298 assert(s.value(v) == value_free);
299 int cmp = order_.compare(v, candidates[0].var());
300 if (cmp > 0) {
301 candidates[0] = *first;
302 c = 1;
303 ms = static_cast<uint32>(-1);
304 }
305 else if (cmp == 0) {
306 if (ms == static_cast<uint32>(-1)) ms = momsScore(s, candidates[0].var());
307 if ( (ls = momsScore(s,v)) > ms) {
308 candidates[0] = *first;
309 c = 1;
310 ms = ls;
311 }
312 else if (ls == ms && c != BERK_NUM_CANDIDATES) {
313 candidates[c++] = *first;
314 }
315 }
316 }
317 return c == 1 ? candidates[0] : candidates[rng_.irand(c)];
318 }
319
selectLiteral(Solver & s,Var v,bool vsids) const320 Literal ClaspBerkmin::selectLiteral(Solver& s, Var v, bool vsids) const {
321 ValueSet pref = s.pref(v);
322 int signScore = order_.occ(v);
323 if (order_.huang && std::abs(signScore) > 32 && !pref.has(ValueSet::user_value)) {
324 return Literal(v, signScore < 0);
325 }
326 // compute expensive sign score only if necessary
327 if (vsids && !pref.has(ValueSet::user_value | ValueSet::pref_value | ValueSet::saved_value)) {
328 int32 w0 = (int32)s.estimateBCP(posLit(v), 5);
329 int32 w1 = (int32)s.estimateBCP(negLit(v), 5);
330 if (w1 != 1 || w0 != w1) { signScore = w0 - w1; }
331 }
332 return DecisionHeuristic::selectLiteral(s, v, signScore);
333 }
334
resetDecay()335 void ClaspBerkmin::Order::resetDecay() {
336 for (Scores::size_type i = 1, end = score.size(); i < end; ++i) {
337 decayedScore(i);
338 score[i].dec = 0;
339 }
340 decay = 0;
341 }
342 /////////////////////////////////////////////////////////////////////////////////////////
343 // ClaspVmtf selection strategy
344 /////////////////////////////////////////////////////////////////////////////////////////
ClaspVmtf(const HeuParams & params)345 ClaspVmtf::ClaspVmtf(const HeuParams& params) : decay_(0) {
346 ClaspVmtf::setConfig(params);
347 }
348
setConfig(const HeuParams & params)349 void ClaspVmtf::setConfig(const HeuParams& params) {
350 nMove_ = params.param ? std::max(params.param, uint32(2)) : 8u;
351 scType_ = params.score != HeuParams::score_auto ? params.score : static_cast<uint32>(HeuParams::score_min);
352 nant_ = params.nant != 0;
353 addOther(types_ = TypeSet(), params.other != HeuParams::other_auto ? params.other : static_cast<uint32>(HeuParams::other_no));
354 if (params.moms) { types_.addSet(Constraint_t::Static); }
355 if (scType_ == HeuParams::score_min) { types_.addSet(Constraint_t::Conflict); }
356 }
357
startInit(const Solver & s)358 void ClaspVmtf::startInit(const Solver& s) {
359 score_.resize(s.numVars()+1, VarInfo(vars_.end()));
360 }
361
endInit(Solver & s)362 void ClaspVmtf::endInit(Solver& s) {
363 bool moms = types_.inSet(Constraint_t::Static);
364 for (Var v = 1; v <= s.numVars(); ++v) {
365 if (s.value(v) == value_free && score_[v].pos_ == vars_.end()) {
366 score_[v].activity(decay_);
367 if (moms) {
368 score_[v].activity_ = momsScore(s, v);
369 score_[v].decay_ = decay_+1;
370 }
371 score_[v].pos_ = vars_.insert(vars_.end(), v);
372 }
373 }
374 if (moms) {
375 vars_.sort(LessLevel(s, score_));
376 for (VarList::iterator it = vars_.begin(), end = vars_.end(); it != end; ++it) {
377 if (score_[*it].decay_ != decay_) {
378 score_[*it].activity_ = 0;
379 score_[*it].decay_ = decay_;
380 }
381 }
382 }
383 front_ = vars_.begin();
384 }
385
updateVar(const Solver & s,Var v,uint32 n)386 void ClaspVmtf::updateVar(const Solver& s, Var v, uint32 n) {
387 if (s.validVar(v)) {
388 growVecTo(score_, v+n, VarInfo(vars_.end()));
389 for (uint32 end = v+n; v != end; ++v) {
390 if (score_[v].pos_ == vars_.end()) { score_[v].pos_ = vars_.insert(vars_.end(), v); }
391 else { front_ = vars_.begin(); }
392 }
393 }
394 else if (v < score_.size()) {
395 if ((v + n) > score_.size()) { n = score_.size() - v; }
396 for (uint32 x = v + n; x-- != v; ) {
397 if (score_[x].pos_ != vars_.end()) {
398 vars_.erase(score_[x].pos_);
399 score_[x].pos_ = vars_.end();
400 }
401 }
402 }
403 }
404
simplify(const Solver & s,LitVec::size_type i)405 void ClaspVmtf::simplify(const Solver& s, LitVec::size_type i) {
406 for (; i < s.numAssignedVars(); ++i) {
407 if (score_[s.trail()[i].var()].pos_ != vars_.end()) {
408 vars_.erase(score_[s.trail()[i].var()].pos_);
409 score_[s.trail()[i].var()].pos_ = vars_.end();
410 }
411 }
412 front_ = vars_.begin();
413 }
414
newConstraint(const Solver & s,const Literal * first,LitVec::size_type size,ConstraintType t)415 void ClaspVmtf::newConstraint(const Solver& s, const Literal* first, LitVec::size_type size, ConstraintType t) {
416 if (t != Constraint_t::Static) {
417 LessLevel comp(s, score_);
418 const bool upAct = types_.inSet(t);
419 const VarVec::size_type mtf = t == Constraint_t::Conflict ? nMove_ : (nMove_*uint32(upAct))/2;
420 for (LitVec::size_type i = 0; i < size; ++i, ++first) {
421 Var v = first->var();
422 score_[v].occ_ += 1 - (((int)first->sign())<<1);
423 if (upAct) { ++score_[v].activity(decay_); }
424 if (mtf && (!nant_ || s.varInfo(v).nant())){
425 if (mtf_.size() < mtf) {
426 mtf_.push_back(v);
427 std::push_heap(mtf_.begin(), mtf_.end(), comp);
428 }
429 else if (comp(v, mtf_[0])) {
430 assert(s.level(v) <= s.level(mtf_[0]));
431 std::pop_heap(mtf_.begin(), mtf_.end(), comp);
432 mtf_.back() = v;
433 std::push_heap(mtf_.begin(), mtf_.end(), comp);
434 }
435 }
436 }
437 for (VarVec::size_type i = 0; i != mtf_.size(); ++i) {
438 Var v = mtf_[i];
439 if (score_[v].pos_ != vars_.end()) {
440 vars_.splice(vars_.begin(), vars_, score_[v].pos_);
441 }
442 }
443 mtf_.clear();
444 front_ = vars_.begin();
445 }
446 }
447
undoUntil(const Solver &,LitVec::size_type)448 void ClaspVmtf::undoUntil(const Solver&, LitVec::size_type) {
449 front_ = vars_.begin();
450 }
451
updateReason(const Solver & s,const LitVec & lits,Literal r)452 void ClaspVmtf::updateReason(const Solver& s, const LitVec& lits, Literal r) {
453 if (scType_ > HeuParams::score_min) {
454 const bool ms = scType_ == HeuParams::score_multi_set;
455 const uint32 D = decay_;
456 for (LitVec::size_type i = 0, e = lits.size(); i != e; ++i) {
457 if (ms || !s.seen(lits[i])) { ++score_[lits[i].var()].activity(D); }
458 }
459 }
460 if (scType_ & 1u) { ++score_[r.var()].activity(decay_); }
461 }
462
bump(const Solver &,const WeightLitVec & lits,double adj)463 bool ClaspVmtf::bump(const Solver&, const WeightLitVec& lits, double adj) {
464 for (WeightLitVec::const_iterator it = lits.begin(), end = lits.end(); it != end; ++it) {
465 score_[it->first.var()].activity(decay_) += static_cast<uint32>(it->second*adj);
466 }
467 return true;
468 }
469
doSelect(Solver & s)470 Literal ClaspVmtf::doSelect(Solver& s) {
471 decay_ += ((s.stats.choices + 1) & 511) == 0;
472 for (; s.value(*front_) != value_free; ++front_) {;}
473 Literal c;
474 if (s.numFreeVars() > 1) {
475 VarList::iterator v2 = front_;
476 uint32 distance = 0;
477 do {
478 ++v2;
479 ++distance;
480 } while (s.value(*v2) != value_free);
481 c = (score_[*front_].activity(decay_) + (distance<<1)+ 3) > score_[*v2].activity(decay_)
482 ? selectLiteral(s, *front_, score_[*front_].occ_)
483 : selectLiteral(s, *v2, score_[*v2].occ_);
484 }
485 else {
486 c = selectLiteral(s, *front_, score_[*front_].occ_);
487 }
488 return c;
489 }
490
selectRange(Solver &,const Literal * first,const Literal * last)491 Literal ClaspVmtf::selectRange(Solver&, const Literal* first, const Literal* last) {
492 Literal best = *first;
493 for (++first; first != last; ++first) {
494 if (score_[first->var()].activity(decay_) > score_[best.var()].activity(decay_)) {
495 best = *first;
496 }
497 }
498 return best;
499 }
500
501 /////////////////////////////////////////////////////////////////////////////////////////
502 // ClaspVsids selection strategy
503 /////////////////////////////////////////////////////////////////////////////////////////
initDecay(uint32 p)504 static double initDecay(uint32 p) {
505 double m = static_cast<double>(p ? p : 0.95);
506 while (m > 1.0) { m /= 10.0; }
507 return m;
508 }
509
510 template <class ScoreType>
ClaspVsids_t(const HeuParams & params)511 ClaspVsids_t<ScoreType>::ClaspVsids_t(const HeuParams& params)
512 : vars_(CmpScore(score_))
513 , inc_(1.0)
514 , acids_(false) {
515 ClaspVsids_t<ScoreType>::setConfig(params);
516 }
517
518 template <class ScoreType>
setConfig(const HeuParams & params)519 void ClaspVsids_t<ScoreType>::setConfig(const HeuParams& params) {
520 addOther(types_ = TypeSet(), params.other != HeuParams::other_auto ? params.other : static_cast<uint32>(HeuParams::other_no));
521 scType_ = params.score != HeuParams::score_auto ? params.score : static_cast<uint32>(HeuParams::score_min);
522 decay_ = Decay(params.decay.init ? initDecay(params.decay.init) : 0.0, initDecay(params.param), params.decay.bump, params.decay.freq);
523 acids_ = params.acids != 0;
524 nant_ = params.nant != 0;
525 if (params.moms) { types_.addSet(Constraint_t::Static); }
526 if (scType_ == HeuParams::score_min) { types_.addSet(Constraint_t::Conflict); }
527 }
528
529 template <class ScoreType>
startInit(const Solver & s)530 void ClaspVsids_t<ScoreType>::startInit(const Solver& s) {
531 score_.resize(s.numVars()+1);
532 occ_.resize(s.numVars()+1);
533 vars_.reserve(s.numVars() + 1);
534 }
535
536 template <class ScoreType>
endInit(Solver & s)537 void ClaspVsids_t<ScoreType>::endInit(Solver& s) {
538 vars_.clear();
539 initScores(s, types_.inSet(Constraint_t::Static));
540 double mx = 0;
541 for (Var v = 1; v <= s.numVars(); ++v) {
542 if (s.value(v) != value_free) { continue; }
543 mx = std::max(mx, score_[v].get());
544 if (!vars_.is_in_queue(v)) { vars_.push(v); }
545 }
546 if (acids_ && mx > inc_) {
547 inc_ = std::ceil(mx);
548 }
549 }
550 template <class ScoreType>
updateVarActivity(const Solver & s,Var v,double f)551 void ClaspVsids_t<ScoreType>::updateVarActivity(const Solver& s, Var v, double f) {
552 if (!nant_ || s.varInfo(v).nant()) {
553 double o = score_[v].get(), n;
554 f = ScoreType::applyFactor(score_, v, f);
555 if (!acids_) { n = o + (f * inc_); }
556 else if (f == 1.0) { n = (o + inc_) / 2.0; }
557 else if (f != 0.0) { n = std::max( (o + inc_ + f) / 2.0, f + o ); }
558 else { return; }
559 score_[v].set(n);
560 if (n > 1e100) { normalize(); }
561 if (vars_.is_in_queue(v)) {
562 if (n >= o) { vars_.increase(v); }
563 else { vars_.decrease(v); }
564 }
565 }
566 }
567 template <class ScoreType>
updateVar(const Solver & s,Var v,uint32 n)568 void ClaspVsids_t<ScoreType>::updateVar(const Solver& s, Var v, uint32 n) {
569 if (s.validVar(v)) {
570 growVecTo(score_, v+n);
571 growVecTo(occ_, v+n);
572 for (uint32 end = v+n; v != end; ++v) { vars_.update(v); }
573 }
574 else {
575 for (uint32 end = v+n; v != end; ++v) { vars_.remove(v); }
576 }
577 }
578 template <class ScoreType>
initScores(Solver & s,bool moms)579 void ClaspVsids_t<ScoreType>::initScores(Solver& s, bool moms) {
580 if (!moms) { return; }
581 double maxS = 0.0, ms;
582 for (Var v = 1; v <= s.numVars(); ++v) {
583 if (s.value(v) == value_free && score_[v].get() == 0.0 && (ms = (double)momsScore(s, v)) != 0.0) {
584 maxS = std::max(maxS, ms);
585 score_[v].set(-ms);
586 }
587 }
588 for (Var v = 1; v <= s.numVars(); ++v) {
589 double d = score_[v].get();
590 if (d < 0) {
591 d *= -1.0;
592 d /= maxS;
593 score_[v].set(d);
594 }
595 }
596 }
597 template <class ScoreType>
simplify(const Solver & s,LitVec::size_type i)598 void ClaspVsids_t<ScoreType>::simplify(const Solver& s, LitVec::size_type i) {
599 for (; i < s.numAssignedVars(); ++i) {
600 vars_.remove(s.trail()[i].var());
601 }
602 }
603
604 template <class ScoreType>
normalize()605 void ClaspVsids_t<ScoreType>::normalize() {
606 const double min = std::numeric_limits<double>::min();
607 const double minD = min * 1e100;
608 inc_ *= 1e-100;
609 for (LitVec::size_type i = 0; i != score_.size(); ++i) {
610 double d = score_[i].get();
611 if (d > 0) {
612 // keep relative ordering but
613 // actively avoid denormals
614 d += minD;
615 d *= 1e-100;
616 }
617 score_[i].set(d);
618 }
619 }
620 template <class ScoreType>
newConstraint(const Solver & s,const Literal * first,LitVec::size_type size,ConstraintType t)621 void ClaspVsids_t<ScoreType>::newConstraint(const Solver& s, const Literal* first, LitVec::size_type size, ConstraintType t) {
622 if (t != Constraint_t::Static) {
623 const bool upAct = types_.inSet(t);
624 for (LitVec::size_type i = 0; i < size; ++i, ++first) {
625 incOcc(*first);
626 if (upAct) {
627 updateVarActivity(s, first->var());
628 }
629 }
630 if (t == Constraint_t::Conflict) {
631 if (decay_.next && --decay_.next == 0 && decay_.lo < decay_.hi) {
632 decay_.lo += decay_.bump / 100.0;
633 decay_.next = decay_.freq;
634 decay_.df = 1.0 / decay_.lo;
635 }
636 if (!acids_) { inc_ *= decay_.df; }
637 else { inc_ += 1.0; }
638 }
639 }
640 }
641 template <class ScoreType>
updateReason(const Solver & s,const LitVec & lits,Literal r)642 void ClaspVsids_t<ScoreType>::updateReason(const Solver& s, const LitVec& lits, Literal r) {
643 if (scType_ > HeuParams::score_min) {
644 const bool ms = scType_ == HeuParams::score_multi_set;
645 for (LitVec::size_type i = 0, end = lits.size(); i != end; ++i) {
646 if (ms || !s.seen(lits[i])) { updateVarActivity(s, lits[i].var()); }
647 }
648 }
649 if ((scType_ & 1u) != 0 && r.var() != 0) { updateVarActivity(s, r.var()); }
650 }
651 template <class ScoreType>
bump(const Solver & s,const WeightLitVec & lits,double adj)652 bool ClaspVsids_t<ScoreType>::bump(const Solver& s, const WeightLitVec& lits, double adj) {
653 double mf = 1.0, f;
654 for (WeightLitVec::const_iterator it = lits.begin(), end = lits.end(); it != end; ++it) {
655 updateVarActivity(s, it->first.var(), (f = it->second*adj));
656 if (acids_ && f > mf) { mf = f; }
657 }
658 if (acids_ && mf > 1.0) {
659 inc_ = std::ceil(mf + inc_);
660 }
661 return true;
662 }
663 template <class ScoreType>
undoUntil(const Solver & s,LitVec::size_type st)664 void ClaspVsids_t<ScoreType>::undoUntil(const Solver& s , LitVec::size_type st) {
665 const LitVec& a = s.trail();
666 for (; st < a.size(); ++st) {
667 if (!vars_.is_in_queue(a[st].var())) {
668 vars_.push(a[st].var());
669 }
670 }
671 }
672 template <class ScoreType>
doSelect(Solver & s)673 Literal ClaspVsids_t<ScoreType>::doSelect(Solver& s) {
674 while ( s.value(vars_.top()) != value_free ) {
675 vars_.pop();
676 }
677 return selectLiteral(s, vars_.top(), occ(vars_.top()));
678 }
679 template <class ScoreType>
selectRange(Solver &,const Literal * first,const Literal * last)680 Literal ClaspVsids_t<ScoreType>::selectRange(Solver&, const Literal* first, const Literal* last) {
681 Literal best = *first;
682 for (++first; first != last; ++first) {
683 if (vars_.key_compare()(first->var(), best.var())) {
684 best = *first;
685 }
686 }
687 return best;
688 }
689 template class ClaspVsids_t<VsidsScore>;
690
691 /////////////////////////////////////////////////////////////////////////////////////////
692 // DomainHeuristic selection strategy
693 /////////////////////////////////////////////////////////////////////////////////////////
DomainHeuristic(const HeuParams & params)694 DomainHeuristic::DomainHeuristic(const HeuParams& params) : ClaspVsids_t<DomScore>(params), domSeen_(0), defMax_(0), defMod_(0), defPref_(0) {
695 frames_.push_back(Frame(0,DomAction::UNDO_NIL));
696 setDefaultMod(static_cast<HeuParams::DomMod>(params.domMod), params.domPref);
697 }
~DomainHeuristic()698 DomainHeuristic::~DomainHeuristic() {}
699
setConfig(const HeuParams & params)700 void DomainHeuristic::setConfig(const HeuParams& params) {
701 ClaspVsids_t<DomScore>::setConfig(params);
702 setDefaultMod(static_cast<HeuParams::DomMod>(params.domMod), params.domPref);
703 }
setDefaultMod(HeuParams::DomMod mod,uint32 prefSet)704 void DomainHeuristic::setDefaultMod(HeuParams::DomMod mod, uint32 prefSet) {
705 defMod_ = (uint16)mod;
706 defPref_= prefSet;
707 }
detach(Solver & s)708 void DomainHeuristic::detach(Solver& s) {
709 if (!actions_.empty()) {
710 for (DomainTable::iterator it = s.sharedContext()->heuristic.begin(), end = s.sharedContext()->heuristic.end(); it != end; ++it) {
711 if (it->hasCondition()) {
712 s.removeWatch(it->cond(), this);
713 }
714 }
715 }
716 while (frames_.back().dl != 0) {
717 s.removeUndoWatch(frames_.back().dl, this);
718 frames_.pop_back();
719 }
720 Var end = std::min(static_cast<Var>(score_.size()), static_cast<Var>(s.numVars() + 1));
721 for (Var v = 0; v != end; ++v) {
722 if (score_[v].sign) { s.setPref(v, ValueSet::user_value, value_free); }
723 }
724 actions_.clear();
725 prios_.clear();
726 domSeen_ = 0;
727 defMax_ = 0;
728 }
startInit(const Solver & s)729 void DomainHeuristic::startInit(const Solver& s) {
730 BaseType::startInit(s);
731 domSeen_ = std::min(domSeen_, s.sharedContext()->heuristic.size());
732 }
initScores(Solver & s,bool moms)733 void DomainHeuristic::initScores(Solver& s, bool moms) {
734 const DomainTable& domTab = s.sharedContext()->heuristic;
735 BaseType::initScores(s, moms);
736 uint32 nKey = (uint32)prios_.size();
737 if (defMax_) {
738 defMax_ = std::min(defMax_, s.numVars()) + 1;
739 for (Var v = 1; v != defMax_; ++v) {
740 if (score_[v].domP >= nKey) {
741 bool sign = score_[v].sign;
742 score_[v] = DomScore(score_[v].value);
743 if (sign) { s.setPref(v, ValueSet::user_value, value_free); }
744 }
745 }
746 defMax_ = 0;
747 }
748 if (domSeen_ < domTab.size()) {
749 // apply new domain modifications
750 VarScoreVec saved;
751 Literal lastW = lit_true();
752 uint32 dKey = nKey;
753 for (DomainTable::iterator it = domTab.begin() + domSeen_, end = domTab.end(); it != end; ++it) {
754 if (s.topValue(it->var()) != value_free || s.isFalse(it->cond())) {
755 continue;
756 }
757 if (score_[it->var()].domP >= nKey){
758 score_[it->var()].setDom(nKey++);
759 prios_.push_back(DomPrio());
760 prios_.back().clear();
761 }
762 uint32 k = addDomAction(*it, s, saved, lastW);
763 if (k > dKey) { dKey = k; }
764 }
765 for (VarScoreVec::value_type x; !saved.empty(); saved.pop_back()) {
766 x = saved.back();
767 score_[x.first].value += x.second;
768 score_[x.first].init = 0;
769 }
770 if (!actions_.empty()) {
771 actions_.back().next = 0;
772 }
773 if ((nKey - dKey) > dKey && s.sharedContext()->solveMode() == SharedContext::solve_once) {
774 PrioVec(prios_.begin(), prios_.begin()+dKey).swap(prios_);
775 }
776 domSeen_ = domTab.size();
777 }
778 // apply default modification
779 if (defMod_) {
780 struct DefAction : public DomainTable::DefaultAction {
781 DomainHeuristic* self; Solver* solver; uint32 key;
782 DefAction(DomainHeuristic& h, Solver& s, uint32 k) : self(&h), solver(&s), key(k) { }
783 virtual void atom(Literal p, HeuParams::DomPref s, uint32 b) {
784 self->addDefAction(*solver, p, b ? b : 1, key + log2(s));
785 }
786 } act(*this, s, nKey + 1);
787 DomainTable::applyDefault(*s.sharedContext(), act, defPref_);
788 }
789 }
790
addDomAction(const DomMod & e,Solver & s,VarScoreVec & initOut,Literal & lastW)791 uint32 DomainHeuristic::addDomAction(const DomMod& e, Solver& s, VarScoreVec& initOut, Literal& lastW) {
792 if (e.comp()) {
793 DomMod level(e.var(), DomModType::Level, e.bias(), e.prio(), e.cond());
794 DomMod sign(e.var(), DomModType::Sign, e.type() == DomModType::True ? 1 : -1, e.prio(), e.cond());
795 uint32 k1 = addDomAction(level, s, initOut, lastW);
796 uint32 k2 = addDomAction(sign, s, initOut, lastW);
797 return std::max(k1, k2);
798 }
799 bool isStatic = !e.hasCondition() || s.topValue(e.cond().var()) == trueValue(e.cond());
800 uint16& sPrio = prio(e.var(), e.type());
801 if (e.prio() < sPrio || (!isStatic && e.type() == DomModType::Init)) {
802 return 0;
803 }
804 if (e.type() == DomModType::Init && score_[e.var()].init == 0) {
805 initOut.push_back(std::make_pair(e.var(), score_[e.var()].value));
806 score_[e.var()].init = 1;
807 }
808 DomAction a = { e.var(), (uint32)e.type(), DomAction::UNDO_NIL, uint32(0), e.bias(), e.prio() };
809 if (a.mod == DomModType::Sign && a.bias != 0) {
810 a.bias = a.bias > 0 ? value_true : value_false;
811 }
812 POTASSCO_ASSERT(e.type() == a.mod, "Invalid dom modifier!");
813 if (isStatic) {
814 applyAction(s, a, sPrio);
815 score_[e.var()].sign |= static_cast<uint32>(e.type() == DomModType::Sign);
816 return 0;
817 }
818 if (e.cond() != lastW) {
819 s.addWatch(lastW = e.cond(), this, (uint32)actions_.size());
820 }
821 else {
822 actions_.back().next = 1;
823 }
824 actions_.push_back(a);
825 return score_[e.var()].domP + 1;
826 }
827
addDefAction(Solver & s,Literal x,int16 lev,uint32 domKey)828 void DomainHeuristic::addDefAction(Solver& s, Literal x, int16 lev, uint32 domKey) {
829 if (s.value(x.var()) != value_free || score_[x.var()].domP < domKey) { return; }
830 const bool signMod = defMod_ < HeuParams::mod_init && ((defMod_ & HeuParams::mod_init) != 0);
831 const bool valMod = defMod_ >= HeuParams::mod_init || ((defMod_ & HeuParams::mod_level)!= 0);
832 if (score_[x.var()].domP > domKey && lev && valMod) {
833 if (defMod_ < HeuParams::mod_init) { score_[x.var()].level += lev; }
834 else if (defMod_ == HeuParams::mod_init) { score_[x.var()].value += (lev*100); }
835 else if (defMod_ == HeuParams::mod_factor) { score_[x.var()].factor += 1 + (lev > 3) + (lev > 15); }
836 }
837 if (signMod) {
838 ValueRep oPref = s.pref(x.var()).get(ValueSet::user_value);
839 ValueRep nPref = (defMod_ & HeuParams::mod_spos) != 0 ? trueValue(x) : falseValue(x);
840 if (oPref == value_free || (score_[x.var()].sign == 1 && domKey != score_[x.var()].domP)) {
841 s.setPref(x.var(), ValueSet::user_value, nPref);
842 score_[x.var()].sign = 1;
843 }
844 else if (score_[x.var()].sign == 1 && oPref != nPref) {
845 s.setPref(x.var(), ValueSet::user_value, value_free);
846 score_[x.var()].sign = 0;
847 }
848 }
849 if (x.var() > defMax_) {
850 defMax_ = x.var();
851 }
852 score_[x.var()].setDom(domKey);
853 }
854
855
doSelect(Solver & s)856 Literal DomainHeuristic::doSelect(Solver& s) {
857 Literal x = BaseType::doSelect(s);
858 s.stats.addDomChoice(score_[x.var()].isDom());
859 return x;
860 }
861
propagate(Solver & s,Literal,uint32 & aId)862 Constraint::PropResult DomainHeuristic::propagate(Solver& s, Literal, uint32& aId) {
863 uint32 n = aId;
864 uint32 D = s.decisionLevel();
865 do {
866 DomAction& a = actions_[n];
867 uint16& prio = this->prio(a.var, a.mod);
868 if (s.value(a.var) == value_free && a.prio >= prio) {
869 applyAction(s, a, prio);
870 if (D != frames_.back().dl) {
871 s.addUndoWatch(D, this);
872 frames_.push_back(Frame(D, DomAction::UNDO_NIL));
873 }
874 pushUndo(frames_.back().head, n);
875 }
876 } while (actions_[n++].next);
877 return PropResult(true, true);
878 }
879
applyAction(Solver & s,DomAction & a,uint16 & gPrio)880 void DomainHeuristic::applyAction(Solver& s, DomAction& a, uint16& gPrio) {
881 std::swap(gPrio, a.prio);
882 switch (a.mod) {
883 default: assert(false); break;
884 case DomModType::Init:
885 score_[a.var].value = a.bias;
886 break;
887 case DomModType::Factor: std::swap(score_[a.var].factor, a.bias); break;
888 case DomModType::Level:
889 std::swap(score_[a.var].level, a.bias);
890 if (vars_.is_in_queue(a.var)) { vars_.update(a.var); }
891 break;
892 case DomModType::Sign:
893 int16 old = s.pref(a.var).get(ValueSet::user_value);
894 s.setPref(a.var, ValueSet::user_value, ValueRep(a.bias));
895 a.bias = old;
896 break;
897 }
898 }
pushUndo(uint32 & head,uint32 actionId)899 void DomainHeuristic::pushUndo(uint32& head, uint32 actionId) {
900 actions_[actionId].undo = head;
901 head = actionId;
902 }
903
undoLevel(Solver & s)904 void DomainHeuristic::undoLevel(Solver& s) {
905 while (frames_.back().dl >= s.decisionLevel()) {
906 for (uint32 n = frames_.back().head; n != DomAction::UNDO_NIL;) {
907 DomAction& a = actions_[n];
908 n = a.undo;
909 applyAction(s, a, prio(a.var, a.mod));
910 }
911 frames_.pop_back();
912 }
913 }
914 template class ClaspVsids_t<DomScore>;
915 }
916