From b1090f43994577b9156a23d85786c2942e035875 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 31 Jul 2017 09:49:11 -0700 Subject: [PATCH] n/a Signed-off-by: Nikolaj Bjorner --- src/sat/ba_solver.cpp | 100 +++++++++++++++++++++++++++++++++---- src/sat/ba_solver.h | 2 + src/sat/sat_extension.h | 18 ++++++- src/sat/sat_simplifier.cpp | 74 ++++++++++++++------------- src/sat/sat_simplifier.h | 2 + 5 files changed, 151 insertions(+), 45 deletions(-) diff --git a/src/sat/ba_solver.cpp b/src/sat/ba_solver.cpp index 0b28c21a7..1f236a9c7 100644 --- a/src/sat/ba_solver.cpp +++ b/src/sat/ba_solver.cpp @@ -1812,8 +1812,8 @@ namespace sat { } } else { - unsigned coeff = 0; - for (unsigned j = 0; j < p.num_watch(); ++j) { + unsigned coeff = 0, j = 0; + for (; j < p.size(); ++j) { if (p[j].second == l) { coeff = p[j].first; break; @@ -1828,10 +1828,11 @@ namespace sat { SASSERT(coeff > 0); unsigned slack = p.slack() - coeff; + j = std::max(j + 1, p.num_watch()); - for (unsigned i = p.num_watch(); i < p.size(); ++i) { - literal lit = p[i].second; - unsigned w = p[i].first; + for (; j < p.size(); ++j) { + literal lit = p[j].second; + unsigned w = p[j].first; SASSERT(l_false == value(lit)); if (slack + w < k) { slack += w; @@ -2118,9 +2119,11 @@ namespace sat { }; void ba_solver::gc() { - std::stable_sort(m_learned.begin(), m_learned.end(), constraint_glue_lt()); - gc_half("glue"); - cleanup_constraints(m_learned, true); + if (m_learned.size() >= 2 * m_constraints.size()) { + std::stable_sort(m_learned.begin(), m_learned.end(), constraint_glue_lt()); + gc_half("glue"); + cleanup_constraints(m_learned, true); + } } void ba_solver::gc_half(char const* st_name) { @@ -2274,7 +2277,7 @@ namespace sat { } while (m_simplify_change || trail_sz < s().init_trail_size()); - IF_VERBOSE(1, verbose_stream() << "(ba.simplify :trail " << trail_sz + IF_VERBOSE(1, verbose_stream() << "(ba.simplify " << " :vars " << s().num_vars() - trail_sz << " :constraints " << m_constraints.size() << " :lemmas " << m_learned.size() @@ -3133,6 +3136,85 @@ namespace sat { return result; } + void ba_solver::init_use_list(ext_use_list& ul) { + ul.init(s().num_vars()); + for (constraint const* cp : m_constraints) { + ext_constraint_idx idx = cp->index(); + if (cp->lit() != null_literal) { + ul.insert(cp->lit(), idx); + ul.insert(~cp->lit(), idx); + } + switch (cp->tag()) { + case card_t: { + card const& c = cp->to_card(); + for (literal l : c) { + ul.insert(l, idx); + } + break; + } + case pb_t: { + pb const& p = cp->to_pb(); + for (wliteral w : p) { + ul.insert(w.second, idx); + } + break; + } + case xor_t: { + xor const& x = cp->to_xor(); + for (literal l : x) { + ul.insert(l, idx); + ul.insert(~l, idx); + } + break; + } + default: + UNREACHABLE(); + } + } + } + + // + // literal is used in a clause (C or l), it + // it occurs negatively in constraint c. + // all literals in C are marked + // + bool ba_solver::is_blocked(literal l, ext_constraint_idx idx) { + constraint const& c = index2constraint(idx); + simplifier& sim = s().m_simplifier; + if (c.lit() != null_literal) return false; + switch (c.tag()) { + case card_t: { + card const& ca = c.to_card(); + unsigned weight = 0; + for (literal l2 : ca) { + if (sim.is_marked(~l2)) ++weight; + } + return weight >= ca.k(); + } + case pb_t: { + pb const& p = c.to_pb(); + unsigned weight = 0, offset = 0; + for (wliteral l2 : p) { + if (~l2.second == l) { + offset = l2.first; + break; + } + } + SASSERT(offset != 0); + for (wliteral l2 : p) { + if (sim.is_marked(~l2.second)) { + weight += std::min(offset, l2.first); + } + } + return weight >= p.k(); + } + default: + break; + } + return false; + } + + void ba_solver::find_mutexes(literal_vector& lits, vector & mutexes) { literal_set slits(lits); bool change = false; diff --git a/src/sat/ba_solver.h b/src/sat/ba_solver.h index d40611dfe..4433017dc 100644 --- a/src/sat/ba_solver.h +++ b/src/sat/ba_solver.h @@ -444,6 +444,8 @@ namespace sat { virtual void pop_reinit(); virtual void gc(); virtual double get_reward(literal l, ext_justification_idx idx, literal_occs_fun& occs) const; + virtual void init_use_list(ext_use_list& ul); + virtual bool is_blocked(literal l, ext_constraint_idx idx); ptr_vector const & constraints() const { return m_constraints; } diff --git a/src/sat/sat_extension.h b/src/sat/sat_extension.h index 87f1904ed..0278bdb61 100644 --- a/src/sat/sat_extension.h +++ b/src/sat/sat_extension.h @@ -31,8 +31,20 @@ namespace sat { class literal_occs_fun { public: - virtual double operator()(literal l) = 0; - + virtual double operator()(literal l) = 0; + }; + + + typedef svector ext_constraint_list; + + class ext_use_list { + vector m_use_list; + public: + void init(unsigned num_vars) { m_use_list.reset(); m_use_list.resize(num_vars*2); } + void insert(literal l, ext_constraint_idx idx) { get(l).push_back(idx); } + ext_constraint_list & get(literal l) { return m_use_list[l.index()]; } + ext_constraint_list const & get(literal l) const { return m_use_list[l.index()]; } + void finalize() { m_use_list.finalize(); } }; class extension { @@ -62,6 +74,8 @@ namespace sat { virtual void gc() = 0; virtual void pop_reinit() = 0; virtual bool validate() = 0; + virtual void init_use_list(ext_use_list& ul) = 0; + virtual bool is_blocked(literal l, ext_constraint_idx) = 0; }; }; diff --git a/src/sat/sat_simplifier.cpp b/src/sat/sat_simplifier.cpp index 9c31f4005..37a7a8cd7 100644 --- a/src/sat/sat_simplifier.cpp +++ b/src/sat/sat_simplifier.cpp @@ -70,7 +70,13 @@ namespace sat { inline watch_list const & simplifier::get_wlist(literal l) const { return s.get_wlist(l); } - inline bool simplifier::is_external(bool_var v) const { return s.is_external(v); } + inline bool simplifier::is_external(bool_var v) const { + return + s.is_assumption(v) || + (s.is_external(v) && + (!m_ext_use_list.get(literal(v, false)).empty() || + !m_ext_use_list.get(literal(v, true)).empty())); + } inline bool simplifier::was_eliminated(bool_var v) const { return s.was_eliminated(v); } @@ -130,6 +136,7 @@ namespace sat { m_visited.finalize(); m_bs_cs.finalize(); m_bs_ls.finalize(); + m_ext_use_list.finalize(); } void simplifier::initialize() { @@ -137,6 +144,7 @@ namespace sat { s.m_cleaner(true); m_last_sub_trail_sz = s.m_trail.size(); m_use_list.init(s.num_vars()); + if (s.m_ext) s.m_ext->init_use_list(m_ext_use_list); m_sub_todo.reset(); m_sub_bin_todo.reset(); m_elim_todo.reset(); @@ -187,7 +195,7 @@ namespace sat { subsume(); if (s.inconsistent()) return; - if (!learned && m_resolution) + if (!learned && m_resolution && s.m_config.m_num_threads == 1) elim_vars(); if (s.inconsistent()) return; @@ -937,7 +945,7 @@ namespace sat { } bool process_var(bool_var v) { - return !s.is_external(v) && !s.was_eliminated(v); + return !s.s.is_assumption(v) && !s.was_eliminated(v); } void operator()(unsigned num_vars) { @@ -989,7 +997,7 @@ namespace sat { } s.unmark_all(c); it.next(); - } + } } for (clause* c : m_to_remove) { s.remove_clause(*c); @@ -1028,33 +1036,34 @@ namespace sat { } bool all_tautology(literal l) { - { - watch_list & wlist = s.get_wlist(l); - m_counter -= wlist.size(); - watch_list::iterator it = wlist.begin(); - watch_list::iterator end = wlist.end(); - for (; it != end; ++it) { - if (!it->is_binary_non_learned_clause()) - continue; - if (!s.is_marked(~it->get_literal())) - return false; - } + watch_list & wlist = s.get_wlist(l); + m_counter -= wlist.size(); + for (auto const& w : wlist) { + if (w.is_binary_non_learned_clause() && + !s.is_marked(~w.get_literal())) + return false; } - { - clause_use_list & neg_occs = s.m_use_list.get(~l); - clause_use_list::iterator it = neg_occs.mk_iterator(); - while (!it.at_end()) { - clause & c = it.curr(); - m_counter -= c.size(); - unsigned sz = c.size(); - unsigned i; - for (i = 0; i < sz; i++) { - if (s.is_marked(~c[i])) - break; - } - if (i == sz) - return false; - it.next(); + + clause_use_list & neg_occs = s.m_use_list.get(~l); + clause_use_list::iterator it = neg_occs.mk_iterator(); + while (!it.at_end()) { + clause & c = it.curr(); + m_counter -= c.size(); + unsigned sz = c.size(); + unsigned i; + for (i = 0; i < sz; i++) { + if (s.is_marked(~c[i])) + break; + } + if (i == sz) + return false; + it.next(); + } + + ext_constraint_list const& ext_list = s.m_ext_use_list.get(~l); + for (ext_constraint_idx idx : ext_list) { + if (!s.s.m_ext->is_blocked(l, idx)) { + return false; } } return true; @@ -1171,8 +1180,8 @@ namespace sat { SASSERT(c1.contains(l)); SASSERT(c2.contains(~l)); bool res = true; + m_elim_counter -= c1.size() + c2.size(); unsigned sz = c1.size(); - m_elim_counter -= sz; for (unsigned i = 0; i < sz; ++i) { literal l2 = c1[i]; if (l == l2) @@ -1183,7 +1192,6 @@ namespace sat { literal not_l = ~l; sz = c2.size(); - m_elim_counter -= sz; for (unsigned i = 0; i < sz; ++i) { literal l2 = c2[i]; if (not_l == l2) @@ -1199,8 +1207,6 @@ namespace sat { sz = c1.size(); for (unsigned i = 0; i < sz; ++i) { literal l2 = c1[i]; - if (l == l2) - continue; m_visited[l2.index()] = false; } return res; diff --git a/src/sat/sat_simplifier.h b/src/sat/sat_simplifier.h index 626d91ff7..5e4dc9de3 100644 --- a/src/sat/sat_simplifier.h +++ b/src/sat/sat_simplifier.h @@ -26,6 +26,7 @@ Revision History: #include"sat_clause_set.h" #include"sat_clause_use_list.h" #include"sat_watched.h" +#include"sat_extension.h" #include"sat_model_converter.h" #include"heap.h" #include"statistics.h" @@ -51,6 +52,7 @@ namespace sat { solver & s; unsigned m_num_calls; use_list m_use_list; + ext_use_list m_ext_use_list; clause_set m_sub_todo; svector m_sub_bin_todo; unsigned m_last_sub_trail_sz; // size of the trail since last cleanup