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 #ifndef __SEARCHER_H__
24 #define __SEARCHER_H__
25
26 #include <array>
27
28 #include "propengine.h"
29 #include "solvertypes.h"
30 #include "time_mem.h"
31 #include "hyperengine.h"
32 #include "MersenneTwister.h"
33 #include "simplefile.h"
34 #include "searchstats.h"
35 #include "gqueuedata.h"
36
37 #ifdef CMS_TESTING_ENABLED
38 #include "gtest/gtest_prod.h"
39 #endif
40
41
42 namespace CMSat {
43
44 class Solver;
45 class SQLStats;
46 class VarReplacer;
47 class EGaussian;
48 class DistillerLong;
49 class ClusteringImp;
50
51 using std::string;
52 using std::cout;
53 using std::endl;
54
55 struct VariableVariance
56 {
57 double avgDecLevelVarLT = 0;
58 double avgTrailLevelVarLT= 0;
59 double avgDecLevelVar = 0;
60 double avgTrailLevelVar = 0;
61 };
62
63 struct ConflictData {
64 uint32_t nHighestLevel;
65 };
66
67 class Searcher : public HyperEngine
68 {
69 public:
70 Searcher(const SolverConf* _conf, Solver* solver, std::atomic<bool>* _must_interrupt_inter);
71 virtual ~Searcher();
72 ///////////////////////////////
73 // Solving
74 //
75 lbool solve(
76 uint64_t max_confls
77 );
78 void finish_up_solve(lbool status);
79 void reduce_db_if_needed();
80 void clean_clauses_if_needed();
81 void check_calc_satzilla_features(bool force = false);
82 void check_calc_vardist_features(bool force = false);
83 void dump_search_loop_stats(double myTime);
84 bool must_abort(lbool status);
85 uint64_t luby_loop_num = 0;
86 MTRand mtrand; ///< random number generator
87
88
89 vector<lbool> model;
90 vector<Lit> conflict; ///<If problem is unsatisfiable (possibly under assumptions), this vector represent the final conflict clause expressed in the assumptions.
91 template<bool update_bogoprops>
92 PropBy propagate();
93
94 ///////////////////////////////
95 // Stats
96 //Restart print status
97 uint64_t lastRestartPrint = 0;
98 uint64_t lastRestartPrintHeader = 0;
99 void print_restart_stat();
100 void print_iteration_solving_stats();
101 void print_restart_header();
102 void print_restart_stat_line() const;
103 void print_restart_stats_base() const;
104 void print_clause_stats() const;
105 uint64_t sumRestarts() const;
106 const SearchHist& getHistory() const;
107 void print_local_restart_budget();
108
109 size_t hyper_bin_res_all(const bool check_for_set_values = true);
110 std::pair<size_t, size_t> remove_useless_bins(bool except_marked = false);
111
112 ///Returns l_Undef if not inside, l_True/l_False otherwise
var_inside_assumptions(const uint32_t var)113 lbool var_inside_assumptions(const uint32_t var) const
114 {
115 #ifdef SLOW_DEBUG
116 assert(var < nVars());
117 #endif
118 return varData[var].assumption;
119 }
lit_inside_assumptions(const Lit lit)120 lbool lit_inside_assumptions(const Lit lit) const
121 {
122 #ifdef SLOW_DEBUG
123 assert(lit.var() < nVars());
124 #endif
125 if (varData[lit.var()].assumption == l_Undef) {
126 return l_Undef;
127 } else {
128 lbool val = varData[lit.var()].assumption;
129 return val ^ lit.sign();
130 }
131 }
132
133 //ChronoBT
134 vector<Trail> add_tmp_canceluntil;
135 template<bool do_insert_var_order = true, bool update_bogoprops = false>
136 void cancelUntil(uint32_t level); ///<Backtrack until a certain level.
137 ConflictData find_conflict_level(PropBy& pb);
138 uint32_t chrono_backtrack = 0;
139 uint32_t non_chrono_backtrack = 0;
140
141 SQLStats* sqlStats = NULL;
142 ClusteringImp *clustering = NULL;
143 void consolidate_watches(const bool full);
144
145 //Gauss
146 #ifdef USE_GAUSS
147 void clear_gauss_matrices();
148 void print_matrix_stats();
149 enum class gauss_ret {g_cont, g_nothing, g_false};
150 gauss_ret gauss_jordan_elim();
151 void check_need_gauss_jordan_disable();
152 vector<EGaussian*> gmatrices;
153 vector<GaussQData> gqueuedata;
154 #endif
155
get_cla_inc()156 double get_cla_inc() const
157 {
158 return cla_inc;
159 }
160
161 //assumptions
162 void check_assumptions_sanity();
163 void unfill_assumptions_set();
164 bool check_order_heap_sanity() const;
165
166 template<bool update_bogoprops>
167 void bump_cl_act(Clause* cl);
168 void simple_create_learnt_clause(
169 PropBy confl,
170 vector<Lit>& out_learnt,
171 bool True_confl
172 );
173
174 #ifdef STATS_NEEDED
175 void dump_restart_sql(rst_dat_type type, int64_t clauseID = -1);
176 uint64_t last_dumped_conflict_rst_data_for_var = std::numeric_limits<uint64_t>::max();
177 #endif
178
179 /////////////////////
180 // Branching
181 /////////////////////
182 double var_inc_vsids;
183 void insert_var_order(const uint32_t x, branch type);
184 void insert_var_order(const uint32_t x);
185 void insert_var_order_all(const uint32_t x);
186 vector<uint32_t> implied_by_learnts; //for glue-based extra var activity bumping
187 void update_branch_params();
188 template<bool update_bogoprops>
189 lbool new_decision();
190 Lit pickBranchLit();
191 uint32_t pick_random_var();
192 uint32_t pick_var_vsids_maple();
193 uint32_t pick_var_vmtf();
194 void vsids_decay_var_act();
195 template<bool update_bogoprops>
196 void vsids_bump_var_act(uint32_t v, double mult = 1.0, bool only_add = false);
197 double backup_random_var_freq = -1; ///<if restart has full random var branch, we save old value here
198 void check_var_in_branch_strategy(uint32_t var) const;
199 void set_branch_strategy(uint32_t iteration_num);
200 void rebuildOrderHeap();
201 void rebuildOrderHeapVMTF();
202 void print_order_heap();
clear_order_heap()203 void clear_order_heap()
204 {
205 order_heap_vsids.clear();
206 order_heap_maple.clear();
207 }
208 uint32_t branch_strategy_num = 0;
209 void bump_var_importance(const uint32_t var);
210 void bump_var_importance_all(const uint32_t var, bool only_add = false, double amount = 1.0);
211
212 /////////////////
213 // Polarities
214 bool pick_polarity(const uint32_t var);
215 void setup_polarity_strategy();
216 void update_polarities_on_backtrack();
217
218 protected:
219 Solver* solver;
220 lbool search();
221
222 ///////////////
223 // Variables
224 ///////////////
225 void new_var(const bool bva, const uint32_t orig_outer) override;
226 void new_vars(const size_t n) override;
227 void save_on_var_memory();
228 void updateVars(
229 const vector<uint32_t>& outerToInter
230 , const vector<uint32_t>& interToOuter
231 );
232
233
234 ///////////////
235 // Reading and writing simplified CNF file
236 ///////////////
237 void save_state(SimpleOutFile& f, const lbool status) const;
238 void load_state(SimpleInFile& f, const lbool status);
239 void write_long_cls(
240 const vector<ClOffset>& clauses
241 , SimpleOutFile& f
242 , const bool red
243 ) const;
244 void read_long_cls(
245 SimpleInFile& f
246 , const bool red
247 );
248 uint64_t read_binary_cls(
249 SimpleInFile& f
250 , bool red
251 );
252 void write_binary_cls(
253 SimpleOutFile& f
254 , bool red
255 ) const;
256
257 //Misc
258 void add_in_partial_solving_stats();
259
260
261 void fill_assumptions_set();
262 void update_assump_conflict_to_orig_outside(vector<Lit>& out_conflict);
263
264 /////////////////////
265 // Learning
266 /////////////////////
267 vector<Lit> learnt_clause;
268 vector<Lit> decision_clause;
269 template<bool update_bogoprops>
270 void analyze_conflict(
271 PropBy confl //The conflict that we are investigating
272 , uint32_t& out_btlevel //backtrack level
273 , uint32_t &glue //glue of the learnt clause
274 , uint32_t &glue_before_minim //glue of the unminimised learnt clause
275 );
276 bool handle_conflict(PropBy confl);// Handles the conflict clause
277 void update_history_stats(size_t backtrack_level, uint32_t glue);
278 template<bool update_bogoprops>
279 void attach_and_enqueue_learnt_clause(Clause* cl, const uint32_t level, const bool enqueue);
280 void print_learning_debug_info() const;
281 void print_learnt_clause() const;
282 template<bool update_bogoprops>
283 void add_literals_from_confl_to_learnt(const PropBy confl, const Lit p, uint32_t nDecisionLevel);
284 template<bool update_bogoprops>
285 void create_learnt_clause(PropBy confl);
286 void debug_print_resolving_clause(const PropBy confl) const;
287 template<bool update_bogoprops>
288 void add_lit_to_learnt(Lit lit, uint32_t nDecisionLevel);
289 void analyze_final_confl_with_assumptions(const Lit p, vector<Lit>& out_conflict);
290 void update_clause_glue_from_analysis(Clause* cl);
291 template<bool update_bogoprops>
292 void minimize_learnt_clause();
293 void watch_based_learnt_minim();
294 void minimize_using_permdiff();
295 void print_fully_minimized_learnt_clause() const;
296 size_t find_backtrack_level_of_learnt();
297 Clause* otf_subsume_last_resolved_clause(Clause* last_resolved_long_cl);
298 void print_debug_resolution_data(const PropBy confl);
299 int pathC;
300 uint64_t more_red_minim_limit_binary_actual;
301 #if defined(STATS_NEEDED) || defined(FINAL_PREDICTOR)
302 AtecedentData<uint16_t> antec_data;
303 #endif
304 Clause* handle_last_confl(
305 const uint32_t glue
306 , const uint32_t old_decision_level
307 , const uint32_t glue_before_minim
308 , const bool is_decision
309 );
310
311 /////////////////////
312 // Search Stats
313 /////////////////////
314 const SearchStats& get_stats() const;
315 size_t mem_used() const;
316 void reset_temp_cl_num();
317 void resetStats(); //For connection with Solver
318 SearchHist hist;
319 double startTime; ///<When solve() was started
320 SearchStats stats;
321
322 /////////////////////
323 // Clause database reduction
324 /////////////////////
325 uint64_t next_lev1_reduce;
326 uint64_t next_lev2_reduce;
327 uint64_t next_lev3_reduce;
328
329 ///////////////
330 // Restart parameters
331 ///////////////
332 struct SearchParams
333 {
SearchParamsSearchParams334 SearchParams()
335 {
336 clear();
337 }
338
clearSearchParams339 void clear()
340 {
341 needToStopSearch = false;
342 conflictsDoneThisRestart = 0;
343 }
344
345 bool needToStopSearch;
346 uint64_t conflictsDoneThisRestart;
347 uint64_t max_confl_to_do;
348 Restart rest_type = Restart::never;
349 };
350 SearchParams params;
351 int64_t increasing_phase_size;
352 int64_t max_confl_this_phase;
353 void check_need_restart();
354 void check_blocking_restart();
355 bool blocked_restart = false;
356 uint64_t max_confl_per_search_solve_call;
357 uint32_t num_search_called = 0;
358 double luby(double y, int x);
359 CMSat::Restart cur_rest_type;
360 void adjust_restart_strategy();
361 void setup_restart_strategy();
362
363 //////////////
364 // Debug
365 //////////////
366 void print_solution_varreplace_status() const;
367
368 //////////////
369 // Conflict minimisation
370 bool litRedundant(Lit p, uint32_t abstract_levels);
371 void recursiveConfClauseMin();
372 void normalClMinim();
373 MyStack<Lit> analyze_stack;
374 uint32_t abstractLevel(const uint32_t x) const;
375 /*void create_otf_subsuming_implicit_clause(const Clause& cl);
376 void create_otf_subsuming_long_clause(Clause& cl, ClOffset offset);*/
377
378
379 bool subset(const vector<Lit>& A, const Clause& B); //Used for on-the-fly subsumption. Does A subsume B? Uses 'seen' to do its work
380
381 ////////////
382 // Transitive on-the-fly self-subsuming resolution
383 void minimise_redundant_more_more(vector<Lit>& cl);
384 void binary_based_morem_minim(vector<Lit>& cl);
385
386
387 friend class Gaussian;
388 friend class DistillerLong;
389 #ifdef CMS_TESTING_ENABLED
390 FRIEND_TEST(SearcherTest, pickpolar_rnd);
391 FRIEND_TEST(SearcherTest, pickpolar_pos);
392 FRIEND_TEST(SearcherTest, pickpolar_neg);
393 FRIEND_TEST(SearcherTest, pickpolar_auto);
394 FRIEND_TEST(SearcherTest, pickpolar_auto_not_changed_by_simp);
395 #endif
396
397 //Clause activites
398 double cla_inc;
399 template<bool update_bogoprops> void decayClauseAct();
400
401 //SQL
402 void dump_search_sql(const double myTime);
403 void set_clause_data(
404 Clause* cl
405 , const uint32_t glue
406 , const uint32_t glue_before_minim
407 , const uint32_t old_decision_level);
408 #ifdef STATS_NEEDED
409 PropStats lastSQLPropStats;
410 SearchStats lastSQLGlobalStats;
411 void dump_sql_clause_data(
412 const uint32_t orig_glue
413 , const uint32_t glue_before_minim
414 , const uint32_t old_decision_level
415 , const uint64_t clid
416 , const bool decision_cl
417 );
418 int dump_this_many_cldata_in_stream = 0;
419 void sql_dump_last_in_solver();
420 void dump_var_for_learnt_cl(const uint32_t v,
421 const uint64_t clid,
422 const bool is_decision);
423 #endif
424
425 #if defined(STATS_NEEDED_BRANCH) || defined(FINAL_PREDICTOR_BRANCH)
426 vector<uint32_t> level_used_for_cl;
427 vector<uint32_t> vars_used_for_cl;
428 vector<unsigned char> level_used_for_cl_arr;
429 #endif
430
431 //Other
432 void print_solution_type(const lbool status) const;
433 uint64_t next_distill = 0;
434
435 //Last time we clean()-ed the clauses, the number of zero-depth assigns was this many
436 size_t lastCleanZeroDepthAssigns;
437 };
438
abstractLevel(const uint32_t x)439 inline uint32_t Searcher::abstractLevel(const uint32_t x) const
440 {
441 return ((uint32_t)1) << (varData[x].level & 31);
442 }
443
get_stats()444 inline const SearchStats& Searcher::get_stats() const
445 {
446 return stats;
447 }
448
getHistory()449 inline const SearchHist& Searcher::getHistory() const
450 {
451 return hist;
452 }
453
add_in_partial_solving_stats()454 inline void Searcher::add_in_partial_solving_stats()
455 {
456 stats.cpu_time = cpuTime() - startTime;
457 }
458
insert_var_order(const uint32_t x)459 inline void Searcher::insert_var_order(const uint32_t x)
460 {
461 insert_var_order(x, branch_strategy);
462 }
463
insert_var_order(const uint32_t x,branch type)464 inline void Searcher::insert_var_order(const uint32_t x, branch type)
465 {
466 #ifdef SLOW_DEUG
467 assert(varData[x].removed == Removed::none
468 && "All variables should be decision vars unless removed");
469 #endif
470
471 switch(type) {
472 case branch::vsids:
473 if (!order_heap_vsids.inHeap(x)) {
474 order_heap_vsids.insert(x);
475 }
476 break;
477 case branch::maple:
478 if (!order_heap_maple.inHeap(x)) {
479 order_heap_maple.insert(x);
480 }
481 break;
482 #ifdef VMTF_NEEDED
483 case branch::vmtf:
484 // For VMTF we need to update the 'queue.unassigned' pointer in case this
485 // variables sits after the variable to which 'queue.unassigned' currently
486 // points. See our SAT'15 paper for more details on this aspect.
487 //
488 if (vmtf_queue.vmtf_bumped < vmtf_btab[x]) {
489 vmtf_update_queue_unassigned (x);
490 }
491 break;
492 #endif
493 }
494 }
495
insert_var_order_all(const uint32_t x)496 inline void Searcher::insert_var_order_all(const uint32_t x)
497 {
498 if (!order_heap_vsids.inHeap(x)) {
499 #ifdef SLOW_DEUG
500 assert(varData[x].removed == Removed::none
501 && "All variables should be decision vars unless removed");
502 #endif
503
504 order_heap_vsids.insert(x);
505 }
506 if (!order_heap_maple.inHeap(x)) {
507 #ifdef SLOW_DEUG
508 assert(varData[x].removed == Removed::none
509 && "All variables should be decision vars unless removed");
510 #endif
511
512 order_heap_maple.insert(x);
513 }
514
515 #ifdef VMTF_NEEDED
516 vmtf_init_enqueue(x);
517 #endif
518 }
519
520 template<bool update_bogoprops>
bump_cl_act(Clause * cl)521 inline void Searcher::bump_cl_act(Clause* cl)
522 {
523 if (update_bogoprops)
524 return;
525
526 assert(!cl->getRemoved());
527
528 double new_val = cla_inc + (double)cl->stats.activity;
529 cl->stats.activity = (float)new_val;
530 if (max_cl_act < new_val) {
531 max_cl_act = new_val;
532 }
533
534
535 if (cl->stats.activity > 1e20F ) {
536 // Rescale. For STATS_NEEDED we rescale ALL
537 #if !defined(STATS_NEEDED) && !defined (FINAL_PREDICTOR)
538 for(ClOffset offs: longRedCls[2]) {
539 cl_alloc.ptr(offs)->stats.activity *= static_cast<float>(1e-20);
540 }
541 #else
542 for(auto& lrcs: longRedCls) {
543 for(ClOffset offs: lrcs) {
544 cl_alloc.ptr(offs)->stats.activity *= static_cast<float>(1e-20);
545 }
546 }
547 #endif
548 cla_inc *= 1e-20;
549 max_cl_act *= 1e-20;
550 assert(cla_inc != 0);
551 }
552 }
553
554 template<bool update_bogoprops>
decayClauseAct()555 inline void Searcher::decayClauseAct()
556 {
557 if (update_bogoprops)
558 return;
559
560 cla_inc *= (1 / conf.clause_decay);
561 }
562
pick_polarity(const uint32_t var)563 inline bool Searcher::pick_polarity(const uint32_t var)
564 {
565 switch(polarity_mode) {
566 case PolarityMode::polarmode_neg:
567 return false;
568
569 case PolarityMode::polarmode_pos:
570 return true;
571
572 case PolarityMode::polarmode_rnd:
573 return mtrand.randInt(1);
574
575 case PolarityMode::polarmode_automatic:
576 return varData[var].polarity;
577
578 case PolarityMode::polarmode_stable:
579 return varData[var].polarity;
580
581 case PolarityMode::polarmode_best_inv:
582 return !varData[var].best_polarity;
583
584 case PolarityMode::polarmode_best:
585 return varData[var].best_polarity;
586
587 #ifdef WEIGHTED_SAMPLING
588 case PolarityMode::polarmode_weighted: {
589 double rnd = mtrand.randDblExc();
590 return rnd < varData[var].weight;
591 }
592 #endif
593
594 default:
595 assert(false);
596 }
597
598 return true;
599 }
600
601 template<bool update_bogoprops>
vsids_bump_var_act(uint32_t var,double mult,bool only_add)602 inline void Searcher::vsids_bump_var_act(uint32_t var, double mult, bool only_add)
603 {
604 if (update_bogoprops) {
605 return;
606 }
607
608 var_act_vsids[var].act += var_inc_vsids * mult;
609 max_vsids_act = std::max(max_vsids_act, var_act_vsids[var].act);
610
611 #ifdef SLOW_DEBUG
612 bool rescaled = false;
613 #endif
614 if (var_act_vsids[var].act > 1e100) {
615 // Rescale:
616
617 for (auto& v: var_act_vsids) {
618 v.act *= 1e-100;
619 }
620 max_vsids_act *= 1e-100;
621
622 #ifdef SLOW_DEBUG
623 rescaled = true;
624 #endif
625
626 //Reset var_inc
627 var_inc_vsids *= 1e-100;
628 }
629
630 // Update order_heap with respect to new activity:
631 if (!only_add && order_heap_vsids.inHeap(var)) {
632 order_heap_vsids.decrease(var);
633 }
634
635 #ifdef SLOW_DEBUG
636 if (rescaled) {
637 assert(order_heap_vsids.heap_property());
638 }
639 #endif
640 }
641
642 } //end namespace
643
644 #endif //__SEARCHER_H__
645