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 SOLVER_H
24 #define SOLVER_H
25
26 #include "constants.h"
27 #include <vector>
28 #include <fstream>
29 #include <iostream>
30 #include <utility>
31 #include <string>
32 #include <algorithm>
33
34 #include "constants.h"
35 #include "solvertypes.h"
36 #include "propengine.h"
37 #include "searcher.h"
38 #include "satzilla_features.h"
39 #include "searchstats.h"
40 #ifdef CMS_TESTING_ENABLED
41 #include "gtest/gtest_prod.h"
42 #endif
43
44 namespace CMSat {
45
46 using std::vector;
47 using std::pair;
48 using std::string;
49
50 class VarReplacer;
51 class ClauseCleaner;
52 class OccSimplifier;
53 class SCCFinder;
54 class DistillerLong;
55 class DistillerLongWithImpl;
56 class StrImplWImpl;
57 class CalcDefPolars;
58 class SolutionExtender;
59 class CompFinder;
60 class CompHandler;
61 class CardFinder;
62 class SubsumeStrengthen;
63 class SubsumeImplicit;
64 class DataSync;
65 class SharedData;
66 class ReduceDB;
67 class InTree;
68 class BreakID;
69
70 struct SolveStats
71 {
72 uint32_t num_simplify = 0;
73 uint32_t num_simplify_this_solve_call = 0;
74 uint32_t num_solve_calls = 0;
75 };
76
77 class Solver : public Searcher
78 {
79 public:
80 Solver(const SolverConf *_conf = NULL,
81 std::atomic<bool>* _must_interrupt_inter = NULL,
82 bool is_mpi = false);
83 ~Solver() override;
84
85 void add_sql_tag(const string& name, const string& val);
86 const vector<std::pair<string, string> >& get_sql_tags() const;
87 void new_external_var();
88 void new_external_vars(size_t n);
89 bool add_clause_outer(const vector<Lit>& lits, bool red = false);
90 bool add_xor_clause_outer(const vector<uint32_t>& vars, bool rhs);
91 void set_var_weight(Lit lit, double weight);
92
93 lbool solve_with_assumptions(const vector<Lit>* _assumptions, bool only_indep_solution);
94 lbool simplify_with_assumptions(const vector<Lit>* _assumptions = NULL);
95 void set_shared_data(SharedData* shared_data);
96
97 //drat for SAT problems
98 void add_empty_cl_to_drat();
99
100 //Querying model
101 lbool model_value (const Lit p) const; ///<Found model value for lit
102 lbool model_value (const uint32_t p) const; ///<Found model value for var
103 lbool full_model_value (const Lit p) const; ///<Found model value for lit
104 lbool full_model_value (const uint32_t p) const; ///<Found model value for var
105 const vector<lbool>& get_model() const;
106 const vector<Lit>& get_final_conflict() const;
107 vector<pair<Lit, Lit> > get_all_binary_xors() const;
108 vector<Xor> get_recovered_xors(const bool xor_together_xors);
109 vector<ActAndOffset> get_vsids_scores() const;
110 vector<Lit> implied_by_tmp_lits;
111 bool implied_by(const std::vector<Lit>& lits,
112 std::vector<Lit>& out_implied
113 );
114
115 //get learnt clauses
116 void start_getting_small_clauses(uint32_t max_len, uint32_t max_glue);
117 bool get_next_small_clause(std::vector<Lit>& out);
118 void end_getting_small_clauses();
119
120 void dump_irred_clauses(std::ostream *out) const;
121 void dump_red_clauses(std::ostream *out) const;
122 void open_file_and_dump_irred_clauses(const std::string &fname) const;
123 void open_file_and_dump_red_clauses(const std::string &fname) const;
124
125 static const char* get_version_tag();
126 static const char* get_version_sha1();
127 static const char* get_compilation_env();
128
129 vector<Lit> get_zero_assigned_lits(const bool backnumber = true, bool only_nvars = false) const;
130 void print_stats(const double cpu_time, const double cpu_time_total) const;
131 void print_stats_time(const double cpu_time, const double cpu_time_total) const;
132 void print_clause_stats() const;
133 size_t get_num_free_vars() const;
134 size_t get_num_nonfree_vars() const;
135 const SolverConf& getConf() const;
136 void setConf(const SolverConf& conf);
137 const BinTriStats& getBinTriStats() const;
138 size_t get_num_long_irred_cls() const;
139 size_t get_num_long_red_cls() const;
140 size_t get_num_vars_elimed() const;
141 uint32_t num_active_vars() const;
142 void print_mem_stats() const;
143 uint64_t print_watch_mem_used(uint64_t totalMem) const;
144 const SolveStats& get_solve_stats() const;
145 const SearchStats& get_stats() const;
146 void add_in_partial_solving_stats();
147 void check_implicit_stats(const bool onlypairs = false) const;
148 void check_stats(const bool allowFreed = false) const;
149 void reset_vsids();
150 void enable_comphandler();
151
152
153 //Checks
154 void check_implicit_propagated() const;
155 bool find_with_watchlist_a_or_b(Lit a, Lit b, int64_t* limit) const;
156
157 //Systems that are used to accompilsh the tasks
158 ClauseCleaner* clauseCleaner = NULL;
159 VarReplacer* varReplacer = NULL;
160 SubsumeImplicit* subsumeImplicit = NULL;
161 DataSync* datasync = NULL;
162 ReduceDB* reduceDB = NULL;
163 InTree* intree = NULL;
164 BreakID* breakid = NULL;
165 OccSimplifier* occsimplifier = NULL;
166 DistillerLong* distill_long_cls = NULL;
167 DistillerLongWithImpl* dist_long_with_impl = NULL;
168 StrImplWImpl* dist_impl_with_impl = NULL;
169 CompHandler* compHandler = NULL;
170 CardFinder* card_finder = NULL;
171
172 SearchStats sumSearchStats;
173 PropStats sumPropStats;
174
175 bool prop_at_head() const;
176 void set_decision_var(const uint32_t var);
177 bool fully_enqueue_these(const vector<Lit>& toEnqueue);
178 bool fully_enqueue_this(const Lit lit);
179 void update_assumptions_after_varreplace();
180
181 //State load/unload
182 void save_state(const string& fname, const lbool status) const;
183 lbool load_state(const string& fname);
184 template<typename A>
185 void parse_v_line(A* in, const size_t lineNum);
186 lbool load_solution_from_file(const string& fname);
187
188 uint64_t getNumLongClauses() const;
189 bool addClause(const vector<Lit>& ps, const bool red = false);
190 bool add_xor_clause_inter(
191 const vector< Lit >& lits
192 , bool rhs
193 , bool attach
194 , bool addDrat = true
195 );
196 void new_var(const bool bva = false, const uint32_t orig_outer = std::numeric_limits<uint32_t>::max()) override;
197 void new_vars(const size_t n) override;
198 void bva_changed();
199
200 //Attaching-detaching clauses
201 void attachClause(
202 const Clause& c
203 #ifdef DEBUG_ATTACH
204 , const bool checkAttach = true
205 #else
206 , const bool checkAttach = false
207 #endif
208 );
209 void attach_bin_clause(
210 const Lit lit1
211 , const Lit lit2
212 , const bool red
213 , const bool checkUnassignedFirst = true
214 );
215 void detach_bin_clause(
216 Lit lit1
217 , Lit lit2
218 , bool red
219 , bool allow_empty_watch = false
220 , bool allow_change_order = false
221 ) {
222 if (red) {
223 binTri.redBins--;
224 } else {
225 binTri.irredBins--;
226 }
227
228 PropEngine::detach_bin_clause(lit1, lit2, red, allow_empty_watch, allow_change_order);
229 }
230 void detachClause(const Clause& c, const bool removeDrat = true);
231 void detachClause(const ClOffset offset, const bool removeDrat = true);
232 void detach_modified_clause(
233 const Lit lit1
234 , const Lit lit2
235 , const uint32_t origSize
236 , const Clause* address
237 );
238 Clause* add_clause_int(
239 const vector<Lit>& lits
240 , const bool red = false
241 , const ClauseStats stats = ClauseStats()
242 , const bool attach = true
243 , vector<Lit>* finalLits = NULL
244 , bool addDrat = true
245 , const Lit drat_first = lit_Undef
246 , const bool sorted = false
247 );
248 template<class T> vector<Lit> clause_outer_numbered(const T& cl) const;
249 template<class T> vector<uint32_t> xor_outer_numbered(const T& cl) const;
250 size_t mem_used() const;
251 void dump_memory_stats_to_sql();
252 void set_sqlite(string filename);
253 //Not Private for testing (maybe could be called from outside)
254 bool renumber_variables(bool must_renumber = true);
255 SatZillaFeatures calculate_satzilla_features();
256 SatZillaFeatures last_solve_satzilla_feature;
257
258 uint32_t undefine(vector<uint32_t>& trail_lim_vars);
259 vector<Lit> get_toplevel_units_internal(bool outer_numbering) const;
260
261 #ifdef USE_GAUSS
262 bool init_all_matrices();
263 void detach_xor_clauses(
264 const set<uint32_t>& clash_vars_unused
265 );
266 bool fully_undo_xor_detach();
267 bool no_irred_nonxor_contains_clash_vars();
268 bool assump_contains_xor_clash();
269 void extend_model_to_detached_xors();
270 void unset_clash_decision_vars(const vector<Xor>& xors);
271 void set_clash_decision_vars();
272 bool find_and_init_all_matrices();
273 #endif
274
275 //assumptions
276 void set_assumptions();
277 vector<Lit> inter_assumptions_tmp; //used by set_assumptions() ONLY
278 void add_assumption(const Lit assump);
279 void check_assigns_for_assumptions() const;
280 bool check_assumptions_contradict_foced_assignment() const;
281
282
283 //if set to TRUE, a clause has been removed during add_clause_int
284 //that contained "lit, ~lit". So "lit" must be set to a value
285 //Contains _outer_ variables
286 vector<bool> undef_must_set_vars;
287
288 //Deleting clauses
289 void free_cl(Clause* cl);
290 void free_cl(ClOffset offs);
291 #ifdef STATS_NEEDED
292 void stats_del_cl(Clause* cl);
293 void stats_del_cl(ClOffset offs);
294 #endif
295
296 //Helper
297 void renumber_xors_to_outside(const vector<Xor>& xors, vector<Xor>& xors_ret);
298 void testing_set_solver_not_fresh();
299
300 private:
301 friend class ClauseDumper;
302 #ifdef CMS_TESTING_ENABLED
303 FRIEND_TEST(SearcherTest, pickpolar_auto_not_changed_by_simp);
304 #endif
305
306 vector<Lit> add_clause_int_tmp_cl;
307 lbool iterate_until_solved();
308 uint64_t mem_used_vardata() const;
309 void check_reconfigure();
310 void reconfigure(int val);
311 bool already_reconfigured = false;
312 long calc_num_confl_to_do_this_iter(const size_t iteration_num) const;
313
314 vector<Lit> finalCl_tmp;
315 bool sort_and_clean_clause(
316 vector<Lit>& ps
317 , const vector<Lit>& origCl
318 , const bool red
319 , const bool sorted = false
320 );
321 void set_up_sql_writer();
322 vector<std::pair<string, string> > sql_tags;
323
324 void check_and_upd_config_parameters();
325 vector<uint32_t> tmp_xor_clash_vars;
326 void check_xor_cut_config_sanity() const;
327 void handle_found_solution(const lbool status, const bool only_indep_solution);
328 void add_every_combination_xor(const vector<Lit>& lits, bool attach, bool addDrat);
329 void add_xor_clause_inter_cleaned_cut(const vector<Lit>& lits, bool attach, bool addDrat);
330 unsigned num_bits_set(const size_t x, const unsigned max_size) const;
331 void check_too_large_variable_number(const vector<Lit>& lits) const;
332
333 lbool simplify_problem_outside();
334 void move_to_outside_assumps(const vector<Lit>* assumps);
335 vector<Lit> back_number_from_outside_to_outer_tmp;
back_number_from_outside_to_outer(const vector<Lit> & lits)336 void back_number_from_outside_to_outer(const vector<Lit>& lits)
337 {
338 back_number_from_outside_to_outer_tmp.clear();
339 for (const Lit lit: lits) {
340 assert(lit.var() < nVarsOutside());
341 if (get_num_bva_vars() > 0 || !fresh_solver) {
342 back_number_from_outside_to_outer_tmp.push_back(map_to_with_bva(lit));
343 assert(back_number_from_outside_to_outer_tmp.back().var() < nVarsOuter());
344 } else {
345 back_number_from_outside_to_outer_tmp.push_back(lit);
346 }
347 }
348 }
349 vector<Lit> outside_assumptions;
350
351 //Stats printing
352 void print_norm_stats(const double cpu_time, const double cpu_time_total) const;
353 void print_min_stats(const double cpu_time, const double cpu_time_total) const;
354 void print_full_restart_stat(const double cpu_time, const double cpu_time_total) const;
355
356 lbool simplify_problem(const bool startup);
357 lbool execute_inprocess_strategy(const bool startup, const string& strategy);
358 SolveStats solveStats;
359 void check_minimization_effectiveness(lbool status);
360 void check_recursive_minimization_effectiveness(const lbool status);
361 void extend_solution(const bool only_indep_solution);
362 void check_too_many_low_glues();
363 bool adjusted_glue_cutoff_if_too_many = false;
364
365 /////////////////////////////
366 // Temporary datastructs -- must be cleared before use
367 mutable std::vector<Lit> tmpCl;
368 mutable std::vector<uint32_t> tmpXor;
369
370
371 //learnt clause querying
372 uint32_t learnt_clause_query_max_len = std::numeric_limits<uint32_t>::max();
373 uint32_t learnt_clause_query_max_glue = std::numeric_limits<uint32_t>::max();
374 uint32_t learnt_clause_query_at = std::numeric_limits<uint32_t>::max();
375 uint32_t learnt_clause_query_watched_at = std::numeric_limits<uint32_t>::max();
376 uint32_t learnt_clause_query_watched_at_sub = std::numeric_limits<uint32_t>::max();
377 vector<uint32_t> learnt_clause_query_outer_to_without_bva_map;
378 bool all_vars_outside(const vector<Lit>& cl) const;
379 void learnt_clausee_query_map_without_bva(vector<Lit>& cl);
380
381 /////////////////////////////
382 //Renumberer
383 double calc_renumber_saving();
384 void free_unused_watches();
385 uint64_t last_full_watch_consolidate = 0;
386 void save_on_var_memory(uint32_t newNumVars);
387 void unSaveVarMem();
388 size_t calculate_interToOuter_and_outerToInter(
389 vector<uint32_t>& outerToInter
390 , vector<uint32_t>& interToOuter
391 );
392 void renumber_clauses(const vector<uint32_t>& outerToInter);
393 void test_renumbering() const;
394 bool clean_xor_clauses_from_duplicate_and_set_vars();
395 bool update_vars_of_xors(vector<Xor>& xors);
396
397 /////////////////////////////
398 // SAT solution verification
399 bool verify_model() const;
400 bool verify_model_implicit_clauses() const;
401 bool verify_model_long_clauses(const vector<ClOffset>& cs) const;
402
403
404 /////////////////////
405 // Data
406 size_t zeroLevAssignsByCNF = 0;
407 struct GivenW {
408 bool pos = false;
409 bool neg = false;
410 };
411 vector<GivenW> weights_given;
412
413 /////////////////////
414 // Clauses
415 bool addClauseHelper(vector<Lit>& ps);
416 bool addClauseInt(vector<Lit>& ps, const bool red = false);
417
418 /////////////////
419 // Debug
420
421 void print_watch_list(watch_subarray_const ws, const Lit lit) const;
422 void print_clause_size_distrib();
423 void check_model_for_assumptions() const;
424 };
425
set_decision_var(const uint32_t var)426 inline void Solver::set_decision_var(const uint32_t var)
427 {
428 insert_var_order_all(var);
429 }
430
getNumLongClauses()431 inline uint64_t Solver::getNumLongClauses() const
432 {
433 return longIrredCls.size() + longRedCls.size();
434 }
435
get_stats()436 inline const SearchStats& Solver::get_stats() const
437 {
438 return sumSearchStats;
439 }
440
get_solve_stats()441 inline const SolveStats& Solver::get_solve_stats() const
442 {
443 return solveStats;
444 }
445
get_num_long_irred_cls()446 inline size_t Solver::get_num_long_irred_cls() const
447 {
448 return longIrredCls.size();
449 }
450
get_num_long_red_cls()451 inline size_t Solver::get_num_long_red_cls() const
452 {
453 return longRedCls.size();
454 }
455
getConf()456 inline const SolverConf& Solver::getConf() const
457 {
458 return conf;
459 }
460
get_sql_tags()461 inline const vector<std::pair<string, string> >& Solver::get_sql_tags() const
462 {
463 return sql_tags;
464 }
465
getBinTriStats()466 inline const BinTriStats& Solver::getBinTriStats() const
467 {
468 return binTri;
469 }
470
471 template<class T>
clause_outer_numbered(const T & cl)472 inline vector<Lit> Solver::clause_outer_numbered(const T& cl) const
473 {
474 tmpCl.clear();
475 for(size_t i = 0; i < cl.size(); i++) {
476 tmpCl.push_back(map_inter_to_outer(cl[i]));
477 }
478
479 return tmpCl;
480 }
481
482 template<class T>
xor_outer_numbered(const T & cl)483 inline vector<uint32_t> Solver::xor_outer_numbered(const T& cl) const
484 {
485 tmpXor.clear();
486 for(size_t i = 0; i < cl.size(); i++) {
487 tmpXor.push_back(map_inter_to_outer(cl[i]));
488 }
489
490 return tmpXor;
491 }
492
move_to_outside_assumps(const vector<Lit> * assumps)493 inline void Solver::move_to_outside_assumps(const vector<Lit>* assumps)
494 {
495
496 if (assumps) {
497 #ifdef SLOW_DEBUG
498 outside_assumptions.clear();
499 for(const Lit lit: *assumps) {
500 if (lit.var() >= nVarsOutside()) {
501 std::cerr << "ERROR: Assumption variable " << (lit.var()+1)
502 << " is too large, you never"
503 << " inserted that variable into the solver. Exiting."
504 << endl;
505 exit(-1);
506 }
507 outside_assumptions.push_back(lit);
508 }
509 #else
510 outside_assumptions.resize(assumps->size());
511 std::copy(assumps->begin(), assumps->end(), outside_assumptions.begin());
512 #endif
513 } else {
514 outside_assumptions.clear();
515 }
516 }
517
simplify_with_assumptions(const vector<Lit> * _assumptions)518 inline lbool Solver::simplify_with_assumptions(
519 const vector<Lit>* _assumptions
520 ) {
521 fresh_solver = false;
522 move_to_outside_assumps(_assumptions);
523 return simplify_problem_outside();
524 }
525
find_with_watchlist_a_or_b(Lit a,Lit b,int64_t * limit)526 inline bool Solver::find_with_watchlist_a_or_b(Lit a, Lit b, int64_t* limit) const
527 {
528 if (watches[a].size() > watches[b].size()) {
529 std::swap(a,b);
530 }
531
532 watch_subarray_const ws = watches[a];
533 *limit -= ws.size();
534 for (const Watched w: ws) {
535 if (!w.isBin())
536 continue;
537
538 if (!w.red()
539 && w.lit2() == b
540 ) {
541 return true;
542 }
543 }
544
545 return false;
546 }
547
get_model()548 inline const vector<lbool>& Solver::get_model() const
549 {
550 return model;
551 }
552
get_final_conflict()553 inline const vector<Lit>& Solver::get_final_conflict() const
554 {
555 return conflict;
556 }
557
setConf(const SolverConf & _conf)558 inline void Solver::setConf(const SolverConf& _conf)
559 {
560 conf = _conf;
561 }
562
prop_at_head()563 inline bool Solver::prop_at_head() const
564 {
565 return qhead == trail.size()
566 // #ifdef USE_GAUSS
567 // && gqhead == trail.size()
568 // #endif
569 ;
570 }
571
model_value(const Lit p)572 inline lbool Solver::model_value (const Lit p) const
573 {
574 if (model[p.var()] == l_Undef)
575 return l_Undef;
576
577 return model[p.var()] ^ p.sign();
578 }
579
model_value(const uint32_t p)580 inline lbool Solver::model_value (const uint32_t p) const
581 {
582 return model[p];
583 }
584
testing_set_solver_not_fresh()585 inline void Solver::testing_set_solver_not_fresh()
586 {
587 fresh_solver = false;
588 }
589
free_cl(Clause * cl)590 inline void Solver::free_cl(Clause* cl)
591 {
592 #ifdef STATS_NEEDED
593 stats_del_cl(cl);
594 #endif
595 cl_alloc.clauseFree(cl);
596 }
597
free_cl(ClOffset offs)598 inline void Solver::free_cl(ClOffset offs)
599 {
600 #ifdef STATS_NEEDED
601 stats_del_cl(offs);
602 #endif
603 cl_alloc.clauseFree(offs);
604 }
605
606 } //end namespace
607
608 #endif //SOLVER_H
609