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