diff --git a/src/math/polysat/constraint.cpp b/src/math/polysat/constraint.cpp index 81347c5ea..a400982bb 100644 --- a/src/math/polysat/constraint.cpp +++ b/src/math/polysat/constraint.cpp @@ -324,35 +324,6 @@ namespace polysat { return out.str(); } - bool constraint::propagate(solver& s, bool is_positive, pvar v) { - LOG_H3("Propagate " << s.m_vars[v] << " in " << signed_constraint(this, is_positive)); - SASSERT(!vars().empty()); - unsigned idx = 0; - if (var(idx) != v) - idx = 1; - SASSERT(v == var(idx)); - // find other watch variable. - for (unsigned i = vars().size(); i-- > 2; ) { - unsigned other_v = vars()[i]; - if (!s.is_assigned(other_v)) { - s.add_watch({this, is_positive}, other_v); - std::swap(vars()[idx], vars()[i]); - return true; - } - } - // at most one variable remains unassigned. - unsigned other_v = var(idx); - propagate_core(s, is_positive, v, other_v); - return false; - } - - void constraint::propagate_core(solver& s, bool is_positive, pvar v, pvar other_v) { - (void)v; - (void)other_v; - narrow(s, is_positive, false); - } - - unsigned constraint::level(solver& s) const { if (s.m_bvars.value(sat::literal(bvar())) != l_undef) return s.m_bvars.level(bvar()); diff --git a/src/math/polysat/constraint.h b/src/math/polysat/constraint.h index b2dd72571..391c1f976 100644 --- a/src/math/polysat/constraint.h +++ b/src/math/polysat/constraint.h @@ -178,8 +178,6 @@ namespace polysat { virtual std::ostream& display(std::ostream& out, lbool status) const = 0; virtual std::ostream& display(std::ostream& out) const = 0; - bool propagate(solver& s, bool is_positive, pvar v); - virtual void propagate_core(solver& s, bool is_positive, pvar v, pvar other_v); virtual bool is_always_false(bool is_positive) const = 0; virtual bool is_currently_false(solver& s, bool is_positive) const = 0; virtual bool is_currently_true(solver& s, bool is_positive) const = 0; @@ -248,8 +246,6 @@ namespace polysat { bool is_positive() const { return m_positive; } bool is_negative() const { return !is_positive(); } - bool propagate(solver& s, pvar v) { return get()->propagate(s, is_positive(), v); } - void propagate_core(solver& s, pvar v, pvar other_v) { get()->propagate_core(s, is_positive(), v, other_v); } bool is_always_false() const { return get()->is_always_false(is_positive()); } bool is_always_true() const { return get()->is_always_false(is_negative()); } bool is_currently_false(solver& s) const { return get()->is_currently_false(s, is_positive()); } diff --git a/src/math/polysat/solver.cpp b/src/math/polysat/solver.cpp index c09e73ad2..ce92182e5 100644 --- a/src/math/polysat/solver.cpp +++ b/src/math/polysat/solver.cpp @@ -31,6 +31,7 @@ namespace polysat { solver::solver(reslimit& lim): m_lim(lim), m_viable(*this), + m_viable_fallback(*this), m_linear_solver(*this), m_conflict(*this), m_simplify(*this), @@ -105,7 +106,8 @@ namespace polysat { pvar v = m_value.size(); m_value.push_back(rational::zero()); m_justification.push_back(justification::unassigned()); - m_viable.push(sz); + m_viable.push_var(sz); + m_viable_fallback.push_var(sz); m_pwatch.push_back({}); m_activity.push_back(0); m_vars.push_back(sz2pdd(sz).mk_var(v)); @@ -122,7 +124,8 @@ namespace polysat { void solver::del_var() { // TODO also remove v from all learned constraints. pvar v = m_value.size() - 1; - m_viable.pop(); + m_viable.pop_var(); + m_viable_fallback.pop_var(); m_value.pop_back(); m_justification.pop_back(); m_pwatch.pop_back(); @@ -267,7 +270,7 @@ namespace polysat { auto& wlist = m_pwatch[v]; unsigned i = 0, j = 0, sz = wlist.size(); for (; i < sz && !is_conflict(); ++i) - if (!wlist[i].propagate(*this, v)) + if (propagate(v, wlist[i])) wlist[j++] = wlist[i]; for (; i < sz; ++i) wlist[j++] = wlist[i]; @@ -275,6 +278,32 @@ namespace polysat { DEBUG_CODE(m_locked_wlist = std::nullopt;); } + bool solver::propagate(pvar v, signed_constraint c) { + LOG_H3("Propagate " << m_vars[v] << " in " << c); + SASSERT(!c->vars().empty()); + unsigned idx = 0; + if (c->var(idx) != v) + idx = 1; + SASSERT(v == c->var(idx)); + // find other watch variable. + for (unsigned i = c->vars().size(); i-- > 2; ) { + unsigned other_v = c->vars()[i]; + if (!is_assigned(other_v)) { + add_watch(c, other_v); + std::swap(c->vars()[idx], c->vars()[i]); + SASSERT(!is_assigned(c->var(0))); + SASSERT(!is_assigned(c->var(1))); + return true; + } + } + // at most one variable remains unassigned. + unsigned other_v = c->var(idx); + if (!is_assigned(other_v)) + m_viable_fallback.push_constraint(other_v, c); + c.narrow(*this, false); + return false; + } + bool solver::propagate(sat::literal lit, clause& cl) { SASSERT(cl.size() >= 2); unsigned idx = cl[0] == ~lit ? 1 : 0; @@ -361,6 +390,10 @@ namespace polysat { m_viable.push_viable(); break; } + case trail_instr_t::viable_constraint_i: { + m_viable_fallback.pop_constraint(); + break; + } case trail_instr_t::assign_i: { auto v = m_search.back().var(); LOG_V("Undo assign_i: v" << v); @@ -451,6 +484,7 @@ namespace polysat { LOG("Decide v" << v); IF_LOGGING(m_viable.log(v)); rational val; + justification j; switch (m_viable.find_viable(v, val)) { case dd::find_t::empty: // NOTE: all such cases should be discovered elsewhere (e.g., during propagation/narrowing) @@ -458,16 +492,40 @@ namespace polysat { DEBUG_CODE( UNREACHABLE(); ); m_free_pvars.unassign_var_eh(v); set_conflict(v); - break; + return; case dd::find_t::singleton: // NOTE: this case may happen legitimately if all other possibilities were excluded by brute force search - assign_core(v, val, justification::propagation(m_level)); + j = justification::propagation(m_level); break; case dd::find_t::multiple: - push_level(); - assign_core(v, val, justification::decision(m_level)); + j = justification::decision(m_level + 1); break; - } + } + // Verify the value we're trying to assign + // TODO: we should add a better way to test constraints under assignments, without modifying the solver state. + m_value[v] = val; + m_search.push_assignment(v, val); + bool is_valid = m_viable_fallback.check_constraints(v); + m_search.pop(); + if (!is_valid) { + // Try to find a valid replacement value + switch (m_viable_fallback.find_viable(v, val)) { + case dd::find_t::singleton: + case dd::find_t::multiple: + // NOTE: I don't think this can happen if viable::find_viable returned a singleton. since all values excluded by viable are true negatives. + SASSERT(!j.is_propagation()); + j = justification::decision(m_level + 1); + break; + case dd::find_t::empty: + m_free_pvars.unassign_var_eh(v); + // TODO: get unsat core from univariate solver + set_conflict(v); + return; + } + } + if (j.is_decision()) + push_level(); + assign_core(v, val, j); } void solver::bdecide(sat::bool_var b) { @@ -484,11 +542,14 @@ namespace polysat { ++m_stats.m_num_propagations; LOG(assignment_pp(*this, v, val) << " by " << j); SASSERT(m_viable.is_viable(v, val)); + SASSERT(j.level() == m_level); + SASSERT(!is_assigned(v)); SASSERT(std::all_of(assignment().begin(), assignment().end(), [v](auto p) { return p.first != v; })); m_value[v] = val; m_search.push_assignment(v, val); m_trail.push_back(trail_instr_t::assign_i); m_justification[v] = j; + SASSERT(m_viable_fallback.check_constraints(v)); #if ENABLE_LINEAR_SOLVER // TODO: convert justification into a format that can be tracked in a depdendency core. m_linear_solver.set_value(v, val, UINT_MAX); @@ -818,6 +879,8 @@ namespace polysat { SASSERT(!c->is_active()); c->set_active(true); add_watch(c); + if (c->vars().size() == 1) + m_viable_fallback.push_constraint(c->var(0), c); c.narrow(*this, true); #if ENABLE_LINEAR_SOLVER m_linear_solver.activate_constraint(c); diff --git a/src/math/polysat/solver.h b/src/math/polysat/solver.h index adacb5abc..f17008f05 100644 --- a/src/math/polysat/solver.h +++ b/src/math/polysat/solver.h @@ -69,6 +69,7 @@ namespace polysat { friend class forbidden_intervals; friend class linear_solver; friend class viable; + friend class viable_fallback; friend class search_state; friend class assignment_pp; friend class assignments_pp; @@ -84,6 +85,7 @@ namespace polysat { mutable scoped_ptr_vector m_pdd; viable m_viable; // viable sets per variable + viable_fallback m_viable_fallback; // fallback for viable, using bitblasting over univariate constraints linear_solver m_linear_solver; conflict m_conflict; simplify m_simplify; @@ -172,6 +174,7 @@ namespace polysat { void propagate(sat::literal lit); void propagate(pvar v); + bool propagate(pvar v, signed_constraint c); void propagate(pvar v, rational const& val, signed_constraint c); bool propagate(sat::literal lit, clause& cl); void erase_watch(pvar v, signed_constraint c); diff --git a/src/math/polysat/trail.h b/src/math/polysat/trail.h index 2b3657157..01d1814d6 100644 --- a/src/math/polysat/trail.h +++ b/src/math/polysat/trail.h @@ -22,6 +22,7 @@ namespace polysat { inc_level_i, viable_add_i, viable_rem_i, + viable_constraint_i, assign_i, assign_bool_i }; diff --git a/src/math/polysat/viable.cpp b/src/math/polysat/viable.cpp index fdb10c4a5..4b7469136 100644 --- a/src/math/polysat/viable.cpp +++ b/src/math/polysat/viable.cpp @@ -33,8 +33,20 @@ namespace polysat { } viable::~viable() { - for (entry* e : m_alloc) - dealloc(e); + for (entry* e : m_alloc) + dealloc(e); + } + + void viable::push_var(unsigned sz) { + m_units.push_back(nullptr); + m_equal_lin.push_back(nullptr); + m_diseq_lin.push_back(nullptr); + } + + void viable::pop_var() { + m_units.pop_back(); + m_equal_lin.pop_back(); + m_diseq_lin.pop_back(); } viable::entry* viable::alloc_entry() { @@ -58,9 +70,12 @@ namespace polysat { case entry_kind::equal_e: e->remove_from(m_equal_lin[v], e); break; - default: + case entry_kind::diseq_e: e->remove_from(m_diseq_lin[v], e); break; + default: + UNREACHABLE(); + break; } m_alloc.push_back(e); m_trail.pop_back(); @@ -711,6 +726,70 @@ namespace polysat { return true; } + //************************************************************************ + // viable_fallback + //************************************************************************ + viable_fallback::viable_fallback(solver& s): + s(s) { + m_usolver_factory = mk_univariate_bitblast_factory(); + } + + void viable_fallback::push_var(unsigned sz) { + auto& mk_solver = *m_usolver_factory; + m_usolver.push_back(mk_solver(sz)); + } + + void viable_fallback::pop_var() { + m_usolver.pop_back(); + } + + void viable_fallback::push_constraint(pvar v, signed_constraint const& c) { + // v is the only unassigned variable in c. + SASSERT(!s.is_assigned(v)); + DEBUG_CODE(for (pvar w : c->vars()) { if (v != w) SASSERT(s.is_assigned(w)); }); + auto& us = *m_usolver[v]; + // TODO: would be enough to push the solver only for new decision levels + us.push(); + unsigned dep = m_constraints[v].size(); + c.add_to_univariate_solver(s, us, dep); + m_constraints[v].push_back(c); + m_constraints_trail.push_back(v); + s.m_trail.push_back(trail_instr_t::viable_constraint_i); + } + + void viable_fallback::pop_constraint() { + pvar v = m_constraints_trail.back(); + m_constraints_trail.pop_back(); + m_constraints[v].pop_back(); + m_usolver[v]->pop(1); + } + + bool viable_fallback::check_constraints(pvar v) { + for (auto const& c : m_constraints[v]) { + // for this check, all variables need to be assigned + DEBUG_CODE(for (pvar w : c->vars()) { SASSERT(s.is_assigned(w)); }); + if (c.is_currently_false(s)) + return false; + SASSERT(c.is_currently_true(s)); + } + return true; + } + + dd::find_t viable_fallback::find_viable(pvar v, rational& out_val) { + auto& us = *m_usolver[v]; + switch (us.check()) { + case l_true: + out_val = us.model(); + // we don't know whether the SMT instance has a unique solution + return dd::find_t::multiple; + case l_false: + return dd::find_t::empty; + default: + // TODO: what should we do here? (SMT solver had resource-out ==> polysat should abort too?) + UNREACHABLE(); + return dd::find_t::empty; + } + } } diff --git a/src/math/polysat/viable.h b/src/math/polysat/viable.h index 885c33e6c..043c764b2 100644 --- a/src/math/polysat/viable.h +++ b/src/math/polysat/viable.h @@ -69,12 +69,11 @@ namespace polysat { ~viable(); // declare and remove var - void push(unsigned) { m_units.push_back(nullptr); m_equal_lin.push_back(nullptr); m_diseq_lin.push_back(nullptr); } - - void pop() { m_units.pop_back(); m_equal_lin.pop_back(); m_diseq_lin.pop_back(); } + void push_var(unsigned sz); + void pop_var(); + // undo adding/removing of entries void pop_viable(); - void push_viable(); /** @@ -186,6 +185,35 @@ namespace polysat { inline std::ostream& operator<<(std::ostream& out, viable::var_pp const& v) { return v.v.display(out, v.var); } + + + class viable_fallback { + solver& s; + + scoped_ptr m_usolver_factory; + scoped_ptr_vector m_usolver; + vector m_constraints; + svector m_constraints_trail; + + public: + viable_fallback(solver& s); + + // declare and remove var + void push_var(unsigned sz); + void pop_var(); + + // add/remove constraints stored in the fallback solver + void push_constraint(pvar v, signed_constraint const& c); + void pop_constraint(); + + // Check whether all constraints for 'v' are satisfied. + bool check_constraints(pvar v); + // bool check_value(pvar v, rational const& val); + + dd::find_t find_viable(pvar v, rational& out_val); + // TODO: get unsat core + }; + } diff --git a/src/test/viable.cpp b/src/test/viable.cpp index c88f34902..43c95b075 100644 --- a/src/test/viable.cpp +++ b/src/test/viable.cpp @@ -33,7 +33,7 @@ namespace polysat { scoped_solverv s; auto xv = s.add_var(3); auto x = s.var(xv); - s.v.push(3); + s.v.push_var(3); rational val; auto c = s.ule(x + 3, x + 5); s.v.intersect(xv, c); @@ -88,7 +88,7 @@ namespace polysat { scoped_solverv s; auto xv = s.add_var(3); auto x = s.var(xv); - s.v.push(3); + s.v.push_var(3); for (auto const& [lo, len] : intervals) add_interval(s, xv, x, lo, len); std::cout << intervals << "\n"; diff --git a/src/util/scoped_ptr_vector.h b/src/util/scoped_ptr_vector.h index 04d29a9f2..3c33cc708 100644 --- a/src/util/scoped_ptr_vector.h +++ b/src/util/scoped_ptr_vector.h @@ -44,6 +44,7 @@ public: void reset() { std::for_each(m_vector.begin(), m_vector.end(), delete_proc()); m_vector.reset(); } void push_back(T * ptr) { m_vector.push_back(ptr); } + void push_back(scoped_ptr&& ptr) { push_back(ptr.detach()); } void pop_back() { SASSERT(!empty()); set(size()-1, nullptr); m_vector.pop_back(); } T * back() const { return m_vector.back(); } T * operator[](unsigned idx) const { return m_vector[idx]; }