1 /*++ 2 Copyright (c) 2011 Microsoft Corporation 3 4 Module Name: 5 6 sat_simplifier.h 7 8 Abstract: 9 10 SAT simplification procedures that use a "full" occurrence list: 11 Subsumption, Blocked Clause Removal, Variable Elimination, ... 12 13 14 Author: 15 16 Leonardo de Moura (leonardo) 2011-05-24. 17 18 Revision History: 19 20 --*/ 21 #pragma once 22 23 #include "sat/sat_types.h" 24 #include "sat/sat_clause.h" 25 #include "sat/sat_clause_set.h" 26 #include "sat/sat_clause_use_list.h" 27 #include "sat/sat_extension.h" 28 #include "sat/sat_watched.h" 29 #include "sat/sat_model_converter.h" 30 #include "util/heap.h" 31 #include "util/statistics.h" 32 #include "util/params.h" 33 34 namespace pb { 35 class solver; 36 } 37 38 namespace sat { 39 class solver; 40 41 class use_list { 42 vector<clause_use_list> m_use_list; 43 44 public: 45 void init(unsigned num_vars); reserve(unsigned num_vars)46 void reserve(unsigned num_vars) { while (m_use_list.size() <= 2*num_vars) m_use_list.push_back(clause_use_list()); } 47 void insert(clause & c); 48 void block(clause & c); 49 void unblock(clause & c); 50 void erase(clause & c); 51 void erase(clause & c, literal l); get(literal l)52 clause_use_list& get(literal l) { return m_use_list[l.index()]; } get(literal l)53 clause_use_list const& get(literal l) const { return m_use_list[l.index()]; } finalize()54 void finalize() { m_use_list.finalize(); } display(std::ostream & out,literal l)55 std::ostream& display(std::ostream& out, literal l) const { return m_use_list[l.index()].display(out); } 56 }; 57 58 class simplifier { 59 friend class pb::solver; 60 friend class elim_vars; 61 solver & s; 62 unsigned m_num_calls; 63 use_list m_use_list; 64 ext_use_list m_ext_use_list; 65 clause_set m_sub_todo; 66 svector<bin_clause> m_sub_bin_todo; 67 unsigned m_last_sub_trail_sz; // size of the trail since last cleanup 68 bool_var_set m_elim_todo; 69 bool m_need_cleanup; 70 tmp_clause m_dummy; 71 72 // simplifier extra variable fields. 73 svector<char> m_visited; // transient 74 75 // counters 76 int m_sub_counter; 77 int m_elim_counter; 78 79 // config 80 bool m_abce; // block clauses using asymmetric added literals 81 bool m_cce; // covered clause elimination 82 bool m_acce; // cce with asymmetric literal addition 83 bool m_bca; // blocked (binary) clause addition. 84 unsigned m_bce_delay; 85 bool m_bce; // blocked clause elimination 86 bool m_ate; // asymmetric tautology elimination 87 unsigned m_bce_at; 88 bool m_retain_blocked_clauses; 89 unsigned m_blocked_clause_limit; 90 bool m_incremental_mode; 91 bool m_resolution; 92 unsigned m_res_limit; 93 unsigned m_res_occ_cutoff; 94 unsigned m_res_occ_cutoff1; 95 unsigned m_res_occ_cutoff2; 96 unsigned m_res_occ_cutoff3; 97 unsigned m_res_lit_cutoff1; 98 unsigned m_res_lit_cutoff2; 99 unsigned m_res_lit_cutoff3; 100 unsigned m_res_cls_cutoff1; 101 unsigned m_res_cls_cutoff2; 102 103 bool m_subsumption; 104 unsigned m_subsumption_limit; 105 bool m_elim_vars; 106 bool m_elim_vars_bdd; 107 unsigned m_elim_vars_bdd_delay; 108 109 // stats 110 unsigned m_num_bce; 111 unsigned m_num_cce; 112 unsigned m_num_acce; 113 unsigned m_num_abce; 114 unsigned m_num_bca; 115 unsigned m_num_ate; 116 unsigned m_num_subsumed; 117 unsigned m_num_elim_vars; 118 unsigned m_num_sub_res; 119 unsigned m_num_elim_lits; 120 121 bool m_learned_in_use_lists; 122 unsigned m_old_num_elim_vars; 123 124 struct size_lt { operatorsize_lt125 bool operator()(clause const * c1, clause const * c2) const { return c1->size() > c2->size(); } 126 }; 127 128 void checkpoint(); 129 130 void initialize(); 131 132 void init_visited(); mark_visited(literal l)133 void mark_visited(literal l) { m_visited[l.index()] = true; } unmark_visited(literal l)134 void unmark_visited(literal l) { m_visited[l.index()] = false; } 135 136 void mark_all_but(clause const & c, literal l); 137 void unmark_all(clause const & c); 138 139 void register_clauses(clause_vector & cs); 140 141 void remove_clause(clause & c, bool is_unique); 142 void set_learned(clause & c); 143 void set_learned(literal l1, literal l2); 144 145 bool_var get_min_occ_var(clause const & c) const; 146 bool subsumes1(clause const & c1, clause const & c2, literal & l); 147 void collect_subsumed1_core(clause const & c, clause_vector & out, literal_vector & out_lits, literal target); 148 void collect_subsumed1(clause const & c, clause_vector & out, literal_vector & out_lits); 149 clause_vector m_bs_cs; 150 literal_vector m_bs_ls; 151 void back_subsumption1(clause & c); 152 void back_subsumption1(literal l1, literal l2, bool learned); 153 154 literal get_min_occ_var0(clause const & c) const; 155 bool subsumes0(clause const & c1, clause const & c2); 156 void collect_subsumed0_core(clause const & c1, clause_vector & out, literal target); 157 void collect_subsumed0(clause const & c1, clause_vector & out); 158 void back_subsumption0(clause & c1); 159 160 bool cleanup_clause(clause & c); 161 bool cleanup_clause(literal_vector & c); 162 void elim_lit(clause & c, literal l); 163 void elim_dup_bins(); 164 bool subsume_with_binaries(); 165 void mark_as_not_learned_core(watch_list & wlist, literal l2); 166 void mark_as_not_learned(literal l1, literal l2); 167 168 void cleanup_watches(); 169 void move_clauses(clause_vector & cs, bool learned); 170 void cleanup_clauses(clause_vector & cs, bool learned, bool vars_eliminated); 171 172 bool is_external(bool_var v) const; is_external(literal l)173 bool is_external(literal l) const { return is_external(l.var()); } 174 bool was_eliminated(bool_var v) const; 175 lbool value(bool_var v) const; 176 lbool value(literal l) const; 177 watch_list & get_wlist(literal l); 178 watch_list const & get_wlist(literal l) const; 179 180 struct blocked_clause_elim; 181 void elim_blocked_clauses(); 182 183 bool single_threaded() const; // { return s.m_config.m_num_threads == 1; } 184 bool bce_enabled_base() const; 185 bool ate_enabled() const; 186 bool bce_enabled() const; 187 bool acce_enabled() const; 188 bool cce_enabled() const; 189 bool abce_enabled() const; 190 bool bca_enabled() const; 191 bool elim_vars_bdd_enabled() const; 192 bool elim_vars_enabled() const; 193 194 unsigned num_nonlearned_bin(literal l) const; 195 unsigned get_to_elim_cost(bool_var v) const; 196 void order_vars_for_elim(bool_var_vector & r); 197 void collect_clauses(literal l, clause_wrapper_vector & r); 198 clause_wrapper_vector m_pos_cls; 199 clause_wrapper_vector m_neg_cls; 200 literal_vector m_new_cls; 201 bool resolve(clause_wrapper const & c1, clause_wrapper const & c2, literal l, literal_vector & r); 202 void save_clauses(model_converter::entry & mc_entry, clause_wrapper_vector const & cs); 203 void add_non_learned_binary_clause(literal l1, literal l2); 204 void remove_bin_clauses(literal l); 205 void remove_clauses(clause_use_list const & cs, literal l); 206 bool try_eliminate(bool_var v); 207 void elim_vars(); 208 209 struct blocked_cls_report; 210 struct subsumption_report; 211 struct elim_var_report; 212 213 class scoped_finalize { 214 simplifier& s; 215 public: scoped_finalize(simplifier & s)216 scoped_finalize(simplifier& s) : s(s) {} ~scoped_finalize()217 ~scoped_finalize() { s.scoped_finalize_fn(); } 218 }; 219 void scoped_finalize_fn(); 220 221 public: 222 simplifier(solver & s, params_ref const & p); 223 ~simplifier(); 224 init_search()225 void init_search() { m_num_calls = 0; } 226 insert_elim_todo(bool_var v)227 void insert_elim_todo(bool_var v) { m_elim_todo.insert(v); } 228 reset_todos()229 void reset_todos() { 230 m_elim_todo.reset(); 231 m_sub_todo.reset(); 232 m_sub_bin_todo.reset(); 233 } 234 235 void operator()(bool learned); 236 237 void updt_params(params_ref const & p); 238 static void collect_param_descrs(param_descrs & d); 239 240 void finalize(); 241 242 void collect_statistics(statistics & st) const; 243 void reset_statistics(); 244 245 void propagate_unit(literal l); 246 void subsume(); 247 is_marked(literal l)248 bool is_marked(literal l) const { return m_visited[l.index()] != 0; } 249 250 }; 251 }; 252 253