1 /******************************************
2 Copyright (c) 2016, Mate Soos
3
4 Permission is hereby granted, free of charge, to any person obtaining a copy
5 of this software and associated documentation files (the "Software"), to deal
6 in the Software without restriction, including without limitation the rights
7 to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
8 copies of the Software, and to permit persons to whom the Software is
9 furnished to do so, subject to the following conditions:
10
11 The above copyright notice and this permission notice shall be included in
12 all copies or substantial portions of the Software.
13
14 THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
15 IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
16 FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
17 AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
18 LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
19 OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN
20 THE SOFTWARE.
21 ***********************************************/
22
23 #include "searcher.h"
24 #include "occsimplifier.h"
25 #include "time_mem.h"
26 #include "solver.h"
27 #include <iomanip>
28 #include "varreplacer.h"
29 #include "clausecleaner.h"
30 #include "propbyforgraph.h"
31 #include <algorithm>
32 #include <sstream>
33 #include <cstddef>
34 #include <cmath>
35 #include <ratio>
36 #include "sqlstats.h"
37 #include "datasync.h"
38 #include "reducedb.h"
39 #include "watchalgos.h"
40 #include "hasher.h"
41 #include "solverconf.h"
42 #include "distillerlong.h"
43 #include "xorfinder.h"
44 #include "vardistgen.h"
45 #include "solvertypes.h"
46 #ifdef USE_GAUSS
47 #include "gaussian.h"
48 #endif
49
50 #ifdef FINAL_PREDICTOR
51 // #include "clustering.h"
52 #endif
53
54 #ifdef FINAL_PREDICTOR_BRANCH
55 #include "predict/maple_predictor_conf0_cluster0.h"
56 #endif
57 //#define DEBUG_RESOLV
58 //#define VERBOSE_DEBUG
59
60 using namespace CMSat;
61 using std::cout;
62 using std::endl;
63
64 //#define VERBOSE_DEBUG_GEN_CONFL_DOT
65
66 #ifdef VERBOSE_DEBUG
67 #define VERBOSE_DEBUG_GEN_CONFL_DOT
68 #endif
69
70 /**
71 @brief Sets a sane default config and allocates handler classes
72 */
Searcher(const SolverConf * _conf,Solver * _solver,std::atomic<bool> * _must_interrupt_inter)73 Searcher::Searcher(const SolverConf *_conf, Solver* _solver, std::atomic<bool>* _must_interrupt_inter) :
74 HyperEngine(
75 _conf
76 , _solver
77 , _must_interrupt_inter
78 )
79 , solver(_solver)
80 , cla_inc(1)
81 {
82 var_inc_vsids = 1;
83 maple_step_size = conf.orig_step_size;
84
85 more_red_minim_limit_binary_actual = conf.more_red_minim_limit_binary;
86 mtrand.seed(conf.origSeed);
87 hist.setSize(conf.shortTermHistorySize, conf.blocking_restart_trail_hist_length);
88 cur_max_temp_red_lev2_cls = conf.max_temp_lev2_learnt_clauses;
89 set_branch_strategy(0);
90 polarity_mode = conf.polarity_mode;
91
92 #ifdef FINAL_PREDICTOR
93 // clustering = new ClusteringImp;
94 #endif
95 }
96
~Searcher()97 Searcher::~Searcher()
98 {
99 #ifdef USE_GAUSS
100 clear_gauss_matrices();
101 #endif
102
103 #ifdef FINAL_PREDICTOR
104 // delete clustering;
105 #endif
106 }
107
new_var(const bool bva,const uint32_t orig_outer)108 void Searcher::new_var(const bool bva, const uint32_t orig_outer)
109 {
110 PropEngine::new_var(bva, orig_outer);
111
112 insert_var_order_all((int)nVars()-1);
113 #ifdef STATS_NEEDED_BRANCH
114 level_used_for_cl_arr.insert(level_used_for_cl_arr.end(), 1, 0);
115 #endif
116 }
117
new_vars(size_t n)118 void Searcher::new_vars(size_t n)
119 {
120 PropEngine::new_vars(n);
121
122 for(int i = n-1; i >= 0; i--) {
123 insert_var_order_all((int)nVars()-i-1);
124 }
125
126 #ifdef STATS_NEEDED_BRANCH
127 level_used_for_cl_arr.insert(level_used_for_cl_arr.end(), n, 0);
128 #endif
129 }
130
save_on_var_memory()131 void Searcher::save_on_var_memory()
132 {
133 PropEngine::save_on_var_memory();
134
135 #ifdef STATS_NEEDED_BRANCH
136 level_used_for_cl_arr.resize(nVars());
137 #endif
138 }
139
updateVars(const vector<uint32_t> &,const vector<uint32_t> & interToOuter)140 void Searcher::updateVars(
141 const vector<uint32_t>& /*outerToInter*/
142 , const vector<uint32_t>& interToOuter
143 ) {
144
145 updateArray(var_act_vsids, interToOuter);
146 updateArray(var_act_maple, interToOuter);
147
148 #ifdef VMTF_NEEDED
149 rebuildOrderHeapVMTF();
150 #endif
151 }
152
153 template<bool update_bogoprops>
add_lit_to_learnt(const Lit lit,uint32_t nDecisionLevel)154 inline void Searcher::add_lit_to_learnt(
155 const Lit lit
156 , uint32_t nDecisionLevel
157 ) {
158 const uint32_t var = lit.var();
159 assert(varData[var].removed == Removed::none);
160
161 #ifdef STATS_NEEDED_BRANCH
162 if (!update_bogoprops) {
163 varData[var].inside_conflict_clause_antecedents++;
164 varData[var].last_seen_in_1uip = sumConflicts;
165 }
166 #endif
167
168 //If var is at level 0, don't do anything with it, just skip
169 if (seen[var] || varData[var].level == 0) {
170 return;
171 }
172 seen[var] = 1;
173
174 if (!update_bogoprops) {
175 #ifdef STATS_NEEDED_BRANCH
176 if (varData[var].level != 0 &&
177 !level_used_for_cl_arr[varData[var].level]
178 ) {
179 level_used_for_cl_arr[varData[var].level] = 1;
180 level_used_for_cl.push_back(varData[var].level);
181 }
182 #endif
183
184 switch(branch_strategy) {
185 case branch::vsids:
186 vsids_bump_var_act<update_bogoprops>(var, 0.5);
187 implied_by_learnts.push_back(var);
188 break;
189
190 case branch::maple:
191 varData[var].maple_conflicted++;
192 break;
193
194 #ifdef VMTF_NEEDED
195 case branch::vmtf:
196 implied_by_learnts.push_back(var);
197 break;
198 #endif
199 }
200 }
201
202 if (varData[var].level >= nDecisionLevel) {
203 pathC++;
204 } else {
205 learnt_clause.push_back(lit);
206 }
207 }
208
recursiveConfClauseMin()209 inline void Searcher::recursiveConfClauseMin()
210 {
211 uint32_t abstract_level = 0;
212 for (size_t i = 1; i < learnt_clause.size(); i++) {
213 //(maintain an abstraction of levels involved in conflict)
214 abstract_level |= abstractLevel(learnt_clause[i].var());
215 }
216
217 size_t i, j;
218 for (i = j = 1; i < learnt_clause.size(); i++) {
219 if (varData[learnt_clause[i].var()].reason.isNULL()
220 || !litRedundant(learnt_clause[i], abstract_level)
221 ) {
222 learnt_clause[j++] = learnt_clause[i];
223 }
224 }
225 learnt_clause.resize(j);
226 }
227
normalClMinim()228 void Searcher::normalClMinim()
229 {
230 size_t i,j;
231 for (i = j = 1; i < learnt_clause.size(); i++) {
232 const PropBy& reason = varData[learnt_clause[i].var()].reason;
233 size_t size;
234 Lit *lits = NULL;
235 PropByType type = reason.getType();
236 if (type == null_clause_t) {
237 learnt_clause[j++] = learnt_clause[i];
238 continue;
239 }
240
241 switch (type) {
242 case binary_t:
243 size = 1;
244 break;
245
246 case clause_t: {
247 Clause* cl2 = cl_alloc.ptr(reason.get_offset());
248 lits = cl2->begin();
249 size = cl2->size()-1;
250 break;
251 }
252
253 #ifdef USE_GAUSS
254 case xor_t: {
255 vector<Lit>* xor_reason = gmatrices[reason.get_matrix_num()]->
256 get_reason(reason.get_row_num());
257 lits = xor_reason->data();
258 size = xor_reason->size()-1;
259 sumAntecedentsLits += size;
260 break;
261 }
262 #endif
263
264 default:
265 release_assert(false);
266 std::exit(-1);
267 }
268
269 for (size_t k = 0; k < size; k++) {
270 Lit p;
271 switch (type) {
272 #ifdef USE_GAUSS
273 case xor_t:
274 #endif
275 case clause_t:
276 p = lits[k+1];
277 break;
278
279 case binary_t:
280 p = reason.lit2();
281 break;
282
283 default:
284 release_assert(false);
285 std::exit(-1);
286 }
287
288 if (!seen[p.var()] && varData[p.var()].level > 0) {
289 learnt_clause[j++] = learnt_clause[i];
290 break;
291 }
292 }
293 }
294 learnt_clause.resize(j);
295 }
296
debug_print_resolving_clause(const PropBy confl) const297 void Searcher::debug_print_resolving_clause(const PropBy confl) const
298 {
299 #ifndef DEBUG_RESOLV
300 //Avoid unused parameter warning
301 (void) confl;
302 #else
303 switch(confl.getType()) {
304 case binary_t: {
305 cout << "resolv bin: " << confl.lit2() << endl;
306 break;
307 }
308
309 case clause_t: {
310 Clause* cl = cl_alloc.ptr(confl.get_offset());
311 cout << "resolv (long): " << *cl << endl;
312 break;
313 }
314
315 case xor_t: {
316 //in the future, we'll have XOR clauses. Not yet.
317 assert(false);
318 exit(-1);
319 break;
320 }
321
322 case null_clause_t: {
323 assert(false);
324 break;
325 }
326 }
327 #endif
328 }
329
update_clause_glue_from_analysis(Clause * cl)330 void Searcher::update_clause_glue_from_analysis(Clause* cl)
331 {
332 assert(cl->red());
333 if (cl->is_ternary_resolvent) {
334 return;
335 }
336 const unsigned new_glue = calc_glue(*cl);
337
338 if (new_glue < cl->stats.glue) {
339 if (cl->stats.glue <= conf.protect_cl_if_improved_glue_below_this_glue_for_one_turn) {
340 cl->stats.ttl = 1;
341 }
342 cl->stats.glue = new_glue;
343
344 if (cl->stats.locked_for_data_gen) {
345 assert(cl->stats.which_red_array == 0);
346 } else if (new_glue <= conf.glue_put_lev0_if_below_or_eq
347 && cl->stats.which_red_array >= 1
348 ) {
349 //move to lev0 if very low glue
350 cl->stats.which_red_array = 0;
351 } else if (new_glue <= conf.glue_put_lev1_if_below_or_eq
352 && conf.glue_put_lev1_if_below_or_eq != 0
353 ) {
354 //move to lev1 if low glue
355 cl->stats.which_red_array = 1;
356 }
357 }
358 }
359
360 template<bool update_bogoprops>
add_literals_from_confl_to_learnt(const PropBy confl,const Lit p,uint32_t nDecisionLevel)361 void Searcher::add_literals_from_confl_to_learnt(
362 const PropBy confl
363 , const Lit p
364 , uint32_t nDecisionLevel
365 ) {
366 #ifdef VERBOSE_DEBUG
367 debug_print_resolving_clause(confl);
368 #endif
369 sumAntecedents++;
370
371 Lit* lits = NULL;
372 size_t size = 0;
373 switch (confl.getType()) {
374 case binary_t : {
375 sumAntecedentsLits += 2;
376 if (confl.isRedStep()) {
377 #if defined(STATS_NEEDED) || defined(FINAL_PREDICTOR)
378 antec_data.binRed++;
379 #endif
380 stats.resolvs.binRed++;
381 } else {
382 #if defined(STATS_NEEDED) || defined(FINAL_PREDICTOR)
383 antec_data.binIrred++;
384 #endif
385 stats.resolvs.binIrred++;
386 }
387 break;
388 }
389
390 case clause_t : {
391 Clause* cl = cl_alloc.ptr(confl.get_offset());
392 assert(!cl->getRemoved());
393 lits = cl->begin();
394 size = cl->size();
395 sumAntecedentsLits += cl->size();
396 if (cl->red()) {
397 stats.resolvs.longRed++;
398 #if defined(STATS_NEEDED) || defined(FINAL_PREDICTOR)
399 antec_data.longRed++;
400 antec_data.age_long_reds.push(sumConflicts - cl->stats.introduced_at_conflict);
401 antec_data.glue_long_reds.push(cl->stats.glue);
402 #endif
403 } else {
404 stats.resolvs.longIrred++;
405 #if defined(STATS_NEEDED) || defined(FINAL_PREDICTOR)
406 antec_data.longIrred++;
407 #endif
408 }
409 #if defined(STATS_NEEDED) || defined(FINAL_PREDICTOR)
410 antec_data.size_longs.push(cl->size());
411 if (!update_bogoprops) {
412 cl->stats.used_for_uip_creation++;
413 cl->stats.sum_uip1_used++;
414 assert(
415 !cl->red() ||
416 cl->stats.introduced_at_conflict != 0 ||
417 solver->conf.simplify_at_startup == 1);
418 }
419 #endif
420
421 //If STATS_NEEDED then bump acitvity of ALL clauses
422 //and set stats on all clauses
423 if (!update_bogoprops
424 && cl->red()
425 #if !defined(STATS_NEEDED) && !defined(FINAL_PREDICTOR)
426 && cl->stats.which_red_array != 0
427 #endif
428 ) {
429 if (conf.update_glues_on_analyze) {
430 update_clause_glue_from_analysis(cl);
431 }
432
433 #if !defined(STATS_NEEDED) && !defined(FINAL_PREDICTOR)
434 if (cl->stats.which_red_array == 1)
435 #endif
436 cl->stats.last_touched = sumConflicts;
437
438 //If stats or predictor, bump all because during final
439 //we will need this data and during dump when stats is on
440 //we also need this data.
441 #if defined(STATS_NEEDED) || defined(FINAL_PREDICTOR)
442 bump_cl_act<update_bogoprops>(cl);
443 #else
444 if (cl->stats.which_red_array == 2) {
445 bump_cl_act<update_bogoprops>(cl);
446 }
447 #endif
448 }
449 break;
450 }
451
452 #ifdef USE_GAUSS
453 case xor_t: {
454 vector<Lit>* xor_reason = gmatrices[confl.get_matrix_num()]->
455 get_reason(confl.get_row_num());
456 lits = xor_reason->data();
457 size = xor_reason->size();
458 sumAntecedentsLits += size;
459 break;
460 }
461 #endif
462
463 case null_clause_t:
464 default:
465 assert(false && "Error in conflict analysis (otherwise should be UIP)");
466 }
467
468 size_t i = 0;
469 bool cont = true;
470 Lit x = lit_Undef;
471 while(cont) {
472 switch (confl.getType()) {
473 case binary_t:
474 if (i == 0) {
475 x = failBinLit;
476 } else {
477 x = confl.lit2();
478 cont = false;
479 }
480 break;
481
482 case clause_t:
483 #ifdef USE_GAUSS
484 case xor_t:
485 #endif
486 x = lits[i];
487 if (i == size-1) {
488 cont = false;
489 }
490 break;
491
492 case null_clause_t:
493 assert(false);
494 break;
495 }
496 if (p == lit_Undef || i > 0) {
497 add_lit_to_learnt<update_bogoprops>(x, nDecisionLevel);
498 }
499 i++;
500 }
501 }
502
503 template<bool update_bogoprops>
minimize_learnt_clause()504 inline void Searcher::minimize_learnt_clause()
505 {
506 const size_t origSize = learnt_clause.size();
507
508 toClear = learnt_clause;
509 if (conf.doRecursiveMinim) {
510 recursiveConfClauseMin();
511 } else {
512 normalClMinim();
513 }
514 for (const Lit lit: toClear) {
515 seen[lit.var()] = 0;
516 }
517 toClear.clear();
518
519 stats.recMinCl += ((origSize - learnt_clause.size()) > 0);
520 stats.recMinLitRem += origSize - learnt_clause.size();
521 }
522
minimize_using_permdiff()523 inline void Searcher::minimize_using_permdiff()
524 {
525 if (conf.doMinimRedMore
526 && learnt_clause.size() > 1
527 ) {
528 stats.permDiff_attempt++;
529 stats.moreMinimLitsStart += learnt_clause.size();
530 watch_based_learnt_minim();
531
532 stats.moreMinimLitsEnd += learnt_clause.size();
533 }
534 }
535
watch_based_learnt_minim()536 inline void Searcher::watch_based_learnt_minim()
537 {
538 MYFLAG++;
539 const auto& ws = watches[~learnt_clause[0]];
540 uint32_t nb = 0;
541 for (const Watched& w: ws) {
542 if (w.isBin()) {
543 Lit imp = w.lit2();
544 if (permDiff[imp.var()] == MYFLAG && value(imp) == l_True) {
545 nb++;
546 permDiff[imp.var()] = MYFLAG - 1;
547 }
548 } else {
549 break;
550 }
551 }
552 uint32_t l = learnt_clause.size() - 1;
553 if (nb > 0) {
554 for (uint32_t i = 1; i < learnt_clause.size() - nb; i++) {
555 if (permDiff[learnt_clause[i].var()] != MYFLAG) {
556 Lit p = learnt_clause[l];
557 learnt_clause[l] = learnt_clause[i];
558 learnt_clause[i] = p;
559 l--;
560 i--;
561 }
562 }
563 learnt_clause.resize(learnt_clause.size()-nb);
564 stats.permDiff_success++;
565 stats.permDiff_rem_lits+=nb;
566 }
567 }
568
print_fully_minimized_learnt_clause() const569 void Searcher::print_fully_minimized_learnt_clause() const
570 {
571 if (conf.verbosity >= 6) {
572 cout << "Final clause: " << learnt_clause << endl;
573 for (uint32_t i = 0; i < learnt_clause.size(); i++) {
574 cout << "lev learnt_clause[" << i << "]:" << varData[learnt_clause[i].var()].level << endl;
575 }
576 }
577 }
578
find_backtrack_level_of_learnt()579 size_t Searcher::find_backtrack_level_of_learnt()
580 {
581 if (learnt_clause.size() <= 1)
582 return 0;
583 else {
584 uint32_t max_i = 1;
585 for (uint32_t i = 2; i < learnt_clause.size(); i++) {
586 if (varData[learnt_clause[i].var()].level > varData[learnt_clause[max_i].var()].level)
587 max_i = i;
588 }
589 std::swap(learnt_clause[max_i], learnt_clause[1]);
590 return varData[learnt_clause[1].var()].level;
591 }
592 }
593
594 template<bool update_bogoprops>
create_learnt_clause(PropBy confl)595 void Searcher::create_learnt_clause(PropBy confl)
596 {
597 pathC = 0;
598 int index = trail.size() - 1;
599 Lit p = lit_Undef;
600
601 Lit lit0 = lit_Error;
602 switch (confl.getType()) {
603 case binary_t : {
604 lit0 = failBinLit;
605 break;
606 }
607 #ifdef USE_GAUSS
608 case xor_t: {
609 vector<Lit>* cl = gmatrices[confl.get_matrix_num()]->
610 get_reason(confl.get_row_num());
611 lit0 = (*cl)[0];
612 break;
613 }
614 #endif
615
616 case clause_t : {
617 lit0 = (*cl_alloc.ptr(confl.get_offset()))[0];
618 break;
619 }
620
621 default:
622 assert(false);
623 }
624 uint32_t nDecisionLevel = varData[lit0.var()].level;
625
626
627 learnt_clause.push_back(lit_Undef); //make space for ~p
628 do {
629 #ifdef DEBUG_RESOLV
630 cout << "p is: " << p << endl;
631 #endif
632
633 add_literals_from_confl_to_learnt<update_bogoprops>(
634 confl, p, nDecisionLevel);
635
636 // Select next implication to look at
637 do {
638 while (!seen[trail[index--].lit.var()]);
639 p = trail[index+1].lit;
640 assert(p != lit_Undef);
641 } while(trail[index+1].lev < nDecisionLevel);
642
643 confl = varData[p.var()].reason;
644 assert(varData[p.var()].level > 0);
645
646 //This clears out vars that haven't been added to learnt_clause,
647 //but their 'seen' has been set
648 seen[p.var()] = 0;
649
650 //Okay, one more path done
651 pathC--;
652 } while (pathC > 0);
653 assert(pathC == 0);
654 learnt_clause[0] = ~p;
655 }
656
simple_create_learnt_clause(PropBy confl,vector<Lit> & out_learnt,bool True_confl)657 void Searcher::simple_create_learnt_clause(
658 PropBy confl,
659 vector<Lit>& out_learnt,
660 bool True_confl
661 ) {
662 int until = -1;
663 int mypathC = 0;
664 Lit p = lit_Undef;
665 int index = trail.size() - 1;
666 assert(decisionLevel() == 1);
667
668 do {
669 if (!confl.isNULL()) {
670 if (confl.getType() == binary_t) {
671 if (p == lit_Undef && True_confl == false) {
672 Lit q = failBinLit;
673 if (!seen[q.var()]) {
674 seen[q.var()] = 1;
675 mypathC++;
676 }
677 }
678 Lit q = confl.lit2();
679 if (!seen[q.var()]) {
680 seen[q.var()] = 1;
681 mypathC++;
682 }
683 } else {
684 const Clause& c = *solver->cl_alloc.ptr(confl.get_offset());
685
686 // if True_confl==true, then choose p begin with the 1st index of c
687 for (uint32_t j = (p == lit_Undef && True_confl == false) ? 0 : 1
688 ; j < c.size()
689 ; j++
690 ) {
691 Lit q = c[j];
692 assert(q.var() < seen.size());
693 if (!seen[q.var()]) {
694 seen[q.var()] = 1;
695 mypathC++;
696 }
697 }
698 }
699 } else {
700 assert(confl.isNULL());
701 out_learnt.push_back(~p);
702 }
703 // if not break, while() will come to the index of trail blow 0, and fatal error occur;
704 if (mypathC == 0) {
705 break;
706 }
707
708 // Select next clause to look at:
709 while (!seen[trail[index--].lit.var()]);
710 // if the reason cr from the 0-level assigned var, we must break avoid move forth further;
711 // but attention that maybe seen[x]=1 and never be clear. However makes no matter;
712 if ((int)trail_lim[0] > index + 1
713 && until == -1
714 ) {
715 until = out_learnt.size();
716 }
717 p = trail[index + 1].lit;
718 confl = varData[p.var()].reason;
719
720 //under normal circumstances this does not happen, but here, it can
721 //reason is undefined for level 0
722 if (varData[p.var()].level == 0) {
723 confl = PropBy();
724 }
725 seen[p.var()] = 0;
726 mypathC--;
727 } while (mypathC >= 0);
728
729 if (until != -1)
730 out_learnt.resize(until);
731 }
732
print_debug_resolution_data(const PropBy confl)733 void Searcher::print_debug_resolution_data(const PropBy confl)
734 {
735 #ifndef DEBUG_RESOLV
736 //Avoid unused parameter warning
737 (void) confl;
738 #else
739 cout << "Before resolution, trail is: " << endl;
740 print_trail();
741 cout << "Conflicting clause: " << confl << endl;
742 cout << "Fail bin lit: " << failBinLit << endl;
743 #endif
744 }
745
746 #ifdef VMTF_NEEDED
747 struct analyze_bumped_rank {
748 Searcher * internal;
analyze_bumped_rankanalyze_bumped_rank749 analyze_bumped_rank (Searcher * i) : internal (i) { }
operator ()analyze_bumped_rank750 uint64_t operator () (const int & a) const {
751 return internal->vmtf_btab[a];
752 }
753 };
754
755
756 struct analyze_bumped_smaller {
757 Searcher * internal;
analyze_bumped_smalleranalyze_bumped_smaller758 analyze_bumped_smaller (Searcher * i) : internal (i) { }
operator ()analyze_bumped_smaller759 bool operator () (const int & a, const int & b) const {
760 const auto s = analyze_bumped_rank (internal) (a);
761 const auto t = analyze_bumped_rank (internal) (b);
762 return s < t;
763 }
764 };
765 #endif
766
767 template<bool update_bogoprops>
analyze_conflict(const PropBy confl,uint32_t & out_btlevel,uint32_t & glue,uint32_t & glue_before_minim)768 void Searcher::analyze_conflict(
769 const PropBy confl
770 , uint32_t& out_btlevel
771 , uint32_t& glue
772 , uint32_t&
773 #if defined(STATS_NEEDED) || defined(FINAL_PREDICTOR)
774 glue_before_minim
775 #endif
776 ) {
777 //Set up environment
778 #if defined(STATS_NEEDED_BRANCH) || defined(FINAL_PREDICTOR_BRANCH)
779 assert(level_used_for_cl.empty());
780 #ifdef SLOW_DEBUG
781 for(auto& x: level_used_for_cl_arr) {
782 assert(x == 0);
783 }
784 #endif
785 #endif
786
787 #if defined(STATS_NEEDED) || defined(FINAL_PREDICTOR)
788 antec_data.clear();
789 #endif
790
791 learnt_clause.clear();
792 assert(toClear.empty());
793 implied_by_learnts.clear();
794 assert(decisionLevel() > 0);
795
796 print_debug_resolution_data(confl);
797 create_learnt_clause<update_bogoprops>(confl);
798 stats.litsRedNonMin += learnt_clause.size();
799 #if defined(STATS_NEEDED) || defined(FINAL_PREDICTOR)
800 glue_before_minim = calc_glue(learnt_clause);
801 #endif
802 minimize_learnt_clause<update_bogoprops>();
803 stats.litsRedFinal += learnt_clause.size();
804
805 //further minimisation 1 -- short, small glue clauses
806 glue = std::numeric_limits<uint32_t>::max();
807 if (learnt_clause.size() <= conf.max_size_more_minim) {
808 glue = calc_glue(learnt_clause);
809 if (glue <= conf.max_glue_more_minim) {
810 minimize_using_permdiff();
811 }
812 }
813 if (glue == std::numeric_limits<uint32_t>::max()) {
814 glue = calc_glue(learnt_clause);
815 }
816 print_fully_minimized_learnt_clause();
817
818 if (learnt_clause.size() > conf.max_size_more_minim
819 && glue <= (conf.glue_put_lev0_if_below_or_eq+2)
820 && conf.doMinimRedMoreMore
821 ) {
822 minimise_redundant_more_more(learnt_clause);
823 }
824
825 #ifdef STATS_NEEDED_BRANCH
826 for(const Lit l: learnt_clause) {
827 varData[l.var()].inside_conflict_clause++;
828 varData[l.var()].inside_conflict_clause_glue += glue;
829 }
830 vars_used_for_cl.clear();
831 for(auto& lev: level_used_for_cl) {
832 vars_used_for_cl.push_back(trail[trail_lim[lev-1]].lit.var());
833 assert(varData[trail[trail_lim[lev-1]].lit.var()].reason == PropBy());
834 assert(level_used_for_cl_arr[lev] == 1);
835 level_used_for_cl_arr[lev] = 0;
836 }
837 level_used_for_cl.clear();
838 #endif
839
840 out_btlevel = find_backtrack_level_of_learnt();
841 if (!update_bogoprops) {
842 switch(branch_strategy) {
843 case branch::vsids:
844 for (const uint32_t var :implied_by_learnts) {
845 if ((int32_t)varData[var].level >= (int32_t)out_btlevel-1) {
846 vsids_bump_var_act<update_bogoprops>(var, 1.0);
847 }
848 }
849 implied_by_learnts.clear();
850 break;
851 case branch::maple: {
852 uint32_t bump_by = 2;
853 assert(toClear.empty());
854 const Lit p = learnt_clause[0];
855 seen[p.var()] = true;
856 toClear.push_back(p);
857 for (int i = learnt_clause.size() - 1; i >= 0; i--) {
858 const uint32_t v = learnt_clause[i].var();
859 if (varData[v].reason.isClause()) {
860 ClOffset offs = varData[v].reason.get_offset();
861 Clause* cl = cl_alloc.ptr(offs);
862 for (const Lit l: *cl) {
863 if (!seen[l.var()]) {
864 seen[l.var()] = true;
865 toClear.push_back(l);
866 varData[l.var()].maple_conflicted+=bump_by;
867 }
868 }
869 } else if (varData[v].reason.getType() == binary_t) {
870 Lit l = varData[v].reason.lit2();
871 if (!seen[l.var()]) {
872 seen[l.var()] = true;
873 toClear.push_back(l);
874 varData[l.var()].maple_conflicted+=bump_by;
875 }
876 l = Lit(v, false);
877 if (!seen[l.var()]) {
878 seen[l.var()] = true;
879 toClear.push_back(l);
880 varData[l.var()].maple_conflicted+=bump_by;
881 }
882 }
883 }
884 for (Lit l: toClear) {
885 seen[l.var()] = 0;
886 }
887 toClear.clear();
888 break;
889 }
890 #ifdef VMTF_NEEDED
891 case branch::vmtf:
892 std::sort(implied_by_learnts.begin(),
893 implied_by_learnts.end(),
894 analyze_bumped_smaller(this));
895
896 for (const uint32_t var :implied_by_learnts) {
897 vmtf_bump_queue(var);
898 }
899 implied_by_learnts.clear();
900 break;
901 #endif
902 default:
903 break;
904 }
905 }
906 sumConflictClauseLits += learnt_clause.size();
907 }
908
litRedundant(const Lit p,uint32_t abstract_levels)909 bool Searcher::litRedundant(const Lit p, uint32_t abstract_levels)
910 {
911 #ifdef DEBUG_LITREDUNDANT
912 cout << "c " << __func__ << " called" << endl;
913 #endif
914
915 analyze_stack.clear();
916 analyze_stack.push(p);
917
918 size_t top = toClear.size();
919 while (!analyze_stack.empty()) {
920 #ifdef DEBUG_LITREDUNDANT
921 cout << "At point in litRedundant: " << analyze_stack.top() << endl;
922 #endif
923
924 const PropBy reason = varData[analyze_stack.top().var()].reason;
925 PropByType type = reason.getType();
926 analyze_stack.pop();
927
928 //Must have a reason
929 assert(!reason.isNULL());
930
931 size_t size;
932 Lit* lits = NULL;
933 switch (type) {
934 case clause_t: {
935 Clause* cl = cl_alloc.ptr(reason.get_offset());
936 lits = cl->begin();
937 size = cl->size()-1;
938 break;
939 }
940
941 #ifdef USE_GAUSS
942 case xor_t: {
943 vector<Lit>* xcl = gmatrices[reason.get_matrix_num()]->
944 get_reason(reason.get_row_num());
945 lits = xcl->data();
946 size = xcl->size()-1;
947 break;
948 }
949 #endif
950
951 case binary_t:
952 size = 1;
953 break;
954
955 case null_clause_t:
956 default:
957 release_assert(false);
958 }
959
960 for (size_t i = 0
961 ; i < size
962 ; i++
963 ) {
964 Lit p2;
965 switch (type) {
966 #ifdef USE_GAUSS
967 case xor_t:
968 #endif
969 case clause_t:
970 p2 = lits[i+1];
971 break;
972
973 case binary_t:
974 p2 = reason.lit2();
975 break;
976
977 case null_clause_t:
978 default:
979 release_assert(false);
980 }
981 stats.recMinimCost++;
982
983 if (!seen[p2.var()] && varData[p2.var()].level > 0) {
984 if (!varData[p2.var()].reason.isNULL()
985 && (abstractLevel(p2.var()) & abstract_levels) != 0
986 ) {
987 seen[p2.var()] = 1;
988 analyze_stack.push(p2);
989 toClear.push_back(p2);
990 } else {
991 //Return to where we started before function executed
992 for (size_t j = top; j < toClear.size(); j++) {
993 seen[toClear[j].var()] = 0;
994 }
995 toClear.resize(top);
996
997 return false;
998 }
999 }
1000 }
1001 }
1002
1003 return true;
1004 }
1005 template void Searcher::analyze_conflict<true>(const PropBy confl
1006 , uint32_t& out_btlevel
1007 , uint32_t& glue
1008 , uint32_t& glue_before_minim
1009 );
1010 template void Searcher::analyze_conflict<false>(const PropBy confl
1011 , uint32_t& out_btlevel
1012 , uint32_t& glue
1013 , uint32_t& glue_before_minim
1014 );
1015
subset(const vector<Lit> & A,const Clause & B)1016 bool Searcher::subset(const vector<Lit>& A, const Clause& B)
1017 {
1018 //Set seen
1019 for (uint32_t i = 0; i != B.size(); i++)
1020 seen[B[i].toInt()] = 1;
1021
1022 bool ret = true;
1023 for (uint32_t i = 0; i != A.size(); i++) {
1024 if (!seen[A[i].toInt()]) {
1025 ret = false;
1026 break;
1027 }
1028 }
1029
1030 //Clear seen
1031 for (uint32_t i = 0; i != B.size(); i++)
1032 seen[B[i].toInt()] = 0;
1033
1034 return ret;
1035 }
1036
analyze_final_confl_with_assumptions(const Lit p,vector<Lit> & out_conflict)1037 void Searcher::analyze_final_confl_with_assumptions(const Lit p, vector<Lit>& out_conflict)
1038 {
1039 out_conflict.clear();
1040 out_conflict.push_back(p);
1041
1042 if (decisionLevel() == 0) {
1043 return;
1044 }
1045
1046 //It's been set at level 0. The seen[] may not be large enough to do
1047 //seen[p.var()] -- we might have mem-saved that
1048 if (varData[p.var()].level == 0) {
1049 return;
1050 }
1051
1052 seen[p.var()] = 1;
1053
1054 assert(!trail_lim.empty());
1055 for (int64_t i = (int64_t)trail.size() - 1; i >= (int64_t)trail_lim[0]; i--) {
1056 const uint32_t x = trail[i].lit.var();
1057 if (seen[x]) {
1058 const PropBy reason = varData[x].reason;
1059 if (reason.isNULL()) {
1060 assert(varData[x].level > 0);
1061 out_conflict.push_back(~trail[i].lit);
1062 } else {
1063 switch(reason.getType()) {
1064 case PropByType::clause_t : {
1065 const Clause& cl = *cl_alloc.ptr(reason.get_offset());
1066 assert(value(cl[0]) == l_True);
1067 for(const Lit lit: cl) {
1068 if (varData[lit.var()].level > 0) {
1069 seen[lit.var()] = 1;
1070 }
1071 }
1072 break;
1073 }
1074
1075 case PropByType::binary_t: {
1076 const Lit lit = reason.lit2();
1077 if (varData[lit.var()].level > 0) {
1078 seen[lit.var()] = 1;
1079 }
1080 break;
1081 }
1082
1083 #ifdef USE_GAUSS
1084 case PropByType::xor_t: {
1085 vector<Lit>* cl = gmatrices[reason.get_matrix_num()]->
1086 get_reason(reason.get_row_num());
1087 assert(value((*cl)[0]) == l_True);
1088 for(const Lit lit: *cl) {
1089 if (varData[lit.var()].level > 0) {
1090 seen[lit.var()] = 1;
1091 }
1092 }
1093 break;
1094 }
1095 #endif
1096
1097 case PropByType::null_clause_t: {
1098 assert(false);
1099 }
1100 }
1101 }
1102 seen[x] = 0;
1103 }
1104 }
1105 seen[p.var()] = 0;
1106
1107 learnt_clause = out_conflict;
1108 minimize_using_permdiff();
1109 out_conflict = learnt_clause;
1110 }
1111
update_assump_conflict_to_orig_outside(vector<Lit> & out_conflict)1112 void Searcher::update_assump_conflict_to_orig_outside(vector<Lit>& out_conflict)
1113 {
1114 if (assumptions.empty()) {
1115 return;
1116 }
1117
1118 vector<AssumptionPair> inter_assumptions;
1119 for(const auto& ass: assumptions) {
1120 inter_assumptions.push_back(
1121 AssumptionPair(map_outer_to_inter(ass.lit_outer), ass.lit_orig_outside));
1122 }
1123
1124 std::sort(inter_assumptions.begin(), inter_assumptions.end());
1125 std::sort(out_conflict.begin(), out_conflict.end());
1126 assert(out_conflict.size() <= assumptions.size());
1127 //They now are in the order where we can go through them linearly
1128
1129 /*cout << "out_conflict: " << out_conflict << endl;
1130 cout << "assumptions: ";
1131 for(AssumptionPair p: assumptions) {
1132 cout << "inter: " << p.lit_inter << " , outer: " << p.lit_orig_outside << " , ";
1133 }
1134 cout << endl;*/
1135
1136 uint32_t at_assump = 0;
1137 uint32_t j = 0;
1138 for(size_t i = 0; i < out_conflict.size(); i++) {
1139 Lit lit = out_conflict[i];
1140
1141 //lit_outer is actually INTER here, because we updated above
1142 while(lit != ~inter_assumptions[at_assump].lit_outer) {
1143 at_assump++;
1144 assert(at_assump < inter_assumptions.size() && "final conflict contains literals that are not from the assumptions!");
1145 }
1146 assert(lit == ~inter_assumptions[at_assump].lit_outer);
1147
1148 //in case of symmetry breaking, we can be in trouble
1149 //then, the orig_outside is actually lit_Undef
1150 //in these cases, the symmetry breaking literal needs to be taken out
1151 if (inter_assumptions[at_assump].lit_orig_outside != lit_Undef) {
1152 //Update to correct outside lit
1153 out_conflict[j++] = ~inter_assumptions[at_assump].lit_orig_outside;
1154 }
1155 }
1156 out_conflict.resize(j);
1157 }
1158
check_blocking_restart()1159 void Searcher::check_blocking_restart()
1160 {
1161 if (conf.do_blocking_restart
1162 && sumConflicts > conf.lower_bound_for_blocking_restart
1163 && hist.glueHist.isvalid()
1164 && hist.trailDepthHistLonger.isvalid()
1165 && decisionLevel() > 0
1166 && trail_lim.size() > 0
1167 && trail.size() > hist.trailDepthHistLonger.avg()*conf.blocking_restart_multip
1168 ) {
1169 hist.glueHist.clear();
1170 if (!blocked_restart) {
1171 stats.blocked_restart_same++;
1172 }
1173 blocked_restart = true;
1174 stats.blocked_restart++;
1175 }
1176 }
1177
print_order_heap()1178 void Searcher::print_order_heap()
1179 {
1180 switch(branch_strategy) {
1181 case branch::vsids:
1182 cout << "vsids heap size: " << order_heap_vsids.size() << endl;
1183 cout << "vsids acts:";
1184 for(auto x: var_act_vsids) {
1185 cout << std::setprecision(12) << x.str() << " ";
1186 }
1187 cout << endl;
1188 cout << "VSID order heap:" << endl;
1189 order_heap_vsids.print_heap();
1190 break;
1191 case branch::maple:
1192 cout << "maple heap size: " << order_heap_maple.size() << endl;
1193 cout << "maple acts:";
1194 for(auto x: var_act_maple) {
1195 cout << std::setprecision(12) << x.str() << " ";
1196 }
1197 cout << endl;
1198 cout << "MAPLE order heap:" << endl;
1199 order_heap_maple.print_heap();
1200 break;
1201 #ifdef VMTF_NEEDED
1202 case branch::vmtf:
1203 assert(false && "Not implemented yet");
1204 break;
1205 #endif
1206 }
1207 }
1208
1209 #ifdef USE_GAUSS
check_need_gauss_jordan_disable()1210 void Searcher::check_need_gauss_jordan_disable()
1211 {
1212 uint32_t num_disabled = 0;
1213 for(uint32_t i = 0; i < gqueuedata.size(); i++) {
1214 auto& gqd = gqueuedata[i];
1215 if (gqd.engaus_disable) {
1216 num_disabled++;
1217 continue;
1218 }
1219
1220 if (conf.gaussconf.autodisable &&
1221 !conf.xor_detach_reattach &&
1222 gmatrices[i]->must_disable(gqd)
1223 ) {
1224 gqd.engaus_disable = true;
1225 num_disabled++;
1226 }
1227
1228 gqd.reset();
1229 gmatrices[i]->update_cols_vals_set();
1230 }
1231 assert(gqhead <= qhead);
1232
1233 if (num_disabled == gqueuedata.size()) {
1234 all_matrices_disabled = true;
1235 gqhead = qhead;
1236 }
1237 }
1238 #endif
1239
search()1240 lbool Searcher::search()
1241 {
1242 assert(ok);
1243 #ifdef SLOW_DEBUG
1244 check_no_duplicate_lits_anywhere();
1245 check_order_heap_sanity();
1246 #endif
1247 const double myTime = cpuTime();
1248
1249 //Stats reset & update
1250 stats.numRestarts++;
1251 hist.clear();
1252 hist.reset_glue_hist_size(conf.shortTermHistorySize);
1253
1254 assert(solver->prop_at_head());
1255
1256 //Loop until restart or finish (SAT/UNSAT)
1257 PropBy confl;
1258 lbool search_ret;
1259
1260 #ifdef VERBOSE_DEBUG
1261 print_order_heap();
1262 #endif
1263 while (!params.needToStopSearch
1264 || !confl.isNULL() //always finish the last conflict
1265 ) {
1266 #ifdef USE_GAUSS
1267 gqhead = qhead;
1268 #endif
1269 confl = propagate_any_order_fast();
1270
1271 if (!confl.isNULL()) {
1272 update_branch_params();
1273
1274 #ifdef STATS_NEEDED
1275 stats.conflStats.update(lastConflictCausedBy);
1276 #endif
1277
1278 print_restart_stat();
1279 #if defined(STATS_NEEDED) || defined(FINAL_PREDICTOR)
1280 hist.trailDepthHist.push(trail.size());
1281 #endif
1282 hist.trailDepthHistLonger.push(trail.size());
1283 if (!handle_conflict(confl)) {
1284 search_ret = l_False;
1285 goto end;
1286 }
1287 check_need_restart();
1288 check_need_gauss_jordan_disable();
1289 } else {
1290 assert(ok);
1291 #ifdef USE_GAUSS
1292 if (!all_matrices_disabled) {
1293 gauss_ret ret = gauss_jordan_elim();
1294 //cout << "ret: " << ret << " -- " << endl;
1295 if (ret == gauss_ret::g_cont) {
1296 //cout << "g_cont" << endl;
1297 check_need_restart();
1298 continue;
1299 }
1300
1301 if (ret == gauss_ret::g_false) {
1302 //cout << "g_false" << endl;
1303 search_ret = l_False;
1304 goto end;
1305 }
1306
1307 assert(ret == gauss_ret::g_nothing);
1308 }
1309 #endif //USE_GAUSS
1310
1311 if (decisionLevel() == 0) {
1312 clean_clauses_if_needed();
1313 }
1314 reduce_db_if_needed();
1315 lbool dec_ret = new_decision<false>();
1316 if (dec_ret != l_Undef) {
1317 search_ret = dec_ret;
1318 goto end;
1319 }
1320 }
1321 }
1322 max_confl_this_phase -= (int64_t)params.conflictsDoneThisRestart;
1323
1324 cancelUntil<true, false>(0);
1325 confl = propagate<false>();
1326 if (!confl.isNULL()) {
1327 ok = false;
1328 search_ret = l_False;
1329 goto end;
1330 }
1331 assert(solver->prop_at_head());
1332 if (!solver->datasync->syncData()) {
1333 search_ret = l_False;
1334 goto end;
1335 }
1336 search_ret = l_Undef;
1337
1338 end:
1339 dump_search_loop_stats(myTime);
1340 return search_ret;
1341 }
1342
update_branch_params()1343 inline void Searcher::update_branch_params()
1344 {
1345 if ((sumConflicts & 0xfff) == 0xfff &&
1346 var_decay < var_decay_max)
1347 {
1348 var_decay += 0.01;
1349 }
1350
1351 if (branch_strategy == branch::maple
1352 && maple_step_size > conf.min_step_size)
1353 {
1354 maple_step_size -= conf.step_size_dec;
1355 #ifdef VERBOSE_DEBUG
1356 cout << "maple step size is now: " << std::setprecision(7) << maple_step_size << endl;
1357 #endif
1358 }
1359 }
1360
dump_search_sql(const double myTime)1361 void Searcher::dump_search_sql(const double myTime)
1362 {
1363 if (solver->sqlStats) {
1364 solver->sqlStats->time_passed_min(
1365 solver
1366 , "search"
1367 , cpuTime()-myTime
1368 );
1369 }
1370 }
1371
1372 /**
1373 @brief Picks a new decision variable to branch on
1374
1375 @returns l_Undef if it should restart instead. l_False if it reached UNSAT
1376 (through simplification)
1377 */
1378 template<bool update_bogoprops>
new_decision()1379 lbool Searcher::new_decision()
1380 {
1381 #ifdef SLOW_DEBUG
1382 assert(solver->prop_at_head());
1383 #endif
1384 Lit next = lit_Undef;
1385 while (decisionLevel() < assumptions.size()) {
1386 // Perform user provided assumption:
1387 const Lit p = map_outer_to_inter(assumptions[decisionLevel()].lit_outer);
1388 #ifdef SLOW_DEBUG
1389 assert(varData[p.var()].removed == Removed::none);
1390 #endif
1391
1392 if (value(p) == l_True) {
1393 // Dummy decision level:
1394 new_decision_level();
1395 #ifdef USE_GAUSS
1396 for(uint32_t i = 0; i < gmatrices.size(); i++) {
1397 assert(gmatrices[i]);
1398 gmatrices[i]->new_decision_level(decisionLevel());
1399 }
1400 #endif
1401 } else if (value(p) == l_False) {
1402 analyze_final_confl_with_assumptions(~p, conflict);
1403 return l_False;
1404 } else {
1405 assert(p.var() < nVars());
1406 stats.decisionsAssump++;
1407 next = p;
1408 break;
1409 }
1410 }
1411
1412 if (next == lit_Undef) {
1413 // New variable decision:
1414 next = pickBranchLit();
1415
1416 //No decision taken, because it's SAT
1417 if (next == lit_Undef)
1418 return l_True;
1419
1420 //Update stats
1421 stats.decisions++;
1422 sumDecisions++;
1423 }
1424
1425 // Increase decision level and enqueue 'next'
1426 assert(value(next) == l_Undef);
1427 new_decision_level();
1428 #ifdef USE_GAUSS
1429 for(uint32_t i = 0; i < gmatrices.size(); i++) {
1430 assert(gmatrices[i]);
1431 gmatrices[i]->new_decision_level(decisionLevel());
1432 }
1433 #endif
1434 enqueue<update_bogoprops>(next);
1435
1436 return l_Undef;
1437 }
1438
update_history_stats(size_t backtrack_level,uint32_t glue)1439 void Searcher::update_history_stats(size_t backtrack_level, uint32_t glue)
1440 {
1441 assert(decisionLevel() > 0);
1442
1443 //short-term averages
1444 hist.branchDepthHist.push(decisionLevel());
1445 #if defined(STATS_NEEDED) || defined(FINAL_PREDICTOR)
1446 hist.backtrackLevelHist.push(backtrack_level);
1447 hist.branchDepthHistQueue.push(decisionLevel());
1448 hist.numResolutionsHist.push(antec_data.num());
1449 #endif
1450 hist.branchDepthDeltaHist.push(decisionLevel() - backtrack_level);
1451 hist.conflSizeHist.push(learnt_clause.size());
1452 hist.trailDepthDeltaHist.push(trail.size() - trail_lim[backtrack_level]);
1453
1454 //long-term averages
1455 #if defined(STATS_NEEDED) || defined(FINAL_PREDICTOR)
1456 hist.numResolutionsHistLT.push(antec_data.num());
1457 hist.decisionLevelHistLT.push(decisionLevel());
1458 const uint32_t overlap = antec_data.sum_size()-(antec_data.num()-1)-learnt_clause.size();
1459 hist.antec_data_sum_sizeHistLT.push(antec_data.sum_size());
1460 hist.overlapHistLT.push(overlap);
1461 #endif
1462 hist.backtrackLevelHistLT.push(backtrack_level);
1463 hist.conflSizeHistLT.push(learnt_clause.size());
1464 hist.trailDepthHistLT.push(trail.size());
1465 if (params.rest_type == Restart::glue) {
1466 hist.glueHistLTLimited.push(
1467 std::min<size_t>(glue, conf.max_glue_cutoff_gluehistltlimited));
1468 }
1469 hist.glueHistLT.push(glue);
1470 hist.glueHist.push(glue);
1471
1472 //Global stats from cnf.h
1473 sumClLBD += glue;
1474 sumClSize += learnt_clause.size();
1475 }
1476
1477 template<bool update_bogoprops>
attach_and_enqueue_learnt_clause(Clause * cl,const uint32_t level,const bool enq)1478 void Searcher::attach_and_enqueue_learnt_clause(
1479 Clause* cl, const uint32_t level, const bool enq)
1480 {
1481 switch (learnt_clause.size()) {
1482 case 0:
1483 assert(false);
1484 case 1:
1485 //Unitary learnt
1486 stats.learntUnits++;
1487 if (enq) enqueue(learnt_clause[0], level, PropBy());
1488
1489 #ifdef STATS_NEEDED
1490 propStats.propsUnit++;
1491 #endif
1492
1493 break;
1494 case 2:
1495 //Binary learnt
1496 stats.learntBins++;
1497 solver->datasync->signalNewBinClause(learnt_clause);
1498 solver->attach_bin_clause(learnt_clause[0], learnt_clause[1], true, enq);
1499 if (enq) enqueue(learnt_clause[0], level, PropBy(learnt_clause[1], true));
1500
1501 #ifdef STATS_NEEDED
1502 propStats.propsBinRed++;
1503 #endif
1504 break;
1505
1506 default:
1507 //Long learnt
1508 stats.learntLongs++;
1509 solver->attachClause(*cl, enq);
1510 if (enq) enqueue(learnt_clause[0], level, PropBy(cl_alloc.get_offset(cl)));
1511 #if defined(STATS_NEEDED) || defined(FINAL_PREDICTOR)
1512 bump_cl_act<update_bogoprops>(cl);
1513 #else
1514 if (cl->stats.which_red_array == 2) {
1515 bump_cl_act<update_bogoprops>(cl);
1516 }
1517 #endif
1518
1519
1520 #ifdef STATS_NEEDED
1521 cl->stats.antec_data = antec_data;
1522 propStats.propsLongRed++;
1523 #endif
1524
1525 break;
1526 }
1527 }
1528
print_learning_debug_info() const1529 inline void Searcher::print_learning_debug_info() const
1530 {
1531 #ifndef VERBOSE_DEBUG
1532 return;
1533 #else
1534 cout
1535 << "Learning:" << learnt_clause
1536 << endl
1537 << "reverting var " << learnt_clause[0].var()+1
1538 << " to " << !learnt_clause[0].sign()
1539 << endl;
1540 #endif
1541 }
1542
print_learnt_clause() const1543 void Searcher::print_learnt_clause() const
1544 {
1545 if (conf.verbosity >= 6) {
1546 cout
1547 << "c learnt clause: "
1548 ;
1549 for(Lit l: learnt_clause) {
1550 cout << l << ": " << value(l) << " ";
1551 }
1552 cout << endl;
1553 }
1554 }
1555
1556 #ifdef STATS_NEEDED
sql_dump_last_in_solver()1557 void Searcher::sql_dump_last_in_solver()
1558 {
1559 if (!sqlStats)
1560 return;
1561
1562 for(auto& red_cls: longRedCls) {
1563 for(auto& offs: red_cls) {
1564 Clause* cl = cl_alloc.ptr(offs);
1565 if (cl->stats.ID != 0) {
1566 sqlStats->cl_last_in_solver(solver, cl->stats.ID);
1567 }
1568 }
1569 }
1570 }
1571 #endif
1572
1573 #ifdef STATS_NEEDED_BRANCH
dump_var_for_learnt_cl(const uint32_t v,const uint64_t clid,const bool is_decision)1574 void Searcher::dump_var_for_learnt_cl(const uint32_t v,
1575 const uint64_t clid,
1576 const bool is_decision)
1577 {
1578 //When it's a decision clause, the REAL clause could have already
1579 //set some variable to having been propagated (due to asserting clause)
1580 //so this assert() no longer holds for all literals
1581 assert(is_decision || varData[v].reason == PropBy());
1582 if (varData[v].dump) {
1583 uint64_t outer_var = map_inter_to_outer(v);
1584 solver->sqlStats->dec_var_clid(
1585 outer_var
1586 , varData[v].sumConflicts_at_picktime
1587 , clid
1588 );
1589 }
1590 }
1591 #endif
1592
1593 #ifdef STATS_NEEDED
dump_sql_clause_data(const uint32_t orig_glue,const uint32_t glue_before_minim,const uint32_t old_decision_level,const uint64_t clid,const bool is_decision)1594 void Searcher::dump_sql_clause_data(
1595 const uint32_t orig_glue
1596 , const uint32_t glue_before_minim
1597 , const uint32_t old_decision_level
1598 , const uint64_t clid
1599 , const bool is_decision
1600 ) {
1601
1602 #ifdef STATS_NEEDED_BRANCH
1603 if (is_decision) {
1604 for(Lit l: learnt_clause) {
1605 dump_var_for_learnt_cl(l.var(), clid, is_decision);
1606 }
1607 } else {
1608 for(uint32_t v: vars_used_for_cl) {
1609 dump_var_for_learnt_cl(v, clid, is_decision);
1610 }
1611 }
1612 #endif
1613
1614 solver->sqlStats->dump_clause_stats(
1615 solver
1616 , clid
1617 , restartID
1618 , orig_glue
1619 , glue_before_minim
1620 , decisionLevel()
1621 , learnt_clause.size()
1622 , antec_data
1623 , old_decision_level
1624 , trail.size()
1625 , params.conflictsDoneThisRestart
1626 , restart_type_to_short_string(params.rest_type)
1627 , hist
1628 , is_decision
1629 );
1630 }
1631 #endif
1632
1633 #ifdef FINAL_PREDICTOR
set_clause_data(Clause * cl,const uint32_t orig_glue,const uint32_t glue_before_minim,const uint32_t old_decision_level)1634 void Searcher::set_clause_data(
1635 Clause* cl
1636 , const uint32_t orig_glue
1637 , const uint32_t glue_before_minim
1638 , const uint32_t old_decision_level
1639 ) {
1640
1641
1642 //definitely a BUG here I think -- should be 2*antec_data.num(), no?
1643 //however, it's the same as how it's dumped in sqlitestats.cpp
1644 // cl->stats.num_overlap_literals = antec_data.sum_size()-(antec_data.num()-1)-cl->size();
1645
1646
1647 // cl->stats.clust_f = clustering->which_is_closest(solver->last_solve_satzilla_feature);
1648 cl->stats.orig_glue = orig_glue;
1649 #ifdef EXTENDED_FEATURES
1650 cl->stats.glue_hist = hist.glueHistLT.avg();
1651 #endif
1652 cl->stats.confl_size_hist_lt = hist.conflSizeHistLT.avg();
1653 cl->stats.glue_hist_queue = hist.glueHist.getLongtTerm().avg();
1654 cl->stats.glue_hist_long = hist.glueHist.avg_nocheck();
1655
1656 cl->stats.num_antecedents = antec_data.num();
1657 cl->stats.antec_overlap_hist = hist.overlapHistLT.avg();
1658 cl->stats.num_total_lits_antecedents = antec_data.sum_size();
1659 cl->stats.branch_depth_hist_queue = hist.branchDepthHistQueue.avg_nocheck();
1660 cl->stats.num_resolutions_hist_lt = hist.numResolutionsHistLT.avg();
1661 cl->stats.glue_before_minim = glue_before_minim;
1662 // cl->stats.trail_depth_hist_longer = hist.trailDepthHistLonger.avg_nocheck();
1663 }
1664 #endif
1665
handle_last_confl(const uint32_t glue,const uint32_t old_decision_level,const uint32_t glue_before_minim,const bool is_decision)1666 Clause* Searcher::handle_last_confl(
1667 const uint32_t glue
1668 , const uint32_t old_decision_level
1669 , const uint32_t glue_before_minim
1670 , const bool is_decision
1671 ) {
1672 #ifdef STATS_NEEDED
1673 bool to_dump = false;
1674 double myrnd = mtrand.randDblExc();
1675 //Unfortunately, we have to change the ratio data dumped as time goes on
1676 //or we run out of space on CNFs that take millions(!) of conflicts
1677 //to solve, such as e_rphp035_05.cnf
1678 double decaying_ratio = (2000.0*1000.0)/((double)sumConflicts+1);
1679 if (decaying_ratio > 1.0) {
1680 decaying_ratio = 1.0;
1681 } else {
1682 //Make it more-than-linearly less
1683 decaying_ratio = ::pow(decaying_ratio, 1.3);
1684 }
1685 if (myrnd <= (conf.dump_individual_cldata_ratio*decaying_ratio)) {
1686 to_dump = true;
1687 if (sqlStats) {
1688 dump_restart_sql(rst_dat_type::cl, clauseID);
1689 }
1690 }
1691 #endif
1692
1693 Clause* cl;
1694 if (learnt_clause.size() <= 2) {
1695 *drat << add << learnt_clause
1696 #ifdef STATS_NEEDED
1697 << (to_dump ? clauseID : 0)
1698 << sumConflicts
1699 #endif
1700 << fin;
1701 cl = NULL;
1702 } else {
1703 cl = cl_alloc.Clause_new(learnt_clause
1704 , sumConflicts
1705 #ifdef STATS_NEEDED
1706 , to_dump ? clauseID : 0
1707 #endif
1708 );
1709 cl->makeRed(sumConflicts);
1710 cl->stats.glue = glue;
1711 #if defined(FINAL_PREDICTOR) || defined(STATS_NEEDED)
1712 cl->stats.orig_glue = glue;
1713 #endif
1714 cl->stats.activity = 0.0f;
1715 ClOffset offset = cl_alloc.get_offset(cl);
1716 unsigned which_arr = 2;
1717
1718 #ifdef STATS_NEEDED
1719 cl->stats.locked_for_data_gen =
1720 mtrand.randDblExc() < conf.lock_for_data_gen_ratio;
1721 #endif
1722
1723 if (cl->stats.locked_for_data_gen) {
1724 which_arr = 0;
1725 } else if (glue <= conf.glue_put_lev0_if_below_or_eq) {
1726 which_arr = 0;
1727 } else if (
1728 glue <= conf.glue_put_lev1_if_below_or_eq
1729 && conf.glue_put_lev1_if_below_or_eq != 0
1730 ) {
1731 which_arr = 1;
1732 } else {
1733 which_arr = 2;
1734 }
1735
1736 if (which_arr == 0) {
1737 stats.red_cl_in_which0++;
1738 }
1739
1740 cl->stats.which_red_array = which_arr;
1741 solver->longRedCls[cl->stats.which_red_array].push_back(offset);
1742
1743 *drat << add << *cl
1744 #ifdef STATS_NEEDED
1745 << sumConflicts
1746 #endif
1747 << fin;
1748 }
1749
1750 #ifdef STATS_NEEDED
1751 if (solver->sqlStats
1752 && drat
1753 && conf.dump_individual_restarts_and_clauses
1754 && to_dump
1755 ) {
1756 if (cl) {
1757 cl->stats.dump_no = 0;
1758 }
1759 dump_this_many_cldata_in_stream--;
1760 dump_sql_clause_data(
1761 glue
1762 , glue_before_minim
1763 , old_decision_level
1764 , clauseID
1765 , is_decision
1766 );
1767 }
1768
1769 if (to_dump) {
1770 clauseID++;
1771 }
1772 #endif
1773
1774 if (cl) {
1775 #ifdef FINAL_PREDICTOR
1776 set_clause_data(cl, glue, glue_before_minim, old_decision_level);
1777 cl->stats.dump_no = 0;
1778 #endif
1779 cl->stats.is_decision = is_decision;
1780 }
1781
1782 return cl;
1783 }
1784
handle_conflict(PropBy confl)1785 bool Searcher::handle_conflict(PropBy confl)
1786 {
1787 stats.conflStats.numConflicts++;
1788 hist.num_conflicts_this_restart++;
1789 sumConflicts++;
1790 params.conflictsDoneThisRestart++;
1791
1792 #ifndef FINAL_PREDICTOR
1793 if (sumConflicts == 100000 && //TODO magic constant
1794 longRedCls[0].size() < 100 &&
1795 //so that in case of some "standard-minisat behavriour" config
1796 //we don't override it
1797 conf.glue_put_lev0_if_below_or_eq != 0
1798 ) {
1799 conf.glue_put_lev0_if_below_or_eq += 2; //TODO magic constant
1800 }
1801 #endif
1802
1803 ConflictData data = find_conflict_level(confl);
1804 if (data.nHighestLevel == 0) {
1805 return false;
1806 }
1807
1808 uint32_t backtrack_level;
1809 uint32_t glue;
1810 uint32_t glue_before_minim;
1811 analyze_conflict<false>(
1812 confl
1813 , backtrack_level //return backtrack level here
1814 , glue //return glue here
1815 , glue_before_minim //return glue before minimization here
1816 );
1817 print_learnt_clause();
1818
1819 update_history_stats(backtrack_level, glue);
1820 uint32_t old_decision_level = decisionLevel();
1821
1822 //Add decision-based clause in case it's short
1823 decision_clause.clear();
1824 if (conf.do_decision_based_cl
1825 && learnt_clause.size() > conf.decision_based_cl_min_learned_size
1826 && decisionLevel() <= conf.decision_based_cl_max_levels
1827 && decisionLevel() >= 2
1828 ) {
1829 for(int i = (int)trail_lim.size()-1; i >= 0; i--) {
1830 Lit l = ~trail[trail_lim[i]].lit;
1831 if (!seen[l.toInt()]) {
1832 decision_clause.push_back(l);
1833 seen[l.toInt()] = 1;
1834 }
1835 }
1836 for(Lit l: decision_clause) {
1837 seen[l.toInt()] = 0;
1838 assert(varData[l.var()].reason == PropBy());
1839 }
1840 }
1841
1842 // check chrono backtrack condition
1843 if (conf.diff_declev_for_chrono > -1
1844 && (((int)decisionLevel() - (int)backtrack_level) >= conf.diff_declev_for_chrono)
1845 ) {
1846 chrono_backtrack++;
1847 cancelUntil(data.nHighestLevel -1);
1848 } else {
1849 non_chrono_backtrack++;
1850 cancelUntil(backtrack_level);
1851 }
1852
1853 print_learning_debug_info();
1854 assert(value(learnt_clause[0]) == l_Undef);
1855 glue = std::min<uint32_t>(glue, std::numeric_limits<uint32_t>::max());
1856 Clause* cl = handle_last_confl(glue, old_decision_level, glue_before_minim, false);
1857 attach_and_enqueue_learnt_clause<false>(cl, backtrack_level, true);
1858
1859 //Add decision-based clause
1860 if (decision_clause.size() > 0) {
1861 int i = decision_clause.size();
1862 while(--i >= 0) {
1863 if (value(decision_clause[i]) == l_True
1864 || value(decision_clause[i]) == l_Undef
1865 ) {
1866 break;
1867 }
1868 }
1869 std::swap(decision_clause[0], decision_clause[i]);
1870
1871 learnt_clause = decision_clause;
1872 print_learnt_clause();
1873 cl = handle_last_confl(learnt_clause.size(), old_decision_level, learnt_clause.size(), true);
1874 attach_and_enqueue_learnt_clause<false>(cl, backtrack_level, false);
1875 }
1876
1877 if (branch_strategy == branch::vsids) {
1878 vsids_decay_var_act();
1879 }
1880 decayClauseAct<false>();
1881
1882 return true;
1883 }
1884
resetStats()1885 void Searcher::resetStats()
1886 {
1887 startTime = cpuTime();
1888
1889 //Rest solving stats
1890 stats.clear();
1891 propStats.clear();
1892 #ifdef STATS_NEEDED
1893 lastSQLPropStats = propStats;
1894 lastSQLGlobalStats = stats;
1895 #endif
1896
1897 lastCleanZeroDepthAssigns = trail.size();
1898 }
1899
check_calc_satzilla_features(bool force)1900 void Searcher::check_calc_satzilla_features(bool force)
1901 {
1902 #ifdef STATS_NEEDED
1903 if (last_satzilla_feature_calc_confl == 0
1904 || (last_satzilla_feature_calc_confl + 10000) < sumConflicts
1905 || force
1906 ) {
1907 last_satzilla_feature_calc_confl = sumConflicts+1;
1908 if (nVars() > 2
1909 && longIrredCls.size() > 1
1910 && (binTri.irredBins + binTri.redBins) > 1
1911 ) {
1912 solver->last_solve_satzilla_feature = solver->calculate_satzilla_features();
1913 }
1914 }
1915 #endif
1916 }
1917
check_calc_vardist_features(bool force)1918 void Searcher::check_calc_vardist_features(bool force)
1919 {
1920 if (!solver->sqlStats) {
1921 return;
1922 }
1923
1924 #ifdef STATS_NEEDED_BRANCH
1925 if (last_vardist_feature_calc_confl == 0
1926 || (last_vardist_feature_calc_confl + 10000) < sumConflicts
1927 || force
1928 ) {
1929 last_vardist_feature_calc_confl = sumConflicts+1;
1930 VarDistGen v(solver);
1931 v.calc();
1932 latest_vardist_feature_calc++;
1933 v.dump();
1934 }
1935 #endif
1936 }
1937
print_restart_header()1938 void Searcher::print_restart_header()
1939 {
1940 //Print restart output header
1941 if (((lastRestartPrintHeader == 0 && sumConflicts > 200) ||
1942 (lastRestartPrintHeader + 1600000) < sumConflicts)
1943 && conf.verbosity
1944 ) {
1945 cout
1946 << "c"
1947 << " " << std::setw(4) << "res"
1948 << " " << std::setw(4) << "pol"
1949 << " " << std::setw(4) << "bran"
1950 << " " << std::setw(5) << "nres"
1951 << " " << std::setw(5) << "conf"
1952 << " " << std::setw(5) << "freevar"
1953 << " " << std::setw(5) << "IrrL"
1954 << " " << std::setw(5) << "IrrB"
1955 << " " << std::setw(7) << "l/longC"
1956 << " " << std::setw(7) << "l/allC";
1957
1958 for(size_t i = 0; i < longRedCls.size(); i++) {
1959 cout << " " << std::setw(4) << "RedL" << i;
1960 }
1961
1962 cout
1963 << " " << std::setw(5) << "RedB"
1964 << " " << std::setw(7) << "l/longC"
1965 << " " << std::setw(7) << "l/allC"
1966 << endl;
1967 lastRestartPrintHeader = sumConflicts+1;
1968 }
1969 }
1970
print_restart_stat_line() const1971 void Searcher::print_restart_stat_line() const
1972 {
1973 print_restart_stats_base();
1974 if (conf.print_full_restart_stat) {
1975 solver->print_clause_stats();
1976 hist.print();
1977 } else {
1978 solver->print_clause_stats();
1979 }
1980
1981 cout << endl;
1982 }
1983
print_restart_stats_base() const1984 void Searcher::print_restart_stats_base() const
1985 {
1986 cout << "c"
1987 << " " << std::setw(4) << restart_type_to_short_string(params.rest_type)
1988 << " " << std::setw(4) << polarity_mode_to_short_string(polarity_mode)
1989 << " " << std::setw(4) << branch_strategy_str_short
1990 << " " << std::setw(5) << sumRestarts();
1991
1992 if (sumConflicts > 20000) {
1993 cout << " " << std::setw(4) << sumConflicts/1000 << "K";
1994 } else {
1995 cout << " " << std::setw(5) << sumConflicts;
1996 }
1997
1998 cout << " " << std::setw(7) << solver->get_num_free_vars();
1999 }
2000
2001 struct MyInvSorter {
operator ()MyInvSorter2002 bool operator()(size_t num, size_t num2)
2003 {
2004 return num > num2;
2005 }
2006 };
2007
2008 struct MyPolarData
2009 {
MyPolarDataMyPolarData2010 MyPolarData (size_t _pos, size_t _neg, size_t _flipped) :
2011 pos(_pos)
2012 , neg(_neg)
2013 , flipped(_flipped)
2014 {}
2015
2016 size_t pos;
2017 size_t neg;
2018 size_t flipped;
2019
operator <MyPolarData2020 bool operator<(const MyPolarData& other) const
2021 {
2022 return (pos + neg) > (other.pos + other.neg);
2023 }
2024 };
2025
2026 #ifdef STATS_NEEDED
dump_restart_sql(rst_dat_type type,int64_t clauseID)2027 inline void Searcher::dump_restart_sql(rst_dat_type type, int64_t clauseID)
2028 {
2029 //don't dump twice for var
2030 if (type == rst_dat_type::var) {
2031 if (last_dumped_conflict_rst_data_for_var == solver->sumConflicts) {
2032 return;
2033 }
2034 last_dumped_conflict_rst_data_for_var = solver->sumConflicts;
2035 }
2036
2037 //Propagation stats
2038 PropStats thisPropStats = propStats - lastSQLPropStats;
2039 SearchStats thisStats = stats - lastSQLGlobalStats;
2040 solver->sqlStats->restart(
2041 restartID
2042 , params.rest_type
2043 , thisPropStats
2044 , thisStats
2045 , solver
2046 , this
2047 , type
2048 , (int64_t)clauseID
2049 );
2050
2051 if (type == rst_dat_type::norm) {
2052 lastSQLPropStats = propStats;
2053 lastSQLGlobalStats = stats;
2054 }
2055 }
2056 #endif
2057
print_restart_stat()2058 void Searcher::print_restart_stat()
2059 {
2060 //Print restart stat
2061 if (conf.verbosity
2062 && !conf.print_all_restarts
2063 && ((lastRestartPrint + conf.print_restart_line_every_n_confl)
2064 < sumConflicts)
2065 ) {
2066 print_restart_stat_line();
2067 lastRestartPrint = sumConflicts;
2068 }
2069 }
2070
reset_temp_cl_num()2071 void Searcher::reset_temp_cl_num()
2072 {
2073 cur_max_temp_red_lev2_cls = conf.max_temp_lev2_learnt_clauses;
2074 }
2075
reduce_db_if_needed()2076 void Searcher::reduce_db_if_needed()
2077 {
2078 #if defined(FINAL_PREDICTOR) || defined(STATS_NEEDED)
2079 if (conf.every_lev3_reduce != 0
2080 && sumConflicts >= next_lev3_reduce
2081 ) {
2082 #ifdef STATS_NEEDED
2083 if (solver->sqlStats) {
2084 solver->reduceDB->dump_sql_cl_data(restart_type_to_short_string(params.rest_type));
2085 }
2086 #endif
2087 #ifdef FINAL_PREDICTOR
2088 solver->reduceDB->handle_lev2_predictor();
2089 cl_alloc.consolidate(solver);
2090 #endif
2091 next_lev3_reduce = sumConflicts + conf.every_lev3_reduce;
2092 }
2093 #endif
2094
2095 #ifndef FINAL_PREDICTOR
2096 if (conf.every_lev1_reduce != 0
2097 && sumConflicts >= next_lev1_reduce
2098 ) {
2099 solver->reduceDB->handle_lev1();
2100 next_lev1_reduce = sumConflicts + conf.every_lev1_reduce;
2101 }
2102
2103 if (conf.every_lev2_reduce != 0) {
2104 if (sumConflicts >= next_lev2_reduce) {
2105 solver->reduceDB->handle_lev2();
2106 cl_alloc.consolidate(solver);
2107 next_lev2_reduce = sumConflicts + conf.every_lev2_reduce;
2108 }
2109 } else {
2110 if (longRedCls[2].size() > cur_max_temp_red_lev2_cls) {
2111 solver->reduceDB->handle_lev2();
2112 cur_max_temp_red_lev2_cls *= conf.inc_max_temp_lev2_red_cls;
2113 cl_alloc.consolidate(solver);
2114 }
2115 }
2116 #endif
2117 }
2118
clean_clauses_if_needed()2119 void Searcher::clean_clauses_if_needed()
2120 {
2121 #ifdef SLOW_DEBUG
2122 assert(decisionLevel() == 0);
2123 assert(qhead == trail.size());
2124 #endif
2125
2126 const size_t newZeroDepthAss = trail.size() - lastCleanZeroDepthAssigns;
2127 if (newZeroDepthAss > 0
2128 && simpDB_props < 0
2129 && newZeroDepthAss > ((double)nVars()*0.05)
2130 ) {
2131 if (conf.verbosity >= 2) {
2132 cout << "c newZeroDepthAss : " << newZeroDepthAss
2133 << " -- "
2134 << (double)newZeroDepthAss/(double)nVars()*100.0
2135 << " % of active vars"
2136 << endl;
2137 }
2138 lastCleanZeroDepthAssigns = trail.size();
2139 solver->clauseCleaner->remove_and_clean_all();
2140
2141 cl_alloc.consolidate(solver);
2142 //TODO this is not needed, but seems to help speed
2143 // perhaps because it re-shuffles
2144 rebuildOrderHeap();
2145
2146 simpDB_props = (litStats.redLits + litStats.irredLits)<<5;
2147 }
2148 }
2149
rebuildOrderHeap()2150 void Searcher::rebuildOrderHeap()
2151 {
2152 if (conf.verbosity) {
2153 cout << "c [branch] rebuilding order heap for all branchings. Current branching: " <<
2154 branch_type_to_string(branch_strategy) << endl;
2155 }
2156 vector<uint32_t> vs;
2157 vs.reserve(nVars());
2158 for (uint32_t v = 0; v < nVars(); v++) {
2159 if (varData[v].removed != Removed::none
2160 //NOTE: the level==0 check is needed because SLS calls this
2161 //when there is a solution already, but we should only skip
2162 //level 0 assignments
2163 || (value(v) != l_Undef && varData[v].level == 0)
2164 ) {
2165 continue;
2166 } else {
2167 vs.push_back(v);
2168 }
2169 }
2170
2171 #ifdef VERBOSE_DEBUG
2172 cout << "c [branch] Building VSDIS order heap" << endl;
2173 #endif
2174 order_heap_vsids.build(vs);
2175
2176 #ifdef VERBOSE_DEBUG
2177 cout << "c [branch] Building MAPLE order heap" << endl;
2178 #endif
2179 order_heap_maple.build(vs);
2180
2181 #ifdef VERBOSE_DEBUG
2182 cout << "c [branch] Building RND order heap" << endl;
2183 #endif
2184
2185 #ifdef VMTF_NEEDED
2186 rebuildOrderHeapVMTF();
2187 #endif
2188 }
2189
2190 #ifdef VMTF_NEEDED
rebuildOrderHeapVMTF()2191 void Searcher::rebuildOrderHeapVMTF()
2192 {
2193 #ifdef VERBOSE_DEBUG
2194 cout << "c [branch] Building VMTF order heap" << endl;
2195 #endif
2196 //TODO fix
2197 return;
2198
2199 vector<uint32_t> vs;
2200 vs.reserve(nVars());
2201 uint32_t v = pick_var_vmtf();
2202 while(v != var_Undef) {
2203 if (varData[v].removed != Removed::none
2204 //NOTE: the level==0 check is needed because SLS calls this
2205 //when there is a solution already, but we should only skip
2206 //level 0 assignements
2207 || (value(v) != l_Undef && varData[v].level == 0)
2208 ) {
2209 //
2210 } else {
2211 vs.push_back(v);
2212 }
2213 v = pick_var_vmtf();
2214 cout << "v: " << v << endl;
2215 }
2216
2217 //Clear it out
2218 vmtf_queue = Queue();
2219 vmtf_btab.clear();
2220 vmtf_links.clear();
2221 vmtf_btab.insert(vmtf_btab.end(), nVars(), 0);
2222 vmtf_links.insert(vmtf_links.end(), nVars(), Link());
2223
2224 //Insert in reverse order
2225 for(int i = (int)vs.size()-1; i >= 0; i--) {
2226 vmtf_init_enqueue(vs[v]);
2227 }
2228 }
2229 #endif
2230
2231 struct branch_type_total{
branch_type_totalbranch_type_total2232 branch_type_total() {}
branch_type_totalbranch_type_total2233 branch_type_total (CMSat::branch _branch,
2234 double _decay_start, double _decay_max,
2235 string _descr, string _descr_short) :
2236 branch(_branch),
2237 decay_start(_decay_start),
2238 decay_max(_decay_max),
2239 descr(_descr),
2240 descr_short(_descr_short)
2241 {}
branch_type_totalbranch_type_total2242 explicit branch_type_total(CMSat::branch _branch) :
2243 branch(_branch)
2244 {}
2245
2246 CMSat::branch branch = CMSat::branch::vsids;
2247 double decay_start = 0.95;
2248 double decay_max = 0.95;
2249 string descr;
2250 string descr_short;
2251 };
2252
set_branch_strategy(uint32_t iteration_num)2253 void Searcher::set_branch_strategy(uint32_t iteration_num)
2254 {
2255 if (iteration_num == 0) {
2256 branch_strategy = branch::vsids;
2257 cur_rest_type = conf.restartType;
2258 var_decay = 0.80;
2259 var_decay_max = 0.95;
2260 return;
2261 }
2262 iteration_num--;
2263
2264 size_t smallest = 0;
2265 size_t start = 0;
2266 size_t total = 0;
2267 branch_type_total select[20];
2268 if (conf.verbosity) {
2269 if (conf.verbosity >= 2) {
2270 cout << "c [branch] orig text: " << conf.branch_strategy_setup << endl;
2271 }
2272 cout << "c [branch] selection: ";
2273 }
2274
2275 while(smallest !=std::string::npos) {
2276 smallest = std::string::npos;
2277
2278 size_t vsidsx = conf.branch_strategy_setup.find("vsidsx", start);
2279 smallest = std::min(vsidsx, smallest);
2280
2281 size_t vsids1 = conf.branch_strategy_setup.find("vsids1", start);
2282 smallest = std::min(vsids1, smallest);
2283
2284 size_t vsids2 = conf.branch_strategy_setup.find("vsids2", start);
2285 smallest = std::min(vsids2, smallest);
2286
2287 #ifdef VMTF_NEEDED
2288 size_t vmtf = conf.branch_strategy_setup.find("vmtf", start);
2289 smallest = std::min(vmtf, smallest);
2290 #endif
2291
2292 size_t maple1 = conf.branch_strategy_setup.find("maple1", start);
2293 smallest = std::min(maple1, smallest);
2294
2295 size_t maple2 = conf.branch_strategy_setup.find("maple2", start);
2296 smallest = std::min(maple2, smallest);
2297
2298 if (smallest == std::string::npos) {
2299 break;
2300 }
2301
2302 if (conf.verbosity && total > 0) {
2303 cout << "+";
2304 }
2305
2306 if (smallest == vsidsx) {
2307 select[total++]= branch_type_total(branch::vsids, 0.80, 0.95, "VSIDSX", "vsx");
2308 if (conf.verbosity) {
2309 cout << select[total-1].descr;
2310 }
2311 }
2312 else if (smallest == vsids1) {
2313 select[total++]= branch_type_total(branch::vsids, 0.92, 0.92, "VSIDS1", "vs1");
2314 if (conf.verbosity) {
2315 cout << select[total-1].descr;
2316 }
2317 }
2318 else if (smallest == vsids2) {
2319 select[total++]= branch_type_total(branch::vsids, 0.99, 0.99, "VSIDS2", "vs2");
2320 if (conf.verbosity) {
2321 cout << select[total-1].descr;
2322 }
2323 }
2324 #ifdef VMTF_NEEDED
2325 else if (smallest == vmtf) {
2326 select[total++]= branch_type_total(branch::vmtf, 0, 0, "VMTF", "vmt");
2327 if (conf.verbosity) {
2328 cout << select[total-1].descr;
2329 }
2330 }
2331 #endif
2332 else if (smallest == maple1) {
2333 //TODO should we do this incremental stuff?
2334 //maple_step_size = conf.orig_step_size;
2335 select[total++]= branch_type_total(branch::maple, 0.70, 0.70, "MAPLE1", "mp1");
2336 if (conf.verbosity) {
2337 cout << select[total-1].descr;
2338 }
2339 }
2340 else if (smallest == maple2) {
2341 //TODO should we do this incremental stuff?
2342 //maple_step_size = conf.orig_step_size;
2343 select[total++]= branch_type_total(branch::maple, 0.90, 0.90, "MAPLE2", "mp2");
2344 if (conf.verbosity) {
2345 cout << select[total-1].descr;
2346 }
2347 } else {
2348 assert(false);
2349 }
2350
2351 //Search for next one. The strings are quite distinct, this works.
2352 start = smallest + 3;
2353
2354 if (total >= 20) {
2355 cout << "ERROR: you cannot give more than 19 branch strategies" << endl;
2356 exit(-1);
2357 }
2358 }
2359 if (conf.verbosity) {
2360 cout << " -- total: " << total << endl;
2361 }
2362
2363 assert(total > 0);
2364 uint32_t which = iteration_num % total;
2365 branch_strategy = select[which].branch;
2366 branch_strategy_str = select[which].descr;
2367 branch_strategy_str_short = select[which].descr_short;
2368 var_decay = select[which].decay_start;
2369 var_decay_max = select[which].decay_max;
2370
2371 if (branch_strategy == branch::maple) {
2372 cur_rest_type = Restart::luby;
2373 } else {
2374 cur_rest_type = conf.restartType;
2375 }
2376
2377 if (conf.verbosity) {
2378 cout << "c [branch] adjusting to: "
2379 << branch_type_to_string(branch_strategy)
2380 << " var_decay_max:" << var_decay << " var_decay:" << var_decay
2381 << " descr: " << select[which].descr
2382 << endl;
2383 }
2384 }
2385
dump_search_loop_stats(double myTime)2386 inline void Searcher::dump_search_loop_stats(double myTime)
2387 {
2388 #if defined(STATS_NEEDED) || defined(FINAL_PREDICTOR)
2389 check_calc_satzilla_features();
2390 check_calc_vardist_features();
2391 #endif
2392
2393 print_restart_header();
2394 dump_search_sql(myTime);
2395 if (conf.verbosity && conf.print_all_restarts) {
2396 print_restart_stat_line();
2397 }
2398 #ifdef STATS_NEEDED
2399 if (sqlStats
2400 && conf.dump_individual_restarts_and_clauses
2401 ) {
2402 dump_restart_sql(rst_dat_type::norm);
2403 }
2404 #endif
2405 restartID++;
2406 }
2407
must_abort(const lbool status)2408 bool Searcher::must_abort(const lbool status) {
2409 if (status != l_Undef) {
2410 if (conf.verbosity >= 6) {
2411 cout
2412 << "c Returned status of search() is " << status << " at confl:"
2413 << sumConflicts
2414 << endl;
2415 }
2416 return true;
2417 }
2418
2419 if (stats.conflStats.numConflicts >= max_confl_per_search_solve_call) {
2420 if (conf.verbosity >= 3) {
2421 cout
2422 << "c search over max conflicts"
2423 << endl;
2424 }
2425 return true;
2426 }
2427
2428 if (cpuTime() >= conf.maxTime) {
2429 if (conf.verbosity >= 3) {
2430 cout
2431 << "c search over max time"
2432 << endl;
2433 }
2434 return true;
2435 }
2436
2437 if (solver->must_interrupt_asap()) {
2438 if (conf.verbosity >= 3) {
2439 cout
2440 << "c search interrupting as requested"
2441 << endl;
2442 }
2443 return true;
2444 }
2445
2446 return false;
2447 }
2448
setup_polarity_strategy()2449 void Searcher::setup_polarity_strategy()
2450 {
2451 //Set to default first
2452 polarity_mode = conf.polarity_mode;
2453 polar_stable_longest_trail_this_iter = 0;
2454
2455 if (polarity_mode == PolarityMode::polarmode_automatic) {
2456 if (branch_strategy_num > 0 &&
2457 conf.polar_stable_every_n > 0 &&
2458 ((branch_strategy_num % (conf.polar_stable_every_n*conf.polar_best_inv_multip_n)) == 0))
2459 {
2460 polarity_mode = PolarityMode::polarmode_best_inv;
2461 }
2462 }
2463
2464 if (polarity_mode == PolarityMode::polarmode_automatic) {
2465 if (branch_strategy_num > 0 &&
2466 conf.polar_stable_every_n > 0 &&
2467 ((branch_strategy_num % (conf.polar_stable_every_n*conf.polar_best_multip_n)) == 0))
2468 {
2469 polarity_mode = PolarityMode::polarmode_best;
2470 }
2471 }
2472
2473 //Stable polarities only make sense in case of automatic polarities
2474 if (polarity_mode == PolarityMode::polarmode_automatic) {
2475 if (
2476 (branch_strategy_num > 0 &&
2477 conf.polar_stable_every_n > 0 &&
2478 ((branch_strategy_num % conf.polar_stable_every_n) == 0)) ||
2479
2480 conf.polar_stable_every_n == 0 ||
2481
2482 (conf.polar_stable_every_n == -1 &&
2483 branch_strategy == branch::vsids) ||
2484
2485 (conf.polar_stable_every_n == -2 &&
2486 branch_strategy == branch::maple) ||
2487
2488 (conf.polar_stable_every_n == -3 &&
2489 branch_strategy_str == "VSIDS1") ||
2490
2491 (conf.polar_stable_every_n == -4 &&
2492 branch_strategy_str == "VSIDS2") ||
2493
2494 (conf.polar_stable_every_n == -5 &&
2495 branch_strategy_str == "MAPLE1") ||
2496
2497 (conf.polar_stable_every_n == -6 &&
2498 branch_strategy_str == "MAPLE2"))
2499 {
2500 polarity_mode = PolarityMode::polarmode_stable;
2501
2502 }
2503 }
2504
2505 if (conf.verbosity) {
2506 cout << "c [polar]"
2507 << " polar mode: " << getNameOfPolarmodeType(polarity_mode)
2508 << " branch strategy num: " << branch_strategy_num
2509 << " branch strategy: " << branch_strategy_str
2510
2511 << endl;
2512 }
2513 }
2514
solve(const uint64_t _max_confls)2515 lbool Searcher::solve(
2516 const uint64_t _max_confls
2517 ) {
2518 assert(ok);
2519 assert(qhead == trail.size());
2520 max_confl_per_search_solve_call = _max_confls;
2521 num_search_called++;
2522 #ifdef SLOW_DEBUG
2523 //When asking for a lot of simple soluitons, search() gets called a lot
2524 check_no_removed_or_freed_cl_in_watch();
2525 #endif
2526
2527 if (conf.verbosity >= 6) {
2528 cout
2529 << "c Searcher::solve() called"
2530 << endl;
2531 }
2532
2533 resetStats();
2534 lbool status = l_Undef;
2535
2536 set_branch_strategy(branch_strategy_num);
2537 setup_restart_strategy();
2538 check_calc_satzilla_features(true);
2539 check_calc_vardist_features(true);
2540 setup_polarity_strategy();
2541
2542 while(stats.conflStats.numConflicts < max_confl_per_search_solve_call
2543 && status == l_Undef
2544 ) {
2545 #ifdef SLOW_DEBUG
2546 assert(solver->check_order_heap_sanity());
2547 #endif
2548
2549 assert(watches.get_smudged_list().empty());
2550 params.clear();
2551 params.max_confl_to_do = max_confl_per_search_solve_call-stats.conflStats.numConflicts;
2552 status = search();
2553 if (status == l_Undef) {
2554 adjust_restart_strategy();
2555 }
2556
2557 if (must_abort(status)) {
2558 goto end;
2559 }
2560
2561 if (status == l_Undef &&
2562 conf.do_distill_clauses &&
2563 sumConflicts > next_distill
2564 ) {
2565 if (!solver->distill_long_cls->distill(true, false)) {
2566 status = l_False;
2567 goto end;
2568 }
2569 next_distill = std::min<double>(
2570 sumConflicts + sumConflicts * conf.distill_increase_conf_ratio + 7000,
2571 sumConflicts + conf.distill_min_confl);
2572 }
2573 }
2574
2575 end:
2576 finish_up_solve(status);
2577 if (status == l_Undef) {
2578 branch_strategy_num++;
2579 }
2580
2581 return status;
2582 }
2583
luby(double y,int x)2584 double Searcher::luby(double y, int x)
2585 {
2586 int size = 1;
2587 int seq;
2588 for (seq = 0
2589 ; size < x + 1
2590 ; seq++
2591 ) {
2592 size = 2 * size + 1;
2593 }
2594
2595 while (size - 1 != x) {
2596 size = (size - 1) >> 1;
2597 seq--;
2598 x = x % size;
2599 }
2600
2601 return std::pow(y, seq);
2602 }
2603
setup_restart_strategy()2604 void Searcher::setup_restart_strategy()
2605 {
2606 // if (conf.verbosity) {
2607 // cout << "c [restart] strategy: "
2608 // << restart_type_to_string(cur_rest_type)
2609 // << endl;
2610 // }
2611
2612 increasing_phase_size = conf.restart_first;
2613 max_confl_this_phase = conf.restart_first;
2614 switch(cur_rest_type) {
2615 case Restart::glue:
2616 params.rest_type = Restart::glue;
2617 break;
2618
2619 case Restart::geom:
2620 params.rest_type = Restart::geom;
2621 break;
2622
2623 case Restart::glue_geom:
2624 params.rest_type = Restart::glue;
2625 break;
2626
2627 case Restart::luby:
2628 params.rest_type = Restart::luby;
2629 break;
2630
2631 case Restart::never:
2632 params.rest_type = Restart::never;
2633 break;
2634 }
2635
2636 print_local_restart_budget();
2637 }
2638
adjust_restart_strategy()2639 void Searcher::adjust_restart_strategy()
2640 {
2641 //Haven't finished the phase. Keep rolling.
2642 if (max_confl_this_phase > 0)
2643 return;
2644
2645 //Note that all of this will be overridden by params.max_confl_to_do
2646 switch(cur_rest_type) {
2647 case Restart::never:
2648 break;
2649
2650 case Restart::glue:
2651 params.rest_type = Restart::glue;
2652 break;
2653
2654 case Restart::geom:
2655 params.rest_type = Restart::geom;
2656 break;
2657
2658 case Restart::luby:
2659 params.rest_type = Restart::luby;
2660 break;
2661
2662 case Restart::glue_geom:
2663 if (params.rest_type == Restart::glue) {
2664 params.rest_type = Restart::geom;
2665 } else {
2666 params.rest_type = Restart::glue;
2667 }
2668 break;
2669 }
2670
2671 switch (params.rest_type) {
2672 //max_confl_this_phase -- for this phase of search
2673 //increasing_phase_size - a value that rolls and increases
2674 // it's start at conf.restart_first and never
2675 // reset
2676 case Restart::luby:
2677 max_confl_this_phase = luby(2, luby_loop_num) * (double)conf.restart_first;
2678 luby_loop_num++;
2679 break;
2680
2681 case Restart::geom:
2682 increasing_phase_size = (double)increasing_phase_size * conf.restart_inc;
2683 max_confl_this_phase = increasing_phase_size;
2684 break;
2685
2686 case Restart::glue:
2687 max_confl_this_phase = conf.ratio_glue_geom *increasing_phase_size;
2688 break;
2689
2690 default:
2691 release_assert(false);
2692 }
2693
2694 print_local_restart_budget();
2695 }
2696
print_local_restart_budget()2697 inline void Searcher::print_local_restart_budget()
2698 {
2699 if (conf.verbosity >= 2 || conf.print_all_restarts) {
2700 cout << "c [restart] at confl " << solver->sumConflicts << " -- "
2701 << "adjusting local restart type: "
2702 << std::left << std::setw(10) << getNameOfRestartType(params.rest_type)
2703 << " budget: " << std::setw(9) << max_confl_this_phase
2704 << std::right
2705 << " maple step_size: " << maple_step_size
2706 << " branching: " << std::setw(2) << branch_type_to_string(branch_strategy)
2707 << " decay: "
2708 << std::setw(4) << std::setprecision(4) << var_decay
2709 << endl;
2710 }
2711 }
2712
check_need_restart()2713 void Searcher::check_need_restart()
2714 {
2715 if ((stats.conflStats.numConflicts & 0xff) == 0xff) {
2716 //It's expensive to check the time all the time
2717 if (cpuTime() > conf.maxTime) {
2718 params.needToStopSearch = true;
2719 }
2720
2721 if (must_interrupt_asap()) {
2722 if (conf.verbosity >= 3)
2723 cout << "c must_interrupt_asap() is set, restartig as soon as possible!" << endl;
2724 params.needToStopSearch = true;
2725 }
2726 }
2727
2728 assert(params.rest_type != Restart::glue_geom);
2729
2730 //dynamic
2731 if (params.rest_type == Restart::glue) {
2732 check_blocking_restart();
2733 if (hist.glueHist.isvalid()
2734 && conf.local_glue_multiplier * hist.glueHist.avg() > hist.glueHistLTLimited.avg()
2735 ) {
2736 params.needToStopSearch = true;
2737 }
2738 }
2739
2740 //respect restart phase's limit
2741 if ((int64_t)params.conflictsDoneThisRestart > max_confl_this_phase) {
2742 params.needToStopSearch = true;
2743 }
2744
2745 //respect Searcher's limit
2746 if (params.conflictsDoneThisRestart > params.max_confl_to_do) {
2747 if (conf.verbosity >= 3) {
2748 cout
2749 << "c Over limit of conflicts for this restart"
2750 << " -- restarting as soon as possible!" << endl;
2751 }
2752 params.needToStopSearch = true;
2753 }
2754
2755 #ifdef VERBOSE_DEBUG
2756 if (params.needToStopSearch) {
2757 cout << "c needToStopSearch set" << endl;
2758 }
2759 #endif
2760 }
2761
print_solution_varreplace_status() const2762 void Searcher::print_solution_varreplace_status() const
2763 {
2764 for(size_t var = 0; var < nVarsOuter(); var++) {
2765 if (varData[var].removed == Removed::replaced
2766 || varData[var].removed == Removed::elimed
2767 ) {
2768 assert(value(var) == l_Undef || varData[var].level == 0);
2769 }
2770
2771 if (conf.verbosity >= 6
2772 && varData[var].removed == Removed::replaced
2773 && value(var) != l_Undef
2774 ) {
2775 cout
2776 << "var: " << var
2777 << " value: " << value(var)
2778 << " level:" << varData[var].level
2779 << " type: " << removed_type_to_string(varData[var].removed)
2780 << endl;
2781 }
2782 }
2783 }
2784
print_solution_type(const lbool status) const2785 void Searcher::print_solution_type(const lbool status) const
2786 {
2787 if (conf.verbosity >= 6) {
2788 if (status == l_True) {
2789 cout << "Solution from Searcher is SAT" << endl;
2790 } else if (status == l_False) {
2791 cout << "Solution from Searcher is UNSAT" << endl;
2792 cout << "OK is: " << okay() << endl;
2793 } else {
2794 cout << "Solutions from Searcher is UNKNOWN" << endl;
2795 }
2796 }
2797 }
2798
finish_up_solve(const lbool status)2799 void Searcher::finish_up_solve(const lbool status)
2800 {
2801 print_solution_type(status);
2802 #ifdef USE_GAUSS
2803 if (conf.verbosity >= 1 && status != l_Undef) {
2804 print_matrix_stats();
2805 }
2806 #endif
2807
2808 if (status == l_True) {
2809 #ifdef SLOW_DEBUG
2810 check_order_heap_sanity();
2811 #endif
2812 assert(solver->prop_at_head());
2813 model = assigns;
2814 cancelUntil(0);
2815 assert(decisionLevel() == 0);
2816
2817 //due to chrono BT we need to propagate once more
2818 PropBy confl = propagate<false>();
2819 assert(confl.isNULL());
2820 assert(solver->prop_at_head());
2821 #ifdef SLOW_DEBUG
2822 print_solution_varreplace_status();
2823 #endif
2824 } else if (status == l_False) {
2825 if (conflict.size() == 0) {
2826 ok = false;
2827 }
2828 cancelUntil(0);
2829 if (ok) {
2830 //due to chrono BT we need to propagate once more
2831 PropBy confl = propagate<false>();
2832 assert(confl.isNULL());
2833 }
2834 } else if (status == l_Undef) {
2835 assert(decisionLevel() == 0);
2836 assert(solver->prop_at_head());
2837 }
2838
2839 #ifdef STATS_NEEDED
2840 sql_dump_last_in_solver();
2841 #endif
2842
2843 stats.cpu_time = cpuTime() - startTime;
2844 if (conf.verbosity >= 4) {
2845 cout << "c Searcher::solve() finished"
2846 << " status: " << status
2847 << " numConflicts : " << stats.conflStats.numConflicts
2848 << " SumConfl: " << sumConflicts
2849 << " max_confl_per_search_solve_call:" << max_confl_per_search_solve_call
2850 << endl;
2851 }
2852
2853 print_iteration_solving_stats();
2854 }
2855
print_iteration_solving_stats()2856 void Searcher::print_iteration_solving_stats()
2857 {
2858 if (conf.verbosity >= 3) {
2859 cout << "c ------ THIS ITERATION SOLVING STATS -------" << endl;
2860 stats.print(propStats.propagations, conf.do_print_times);
2861 propStats.print(stats.cpu_time);
2862 print_stats_line("c props/decision"
2863 , float_div(propStats.propagations, stats.decisions)
2864 );
2865 print_stats_line("c props/conflict"
2866 , float_div(propStats.propagations, stats.conflStats.numConflicts)
2867 );
2868 cout << "c ------ THIS ITERATION SOLVING STATS -------" << endl;
2869 }
2870 }
2871
pickBranchLit()2872 inline Lit Searcher::pickBranchLit()
2873 {
2874 #ifdef VERBOSE_DEBUG
2875 print_order_heap();
2876 cout << "picking decision variable, dec. level: "
2877 << decisionLevel() << endl;
2878 #endif
2879
2880 uint32_t v = var_Undef;
2881 switch (branch_strategy) {
2882 case branch::vsids:
2883 case branch::maple:
2884 v = pick_var_vsids_maple();
2885 break;
2886 #ifdef VMTF_NEEDED
2887 case branch::vmtf:
2888 v = pick_var_vmtf();
2889 break;
2890 #endif
2891 }
2892
2893 Lit next;
2894 if (v != var_Undef) {
2895 next = Lit(v, !pick_polarity(v));
2896 } else {
2897 next = lit_Undef;
2898 }
2899
2900 #ifdef SLOW_DEBUG
2901 if (next != lit_Undef) {
2902 assert(solver->varData[next.var()].removed == Removed::none);
2903 }
2904 #endif
2905
2906 return next;
2907 }
2908
2909 #ifdef VMTF_NEEDED
pick_var_vmtf()2910 uint32_t Searcher::pick_var_vmtf()
2911 {
2912 uint64_t searched = 0;
2913 uint32_t res = vmtf_queue.unassigned;
2914 while (res != std::numeric_limits<uint32_t>::max()
2915 && value(res) != l_Undef
2916 ) {
2917 res = vmtf_link(res).prev;
2918 searched++;
2919 }
2920
2921 if (res == std::numeric_limits<uint32_t>::max()) {
2922 return var_Undef;
2923 }
2924
2925 if (searched) {
2926 vmtf_update_queue_unassigned(res);
2927 }
2928 //LOG ("next queue decision variable %d vmtf_bumped %" PRId64 "", res, vmtf_bumped (res));
2929 return res;
2930 }
2931 #endif
2932
pick_var_vsids_maple()2933 uint32_t Searcher::pick_var_vsids_maple()
2934 {
2935 Heap<VarOrderLt> &order_heap = (branch_strategy == branch::vsids) ? order_heap_vsids : order_heap_maple;
2936 uint32_t v = var_Undef;
2937 while (v == var_Undef || value(v) != l_Undef) {
2938 //There is no more to branch on. Satisfying assignment found.
2939 if (order_heap.empty()) {
2940 return var_Undef;
2941 }
2942
2943 //Adjust maple to account for time passed
2944 if (branch_strategy == branch::maple) {
2945 uint32_t v2 = order_heap_maple[0];
2946 uint32_t age = sumConflicts - varData[v2].maple_cancelled;
2947 while (age > 0) {
2948 double decay = pow(var_decay, age);
2949 var_act_maple[v2].act *= decay;
2950 if (order_heap_maple.inHeap(v2)) {
2951 order_heap_maple.increase(v2);
2952 }
2953 varData[v2].maple_cancelled = sumConflicts;
2954 v2 = order_heap_maple[0];
2955 age = sumConflicts - varData[v2].maple_cancelled;
2956 }
2957 }
2958 v = order_heap.removeMin();
2959 }
2960 return v;
2961 }
2962
binary_based_morem_minim(vector<Lit> & cl)2963 void Searcher::binary_based_morem_minim(vector<Lit>& cl)
2964 {
2965 int64_t limit = more_red_minim_limit_binary_actual;
2966 const size_t first_n_lits_of_cl =
2967 std::min<size_t>(conf.max_num_lits_more_more_red_min, cl.size());
2968 for (size_t at_lit = 0; at_lit < first_n_lits_of_cl; at_lit++) {
2969 Lit lit = cl[at_lit];
2970 //Already removed this literal
2971 if (seen[lit.toInt()] == 0)
2972 continue;
2973
2974 //Watchlist-based minimisation
2975 watch_subarray_const ws = watches[lit];
2976 for (const Watched* i = ws.begin() , *end = ws.end()
2977 ; i != end && limit > 0
2978 ; i++
2979 ) {
2980 limit--;
2981 if (i->isBin()) {
2982 if (seen[(~i->lit2()).toInt()]) {
2983 stats.binTriShrinkedClause++;
2984 seen[(~i->lit2()).toInt()] = 0;
2985 }
2986 continue;
2987 }
2988 break;
2989 }
2990 }
2991 }
2992
minimise_redundant_more_more(vector<Lit> & cl)2993 void Searcher::minimise_redundant_more_more(vector<Lit>& cl)
2994 {
2995 stats.furtherShrinkAttempt++;
2996 for (const Lit lit: cl) {
2997 seen[lit.toInt()] = 1;
2998 }
2999
3000 binary_based_morem_minim(cl);
3001
3002 //Finally, remove the literals that have seen[literal] = 0
3003 //Here, we can count do stats, etc.
3004 bool changedClause = false;
3005 vector<Lit>::iterator i = cl.begin();
3006 vector<Lit>::iterator j= i;
3007
3008 //never remove the 0th literal -- TODO this is a bad thing
3009 //we should be able to remove this, but I can't figure out how to
3010 //reorder the clause then
3011 seen[cl[0].toInt()] = 1;
3012 for (vector<Lit>::iterator end = cl.end(); i != end; i++) {
3013 if (seen[i->toInt()]) {
3014 *j++ = *i;
3015 } else {
3016 changedClause = true;
3017 }
3018 seen[i->toInt()] = 0;
3019 }
3020 stats.furtherShrinkedSuccess += changedClause;
3021 cl.resize(cl.size() - (i-j));
3022 }
3023
sumRestarts() const3024 uint64_t Searcher::sumRestarts() const
3025 {
3026 return stats.numRestarts + solver->get_stats().numRestarts;
3027 }
3028
hyper_bin_res_all(const bool check_for_set_values)3029 size_t Searcher::hyper_bin_res_all(const bool check_for_set_values)
3030 {
3031 size_t added = 0;
3032
3033 for(std::set<BinaryClause>::const_iterator
3034 it = solver->needToAddBinClause.begin()
3035 , end = solver->needToAddBinClause.end()
3036 ; it != end
3037 ; ++it
3038 ) {
3039 lbool val1 = value(it->getLit1());
3040 lbool val2 = value(it->getLit2());
3041
3042 if (conf.verbosity >= 6) {
3043 cout
3044 << "c Attached hyper-bin: "
3045 << it->getLit1() << "(val: " << val1 << " )"
3046 << ", " << it->getLit2() << "(val: " << val2 << " )"
3047 << endl;
3048 }
3049
3050 //If binary is satisfied, skip
3051 if (check_for_set_values
3052 && (val1 == l_True || val2 == l_True)
3053 ) {
3054 continue;
3055 }
3056
3057 if (check_for_set_values) {
3058 assert(val1 == l_Undef && val2 == l_Undef);
3059 }
3060
3061 solver->attach_bin_clause(it->getLit1(), it->getLit2(), true, false);
3062 added++;
3063 }
3064 solver->needToAddBinClause.clear();
3065
3066 return added;
3067 }
3068
3069 #ifdef USE_GAUSS
gauss_jordan_elim()3070 Searcher::gauss_ret Searcher::gauss_jordan_elim()
3071 {
3072 #ifdef VERBOSE_DEBUG
3073 cout << "Gauss searcher::Gauss_elimination called, declevel: " << decisionLevel() << endl;
3074 #endif
3075
3076 for(uint32_t i = 0; i < gqueuedata.size(); i++) {
3077 if (gqueuedata[i].engaus_disable) {
3078 continue;
3079 }
3080 gqueuedata[i].reset();
3081 gmatrices[i]->update_cols_vals_set();
3082 }
3083
3084 bool confl_in_gauss = false;
3085 while (gqhead < trail.size()
3086 && !confl_in_gauss
3087 ) {
3088 const Lit p = trail[gqhead].lit;
3089 uint32_t currLevel = trail[gqhead].lev;
3090 gqhead++;
3091
3092 assert(gwatches.size() > p.var());
3093 vec<GaussWatched>& ws = gwatches[p.var()];
3094 GaussWatched* i = ws.begin();
3095 GaussWatched* j = i;
3096 const GaussWatched* end = ws.end();
3097 #ifdef VERBOSE_DEBUG
3098 cout << "New GQHEAD: " << p << endl;
3099 #endif
3100
3101 for (; i != end; i++) {
3102 if (gqueuedata[i->matrix_num].engaus_disable) {
3103 //remove watch and continue
3104 continue;
3105 }
3106
3107 gqueuedata[i->matrix_num].new_resp_var = std::numeric_limits<uint32_t>::max();
3108 gqueuedata[i->matrix_num].new_resp_row = std::numeric_limits<uint32_t>::max();
3109 gqueuedata[i->matrix_num].do_eliminate = false;
3110 gqueuedata[i->matrix_num].currLevel = currLevel;
3111
3112 if (gmatrices[i->matrix_num]->find_truths(
3113 i, j, p.var(), i->row_n, gqueuedata[i->matrix_num])
3114 ) {
3115 continue;
3116 } else {
3117 confl_in_gauss = true;
3118 i++;
3119 break;
3120 }
3121 }
3122
3123 for (; i != end; i++) {
3124 *j++ = *i;
3125 }
3126 ws.shrink(i-j);
3127
3128 for (size_t g = 0; g < gqueuedata.size(); g++) {
3129 if (gqueuedata[g].engaus_disable)
3130 continue;
3131
3132 if (gqueuedata[g].do_eliminate) {
3133 gmatrices[g]->eliminate_col(p.var(), gqueuedata[g]);
3134 confl_in_gauss |= (gqueuedata[g].ret == gauss_res::confl);
3135 }
3136 }
3137 }
3138
3139 #ifdef SLOW_DEBUG
3140 if (!confl_in_gauss) {
3141 for (size_t g = 0; g < gqueuedata.size(); g++) {
3142 if (gqueuedata[g].engaus_disable)
3143 continue;
3144
3145 assert(solver->gqhead == solver->trail.size());
3146 gmatrices[g]->check_invariants();
3147 }
3148 }
3149 #endif
3150
3151 gauss_ret finret = gauss_ret::g_nothing;
3152 for (GaussQData& gqd: gqueuedata) {
3153 if (gqd.engaus_disable)
3154 continue;
3155
3156 //There was a conflict but this is not that matrix.
3157 //Just skip.
3158 if (confl_in_gauss && gqd.ret != gauss_res::confl) {
3159 continue;
3160 }
3161
3162 switch (gqd.ret) {
3163 case gauss_res::confl :{
3164 gqd.num_conflicts++;
3165 gqhead = qhead = trail.size();
3166 bool ret = handle_conflict(gqd.confl);
3167 if (!ret) return gauss_ret::g_false;
3168 return gauss_ret::g_cont;
3169 }
3170
3171 case gauss_res::prop:
3172 gqd.num_props++;
3173 finret = gauss_ret::g_cont;
3174
3175 case gauss_res::none:
3176 //nothing
3177 break;
3178
3179 default:
3180 assert(false);
3181 return gauss_ret::g_nothing;
3182 }
3183 }
3184 #ifdef VERBOSE_DEBUG
3185 cout << "Exiting GJ" << endl;
3186 #endif
3187 return finret;
3188 }
3189 #endif //USE_GAUSS
3190
remove_useless_bins(bool except_marked)3191 std::pair<size_t, size_t> Searcher::remove_useless_bins(bool except_marked)
3192 {
3193 size_t removedIrred = 0;
3194 size_t removedRed = 0;
3195
3196 if (conf.doTransRed) {
3197 for(std::set<BinaryClause>::iterator
3198 it = uselessBin.begin()
3199 , end = uselessBin.end()
3200 ; it != end
3201 ; ++it
3202 ) {
3203 propStats.otfHyperTime += 2;
3204 if (conf.verbosity >= 10) {
3205 cout << "Removing binary clause: " << *it << endl;
3206 }
3207 propStats.otfHyperTime += solver->watches[it->getLit1()].size()/2;
3208 propStats.otfHyperTime += solver->watches[it->getLit2()].size()/2;
3209 bool removed;
3210 if (except_marked) {
3211 bool rem1 = removeWBin_except_marked(solver->watches, it->getLit1(), it->getLit2(), it->isRed());
3212 bool rem2 = removeWBin_except_marked(solver->watches, it->getLit2(), it->getLit1(), it->isRed());
3213 assert(rem1 == rem2);
3214 removed = rem1;
3215 } else {
3216 removeWBin(solver->watches, it->getLit1(), it->getLit2(), it->isRed());
3217 removeWBin(solver->watches, it->getLit2(), it->getLit1(), it->isRed());
3218 removed = true;
3219 }
3220
3221 if (!removed) {
3222 continue;
3223 }
3224
3225 //Update stats
3226 if (it->isRed()) {
3227 solver->binTri.redBins--;
3228 removedRed++;
3229 } else {
3230 solver->binTri.irredBins--;
3231 removedIrred++;
3232 }
3233 *drat << del << it->getLit1() << it->getLit2() << fin;
3234
3235 #ifdef VERBOSE_DEBUG_FULLPROP
3236 cout << "Removed bin: "
3237 << it->getLit1() << " , " << it->getLit2()
3238 << " , red: " << it->isRed() << endl;
3239 #endif
3240 }
3241 }
3242 uselessBin.clear();
3243
3244 return std::make_pair(removedIrred, removedRed);
3245 }
3246
3247 template<bool update_bogoprops>
propagate()3248 PropBy Searcher::propagate() {
3249 const size_t origTrailSize = trail.size();
3250
3251 PropBy ret;
3252 ret = propagate_any_order<update_bogoprops>();
3253
3254 //Drat -- If declevel 0 propagation, we have to add the unitaries
3255 if (decisionLevel() == 0 &&
3256 (drat->enabled() || conf.simulate_drat)
3257 ) {
3258 for(size_t i = origTrailSize; i < trail.size(); i++) {
3259 #ifdef DEBUG_DRAT
3260 if (conf.verbosity >= 6) {
3261 cout
3262 << "c 0-level enqueue:"
3263 << trail[i]
3264 << endl;
3265 }
3266 #endif
3267 *drat << add << trail[i].lit
3268 #ifdef STATS_NEEDED
3269 << 0
3270 << sumConflicts
3271 #endif
3272 << fin;
3273 }
3274 if (!ret.isNULL()) {
3275 *drat << add
3276 #ifdef STATS_NEEDED
3277 << 0
3278 << sumConflicts
3279 #endif
3280 << fin;
3281 }
3282 }
3283
3284 return ret;
3285 }
3286 template PropBy Searcher::propagate<true>();
3287 template PropBy Searcher::propagate<false>();
3288
mem_used() const3289 size_t Searcher::mem_used() const
3290 {
3291 size_t mem = HyperEngine::mem_used();
3292 mem += var_act_vsids.capacity()*sizeof(double);
3293 mem += var_act_maple.capacity()*sizeof(double);
3294 mem += order_heap_vsids.mem_used();
3295 mem += order_heap_maple.mem_used();
3296 #ifdef VMTF_NEEDED
3297 mem += vmtf_btab.capacity()*sizeof(uint64_t);
3298 mem += vmtf_links.capacity()*sizeof(Link);
3299 #endif
3300 mem += learnt_clause.capacity()*sizeof(Lit);
3301 mem += hist.mem_used();
3302 mem += conflict.capacity()*sizeof(Lit);
3303 mem += model.capacity()*sizeof(lbool);
3304 mem += analyze_stack.mem_used();
3305 mem += assumptions.capacity()*sizeof(Lit);
3306
3307 return mem;
3308 }
3309
fill_assumptions_set()3310 void Searcher::fill_assumptions_set()
3311 {
3312 #ifdef SLOW_DEBUG
3313 for(auto x: varData) {
3314 assert(x.assumption == l_Undef);
3315 }
3316 #endif
3317
3318 for(const AssumptionPair lit_pair: assumptions) {
3319 const Lit lit = map_outer_to_inter(lit_pair.lit_outer);
3320 varData[lit.var()].assumption = lit.sign() ? l_False : l_True;
3321 }
3322 }
3323
unfill_assumptions_set()3324 void Searcher::unfill_assumptions_set()
3325 {
3326 for(const AssumptionPair lit_pair: assumptions) {
3327 const Lit lit = map_outer_to_inter(lit_pair.lit_outer);
3328 varData[lit.var()].assumption = l_Undef;
3329 }
3330
3331 #ifdef SLOW_DEBUG
3332 for(auto x: varData) {
3333 assert(x.assumption == l_Undef);
3334 }
3335 #endif
3336 }
3337
vsids_decay_var_act()3338 void Searcher::vsids_decay_var_act()
3339 {
3340 assert(branch_strategy == branch::vsids);
3341 var_inc_vsids *= (1.0 / var_decay);
3342 }
3343
consolidate_watches(const bool full)3344 void Searcher::consolidate_watches(const bool full)
3345 {
3346 double t = cpuTime();
3347 if (full) {
3348 watches.full_consolidate();
3349 } else {
3350 watches.consolidate();
3351 }
3352 double time_used = cpuTime() - t;
3353
3354 if (conf.verbosity) {
3355 cout
3356 << "c [consolidate] "
3357 << (full ? "full" : "mini")
3358 << conf.print_times(time_used)
3359 << endl;
3360 }
3361
3362 std::stringstream ss;
3363 ss << "consolidate " << (full ? "full" : "mini") << " watches";
3364 if (sqlStats) {
3365 sqlStats->time_passed_min(
3366 solver
3367 , ss.str()
3368 , time_used
3369 );
3370 }
3371 }
3372
write_long_cls(const vector<ClOffset> & clauses,SimpleOutFile & f,const bool red) const3373 void Searcher::write_long_cls(
3374 const vector<ClOffset>& clauses
3375 , SimpleOutFile& f
3376 , const bool red
3377 ) const {
3378 f.put_uint64_t(clauses.size());
3379 for(ClOffset c: clauses)
3380 {
3381 Clause& cl = *cl_alloc.ptr(c);
3382 assert(cl.size() > 2);
3383 f.put_uint32_t(cl.size());
3384 for(const Lit l: cl)
3385 {
3386 f.put_lit(l);
3387 }
3388 if (red) {
3389 assert(cl.red());
3390 f.put_struct(cl.stats);
3391 }
3392 }
3393 }
3394
read_long_cls(SimpleInFile & f,const bool red)3395 void Searcher::read_long_cls(
3396 SimpleInFile& f
3397 , const bool red
3398 ) {
3399 uint64_t num_cls = f.get_uint64_t();
3400
3401 vector<Lit> tmp_cl;
3402 for(size_t i = 0; i < num_cls; i++)
3403 {
3404 tmp_cl.clear();
3405
3406 uint32_t sz = f.get_uint32_t();
3407 for(size_t j = 0; j < sz; j++)
3408 {
3409 tmp_cl.push_back(f.get_lit());
3410 }
3411 ClauseStats cl_stats;
3412 if (red) {
3413 f.get_struct(cl_stats);
3414 }
3415
3416 Clause* cl = cl_alloc.Clause_new(tmp_cl
3417 , cl_stats.last_touched
3418 #ifdef STATS_NEEDED
3419 , cl_stats.ID
3420 #endif
3421 );
3422 if (red) {
3423 cl->makeRed(sumConflicts);
3424 }
3425 cl->stats = cl_stats;
3426 attachClause(*cl);
3427 const ClOffset offs = cl_alloc.get_offset(cl);
3428 if (red) {
3429 assert(cl->stats.which_red_array < longRedCls.size());
3430 longRedCls[cl->stats.which_red_array].push_back(offs);
3431 litStats.redLits += cl->size();
3432 } else {
3433 longIrredCls.push_back(offs);
3434 litStats.irredLits += cl->size();
3435 }
3436 }
3437 }
3438
write_binary_cls(SimpleOutFile & f,bool red) const3439 void Searcher::write_binary_cls(
3440 SimpleOutFile& f
3441 , bool red
3442 ) const {
3443 if (red) {
3444 f.put_uint64_t(binTri.redBins);
3445 } else {
3446 f.put_uint64_t(binTri.irredBins);
3447 }
3448
3449 size_t at = 0;
3450 for(watch_subarray_const ws: watches)
3451 {
3452 Lit lit1 = Lit::toLit(at);
3453 at++;
3454 for(Watched w: ws)
3455 {
3456 if (w.isBin() && w.red() == red) {
3457 assert(lit1 != w.lit2());
3458 if (lit1 < w.lit2()) {
3459 f.put_lit(lit1);
3460 f.put_lit(w.lit2());
3461 }
3462 }
3463 }
3464 }
3465 }
3466
read_binary_cls(SimpleInFile & f,bool red)3467 uint64_t Searcher::read_binary_cls(
3468 SimpleInFile& f
3469 , bool red
3470 ) {
3471 uint64_t num = f.get_uint64_t();
3472 for(uint64_t i = 0; i < num; i++)
3473 {
3474 const Lit lit1 = f.get_lit();
3475 const Lit lit2 = f.get_lit();
3476 attach_bin_clause(lit1, lit2, red);
3477 }
3478 return num;
3479 }
3480
save_state(SimpleOutFile & f,const lbool status) const3481 void Searcher::save_state(SimpleOutFile& f, const lbool status) const
3482 {
3483 assert(decisionLevel() == 0);
3484 PropEngine::save_state(f);
3485
3486 f.put_vector(var_act_vsids);
3487 f.put_vector(var_act_maple);
3488 f.put_vector(model);
3489 f.put_vector(conflict);
3490
3491 //Clauses
3492 if (status == l_Undef) {
3493 write_binary_cls(f, false);
3494 write_binary_cls(f, true);
3495 write_long_cls(longIrredCls, f, false);
3496 for(auto& lredcls: longRedCls) {
3497 write_long_cls(lredcls, f, true);
3498 }
3499 }
3500 }
3501
load_state(SimpleInFile & f,const lbool status)3502 void Searcher::load_state(SimpleInFile& f, const lbool status)
3503 {
3504 assert(decisionLevel() == 0);
3505 PropEngine::load_state(f);
3506
3507 f.get_vector(var_act_vsids);
3508 f.get_vector(var_act_maple);
3509 for(size_t i = 0; i < nVars(); i++) {
3510 if (varData[i].removed == Removed::none
3511 && value(i) == l_Undef
3512 ) {
3513 insert_var_order_all(i);
3514 }
3515 }
3516 f.get_vector(model);
3517 f.get_vector(conflict);
3518
3519 //Clauses
3520 if (status == l_Undef) {
3521 binTri.irredBins = read_binary_cls(f, false);
3522 binTri.redBins =read_binary_cls(f, true);
3523 read_long_cls(f, false);
3524 for(size_t i = 0; i < longRedCls.size(); i++) {
3525 read_long_cls(f, true);
3526 }
3527 }
3528 }
3529
update_polarities_on_backtrack()3530 inline void Searcher::update_polarities_on_backtrack()
3531 {
3532 if (polarity_mode == PolarityMode::polarmode_stable &&
3533 polar_stable_longest_trail_this_iter < trail.size())
3534 {
3535 for(const auto t: trail) {
3536 if (t.lit == lit_Undef) {
3537 continue;
3538 }
3539 varData[t.lit.var()].polarity = !t.lit.sign();
3540 }
3541 polar_stable_longest_trail_this_iter = trail.size();
3542 //cout << "polar_stable_longest_trail: " << polar_stable_longest_trail << endl;
3543 }
3544
3545 //Just update in case it's the longest
3546 if (longest_trail_ever < trail.size()) {
3547 for(const auto t: trail) {
3548 if (t.lit == lit_Undef) {
3549 continue;
3550 }
3551 varData[t.lit.var()].best_polarity = !t.lit.sign();
3552 }
3553 longest_trail_ever = trail.size();
3554 }
3555 }
3556
3557
3558 //Normal running
3559 template
3560 void Searcher::cancelUntil<true, false>(uint32_t level);
3561
3562 //During inprocessing, dont update anyting really (probing, distilling)
3563 template
3564 void Searcher::cancelUntil<false, true>(uint32_t level);
3565
3566 template<bool do_insert_var_order, bool update_bogoprops>
cancelUntil(uint32_t blevel)3567 void Searcher::cancelUntil(uint32_t blevel)
3568 {
3569 #ifdef VERBOSE_DEBUG
3570 cout << "Canceling until level " << blevel;
3571 if (blevel > 0) cout << " sublevel: " << trail_lim[blevel];
3572 cout << endl;
3573 #endif
3574
3575 if (decisionLevel() > blevel) {
3576 update_polarities_on_backtrack();
3577
3578 add_tmp_canceluntil.clear();
3579 #ifdef USE_GAUSS
3580 if (!all_matrices_disabled) {
3581 for (uint32_t i = 0; i < gmatrices.size(); i++) {
3582 if (gmatrices[i] && !gqueuedata[i].engaus_disable) {
3583 //cout << "->Gauss canceling" << endl;
3584 gmatrices[i]->canceling();
3585 } else {
3586 //cout << "->Gauss NULL" << endl;
3587 }
3588 }
3589 }
3590 #endif //USE_GAUSS
3591
3592 //Go through in reverse order, unassign & insert then
3593 //back to the vars to be branched upon
3594 for (int sublevel = trail.size()-1
3595 ; sublevel >= (int)trail_lim[blevel]
3596 ; sublevel--
3597 ) {
3598 #ifdef VERBOSE_DEBUG
3599 cout
3600 << "Canceling lit " << trail[sublevel].lit
3601 << " sublevel: " << sublevel
3602 << endl;
3603 #endif
3604
3605 #ifdef ANIMATE3D
3606 std:cerr << "u " << var << endl;
3607 #endif
3608
3609 const uint32_t var = trail[sublevel].lit.var();
3610 assert(value(var) != l_Undef);
3611
3612 #ifdef STATS_NEEDED_BRANCH
3613 if (!update_bogoprops) {
3614 varData[var].last_canceled = sumConflicts;
3615 }
3616 if (!update_bogoprops && varData[var].reason == PropBy()) {
3617 //we want to dump & this was a decision var
3618 uint64_t sumConflicts_during = sumConflicts - varData[var].sumConflicts_at_picktime;
3619 uint64_t sumDecisions_during = sumDecisions - varData[var].sumDecisions_at_picktime;
3620 uint64_t sumPropagations_during = sumPropagations - varData[var].sumPropagations_at_picktime;
3621 uint64_t sumAntecedents_during = sumAntecedents - varData[var].sumAntecedents_at_picktime;
3622 uint64_t sumAntecedentsLits_during = sumAntecedentsLits - varData[var].sumAntecedentsLits_at_picktime;
3623 uint64_t sumConflictClauseLits_during = sumConflictClauseLits - varData[var].sumConflictClauseLits_at_picktime;
3624 uint64_t sumDecisionBasedCl_during = sumDecisionBasedCl - varData[var].sumDecisionBasedCl_at_picktime;
3625 uint64_t sumClLBD_during = sumClLBD - varData[var].sumClLBD_at_picktime;
3626 uint64_t sumClSize_during = sumClSize - varData[var].sumClSize_at_picktime;
3627 double rel_activity_at_fintime =
3628 std::log2(var_act_vsids[var]+10e-300)/std::log2(max_vsids_act+10e-300);
3629
3630 uint64_t inside_conflict_clause_during =
3631 varData[var].inside_conflict_clause - varData[var].inside_conflict_clause_at_picktime;
3632
3633 uint64_t inside_conflict_clause_glue_during =
3634 varData[var].inside_conflict_clause_glue - varData[var].inside_conflict_clause_glue_at_picktime;
3635
3636 uint64_t inside_conflict_clause_antecedents_during =
3637 varData[var].inside_conflict_clause_antecedents -
3638 varData[var].inside_conflict_clause_antecedents_at_picktime;
3639
3640 if (varData[var].dump) {
3641 uint64_t outer_var = map_inter_to_outer(var);
3642
3643 solver->sqlStats->var_data_fintime(
3644 solver
3645 , outer_var
3646 , varData[var]
3647 , rel_activity_at_fintime
3648 );
3649 }
3650
3651 //if STATS_NEEDED we only update for decisions, otherwise, all the time
3652 varData[var].sumConflicts_below_during += sumConflicts_during;
3653 varData[var].sumDecisions_below_during += sumDecisions_during;
3654 varData[var].sumPropagations_below_during += sumPropagations_during;
3655 varData[var].sumAntecedents_below_during += sumAntecedents_during;
3656 varData[var].sumAntecedentsLits_below_during += sumAntecedentsLits_during;
3657 varData[var].sumConflictClauseLits_below_during += sumConflictClauseLits_during;
3658 varData[var].sumDecisionBasedCl_below_during += sumDecisionBasedCl_during;
3659 varData[var].sumClLBD_below_during += sumClLBD_during;
3660 varData[var].sumClSize_below_during += sumClSize_during;
3661
3662 varData[var].inside_conflict_clause_during +=
3663 inside_conflict_clause_during;
3664
3665 varData[var].inside_conflict_clause_glue_during += inside_conflict_clause_glue_during;
3666
3667 varData[var].inside_conflict_clause_antecedents_during +=
3668 inside_conflict_clause_antecedents_during;
3669 }
3670 #endif
3671
3672
3673 if (trail[sublevel].lev <= blevel) {
3674 add_tmp_canceluntil.push_back(trail[sublevel]);
3675 } else {
3676 if (!update_bogoprops && branch_strategy == branch::maple) {
3677 assert(sumConflicts >= varData[var].maple_last_picked);
3678 uint32_t age = sumConflicts - varData[var].maple_last_picked;
3679 if (age > 0) {
3680 //adjusted reward -> higher if conflicted more or quicker
3681 double adjusted_reward = ((double)(varData[var].maple_conflicted)) / ((double)age);
3682
3683 double old_activity = var_act_maple[var].act;
3684 var_act_maple[var].act =
3685 maple_step_size * adjusted_reward + ((1.0 - maple_step_size ) * old_activity);
3686
3687 if (order_heap_maple.inHeap(var)) {
3688 if (var_act_maple[var].act > old_activity)
3689 order_heap_maple.decrease(var);
3690 else
3691 order_heap_maple.increase(var);
3692 }
3693 #ifdef VERBOSE_DEBUG
3694 cout << "Adjusting reward. Var: " << var+1 << " conflicted:" << std::setprecision(12) << varData[var].maple_conflicted
3695 << " old act: " << old_activity << " new act: " << var_act_maple[var] << endl
3696 << " step_size: " << maple_step_size
3697 << " age: " << age << " sumconflicts: " << sumConflicts << " last picked: " << varData[var].maple_last_picked
3698 << endl;
3699 #endif
3700 }
3701 varData[var].maple_cancelled = sumConflicts;
3702 }
3703
3704 assigns[var] = l_Undef;
3705 if (do_insert_var_order) {
3706 insert_var_order(var);
3707 }
3708 }
3709
3710 #ifdef VERBOSE_DEBUG
3711 cout << "c Updating score by 2 for " << (trail[sublevel].lit)
3712 << " " << lit_ind << endl;
3713 #endif
3714 }
3715 qhead = trail_lim[blevel];
3716 #ifdef USE_GAUSS
3717 gqhead = qhead;
3718 #endif
3719 trail.resize(trail_lim[blevel]);
3720 trail_lim.resize(blevel);
3721
3722 for (int nLitId = (int)add_tmp_canceluntil.size() - 1; nLitId >= 0; --nLitId) {
3723 trail.push_back(add_tmp_canceluntil[nLitId]);
3724 }
3725
3726 add_tmp_canceluntil.clear();
3727 }
3728
3729 #ifdef VERBOSE_DEBUG
3730 cout << "Canceling finished. Now at level: " << decisionLevel();
3731 if (trail.size() > 0) {
3732 cout << " sublevel: " << trail.size()-1;
3733 }
3734 cout << endl;
3735 #endif
3736 }
3737
check_var_in_branch_strategy(uint32_t int_var) const3738 void Searcher::check_var_in_branch_strategy(uint32_t int_var) const
3739 {
3740 switch(branch_strategy) {
3741 case branch::vsids:
3742 assert(order_heap_vsids.inHeap(int_var));
3743 break;
3744
3745 case branch::maple:
3746 assert(order_heap_maple.inHeap(int_var));
3747 break;
3748
3749 #ifdef VMTF_NEEDED
3750 case branch::vmtf:
3751 assert(false);
3752 //TODO VMTF
3753 break;
3754 #endif
3755 }
3756 }
3757
3758
find_conflict_level(PropBy & pb)3759 ConflictData Searcher::find_conflict_level(PropBy& pb)
3760 {
3761 ConflictData data;
3762
3763 if (pb.getType() == PropByType::binary_t) {
3764 data.nHighestLevel = varData[failBinLit.var()].level;
3765
3766 if (data.nHighestLevel == decisionLevel()
3767 && varData[pb.lit2().var()].level == decisionLevel()
3768 ) {
3769 return data;
3770 }
3771
3772 uint32_t highestId = 0;
3773 // find the largest decision level in the clause
3774 uint32_t nLevel = varData[pb.lit2().var()].level;
3775 if (nLevel > data.nHighestLevel) {
3776 highestId = 1;
3777 data.nHighestLevel = nLevel;
3778 }
3779
3780 //TODO
3781 // we might want to swap here if highestID is not 0
3782 if (highestId != 0) {
3783 Lit back = pb.lit2();
3784 pb = PropBy(failBinLit, pb.isRedStep());
3785 failBinLit = back;
3786 }
3787
3788 } else {
3789 Lit* clause = NULL;
3790 uint32_t size = 0;
3791 ClOffset offs;
3792 switch(pb.getType()) {
3793 case PropByType::clause_t: {
3794 offs = pb.get_offset();
3795 Clause& conflCl = *cl_alloc.ptr(offs);
3796 clause = conflCl.getData();
3797 size = conflCl.size();
3798 break;
3799 }
3800
3801 #ifdef USE_GAUSS
3802 case PropByType::xor_t: {
3803 vector<Lit>* cl = gmatrices[pb.get_matrix_num()]->
3804 get_reason(pb.get_row_num());
3805 clause = cl->data();
3806 size = cl->size();
3807 break;
3808 }
3809 #endif
3810
3811 case PropByType::binary_t:
3812 case PropByType::null_clause_t:
3813 assert(false);
3814 break;
3815 }
3816
3817 data.nHighestLevel = varData[clause[0].var()].level;
3818 if (data.nHighestLevel == decisionLevel()
3819 && varData[clause[1].var()].level == decisionLevel()
3820 ) {
3821 return data;
3822 }
3823
3824 uint32_t highestId = 0;
3825 // find the largest decision level in the clause
3826 for (uint32_t nLitId = 1; nLitId < size; ++nLitId) {
3827 uint32_t nLevel = varData[clause[nLitId].var()].level;
3828 if (nLevel > data.nHighestLevel) {
3829 highestId = nLitId;
3830 data.nHighestLevel = nLevel;
3831 }
3832 }
3833
3834 if (highestId != 0) {
3835 std::swap(clause[0], clause[highestId]);
3836 if (highestId > 1 && pb.getType() == clause_t) {
3837 removeWCl(watches[clause[highestId]], pb.get_offset());
3838 watches[clause[0]].push(Watched(offs, clause[1]));
3839 }
3840 }
3841 }
3842
3843 return data;
3844 }
3845
check_order_heap_sanity() const3846 inline bool Searcher::check_order_heap_sanity() const
3847 {
3848 if (conf.sampling_vars) {
3849 for(uint32_t outside_var: *conf.sampling_vars) {
3850 uint32_t outer_var = map_to_with_bva(outside_var);
3851 outer_var = solver->varReplacer->get_var_replaced_with_outer(outer_var);
3852 uint32_t int_var = map_outer_to_inter(outer_var);
3853
3854 assert(varData[int_var].removed == Removed::none ||
3855 varData[int_var].removed == Removed::decomposed);
3856
3857 if (int_var < nVars() &&
3858 varData[int_var].removed == Removed::none &&
3859 value(int_var) == l_Undef
3860 ) {
3861 check_var_in_branch_strategy(int_var);
3862 }
3863 }
3864 }
3865
3866 for(size_t i = 0; i < nVars(); i++)
3867 {
3868 if (varData[i].removed == Removed::none
3869 && value(i) == l_Undef)
3870 {
3871 check_var_in_branch_strategy(i);
3872 }
3873 }
3874 assert(order_heap_vsids.heap_property());
3875 assert(order_heap_maple.heap_property());
3876
3877 return true;
3878 }
3879
3880 #ifdef USE_GAUSS
clear_gauss_matrices()3881 void Searcher::clear_gauss_matrices()
3882 {
3883 xor_clauses_updated = true;
3884 for(uint32_t i = 0; i < gqueuedata.size(); i++) {
3885 auto gqd = gqueuedata[i];
3886 if (conf.verbosity >= 2) {
3887 cout
3888 << "c [mat" << i << "] num_props : "
3889 << print_value_kilo_mega(gqd.num_props) << endl
3890 << "c [mat" << i << "] num_conflicts : "
3891 << print_value_kilo_mega(gqd.num_conflicts) << endl;
3892 }
3893 }
3894
3895 if (conf.verbosity >= 1) {
3896 print_matrix_stats();
3897 }
3898 for(EGaussian* g: gmatrices) {
3899 delete g;
3900 }
3901 for(auto& w: gwatches) {
3902 w.clear();
3903 }
3904 gmatrices.clear();
3905 gqueuedata.clear();
3906 }
3907
print_matrix_stats()3908 void Searcher::print_matrix_stats()
3909 {
3910 for(EGaussian* g: gmatrices) {
3911 if (g) {
3912 g->print_matrix_stats(conf.verbosity);
3913 }
3914 }
3915 }
3916 #endif
3917
check_assumptions_sanity()3918 void Searcher::check_assumptions_sanity()
3919 {
3920 for(AssumptionPair& lit_pair: assumptions) {
3921 Lit inter_lit = map_outer_to_inter(lit_pair.lit_outer);
3922 assert(inter_lit.var() < varData.size());
3923 assert(varData[inter_lit.var()].removed == Removed::none);
3924 if (varData[inter_lit.var()].assumption == l_Undef) {
3925 cout << "Assump " << inter_lit << " has .assumption : "
3926 << varData[inter_lit.var()].assumption << endl;
3927 }
3928 assert(varData[inter_lit.var()].assumption != l_Undef);
3929 }
3930 }
3931
bump_var_importance_all(const uint32_t var,bool only_add,double amount)3932 void Searcher::bump_var_importance_all(const uint32_t var, bool only_add, double amount)
3933 {
3934 vsids_bump_var_act<false>(var, amount, only_add);
3935 varData[var].maple_conflicted += int(2*amount);
3936 #ifdef VMTF_NEEDED
3937 vmtf_bump_queue(var);
3938 #endif
3939 }
3940
3941
bump_var_importance(const uint32_t var)3942 void Searcher::bump_var_importance(const uint32_t var)
3943 {
3944 switch(branch_strategy) {
3945 case branch::vsids:
3946 vsids_bump_var_act<false>(var);
3947 break;
3948
3949 case branch::maple:
3950 varData[var].maple_conflicted+=2;
3951 break;
3952
3953 #ifdef VMTF_NEEDED
3954 case branch::vmtf:
3955 vmtf_bump_queue(var);
3956 break;
3957 #endif
3958 }
3959 }
3960