From 7580644d150d04b15d15ee1875a52b5c8a4fa6c5 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 29 Jun 2017 08:11:27 -0700 Subject: [PATCH] n/a Signed-off-by: Nikolaj Bjorner --- src/sat/ba_solver.cpp | 473 +++++++++++++++++++++++----------------- src/sat/ba_solver.h | 84 +++---- src/sat/sat_extension.h | 1 + src/sat/sat_solver.cpp | 57 ++--- 4 files changed, 336 insertions(+), 279 deletions(-) diff --git a/src/sat/ba_solver.cpp b/src/sat/ba_solver.cpp index d29ec509f..7d9e16df0 100644 --- a/src/sat/ba_solver.cpp +++ b/src/sat/ba_solver.cpp @@ -53,7 +53,7 @@ namespace sat { } ba_solver::card::card(literal lit, literal_vector const& lits, unsigned k): - constraint(card_t, lit, lits.size()), + constraint(card_t, lit, lits.size(), get_obj_size(lits.size())), m_k(k) { for (unsigned i = 0; i < size(); ++i) { m_lits[i] = lits[i]; @@ -104,7 +104,7 @@ namespace sat { } ba_solver::pb::pb(literal lit, svector const& wlits, unsigned k): - constraint(pb_t, lit, wlits.size()), + constraint(pb_t, lit, wlits.size(), get_obj_size(wlits.size())), m_k(k), m_slack(0), m_num_watch(0), @@ -137,8 +137,7 @@ namespace sat { } ba_solver::xor::xor(literal lit, literal_vector const& lits): - constraint(xor_t, lit, lits.size()) - { + constraint(xor_t, lit, lits.size(), get_obj_size(lits.size())) { for (unsigned i = 0; i < size(); ++i) { m_lits[i] = lits[i]; } @@ -169,9 +168,9 @@ namespace sat { } DEBUG_CODE( bool is_false = false; - for (unsigned k = 0; k < sz; ++k) { - SASSERT(!is_false || value(c[k]) == l_false); - is_false = value(c[k]) == l_false; + for (literal l : c) { + SASSERT(!is_false || value(l) == l_false); + is_false = value(l) == l_false; }); // j is the number of non-false, sz - j the number of false. @@ -220,7 +219,18 @@ namespace sat { get_wlist(~lit).push_back(watched(c.index())); } - void ba_solver::assign(card& c, literal lit) { + void ba_solver::set_conflict(constraint& c, literal lit) { + m_stats.m_num_conflicts++; + TRACE("sat", display(tout, c, true); ); + SASSERT(validate_conflict(c)); + if (c.is_xor() && value(lit) == l_true) lit.neg(); + SASSERT(value(lit) == l_false); + set_conflict(justification::mk_ext_justification(c.index()), ~lit); + SASSERT(inconsistent()); + } + + + void ba_solver::assign(constraint& c, literal lit) { switch (value(lit)) { case l_true: break; @@ -228,17 +238,14 @@ namespace sat { set_conflict(c, lit); break; default: - m_stats.m_num_card_propagations++; + m_stats.m_num_propagations++; m_num_propagations_since_pop++; //TRACE("sat", tout << "#prop: " << m_stats.m_num_propagations << " - " << c.lit() << " => " << lit << "\n";); - SASSERT(validate_unit_propagation(c)); + SASSERT(validate_unit_propagation(c, lit)); if (get_config().m_drat) { svector ps; literal_vector lits; - if (c.lit() != null_literal) lits.push_back(~c.lit()); - for (unsigned i = c.k(); i < c.size(); ++i) { - lits.push_back(c[i]); - } + get_antecedents(lit, c, lits); lits.push_back(lit); ps.push_back(drat::premise(drat::s_ext(), c.lit())); // null_literal case. drat_add(lits, ps); @@ -248,15 +255,6 @@ namespace sat { } } - void ba_solver::set_conflict(card& c, literal lit) { - m_stats.m_num_card_conflicts++; - TRACE("sat", display(tout, c, true); ); - SASSERT(validate_conflict(c)); - SASSERT(value(lit) == l_false); - set_conflict(justification::mk_ext_justification(c.index()), ~lit); - SASSERT(inconsistent()); - } - // pb: @@ -370,6 +368,10 @@ namespace sat { add_index(p, index, lit); } SASSERT(index < num_watch); + if (index >= num_watch) { + std::cout << "BAD assign. " << alit << " not found within " << num_watch << "\n"; + std::cout << p << "\n"; + } unsigned index1 = index + 1; for (; m_a_max == 0 && index1 < num_watch; ++index1) { @@ -423,6 +425,10 @@ namespace sat { while (!m_pb_undef.empty()) { index1 = m_pb_undef.back(); if (index1 == num_watch) index1 = index; // it was swapped with index above. + if (index1 >= num_watch) { + std::cout << "BAD assignment at position " << index1 << " with " << num_watch << "\n"; + std::cout << p << "\n"; + } literal lit = p[index1].second; SASSERT(value(lit) == l_undef); TRACE("sat", tout << index1 << " " << lit << "\n";); @@ -450,43 +456,7 @@ namespace sat { } void ba_solver::clear_watch(pb& p) { - unsigned sz = p.size(); - for (unsigned i = 0; i < sz; ++i) { - unwatch_literal(p[i].second, p); - } - } - - void ba_solver::set_conflict(pb& p, literal lit) { - m_stats.m_num_pb_conflicts++; - TRACE("sat", display(tout, p, true); ); - // SASSERT(validate_conflict(p)); - SASSERT(value(lit) == l_false); - set_conflict(justification::mk_ext_justification(p.index()), ~lit); - SASSERT(inconsistent()); - } - - void ba_solver::assign(pb& p, literal lit) { - switch (value(lit)) { - case l_true: - break; - case l_false: - set_conflict(p, lit); - break; - default: - SASSERT(validate_unit_propagation(p, lit)); - m_stats.m_num_pb_propagations++; - m_num_propagations_since_pop++; - if (get_config().m_drat) { - svector ps; - literal_vector lits; - get_pb_antecedents(lit, p, lits); - lits.push_back(lit); - ps.push_back(drat::premise(drat::s_ext(), p.lit())); - drat_add(lits, ps); - } - assign(lit, justification::mk_ext_justification(p.index())); - break; - } + for (wliteral wl : p) unwatch_literal(wl.second, p); } void ba_solver::unit_propagation_simplification(literal lit, literal_vector const& lits) { @@ -515,9 +485,7 @@ namespace sat { bool ba_solver::is_cardinality(pb const& p) { if (p.size() == 0) return false; unsigned w = p[0].first; - for (unsigned i = 1; i < p.size(); ++i) { - if (w != p[i].first) return false; - } + for (wliteral wl : p) if (w != wl.first) return false; return true; } @@ -604,6 +572,7 @@ namespace sat { // std::cout << "new size: " << sz << " old size " << p.size() << "\n"; p.update_size(sz); p.update_k(p.k() - true_val); + p.update_max_sum(); // display(verbose_stream(), c, true); if (p.lit() == null_literal) { init_watch(p, true); @@ -617,11 +586,13 @@ namespace sat { } } - void ba_solver::remove_constraint(pb& p) { - clear_watch(p); - nullify_tracking_literal(p); - p.remove(); - m_constraint_removed = true; + void ba_solver::display(std::ostream& out, constraint const& c, bool values) const { + switch (c.tag()) { + case card_t: display(out, c.to_card(), values); break; + case pb_t: display(out, c.to_pb(), values); break; + case xor_t: display(out, c.to_xor(), values); break; + default: UNREACHABLE(); break; + } } void ba_solver::display(std::ostream& out, pb const& p, bool values) const { @@ -711,44 +682,6 @@ namespace sat { } } - void ba_solver::assign(xor& x, literal lit) { - SASSERT(!inconsistent()); - switch (value(lit)) { - case l_true: - break; - case l_false: - set_conflict(x, lit); - SASSERT(inconsistent()); - break; - default: - m_stats.m_num_xor_propagations++; - m_num_propagations_since_pop++; - if (get_config().m_drat) { - svector ps; - literal_vector lits; - if (x.lit() != null_literal) lits.push_back(~x.lit()); - for (unsigned i = 1; i < x.size(); ++i) { - lits.push_back(x[i]); - } - lits.push_back(lit); - ps.push_back(drat::premise(drat::s_ext(), x.lit())); - drat_add(lits, ps); - } - TRACE("sat", display(tout << lit << " ", x, true);); - assign(lit, justification::mk_ext_justification(x.index())); - break; - } - } - - void ba_solver::set_conflict(xor& x, literal lit) { - m_stats.m_num_xor_conflicts++; - TRACE("sat", display(tout, x, true); ); - if (value(lit) == l_true) lit.neg(); - SASSERT(validate_conflict(x)); - TRACE("sat", display(tout << lit << " ", x, true);); - set_conflict(justification::mk_ext_justification(x.index()), ~lit); - SASSERT(inconsistent()); - } lbool ba_solver::add_assign(xor& x, literal alit) { // literal is assigned @@ -854,6 +787,8 @@ namespace sat { m_active_vars.reset(); } + static bool _debug_conflict = false; + bool ba_solver::resolve_conflict() { if (0 == m_num_propagations_since_pop) { return false; @@ -879,6 +814,8 @@ namespace sat { vector jus; + // if (null_literal != consequent) std::cout << "resolve " << consequent << " " << value(consequent) << "\n"; + do { if (offset == 0) { @@ -900,6 +837,11 @@ namespace sat { DEBUG_CODE(justification2pb(js, consequent, offset, m_B);); + if (_debug_conflict) { + std::cout << consequent << "\n"; + s().display_justification(std::cout, js); + std::cout << "\n"; + } switch(js.get_kind()) { case justification::NONE: SASSERT (consequent != null_literal); @@ -940,12 +882,12 @@ namespace sat { } case justification::EXT_JUSTIFICATION: { constraint& cnstr = index2constraint(js.get_ext_justification_idx()); + ++m_stats.m_num_resolves; switch (cnstr.tag()) { case card_t: { card& c = cnstr.to_card(); m_bound += offset * c.k(); process_card(c, offset); - ++m_stats.m_num_card_resolves; break; } case pb_t: { @@ -953,10 +895,13 @@ namespace sat { m_lemma.reset(); m_bound += offset; inc_coeff(consequent, offset); - get_pb_antecedents(consequent, p, m_lemma); + get_antecedents(consequent, p, m_lemma); TRACE("sat", display(tout, p, true); tout << m_lemma << "\n";); + if (_debug_conflict) { + std::cout << consequent << " "; + std::cout << "antecedents: " << m_lemma << "\n"; + } for (literal l : m_lemma) process_antecedent(~l, offset); - ++m_stats.m_num_pb_resolves; break; } case xor_t: { @@ -966,7 +911,6 @@ namespace sat { inc_coeff(consequent, offset); get_xor_antecedents(consequent, idx, js, m_lemma); for (literal l : m_lemma) process_antecedent(~l, offset); - ++m_stats.m_num_xor_resolves; break; } default: @@ -1118,6 +1062,19 @@ namespace sat { s().reset_mark(v); --m_num_marks; } + if (idx == 0 && !_debug_conflict) { + _debug_conflict = true; + // s().display(std::cout); + std::cout << s().m_not_l << "\n"; + for (literal l : lits) { + if (s().is_marked(l.var())) { + std::cout << "missing mark: " << l << "\n"; + s().reset_mark(l.var()); + } + } + m_num_marks = 0; + resolve_conflict(); + } --idx; } return false; @@ -1185,7 +1142,8 @@ namespace sat { } void ba_solver::add_at_least(literal lit, literal_vector const& lits, unsigned k) { - card* c = new (memory::allocate(card::get_obj_size(lits.size()))) card(lit, lits, k); + void * mem = m_allocator.allocate(card::get_obj_size(lits.size())); + card* c = new (mem) card(lit, lits, k); add_constraint(c); } @@ -1222,7 +1180,8 @@ namespace sat { } void ba_solver::add_pb_ge(literal lit, svector const& wlits, unsigned k) { - pb* p = new (memory::allocate(pb::get_obj_size(wlits.size()))) pb(lit, wlits, k); + void * mem = m_allocator.allocate(pb::get_obj_size(wlits.size())); + pb* p = new (mem) pb(lit, wlits, k); add_constraint(p); } @@ -1236,7 +1195,8 @@ namespace sat { } void ba_solver::add_xor(literal lit, literal_vector const& lits) { - xor* x = new (memory::allocate(xor::get_obj_size(lits.size()))) xor(lit, lits); + void * mem = m_allocator.allocate(xor::get_obj_size(lits.size())); + xor* x = new (mem) xor(lit, lits); add_constraint(x); for (literal l : lits) s().set_external(l.var()); // TBD: determine if goal2sat does this. } @@ -1287,7 +1247,6 @@ namespace sat { unsigned level = lvl(l); bool_var v = l.var(); SASSERT(js.get_kind() == justification::EXT_JUSTIFICATION); - SASSERT(index2constraint(index).is_xor()); TRACE("sat", tout << l << ": " << js << "\n"; tout << s().m_trail << "\n";); unsigned num_marks = 0; @@ -1362,24 +1321,47 @@ namespace sat { TRACE("sat", tout << r << "\n";); } - void ba_solver::get_pb_antecedents(literal l, pb const& p, literal_vector& r) { + void ba_solver::get_antecedents(literal l, pb const& p, literal_vector& r) { if (p.lit() != null_literal) r.push_back(p.lit()); SASSERT(p.lit() == null_literal || value(p.lit()) == l_true); TRACE("sat", display(tout, p, true);); if (value(l) == l_false) { + // The literal comes from a conflict. + // it is forced true, but assigned to false. unsigned slack = 0; unsigned miss = 0; + unsigned worth = 0; + unsigned k = p.k(); for (wliteral wl : p) { literal lit = wl.second; - if (lit != l && value(lit) == l_false) { - r.push_back(~lit); + if (lit == l) { + worth = wl.first; + } + else if (value(lit) == l_false) { miss += wl.first; - } + } else { slack += wl.first; } } + SASSERT(slack < k); + SASSERT(0 < worth); + + slack += worth; + for (wliteral wl : p) { + literal lit = wl.second; + if (lit != l && value(lit) == l_false) { + unsigned w = wl.first; + if (slack + w >= k) { + r.push_back(~lit); + } + else { + slack += w; + std::cout << "increase slack by " << w << " to " << slack << " worth: " << worth << "\n"; + } + } + } #if 0 std::cout << p << "\n"; std::cout << r << "\n"; @@ -1388,7 +1370,6 @@ namespace sat { return; } - // unsigned coeff = get_coeff(p, l); unsigned coeff = 0; for (unsigned j = 0; j < p.num_watch(); ++j) { if (p[j].second == l) { @@ -1396,6 +1377,11 @@ namespace sat { break; } } + + if (_debug_conflict) { + std::cout << p << "\n"; + std::cout << l << " " << coeff << " num_watch: " << p.num_watch() << "\n"; + } CTRACE("sat", coeff == 0, display(tout << l << " coeff: " << coeff << "\n", p, true);); @@ -1423,7 +1409,7 @@ namespace sat { // no-op } - void ba_solver::get_card_antecedents(literal l, card const& c, literal_vector& r) { + void ba_solver::get_antecedents(literal l, card const& c, literal_vector& r) { DEBUG_CODE( bool found = false; for (unsigned i = 0; !found && i < c.k(); ++i) { @@ -1439,7 +1425,7 @@ namespace sat { } } - void ba_solver::get_xor_antecedents(literal l, xor const& x, literal_vector& r) { + void ba_solver::get_antecedents(literal l, xor const& x, literal_vector& r) { if (x.lit() != null_literal) r.push_back(x.lit()); // TRACE("sat", display(tout << l << " ", x, true);); SASSERT(x.lit() == null_literal || value(x.lit()) == l_true); @@ -1459,15 +1445,68 @@ namespace sat { } void ba_solver::get_antecedents(literal l, ext_justification_idx idx, literal_vector & r) { - constraint& c = index2constraint(idx); + get_antecedents(l, index2constraint(idx), r); + } + + void ba_solver::get_antecedents(literal l, constraint const& c, literal_vector& r) { switch (c.tag()) { - case card_t: get_card_antecedents(l, c.to_card(), r); break; - case pb_t: get_pb_antecedents(l, c.to_pb(), r); break; - case xor_t: get_xor_antecedents(l, c.to_xor(), r); break; + case card_t: get_antecedents(l, c.to_card(), r); break; + case pb_t: get_antecedents(l, c.to_pb(), r); break; + case xor_t: get_antecedents(l, c.to_xor(), r); break; default: UNREACHABLE(); break; } } + bool ba_solver::validate_unit_propagation(constraint const& c, literal l) const { + switch (c.tag()) { + case card_t: return validate_unit_propagation(c.to_card(), l); + case pb_t: return validate_unit_propagation(c.to_pb(), l); + case xor_t: return true; + default: UNREACHABLE(); break; + } + return false; + } + + bool ba_solver::validate_conflict(constraint const& c) const { + switch (c.tag()) { + case card_t: return validate_conflict(c.to_card()); + case pb_t: return validate_conflict(c.to_pb()); + case xor_t: return validate_conflict(c.to_xor()); + default: UNREACHABLE(); break; + } + return false; + } + + /** + \brief Lex on (glue, size) + */ + struct constraint_glue_lt { + bool operator()(ba_solver::constraint const * c1, ba_solver::constraint const * c2) const { + return + (c1->glue() < c2->glue()) || + (c1->glue() == c2->glue() && c1->size() < c2->size()); + } + }; + + void ba_solver::gc() { + std::stable_sort(m_learned.begin(), m_learned.end(), constraint_glue_lt()); + gc_half("glue"); + cleanup_constraints(m_learned); + } + + void ba_solver::gc_half(char const* st_name) { + TRACE("sat", tout << "gc\n";); + unsigned sz = m_learned.size(); + unsigned new_sz = sz/2; + unsigned j = new_sz; + for (unsigned i = new_sz; i < sz; i++) { + remove_constraint(*(m_learned[i])); + } + m_learned.shrink(j); + IF_VERBOSE(SAT_VB_LVL, verbose_stream() << "(sat-gc :strategy " << st_name << " :deleted " << (sz - j) << ")\n";); + + } + void ba_solver::nullify_tracking_literal(constraint& c) { if (c.lit() != null_literal) { get_wlist(c.lit()).erase(watched(c.index())); @@ -1476,9 +1515,21 @@ namespace sat { } } - void ba_solver::remove_constraint(card& c) { - clear_watch(c); + void ba_solver::remove_constraint(constraint& c) { nullify_tracking_literal(c); + switch (c.tag()) { + case card_t: + clear_watch(c.to_card()); + break; + case pb_t: + clear_watch(c.to_pb()); + break; + case xor_t: + clear_watch(c.to_xor()); + break; + default: + UNREACHABLE(); + } c.remove(); m_constraint_removed = true; } @@ -1616,9 +1667,7 @@ namespace sat { // assigned l_true. if (index != bound) { c.swap(index, bound); - } - SASSERT(validate_unit_propagation(c)); - + } for (unsigned i = 0; i < bound && !inconsistent(); ++i) { assign(c, c[i]); } @@ -1639,23 +1688,11 @@ namespace sat { void ba_solver::pop_constraint() { constraint* c = m_constraints.back(); m_constraints.pop_back(); - nullify_tracking_literal(*c); - switch (c->tag()) { - case card_t: - clear_watch(c->to_card()); - break; - case pb_t: - clear_watch(c->to_pb()); - break; - case xor_t: - clear_watch(c->to_xor()); - break; - default: - UNREACHABLE(); - } - dealloc(c); + remove_constraint(*c); + m_allocator.deallocate(c->obj_size(), c); } + void ba_solver::pop(unsigned n) { TRACE("sat_verbose", tout << "pop:" << n << "\n";); unsigned new_lim = m_constraint_lim.size() - n; @@ -1693,7 +1730,15 @@ namespace sat { m_constraint_removed = false; trail_sz = s().init_trail_size(); for (constraint* c : m_constraints) simplify(*c); - gc(); + init_use_lists(); + remove_unused_defs(); + // take ownership of interface variables + for (constraint* c : m_constraints) { + if (c->lit() != null_literal) m_var_used[c->lit().var()] = true; + } + set_non_external(); + elim_pure(); + subsumption(); cleanup_clauses(); cleanup_constraints(); } @@ -1910,15 +1955,17 @@ namespace sat { return; } - p.update_size(sz); - p.update_k(k); - for (unsigned i = 0; i < sz; ++i) { wliteral wl = p[i]; unsigned w = std::min(k, wl.first); p[i] = wliteral(w, wl.second); } + p.update_size(sz); + p.update_k(k); + p.update_max_sum(); + + literal root = null_literal; if (p.lit() != null_literal) root = m_roots[p.lit().index()]; @@ -2000,9 +2047,7 @@ namespace sat { - resolution - blocked literals */ - void ba_solver::gc() { - - // remove constraints where indicator literal isn't used. + void ba_solver::init_use_lists() { m_visited.resize(s().num_vars()*2, false); m_clause_use_list.init(s().num_vars()); m_var_used.reset(); @@ -2051,6 +2096,10 @@ namespace sat { } } } + } + + void ba_solver::remove_unused_defs() { + // remove constraints where indicator literal isn't used. for (constraint* cp : m_constraints) { switch (cp->tag()) { case card_t: { @@ -2081,12 +2130,9 @@ namespace sat { break; } } + } - // take ownership of interface variables - for (constraint* cp : m_constraints) { - if (cp->lit() != null_literal) m_var_used[cp->lit().var()] = true; - } - + unsigned ba_solver::set_non_external() { // set variables to be non-external if they are not used in theory constraints. unsigned ext = 0; for (unsigned v = 0; v < s().num_vars(); ++v) { @@ -2095,7 +2141,11 @@ namespace sat { ++ext; } } + IF_VERBOSE(10, verbose_stream() << "non-external variables converted: " << ext << "\n";); + return ext; + } + unsigned ba_solver::elim_pure() { // eliminate pure literals unsigned pure_literals = 0; for (unsigned v = 0; v < s().num_vars(); ++v) { @@ -2113,10 +2163,11 @@ namespace sat { ++pure_literals; } } - IF_VERBOSE(10, - verbose_stream() << "non-external variables converted: " << ext << "\n"; - verbose_stream() << "pure literals converted: " << pure_literals << "\n";); + IF_VERBOSE(10, verbose_stream() << "pure literals converted: " << pure_literals << "\n";); + return pure_literals; + } + void ba_solver::subsumption() { unsigned bin_sub = m_stats.m_num_bin_subsumes; unsigned clause_sub = m_stats.m_num_clause_subsumes; unsigned card_sub = m_stats.m_num_card_subsumes; @@ -2163,13 +2214,19 @@ namespace sat { void ba_solver::cleanup_constraints() { if (!m_constraint_removed) return; - ptr_vector::iterator it = m_constraints.begin(); + cleanup_constraints(m_constraints); + cleanup_constraints(m_learned); + m_constraint_removed = false; + } + + void ba_solver::cleanup_constraints(ptr_vector& cs) { + ptr_vector::iterator it = cs.begin(); ptr_vector::iterator it2 = it; - ptr_vector::iterator end = m_constraints.end(); + ptr_vector::iterator end = cs.end(); for (; it != end; ++it) { constraint& c = *(*it); if (c.was_removed()) { - dealloc(&c); + m_allocator.deallocate(c.obj_size(), &c); } else { if (it != it2) { @@ -2178,8 +2235,7 @@ namespace sat { ++it2; } } - m_constraints.set_end(it2); - m_constraint_removed = false; + cs.set_end(it2); } /* @@ -2517,54 +2573,74 @@ namespace sat { } void ba_solver::collect_statistics(statistics& st) const { - st.update("cardinality propagations", m_stats.m_num_card_propagations); - st.update("cardinality conflicts", m_stats.m_num_card_conflicts); - st.update("cardinality resolves", m_stats.m_num_card_resolves); - st.update("xor propagations", m_stats.m_num_xor_propagations); - st.update("xor conflicts", m_stats.m_num_xor_conflicts); - st.update("xor resolves", m_stats.m_num_xor_resolves); - st.update("pb propagations", m_stats.m_num_pb_propagations); - st.update("pb conflicts", m_stats.m_num_pb_conflicts); - st.update("pb resolves", m_stats.m_num_pb_resolves); + st.update("ba propagations", m_stats.m_num_propagations); + st.update("ba conflicts", m_stats.m_num_conflicts); + st.update("ba resolves", m_stats.m_num_resolves); } - bool ba_solver::validate_conflict(card& c) { - if (!validate_unit_propagation(c)) return false; + bool ba_solver::validate_conflict(card const& c) const { + if (c.lit() != null_literal && value(c.lit()) != l_true) { + return false; + } + for (unsigned i = c.k(); i < c.size(); ++i) { + if (value(c[i]) != l_false) return false; + } for (unsigned i = 0; i < c.k(); ++i) { if (value(c[i]) == l_false) return true; } return false; } - bool ba_solver::validate_conflict(xor& x) { + + bool ba_solver::validate_conflict(xor const& x) const { return !parity(x, 0); } - bool ba_solver::validate_unit_propagation(card const& c) { + + bool ba_solver::validate_conflict(pb const& p) const { + unsigned slack = 0; + for (wliteral wl : p) { + if (value(wl.second) != l_false) { + slack += wl.first; + } + } + return slack < p.k(); + } + + bool ba_solver::validate_unit_propagation(card const& c, literal alit) const { + (void) alit; if (c.lit() != null_literal && value(c.lit()) != l_true) return false; for (unsigned i = c.k(); i < c.size(); ++i) { if (value(c[i]) != l_false) return false; } return true; } - bool ba_solver::validate_unit_propagation(pb const& p, literal alit) { + + bool ba_solver::validate_unit_propagation(pb const& p, literal alit) const { if (p.lit() != null_literal && value(p.lit()) != l_true) return false; unsigned sum = 0; TRACE("sat", display(tout << "validate: " << alit << "\n", p, true);); - for (unsigned i = 0; i < p.size(); ++i) { - literal lit = p[i].second; + for (wliteral wl : p) { + literal lit = wl.second; lbool val = value(lit); if (val != l_false && lit != alit) { - sum += p[i].first; + sum += wl.first; } } return sum < p.k(); } + bool ba_solver::validate_unit_propagation(xor const& x, literal alit) const { + if (value(x.lit()) != l_true) return false; + for (unsigned i = 1; i < x.size(); ++i) { + if (value(x[i]) == l_undef) return false; + } + return true; + } + bool ba_solver::validate_lemma() { int val = -m_bound; normalize_active_coeffs(); - for (unsigned i = 0; i < m_active_vars.size(); ++i) { - bool_var v = m_active_vars[i]; + for (bool_var v : m_active_vars) { int coeff = get_coeff(v); literal lit(v, false); SASSERT(coeff != 0); @@ -2582,8 +2658,7 @@ namespace sat { void ba_solver::active2pb(ineq& p) { normalize_active_coeffs(); p.reset(m_bound); - for (unsigned i = 0; i < m_active_vars.size(); ++i) { - bool_var v = m_active_vars[i]; + for (bool_var v : m_active_vars) { literal lit(v, get_coeff(v) < 0); p.m_lits.push_back(lit); p.m_coeffs.push_back(get_abs_coeff(v)); @@ -2610,9 +2685,7 @@ namespace sat { case justification::CLAUSE: { ineq.reset(offset); clause & c = *(s().m_cls_allocator.get_clause(js.get_clause_offset())); - unsigned sz = c.size(); - for (unsigned i = 0; i < sz; i++) - ineq.push(c[i], offset); + for (literal l : c) ineq.push(l, offset); break; } case justification::EXT_JUSTIFICATION: { @@ -2622,29 +2695,23 @@ namespace sat { case card_t: { card& c = cnstr.to_card(); ineq.reset(offset*c.k()); - for (unsigned i = 0; i < c.size(); ++i) { - ineq.push(c[i], offset); - } + for (literal l : c) ineq.push(l, offset); if (c.lit() != null_literal) ineq.push(~c.lit(), offset*c.k()); break; } case pb_t: { pb& p = cnstr.to_pb(); ineq.reset(p.k()); - for (unsigned i = 0; i < p.size(); ++i) { - ineq.push(p[i].second, p[i].first); - } + for (wliteral wl : p) ineq.push(wl.second, wl.first); if (p.lit() != null_literal) ineq.push(~p.lit(), p.k()); break; } case xor_t: { xor& x = cnstr.to_xor(); literal_vector ls; - get_xor_antecedents(lit, x, ls); + get_antecedents(lit, x, ls); ineq.reset(offset); - for (unsigned i = 0; i < ls.size(); ++i) { - ineq.push(~ls[i], offset); - } + for (literal l : ls) ineq.push(~l, offset); literal lxor = x.lit(); if (lxor != null_literal) ineq.push(~lxor, offset); break; @@ -2729,13 +2796,13 @@ namespace sat { } bool ba_solver::validate_conflict(literal_vector const& lits, ineq& p) { - for (unsigned i = 0; i < lits.size(); ++i) { - if (value(lits[i]) != l_false) { - TRACE("sat", tout << "literal " << lits[i] << " is not false\n";); + for (literal l : lits) { + if (value(l) != l_false) { + TRACE("sat", tout << "literal " << l << " is not false\n";); return false; } } - unsigned value = 0; + unsigned value = 0; for (unsigned i = 0; i < p.m_lits.size(); ++i) { unsigned coeff = p.m_coeffs[i]; if (!lits.contains(p.m_lits[i])) { diff --git a/src/sat/ba_solver.h b/src/sat/ba_solver.h index 950580b20..ca6b0d093 100644 --- a/src/sat/ba_solver.h +++ b/src/sat/ba_solver.h @@ -32,15 +32,9 @@ namespace sat { friend class local_search; struct stats { - unsigned m_num_card_propagations; - unsigned m_num_card_conflicts; - unsigned m_num_card_resolves; - unsigned m_num_xor_propagations; - unsigned m_num_xor_conflicts; - unsigned m_num_xor_resolves; - unsigned m_num_pb_propagations; - unsigned m_num_pb_conflicts; - unsigned m_num_pb_resolves; + unsigned m_num_propagations; + unsigned m_num_conflicts; + unsigned m_num_resolves; unsigned m_num_bin_subsumes; unsigned m_num_clause_subsumes; unsigned m_num_card_subsumes; @@ -64,9 +58,11 @@ namespace sat { tag_t m_tag; bool m_removed; literal m_lit; + unsigned m_glue; unsigned m_size; + size_t m_obj_size; public: - constraint(tag_t t, literal l, unsigned sz): m_tag(t), m_removed(false), m_lit(l), m_size(sz) {} + constraint(tag_t t, literal l, unsigned sz, size_t osz): m_tag(t), m_removed(false), m_lit(l), m_glue(0), m_size(sz), m_obj_size(osz) {} ext_constraint_idx index() const { return reinterpret_cast(this); } tag_t tag() const { return m_tag; } literal lit() const { return m_lit; } @@ -76,8 +72,10 @@ namespace sat { bool was_removed() const { return m_removed; } void remove() { m_removed = true; } void nullify_literal() { m_lit = null_literal; } + unsigned glue() const { return m_glue; } + void set_glue(unsigned g) { m_glue = g; } - + size_t obj_size() const { return m_obj_size; } card& to_card(); pb& to_pb(); xor& to_xor(); @@ -117,7 +115,6 @@ namespace sat { unsigned m_num_watch; unsigned m_max_sum; wliteral m_wlits[0]; - void update_max_sum(); public: static size_t get_obj_size(unsigned num_lits) { return sizeof(pb) + num_lits * sizeof(wliteral); } pb(literal lit, svector const& wlits, unsigned k); @@ -136,6 +133,7 @@ namespace sat { void swap(unsigned i, unsigned j) { std::swap(m_wlits[i], m_wlits[j]); } void negate(); void update_k(unsigned k) { m_k = k; } + void update_max_sum(); literal_vector literals() const { literal_vector lits; for (auto wl : *this) lits.push_back(wl.second); return lits; } }; @@ -162,14 +160,15 @@ namespace sat { void push(literal l, unsigned c) { m_lits.push_back(l); m_coeffs.push_back(c); } }; - solver* m_solver; - lookahead* m_lookahead; - stats m_stats; + solver* m_solver; + lookahead* m_lookahead; + stats m_stats; + small_object_allocator m_allocator; + ptr_vector m_constraints; - - // watch literals - unsigned_vector m_constraint_lim; + ptr_vector m_learned; + unsigned_vector m_constraint_lim; // conflict resolution unsigned m_num_marks; @@ -190,8 +189,6 @@ namespace sat { void inc_parity(bool_var v); void reset_parity(bool_var v); - void pop_constraint(); - solver& s() const { return *m_solver; } @@ -206,7 +203,6 @@ namespace sat { bool m_constraint_removed; literal_vector m_roots; unsigned_vector m_weights; - void gc(); bool subsumes(card& c1, card& c2, literal_vector& comp); bool subsumes(card& c1, clause& c2, literal_vector& comp); bool subsumed(card& c1, literal l1, literal l2); @@ -218,11 +214,22 @@ namespace sat { bool is_marked(literal l) const { return m_visited[l.index()] != 0; } unsigned get_num_non_learned_bin(literal l); literal get_min_occurrence_literal(card const& c); + void init_use_lists(); + void remove_unused_defs(); + unsigned set_non_external(); + unsigned elim_pure(); + void subsumption(); void subsumption(card& c1); + void gc_half(char const* _method); + void cleanup_clauses(); void cleanup_constraints(); + void cleanup_constraints(ptr_vector& cs); + void remove_constraint(constraint& c); // constraints + constraint& index2constraint(size_t idx) const { return *reinterpret_cast(idx); } + void pop_constraint(); void unwatch_literal(literal w, constraint& c); void watch_literal(literal w, constraint& c); void watch_literal(wliteral w, pb& p); @@ -232,18 +239,20 @@ namespace sat { lbool add_assign(constraint& c, literal l); void simplify(constraint& c); void nullify_tracking_literal(constraint& c); + void set_conflict(constraint& c, literal lit); + void assign(constraint& c, literal lit); + void get_antecedents(literal l, constraint const& c, literal_vector & r); + bool validate_conflict(constraint const& c) const; + bool validate_unit_propagation(constraint const& c, literal alit) const; // cardinality void init_watch(card& c, bool is_true); - void assign(card& c, literal lit); lbool add_assign(card& c, literal lit); - void set_conflict(card& c, literal lit); void clear_watch(card& c); void reset_coeffs(); void reset_marked_literals(); - void get_card_antecedents(literal l, card const& c, literal_vector & r); + void get_antecedents(literal l, card const& c, literal_vector & r); void simplify(card& c); - void remove_constraint(card& c); void unit_propagation_simplification(literal lit, literal_vector const& lits); void flush_roots(card& c); void recompile(card& c); @@ -251,34 +260,27 @@ namespace sat { // xor specific functionality void clear_watch(xor& x); void init_watch(xor& x, bool is_true); - void assign(xor& x, literal lit); - void set_conflict(xor& x, literal lit); bool parity(xor const& x, unsigned offset) const; lbool add_assign(xor& x, literal alit); void get_xor_antecedents(literal l, unsigned index, justification js, literal_vector& r); - void get_xor_antecedents(literal l, xor const& x, literal_vector & r); + void get_antecedents(literal l, xor const& x, literal_vector & r); void simplify(xor& x); void flush_roots(xor& x); - - constraint& index2constraint(size_t idx) const { return *reinterpret_cast(idx); } - // pb functionality unsigned m_a_max; void init_watch(pb& p, bool is_true); lbool add_assign(pb& p, literal alit); void add_index(pb& p, unsigned index, literal lit); void clear_watch(pb& p); - void set_conflict(pb& p, literal lit); - void assign(pb& p, literal l); - void get_pb_antecedents(literal l, pb const& p, literal_vector & r); + void get_antecedents(literal l, pb const& p, literal_vector & r); void simplify(pb& p); void simplify2(pb& p); bool is_cardinality(pb const& p); - void remove_constraint(pb& p); void flush_roots(pb& p); void recompile(pb& p); + // access solver inline lbool value(literal lit) const { return m_lookahead ? m_lookahead->value(lit) : m_solver->value(lit); } inline unsigned lvl(literal lit) const { return m_solver->lvl(lit); } inline unsigned lvl(bool_var v) const { return m_solver->lvl(v); } @@ -301,12 +303,14 @@ namespace sat { void cut(); // validation utilities - bool validate_conflict(card& c); - bool validate_conflict(xor& x); + bool validate_conflict(card const& c) const; + bool validate_conflict(xor const& x) const; + bool validate_conflict(pb const& p) const; bool validate_assign(literal_vector const& lits, literal lit); bool validate_lemma(); - bool validate_unit_propagation(card const& c); - bool validate_unit_propagation(pb const& p, literal lit); + bool validate_unit_propagation(card const& c, literal alit) const; + bool validate_unit_propagation(pb const& p, literal alit) const; + bool validate_unit_propagation(xor const& x, literal alit) const; bool validate_conflict(literal_vector const& lits, ineq& p); ineq m_A, m_B, m_C; @@ -315,6 +319,7 @@ namespace sat { bool validate_resolvent(); void display(std::ostream& out, ineq& p) const; + void display(std::ostream& out, constraint const& c, bool values) const; void display(std::ostream& out, card const& c, bool values) const; void display(std::ostream& out, pb const& p, bool values) const; void display(std::ostream& out, xor const& c, bool values) const; @@ -349,6 +354,7 @@ namespace sat { virtual void collect_statistics(statistics& st) const; virtual extension* copy(solver* s); virtual void find_mutexes(literal_vector& lits, vector & mutexes); + virtual void gc(); ptr_vector const & constraints() const { return m_constraints; } diff --git a/src/sat/sat_extension.h b/src/sat/sat_extension.h index d3a58810c..642171610 100644 --- a/src/sat/sat_extension.h +++ b/src/sat/sat_extension.h @@ -52,6 +52,7 @@ namespace sat { virtual void collect_statistics(statistics& st) const = 0; virtual extension* copy(solver* s) = 0; virtual void find_mutexes(literal_vector& lits, vector & mutexes) = 0; + virtual void gc() = 0; }; }; diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp index 341bcc906..7a6955ef8 100644 --- a/src/sat/sat_solver.cpp +++ b/src/sat/sat_solver.cpp @@ -1641,6 +1641,7 @@ namespace sat { UNREACHABLE(); break; } + if (m_ext) m_ext->gc(); m_conflicts_since_gc = 0; m_gc_threshold += m_config.m_gc_increment; CASSERT("sat_gc_bug", check_invariant()); @@ -3148,26 +3149,16 @@ namespace sat { } unsigned solver::num_clauses() const { - unsigned num_cls = 0; - num_cls += m_trail.size(); // units; - vector::const_iterator it = m_watches.begin(); - vector::const_iterator end = m_watches.end(); - for (unsigned l_idx = 0; it != end; ++it, ++l_idx) { - literal l = ~to_literal(l_idx); - watch_list const & wlist = *it; - watch_list::const_iterator it2 = wlist.begin(); - watch_list::const_iterator end2 = wlist.end(); - for (; it2 != end2; ++it2) { - if (it2->is_binary_clause() && l.index() < it2->get_literal().index()) + unsigned num_cls = m_trail.size(); // units; + unsigned l_idx = 0; + for (auto const& wl : m_watches) { + literal l = ~to_literal(l_idx++); + for (auto const& w : wl) { + if (w.is_binary_clause() && l.index() < w.get_literal().index()) num_cls++; } } - clause_vector const * vs[2] = { &m_clauses, &m_learned }; - for (unsigned i = 0; i < 2; i++) { - clause_vector const & cs = *(vs[i]); - num_cls += cs.size(); - } - return num_cls; + return num_cls + m_clauses.size() + m_learned.size(); } void solver::display_dimacs(std::ostream & out) const { @@ -3175,28 +3166,21 @@ namespace sat { for (unsigned i = 0; i < m_trail.size(); i++) { out << dimacs_lit(m_trail[i]) << " 0\n"; } - vector::const_iterator it = m_watches.begin(); - vector::const_iterator end = m_watches.end(); - for (unsigned l_idx = 0; it != end; ++it, ++l_idx) { - literal l = ~to_literal(l_idx); - watch_list const & wlist = *it; - watch_list::const_iterator it2 = wlist.begin(); - watch_list::const_iterator end2 = wlist.end(); - for (; it2 != end2; ++it2) { - if (it2->is_binary_clause() && l.index() < it2->get_literal().index()) - out << dimacs_lit(l) << " " << dimacs_lit(it2->get_literal()) << " 0\n"; + unsigned l_idx = 0; + for (auto const& wlist : m_watches) { + literal l = ~to_literal(l_idx++); + for (auto const& w : wlist) { + if (w.is_binary_clause() && l.index() < w.get_literal().index()) + out << dimacs_lit(l) << " " << dimacs_lit(w.get_literal()) << " 0\n"; } } clause_vector const * vs[2] = { &m_clauses, &m_learned }; for (unsigned i = 0; i < 2; i++) { clause_vector const & cs = *(vs[i]); - clause_vector::const_iterator it = cs.begin(); - clause_vector::const_iterator end = cs.end(); - for (; it != end; ++it) { - clause const & c = *(*it); - unsigned sz = c.size(); - for (unsigned j = 0; j < sz; j++) - out << dimacs_lit(c[j]) << " "; + for (auto cp : cs) { + for (literal l : *cp) { + out << dimacs_lit(l) << " "; + } out << "0\n"; } } @@ -3269,9 +3253,8 @@ namespace sat { */ bool solver::is_unit(clause const & c) const { bool found_undef = false; - unsigned sz = c.size(); - for (unsigned i = 0; i < sz; i++) { - switch (value(c[i])) { + for (literal l : c) { + switch (value(l)) { case l_undef: if (found_undef) return false;