From fa3886136b1e7ec353e221850d6174f2933516e7 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 18 Sep 2021 22:18:15 -0400 Subject: [PATCH] adding Boolean propagation, watch; and factoring --- src/math/dd/dd_pdd.cpp | 104 +++++++++++++++++-- src/math/dd/dd_pdd.h | 8 ++ src/math/polysat/boolean.cpp | 13 ++- src/math/polysat/boolean.h | 12 +++ src/math/polysat/conflict_core.cpp | 34 ++++-- src/math/polysat/conflict_core.h | 2 + src/math/polysat/constraint.cpp | 53 ++++++++-- src/math/polysat/constraint.h | 10 +- src/math/polysat/explain.cpp | 40 +++++++ src/math/polysat/explain.h | 2 + src/math/polysat/solver.cpp | 155 ++++++++++++++-------------- src/math/polysat/solver.h | 9 +- src/math/polysat/ule_constraint.cpp | 11 +- src/test/polysat.cpp | 20 ++-- src/util/var_queue.h | 2 +- 15 files changed, 341 insertions(+), 134 deletions(-) diff --git a/src/math/dd/dd_pdd.cpp b/src/math/dd/dd_pdd.cpp index f71bfbdc3..fe6b5fe66 100644 --- a/src/math/dd/dd_pdd.cpp +++ b/src/math/dd/dd_pdd.cpp @@ -914,14 +914,10 @@ namespace dd { bool pdd_manager::resolve(unsigned v, pdd const& p, pdd const& q, pdd& r) { unsigned const l = p.degree(v); unsigned const m = q.degree(v); - if (l < m) { - // no reduction + // no reduction + if (l < m || m == 0) return false; - } - if (m == 0) { - // no reduction (result would still contain v^l) - return false; - } + pdd a = zero(); pdd b = zero(); pdd c = zero(); @@ -938,6 +934,100 @@ namespace dd { return true; } + /** + * Reduce polynomial a with respect to b by eliminating terms using v + * + * a := a1*v^l + a2 + * b := b1*v^m + b2 + * l >= m + * q, r := quot_rem(a1, b1) + * r = 0 + * result := reduce(v, q*b2*v^{l-m}, b) + reduce(v, a2, b) + */ + pdd pdd_manager::reduce(unsigned v, pdd const& a, pdd const& b) { + unsigned const l = a.degree(v); + unsigned const m = b.degree(v); + // no reduction + if (l < m || m == 0) + return a; + + pdd a1 = zero(); + pdd a2 = zero(); + pdd b1 = zero(); + pdd b2 = zero(); + pdd q = zero(); + pdd r = zero(); + a.factor(v, l, a1, a2); + b.factor(v, m, b1, b2); + + quot_rem(a1, b1, q, r); + if (r.is_zero()) { + std::cout << a1 << " " << b1 << " " << q << "\n"; + SASSERT(q * b1 == a1); + a1 = -q * pow(mk_var(v), l - m) * b2; + if (l > m) + a1 = reduce(v, a1, b); + } + else + a1 = a1 * pow(mk_var(v), l); + a2 = a2.reduce(v, b); + + pdd result = a1 + a2; + return result; + } + + /** + * quotient/remainder of 'a' divided by 'b' + * a := x*hi + lo + * x > level(b): + * hi = q1*b + r1 + * lo = q2*b + r2 + * x*hi + lo = (x*q1 + q2)*b + (x*r1 + r2) + * q := x*q1 + q2 + * r := x*r1 + r2 + * Some special cases. + * General multi-variable polynomial division is TBD. + */ + void pdd_manager::quot_rem(pdd const& a, pdd const& b, pdd& q, pdd& r) { + if (level(a.root) > level(b.root)) { + pdd q1(*this), q2(*this), r1(*this), r2(*this); + quot_rem(a.hi(), b, q1, r1); + quot_rem(a.lo(), b, q2, r2); + q = mk_var(a.var()) * q1 + q2; + r = mk_var(a.var()) * r1 + r2; + } + else if (level(a.root) < level(b.root)) { + q = zero(); + r = a; + } + else if (a == b) { + q = one(); + r = zero(); + } + else if (a.is_val() && b.is_val() && divides(b.val(), a.val())) { + q = mk_val(a.val() / b.val()); + r = zero(); + } + else if (a.is_val() || b.is_val()) { + q = zero(); + r = a; + } + else { + SASSERT(level(a.root) == level(b.root)); + pdd q1(*this), q2(*this), r1(*this), r2(*this); + quot_rem(a.hi(), b.hi(), q1, r1); + quot_rem(a.lo(), b.lo(), q2, r2); + if (q1 == q2 && r1.is_zero() && r2.is_zero()) { + q = q1; + r = zero(); + } + else { + q = zero(); + r = a; + } + } + } + /** * Returns the largest j such that 2^j divides p. */ diff --git a/src/math/dd/dd_pdd.h b/src/math/dd/dd_pdd.h index 9ad8c766f..e00ce9605 100644 --- a/src/math/dd/dd_pdd.h +++ b/src/math/dd/dd_pdd.h @@ -23,6 +23,11 @@ Abstract: - try_spoly(a, b, c) returns true if lt(a) and lt(b) have a non-trivial overlap. c is the resolvent (S polynomial). + - reduce(v, a, b) reduces 'a' using b = 0 with respect to eliminating v. + Given b = v^l*b1 + b2, where l is the leading coefficient of v in b + Given a = v^m*a1 + b2, where m >= l is the leading coefficient of v in b. + reduce(a1, b1)*v^{m - l} + reduce(v, a2, b); + Author: Nikolaj Bjorner (nbjorner) 2019-12-17 @@ -333,6 +338,8 @@ namespace dd { pdd subst_val(pdd const& a, vector> const& s); pdd subst_val(pdd const& a, unsigned v, rational const& val); bool resolve(unsigned v, pdd const& p, pdd const& q, pdd& r); + pdd reduce(unsigned v, pdd const& a, pdd const& b); + void quot_rem(pdd const& a, pdd const& b, pdd& q, pdd& r); pdd pow(pdd const& p, unsigned j); bool is_linear(PDD p) { return degree(p) == 1; } @@ -419,6 +426,7 @@ namespace dd { void factor(unsigned v, unsigned degree, pdd& lc, pdd& rest) const { m.factor(*this, v, degree, lc, rest); } bool factor(unsigned v, unsigned degree, pdd& lc) const { return m.factor(*this, v, degree, lc); } bool resolve(unsigned v, pdd const& other, pdd& result) { return m.resolve(v, *this, other, result); } + pdd reduce(unsigned v, pdd const& other) const { return m.reduce(v, *this, other); } pdd subst_val(vector> const& s) const { return m.subst_val(*this, s); } pdd subst_val(unsigned v, rational const& val) const { return m.subst_val(*this, v, val); } diff --git a/src/math/polysat/boolean.cpp b/src/math/polysat/boolean.cpp index b43c94418..e2304fd9c 100644 --- a/src/math/polysat/boolean.cpp +++ b/src/math/polysat/boolean.cpp @@ -17,8 +17,9 @@ Author: namespace polysat { sat::bool_var bool_var_manager::new_var() { + sat::bool_var var; if (m_unused.empty()) { - sat::bool_var var = size(); + var = size(); m_value.push_back(l_undef); m_value.push_back(l_undef); m_level.push_back(UINT_MAX); @@ -26,18 +27,19 @@ namespace polysat { m_lemma.push_back(nullptr); m_watch.push_back({}); m_watch.push_back({}); - return var; + m_activity.push_back(0); } else { - sat::bool_var var = m_unused.back(); + var = m_unused.back(); m_unused.pop_back(); SASSERT_EQ(m_level[var], UINT_MAX); SASSERT_EQ(m_value[2*var], l_undef); SASSERT_EQ(m_value[2*var+1], l_undef); SASSERT_EQ(m_reason[var], nullptr); SASSERT_EQ(m_lemma[var], nullptr); - return var; } + m_free_vars.mk_var_eh(var); + return var; } void bool_var_manager::del_var(sat::bool_var var) { @@ -50,6 +52,7 @@ namespace polysat { m_lemma[var] = nullptr; m_watch[lit.index()].reset(); m_watch[(~lit).index()].reset(); + m_free_vars.del_var_eh(var); // TODO: this is disabled for now, since re-using variables for different constraints may be confusing during debugging. Should be enabled later. // m_unused.push_back(var); } @@ -61,6 +64,7 @@ namespace polysat { m_level[lit.var()] = lvl; m_reason[lit.var()] = reason; m_lemma[lit.var()] = lemma; + m_free_vars.del_var_eh(lit.var()); } void bool_var_manager::unassign(sat::literal lit) { @@ -70,6 +74,7 @@ namespace polysat { m_level[lit.var()] = UINT_MAX; m_reason[lit.var()] = nullptr; m_lemma[lit.var()] = nullptr; + m_free_vars.unassign_var_eh(lit.var()); } std::ostream& bool_var_manager::display(std::ostream& out) const { diff --git a/src/math/polysat/boolean.h b/src/math/polysat/boolean.h index aa1b512a2..ae5b8689b 100644 --- a/src/math/polysat/boolean.h +++ b/src/math/polysat/boolean.h @@ -28,9 +28,13 @@ namespace polysat { // For enumerative backtracking we store the lemma we're handling with a certain decision svector m_lemma; + var_queue m_free_vars; // free Boolean variables vector> m_watch; // watch list for literals into clauses public: + + bool_var_manager(): m_free_vars(m_activity) {} + // allocated size (not the number of active variables) unsigned size() const { return m_level.size(); } @@ -52,8 +56,16 @@ namespace polysat { clause* lemma(sat::bool_var var) const { SASSERT(is_decision(var)); return m_lemma[var]; } + + ptr_vector& watch(sat::literal lit) { return m_watch[lit.index()]; } unsigned_vector& activity() { return m_activity; } + bool can_decide() const { return !m_free_vars.empty(); } + sat::bool_var next_var() { return m_free_vars.next_var(); } + + // TODO connect activity updates with solver + void inc_activity(sat::literal lit) { m_activity[lit.var()]++; } + void dec_activity(sat::literal lit) { m_activity[lit.var()] /= 2; } /// Set the given literal to true void assign(sat::literal lit, unsigned lvl, clause* reason, clause* lemma); diff --git a/src/math/polysat/conflict_core.cpp b/src/math/polysat/conflict_core.cpp index 3f2ed6abd..d30da7341 100644 --- a/src/math/polysat/conflict_core.cpp +++ b/src/math/polysat/conflict_core.cpp @@ -51,7 +51,7 @@ namespace polysat { std::ostream& conflict_core::display(std::ostream& out) const { char const* sep = ""; for (auto c : *this) - out << sep << c, sep = " ; "; + out << sep << c->bvar2string() << " " << c, sep = " ; "; if (!m_vars.empty()) out << " vars"; for (auto v : m_vars) @@ -102,8 +102,19 @@ namespace polysat { SASSERT(!empty()); } + void conflict_core::set(clause const& cl) { + LOG("Conflict: " << cl); + SASSERT(empty()); + for (auto lit : cl) { + auto c = s().lit2cnstr(lit); + c->set_var_dependent(); + insert(~c); + } + SASSERT(!empty()); + } + void conflict_core::insert(signed_constraint c) { - LOG("inserting: " << c << " " << c.is_always_true() << " " << c->is_marked() << " " << c->has_bvar()); + LOG("inserting: " << c); // Skip trivial constraints // (e.g., constant ones such as "4 > 1"... only true ones should appear, otherwise the lemma would be a tautology) if (c.is_always_true()) @@ -152,6 +163,8 @@ namespace polysat { SASSERT(std::all_of(m_constraints.begin(), m_constraints.end(), [](auto c){ return !c->has_bvar(); })); bool core_has_pos = contains_literal(sat::literal(var)); bool core_has_neg = contains_literal(~sat::literal(var)); + std::cout << cl << "\n"; + std::cout << *this << "\n"; DEBUG_CODE({ bool clause_has_pos = std::count(cl.begin(), cl.end(), sat::literal(var)) > 0; bool clause_has_neg = std::count(cl.begin(), cl.end(), ~sat::literal(var)) > 0; @@ -183,23 +196,23 @@ namespace polysat { auto it = m_saturation_premises.find_iterator(c); if (it == m_saturation_premises.end()) return; - unsigned active_level = 0; auto& premises = it->m_value; clause_builder c_lemma(s()); for (auto premise : premises) { LOG_H3("premise: " << premise); keep(premise); - SASSERT(premise->has_bvar()); + SASSERT(premise->has_bvar()); SASSERT(premise.is_currently_true(s()) || premise.bvalue(s()) == l_true); // otherwise the propagation doesn't make sense c_lemma.push(~premise.blit()); - active_level = std::max(active_level, premise.level(s())); } c_lemma.push(c.blit()); - clause* cl = cm().store(c_lemma.build()); - if (cl->size() == 1) - c->set_unit_clause(cl); - s().propagate_bool_at(active_level, c.blit(), cl); + clause_ref lemma = c_lemma.build(); + cm().store(lemma.get(), s()); + if (lemma->size() == 1) + c->set_unit_clause(lemma.get()); + if (s().m_bvars.value(c.blit()) == l_undef) + s().propagate_bool_at(s().level(*lemma), c.blit(), lemma.get()); } clause_builder conflict_core::build_core_lemma() { @@ -207,7 +220,8 @@ namespace polysat { LOG("core: " << *this); clause_builder lemma(s()); - for (auto c : m_constraints) { + while (!m_constraints.empty()) { + signed_constraint c = m_constraints.back(); SASSERT(!c->has_bvar()); keep(c); } diff --git a/src/math/polysat/conflict_core.h b/src/math/polysat/conflict_core.h index f306289e9..1533a5465 100644 --- a/src/math/polysat/conflict_core.h +++ b/src/math/polysat/conflict_core.h @@ -83,6 +83,8 @@ namespace polysat { void set(signed_constraint c); /** conflict because there is no viable value for the variable v */ void set(pvar v); + /** all literals in clause are false */ + void set(clause const& cl); void insert(signed_constraint c); void insert(signed_constraint c, vector premises); diff --git a/src/math/polysat/constraint.cpp b/src/math/polysat/constraint.cpp index cbd53ce6c..b3d08f73c 100644 --- a/src/math/polysat/constraint.cpp +++ b/src/math/polysat/constraint.cpp @@ -55,13 +55,11 @@ namespace polysat { m_constraints.push_back(c); } - - clause* constraint_manager::store(clause_ref cl_ref) { - clause* cl = cl_ref.get(); + void constraint_manager::store(clause* cl, solver& s) { while (m_clauses.size() <= cl->level()) m_clauses.push_back({}); - m_clauses[cl->level()].push_back(std::move(cl_ref)); - return cl; + m_clauses[cl->level()].push_back(cl); + watch(*cl, s); } void constraint_manager::register_external(signed_constraint c) { @@ -94,13 +92,48 @@ namespace polysat { // Release constraints at the given level and above. void constraint_manager::release_level(unsigned lvl) { for (unsigned l = m_clauses.size(); l-- > lvl; ) { - for (auto const& cl : m_clauses[l]) { + for (auto& cl : m_clauses[l]) { + unwatch(*cl); SASSERT_EQ(cl->m_ref_count, 1); // otherwise there is a leftover reference somewhere } m_clauses[l].reset(); } } + // find literals that are not propagated to false + // if clause is unsat then assign arbitrary + // solver handles unsat clauses by creating a conflict. + // solver also can propagate, but need to check that it does indeed. + void constraint_manager::watch(clause& cl, solver& s) { + if (cl.size() <= 1) + return; + bool first = true; + for (unsigned i = 0; i < cl.size(); ++i) { + if (m_bvars.is_false(cl[i])) + continue; + m_bvars.watch(cl[i]).push_back(&cl); + std::swap(cl[!first], cl[i]); + if (!first) + return; + first = false; + } + + if (first) + m_bvars.watch(cl[0]).push_back(&cl); + m_bvars.watch(cl[1]).push_back(&cl); + if (first) + s.set_conflict(cl); + else + s.propagate_bool_at(s.level(cl), cl[0], &cl); + } + + void constraint_manager::unwatch(clause& cl) { + if (cl.size() <= 1) + return; + m_bvars.watch(~cl[0]).erase(&cl); + m_bvars.watch(~cl[1]).erase(&cl); + } + constraint_manager::~constraint_manager() { // Release explicitly to check for leftover references in debug mode, // and to make sure all constraints are destructed before the bvar->constraint mapping. @@ -219,11 +252,12 @@ namespace polysat { return *dynamic_cast(this); } - std::ostream& constraint::display_extra(std::ostream& out) const { + std::string constraint::bvar2string() const { + std::stringstream out; out << " (b"; if (has_bvar()) { out << bvar(); } else { out << "_"; } out << ")"; - return out; + return out.str(); } bool constraint::propagate(solver& s, bool is_positive, pvar v) { @@ -265,7 +299,8 @@ namespace polysat { return s.m_bvars.level(bvar()); unsigned level = 0; for (auto v : vars()) - level = std::max(level, s.get_level(v)); + if (s.is_assigned(v)) + level = std::max(level, s.get_level(v)); return level; } diff --git a/src/math/polysat/constraint.h b/src/math/polysat/constraint.h index 1451fe7e1..32e7a413c 100644 --- a/src/math/polysat/constraint.h +++ b/src/math/polysat/constraint.h @@ -64,6 +64,9 @@ namespace polysat { void gc_constraints(solver& s); void gc_clauses(solver& s); + void watch(clause& cl, solver& s); + void unwatch(clause& cl); + public: constraint_manager(bool_var_manager& bvars): m_bvars(bvars) {} ~constraint_manager(); @@ -72,7 +75,7 @@ namespace polysat { void erase_bvar(constraint* c); // sat::literal get_or_assign_blit(signed_constraint& c); - clause* store(clause_ref cl); + void store(clause* cl, solver& s); /// Register a unit clause with an external dependency. void register_external(signed_constraint c); @@ -146,9 +149,7 @@ namespace polysat { sat::bool_var m_bvar = sat::null_bool_var; constraint(constraint_manager& m, ckind_t k): m_kind(k) {} - - protected: - std::ostream& display_extra(std::ostream& out) const; + public: virtual ~constraint() {} @@ -179,6 +180,7 @@ namespace polysat { bool contains_var(pvar v) const { return m_vars.contains(v); } bool has_bvar() const { return m_bvar != sat::null_bool_var; } sat::bool_var bvar() const { return m_bvar; } + std::string bvar2string() const; unsigned level(solver& s) const; clause* unit_clause() const { return m_unit_clause; } diff --git a/src/math/polysat/explain.cpp b/src/math/polysat/explain.cpp index fc86f1449..5af66c8a0 100644 --- a/src/math/polysat/explain.cpp +++ b/src/math/polysat/explain.cpp @@ -92,8 +92,48 @@ namespace polysat { return l_false; } + void ex_polynomial_superposition::reduce_by(pvar v, conflict_core& core) { + return; + bool progress = true; + while (progress) { + progress = false; + for (auto c : core) { + if (is_positive_equality_over(v, c) && reduce_by(v, c, core)) { + progress = true; + break; + } + } + } + } + + bool ex_polynomial_superposition::reduce_by(pvar v, signed_constraint eq, conflict_core& core) { + pdd p = eq->to_ule().p(); + for (auto c : core) { + if (c == eq) + continue; + if (c->is_ule()) { + auto lhs = c->to_ule().lhs(); + auto rhs = c->to_ule().rhs(); + auto a = lhs.reduce(v, p); + auto b = rhs.reduce(v, p); + if (a == lhs && b == rhs) + continue; + auto c2 = s().ule(a, b); + if (!c.is_positive()) + c2 = ~c2; + vector premises; + premises.push_back(eq); + premises.push_back(c); + core.replace(c, c2, premises); + return true; + } + } + return false; + } + bool ex_polynomial_superposition::try_explain(pvar v, conflict_core& core) { LOG_H3("Trying polynomial superposition..."); + reduce_by(v, core); lbool result = l_undef; while (result == l_undef) result = try_explain1(v, core); diff --git a/src/math/polysat/explain.h b/src/math/polysat/explain.h index b942b28a7..80089d161 100644 --- a/src/math/polysat/explain.h +++ b/src/math/polysat/explain.h @@ -37,6 +37,8 @@ namespace polysat { bool is_positive_equality_over(pvar v, signed_constraint const& c); signed_constraint resolve1(pvar v, signed_constraint c1, signed_constraint c2); signed_constraint find_replacement(signed_constraint c2, pvar v, conflict_core& core); + void reduce_by(pvar v, conflict_core& core); + bool reduce_by(pvar, signed_constraint c, conflict_core& core); lbool try_explain1(pvar v, conflict_core& core); public: bool try_explain(pvar v, conflict_core& core) override; diff --git a/src/math/polysat/solver.cpp b/src/math/polysat/solver.cpp index 7b342c880..e6834ffa6 100644 --- a/src/math/polysat/solver.cpp +++ b/src/math/polysat/solver.cpp @@ -42,7 +42,6 @@ namespace polysat { m_conflict(*this), m_bvars(), m_free_pvars(m_activity), - m_free_bvars(m_bvars.activity()), m_constraints(m_bvars) { } @@ -144,8 +143,9 @@ namespace polysat { if (is_conflict()) return; // no need to do anything if we already have a conflict at base level m_constraints.ensure_bvar(c.get()); - clause* unit = m_constraints.store(clause::from_unit(m_level, c, mk_dep_ref(dep))); - c->set_unit_clause(unit); + clause_ref unit = clause::from_unit(m_level, c, mk_dep_ref(dep)); + m_constraints.store(unit.get(), *this); + c->set_unit_clause(unit.get()); if (dep != null_dependency && !c->is_external()) { m_constraints.register_external(c); m_trail.push_back(trail_instr_t::ext_constraint_i); @@ -203,16 +203,16 @@ namespace polysat { } void solver::propagate_watch(sat::literal lit) { + LOG("propagate " << lit); auto& wlist = m_bvars.watch(~lit); - unsigned end = 0; + unsigned j = 0, end = 0; unsigned sz = wlist.size(); - bool flush = false; - for (unsigned j = 0; j < sz && !is_conflict(); ++j) { + for (; j < sz && !is_conflict(); ++j) { clause& cl = *wlist[j]; SASSERT(cl.size() >= 2); - unsigned idx = cl[0] == lit ? 1 : 0; - SASSERT(cl[1 - idx] == lit); - if (flush || m_bvars.is_true(cl[idx])) { + unsigned idx = cl[0] == ~lit ? 1 : 0; + SASSERT(cl[1 - idx] == ~lit); + if (m_bvars.is_true(cl[idx])) { wlist[end++] = &cl; continue; } @@ -226,15 +226,13 @@ namespace polysat { wlist[end++] = &cl; if (m_bvars.is_false(cl[idx])) { set_conflict(cl); - flush = true; - continue; + ++j; + break; } - unsigned level = 0; - for (i = 0; i < cl.size(); ++i) - if (cl[i] != lit) - level = std::max(level, m_bvars.level(cl[i])); - assign_bool(level, cl[1 - idx], &cl, nullptr); + assign_bool(level(cl), cl[idx], &cl, nullptr); } + for (; j < sz; ++j) + wlist[end++] = wlist[j]; wlist.shrink(end); } @@ -252,7 +250,7 @@ namespace polysat { void solver::propagate(sat::literal lit) { LOG_H2("Propagate bool " << lit); - signed_constraint c = m_constraints.lookup(lit); + signed_constraint c = lit2cnstr(lit); SASSERT(c); activate_constraint(c); propagate_watch(lit); @@ -289,6 +287,8 @@ namespace polysat { } void solver::pop_levels(unsigned num_levels) { + if (num_levels == 0) + return; SASSERT(m_level >= num_levels); unsigned const target_level = m_level - num_levels; vector replay; @@ -301,10 +301,8 @@ namespace polysat { case trail_instr_t::qhead_i: { pop_qhead(); for (unsigned i = m_search.size(); i-- > m_qhead; ) - if (m_search[i].is_boolean()) { - auto c = m_constraints.lookup(m_search[i].lit()); - deactivate_constraint(c); - } + if (m_search[i].is_boolean()) + deactivate_constraint(lit2cnstr(m_search[i].lit())); break; } case trail_instr_t::add_var_i: { @@ -407,8 +405,8 @@ namespace polysat { void solver::decide() { LOG_H2("Decide"); SASSERT(can_decide()); - if (!m_free_bvars.empty()) - bdecide(m_free_bvars.next_var()); + if (m_bvars.can_decide()) + bdecide(m_bvars.next_var()); else pdecide(m_free_pvars.next_var()); } @@ -434,10 +432,10 @@ namespace polysat { assign_core(v, val, justification::decision(m_level)); break; } - } + } void solver::bdecide(sat::bool_var b) { - + decide_bool(sat::literal(b), nullptr); } void solver::assign_core(pvar v, rational const& val, justification const& j) { @@ -467,8 +465,7 @@ namespace polysat { } void solver::set_conflict(clause& cl) { - for (auto lit : cl) - set_conflict(~m_constraints.lookup(lit)); + m_conflict.set(cl); } /** @@ -498,8 +495,6 @@ namespace polysat { SASSERT(is_conflict()); - // TODO: subsequent changes to the conflict should update the marks incrementally - if (m_conflict.conflict_var() != null_var) { // This case corresponds to a propagation of conflict_var, except it's not explicitly on the stack. resolve_value(m_conflict.conflict_var()); @@ -584,12 +579,12 @@ namespace polysat { } void solver::learn_lemma(pvar v, clause_ref lemma) { - LOG("Learning: " << show_deref(lemma)); if (!lemma) return; + LOG("Learning: " << show_deref(lemma)); SASSERT(lemma->size() > 0); lemma->set_justified_var(v); - add_lemma(lemma); + add_lemma(*lemma); decide_bool(*lemma); } @@ -600,24 +595,24 @@ namespace polysat { LOG("Boolean assignment: " << m_bvars); // To make a guess, we need to find an unassigned literal that is not false in the current model. - auto is_suitable = [this](sat::literal lit) -> bool { - if (m_bvars.value(lit) == l_false) // already assigned => cannot decide on this (comes from either lemma LHS or previously decided literals that are now changed to propagation) - return false; - SASSERT(m_bvars.value(lit) != l_true); // cannot happen in a valid lemma - signed_constraint c = m_constraints.lookup(lit); - SASSERT(!c.is_currently_true(*this)); // should not happen in a valid lemma - return !c.is_currently_false(*this); - }; sat::literal choice = sat::null_literal; unsigned num_choices = 0; // TODO: should probably cache this? (or rather the suitability of each literal... it won't change until we backtrack beyond the current point) for (sat::literal lit : lemma) { - if (is_suitable(lit)) { - num_choices++; - if (choice == sat::null_literal) - choice = lit; + switch (m_bvars.value(lit)) { + case l_true: + return; + case l_false: + continue; + default: + if (lit2cnstr(lit).is_currently_false(*this)) + continue; + break; } + num_choices++; + if (choice == sat::null_literal) + choice = lit; } LOG_V("num_choices: " << num_choices); if (choice == sat::null_literal) { @@ -627,13 +622,13 @@ namespace polysat { return; } - signed_constraint c = m_constraints.lookup(choice); + signed_constraint c = lit2cnstr(choice); push_cjust(lemma.justified_var(), c); if (num_choices == 1) propagate_bool(choice, &lemma); else - decide_bool(choice, lemma); + decide_bool(choice, &lemma); } /** @@ -710,23 +705,23 @@ namespace polysat { // The lemma where 'lit' comes from. // Currently, boolean decisions always come from guessing a literal of a learned non-unit lemma. clause* lemma = m_bvars.lemma(var); // need to grab this while 'lit' is still assigned - SASSERT(lemma); backjump(m_bvars.level(var) - 1); - add_lemma(reason); - propagate_bool(~lit, reason.get()); + add_lemma(*reason); + // propagate_bool(~lit, reason.get()); if (is_conflict()) { LOG_H1("Conflict during revert_bool_decision/propagate_bool!"); return; } - decide_bool(*lemma); + if (lemma) + decide_bool(*lemma); } - void solver::decide_bool(sat::literal lit, clause& lemma) { + void solver::decide_bool(sat::literal lit, clause* lemma) { push_level(); LOG_H2("Decide boolean literal " << lit << " @ " << m_level); - assign_bool(m_level, lit, nullptr, &lemma); + assign_bool(m_level, lit, nullptr, lemma); } void solver::propagate_bool(sat::literal lit, clause* reason) { @@ -740,8 +735,19 @@ namespace polysat { assign_bool(level, lit, reason, nullptr); } + unsigned solver::level(clause const& cl) { + unsigned lvl = 0; + for (auto lit : cl) { + auto c = lit2cnstr(lit); + if (m_bvars.is_false(lit) || c.is_currently_false(*this)) + lvl = std::max(lvl, c.level(*this)); + } + return lvl; + } + /// Assign a boolean literal and put it on the search stack void solver::assign_bool(unsigned level, sat::literal lit, clause* reason, clause* lemma) { + SASSERT(!m_bvars.is_true(lit)); LOG("Assigning boolean literal: " << lit); m_bvars.assign(lit, level, reason, lemma); m_trail.push_back(trail_instr_t::assign_bool_i); @@ -773,9 +779,7 @@ namespace polysat { void solver::backjump(unsigned new_level) { LOG_H3("Backjumping to level " << new_level << " from level " << m_level); - unsigned num_levels = m_level - new_level; - if (num_levels > 0) - pop_levels(num_levels); + pop_levels(m_level - new_level); } /** @@ -786,30 +790,23 @@ namespace polysat { } // Add lemma to storage but do not activate it - void solver::add_lemma(clause_ref lemma) { - if (!lemma) - return; - bool non_propagated_literal = false; - LOG("Lemma: " << show_deref(lemma)); - for (sat::literal lit : *lemma) { - LOG(" Literal " << lit << " is: " << m_constraints.lookup(lit)); - signed_constraint c = m_constraints.lookup(lit); + void solver::add_lemma(clause& lemma) { + + LOG("Lemma: " << lemma); + for (sat::literal lit : lemma) { + LOG(" Literal " << lit << " is: " << lit2cnstr(lit)); // Check that fully evaluated constraints are on the stack - SASSERT(!c.is_currently_true(*this)); + SASSERT(!lit2cnstr(lit).is_currently_true(*this)); // literals that are added from m_conflict.m_vars have not been assigned. // they are false in the current model. - if (!m_bvars.is_assigned(lit) && c.is_currently_false(*this)) { - non_propagated_literal = true; - } // SASSERT(m_bvars.is_assigned(lit) || !c.is_currently_false(*this)); // TODO: work out invariant for the lemma. It should be impossible to extend the model in a way that makes the lemma true. } - // SASSERT(!non_propagated_literal); - SASSERT(lemma->size() > 0); - clause* cl = m_constraints.store(std::move(lemma)); - if (cl->size() == 1) { - signed_constraint c = m_constraints.lookup((*cl)[0]); - c->set_unit_clause(cl); + SASSERT(lemma.size() > 0); + m_constraints.store(&lemma, *this); + if (lemma.size() == 1) { + signed_constraint c = lit2cnstr(lemma[0]); + c->set_unit_clause(&lemma); } } @@ -854,7 +851,7 @@ namespace polysat { if (item.is_assignment()) { pvar v = item.var(); auto j = m_justification[v]; - out << "\t" << assignment_pp(*this, v, get_value(v)) << " @" << j.level(); + out << "\t" << assignment_pp(*this, v, get_value(v)) << " @" << j.level(); if (j.is_propagation()) out << " " << m_cjust[v]; out << "\n"; @@ -869,15 +866,13 @@ namespace polysat { } out << "Constraints:\n"; for (auto c : m_constraints) - out << "\t" << *c << "\n"; + out << "\t" << c->bvar2string() << ": " << *c << "\n"; out << "Clauses:\n"; for (auto cls : m_constraints.clauses()) { for (auto cl : cls) { out << "\t" << *cl << "\n"; - for (auto lit : *cl) { - auto c = m_constraints.lookup(lit); - out << "\t\t" << lit << ": " << c << "\n"; - } + for (auto lit : *cl) + out << "\t\t" << lit << ": " << lit2cnstr(lit) << "\n"; } } return out; @@ -959,7 +954,7 @@ namespace polysat { bool ok = true; for (sat::bool_var v = m_bvars.size(); v-- > 0; ) { sat::literal lit(v); - auto c = m_constraints.lookup(lit); + auto c = lit2cnstr(lit); if (!std::all_of(c->vars().begin(), c->vars().end(), [&](auto v) { return is_assigned(v); })) continue; ok &= (m_bvars.value(lit) != l_true) || !c.is_currently_false(*this); @@ -979,7 +974,7 @@ namespace polysat { bool all_ok = true; for (auto s : m_search) { if (s.is_boolean()) { - bool ok = m_constraints.lookup(s.lit()).is_currently_true(*this); + bool ok = lit2cnstr(s.lit()).is_currently_true(*this); LOG((ok ? "PASS" : "FAIL") << ": " << s.lit()); all_ok = all_ok && ok; } diff --git a/src/math/polysat/solver.h b/src/math/polysat/solver.h index d6ac074ab..54601faa5 100644 --- a/src/math/polysat/solver.h +++ b/src/math/polysat/solver.h @@ -76,7 +76,6 @@ namespace polysat { conflict_core m_conflict; bool_var_manager m_bvars; // Map boolean variables to constraints var_queue m_free_pvars; // free poly vars - var_queue m_free_bvars; // free Boolean variables stats m_stats; uint64_t m_max_conflicts = std::numeric_limits::max(); @@ -155,9 +154,10 @@ namespace polysat { void activate_constraint(signed_constraint c); void deactivate_constraint(signed_constraint c); void decide_bool(clause& lemma); - void decide_bool(sat::literal lit, clause& lemma); + void decide_bool(sat::literal lit, clause* lemma); void propagate_bool(sat::literal lit, clause* reason); void propagate_bool_at(unsigned level, sat::literal lit, clause* reason); + unsigned level(clause const& cl); void assign_core(pvar v, rational const& val, justification const& j); bool is_assigned(pvar v) const { return !m_justification[v].is_unassigned(); } @@ -179,7 +179,7 @@ namespace polysat { void set_conflict(clause& cl); void set_conflict(pvar v); - bool can_decide() const { return !m_free_pvars.empty() || !m_free_bvars.empty(); } + bool can_decide() const { return !m_free_pvars.empty() || m_bvars.can_decide(); } void decide(); void pdecide(pvar v); void bdecide(sat::bool_var b); @@ -206,7 +206,7 @@ namespace polysat { void report_unsat(); void learn_lemma(pvar v, clause_ref lemma); void backjump(unsigned new_level); - void add_lemma(clause_ref lemma); + void add_lemma(clause& lemma); signed_constraint eq(pdd const& p); signed_constraint diseq(pdd const& p); @@ -218,6 +218,7 @@ namespace polysat { signed_constraint ult(pdd const& p, pdd const& q); signed_constraint sle(pdd const& p, pdd const& q); signed_constraint slt(pdd const& p, pdd const& q); + signed_constraint lit2cnstr(sat::literal lit) const { return m_constraints.lookup(lit); } void ext_constraint(signed_constraint c, unsigned dep, bool activate); static void insert_constraint(signed_constraints& cs, signed_constraint c); void assert_ext_constraint(signed_constraint c); diff --git a/src/math/polysat/ule_constraint.cpp b/src/math/polysat/ule_constraint.cpp index 05620739b..e376effcb 100644 --- a/src/math/polysat/ule_constraint.cpp +++ b/src/math/polysat/ule_constraint.cpp @@ -38,18 +38,11 @@ namespace polysat { else if (status == l_true) out << " <= "; else if (status == l_false) out << " > "; else out << " <=/> "; - out << m_rhs; - return display_extra(out); + return out << m_rhs; } std::ostream& ule_constraint::display(std::ostream& out) const { - out << m_lhs; - if (is_eq()) - out << " == "; - else - out << " <= "; - out << m_rhs; - return display_extra(out); + return out << m_lhs << (is_eq() ? " == " : " <= ") << m_rhs; } void ule_constraint::narrow(solver& s, bool is_positive) { diff --git a/src/test/polysat.cpp b/src/test/polysat.cpp index 640c7378c..8536004ac 100644 --- a/src/test/polysat.cpp +++ b/src/test/polysat.cpp @@ -867,29 +867,35 @@ namespace polysat { void tst_polysat() { + + polysat::test_p3(); + + polysat::test_l2(); + + // polysat::test_subst(); + // return; // not working // polysat::test_fixed_point_arith_div_mul_inverse(); - // polysat::test_cjust(); - polysat::test_monot_bounds_simple(8); - return; + + //polysat::test_monot_bounds_simple(8); // working polysat::test_fixed_point_arith_mul_div_inverse(); - polysat::test_subst(); + polysat::test_monot_bounds(8); polysat::test_add_conflicts(); polysat::test_wlist(); polysat::test_l1(); - polysat::test_l2(); + polysat::test_l3(); polysat::test_l4(); polysat::test_l5(); polysat::test_p1(); polysat::test_p2(); - polysat::test_p3(); + polysat::test_ineq_basic1(); polysat::test_ineq_basic2(); polysat::test_ineq_basic3(); @@ -897,6 +903,8 @@ void tst_polysat() { polysat::test_ineq_basic5(); polysat::test_ineq_basic6(); polysat::test_monot_bounds(2); + polysat::test_cjust(); + // inefficient conflicts: // Takes time: polysat::test_monot_bounds_full(); diff --git a/src/util/var_queue.h b/src/util/var_queue.h index 4421b6e0f..62df77784 100644 --- a/src/util/var_queue.h +++ b/src/util/var_queue.h @@ -52,7 +52,7 @@ public: void mk_var_eh(var v) { m_queue.reserve(v+1); - m_queue.insert(v); + unassign_var_eh(v); } void del_var_eh(var v) {