From afde0e993cb65ae83a7477cb559db7b3eae8e843 Mon Sep 17 00:00:00 2001 From: Jakob Rath Date: Fri, 16 Dec 2022 13:02:54 +0100 Subject: [PATCH] Add bitblasting fallback to viable::query (integration between conflict/viable is still messy) --- src/math/polysat/conflict.cpp | 12 + src/math/polysat/conflict.h | 6 +- src/math/polysat/solver.cpp | 2 +- .../polysat/univariate/univariate_solver.cpp | 19 +- .../polysat/univariate/univariate_solver.h | 4 +- src/math/polysat/viable.cpp | 315 ++++++++++++------ src/math/polysat/viable.h | 90 ++++- src/test/viable.cpp | 9 +- 8 files changed, 336 insertions(+), 121 deletions(-) diff --git a/src/math/polysat/conflict.cpp b/src/math/polysat/conflict.cpp index 51fd38f89..51e605d19 100644 --- a/src/math/polysat/conflict.cpp +++ b/src/math/polysat/conflict.cpp @@ -182,6 +182,15 @@ namespace polysat { SASSERT(s.at_base_level()); m_level = s.m_level; SASSERT(!empty()); + // TODO: logger().begin_conflict??? + // TODO: check uses of logger().begin_conflict(). sometimes we call it before adding constraints, sometimes after... + } + + void conflict::init_empty() { + SASSERT(empty()); + m_level = s.m_level; + SASSERT(!empty()); + // TODO: logger().begin_conflict??? } void conflict::init(signed_constraint c) { @@ -193,11 +202,13 @@ namespace polysat { logger().begin_conflict(); } +#if 0 void conflict::set(signed_constraint c) { SASSERT(!empty()); remove_all(); set_impl(c); } +#endif void conflict::set_impl(signed_constraint c) { if (c.bvalue(s) == l_false) { @@ -233,6 +244,7 @@ namespace polysat { void conflict::init(pvar v, bool by_viable_fallback) { LOG("Conflict: viable v" << v); SASSERT(empty()); + SASSERT(!s.is_assigned(v)); m_level = s.m_level; if (by_viable_fallback) { logger().begin_conflict(header_with_var("unsat core from viable fallback for v", v)); diff --git a/src/math/polysat/conflict.h b/src/math/polysat/conflict.h index ac529b382..813a6a8a7 100644 --- a/src/math/polysat/conflict.h +++ b/src/math/polysat/conflict.h @@ -85,7 +85,7 @@ namespace polysat { scoped_ptr m_resolver; // current conflict core consists of m_literals and m_vars - indexed_uint_set m_literals; // set of boolean literals in the conflict + indexed_uint_set m_literals; // set of boolean literals in the conflict; TODO: why not sat::literal_set uint_set m_vars; // variable assignments used as premises, shorthand for literals (x := v) unsigned_vector m_var_occurrences; // for each variable, the number of constraints in m_literals that contain it @@ -135,9 +135,13 @@ namespace polysat { void init(clause const& cl); /** conflict because there is no viable value for the variable v */ void init(pvar v, bool by_viable_fallback); + /** start empty conflict, constraints to be added by caller */ + void init_empty(); // TODO: remove... rather have all types of conflicts explicitly listed here. +#if 0 /** replace the current conflict by a single constraint */ void set(signed_constraint c); +#endif bool contains(signed_constraint c) const { SASSERT(c); return contains(c.blit()); } bool contains(sat::literal lit) const; diff --git a/src/math/polysat/solver.cpp b/src/math/polysat/solver.cpp index dba5ba363..7cadf8106 100644 --- a/src/math/polysat/solver.cpp +++ b/src/math/polysat/solver.cpp @@ -652,7 +652,7 @@ namespace polysat { // (fail here in debug mode so we notice if we miss some) DEBUG_CODE( UNREACHABLE(); ); m_free_pvars.unassign_var_eh(v); - set_conflict(v, false); + SASSERT(is_conflict()); return; case find_t::singleton: // NOTE: this case may happen legitimately if all other possibilities were excluded by brute force search diff --git a/src/math/polysat/univariate/univariate_solver.cpp b/src/math/polysat/univariate/univariate_solver.cpp index e66a521c3..0e75cd98e 100644 --- a/src/math/polysat/univariate/univariate_solver.cpp +++ b/src/math/polysat/univariate/univariate_solver.cpp @@ -26,6 +26,12 @@ Author: namespace polysat { + univariate_solver::dep_vector univariate_solver::unsat_core() { + dep_vector deps; + unsat_core(deps); + return deps; + } + class univariate_bitblast_solver : public univariate_solver { // TODO: does it make sense to share m and bv between different solver instances? // TODO: consider pooling solvers to save setup overhead, see if solver/solver_pool.h can be used @@ -33,6 +39,7 @@ namespace polysat { scoped_ptr bv; scoped_ptr s; unsigned bit_width; + unsigned m_scope_level = 0; func_decl_ref x_decl; expr_ref x; vector model_cache; @@ -67,15 +74,22 @@ namespace polysat { } void push() override { + m_scope_level++; push_cache(); s->push(); } void pop(unsigned n) override { + SASSERT(scope_level() >= n); + m_scope_level -= n; pop_cache(); s->pop(n); } + unsigned scope_level() override { + return m_scope_level; + } + expr* mk_numeral(rational const& r) const { return bv->mk_numeral(r, bit_width); } @@ -198,8 +212,8 @@ namespace polysat { return s->check_sat(); } - dep_vector unsat_core() override { - dep_vector deps; + void unsat_core(dep_vector& deps) override { + deps.reset(); expr_ref_vector core(m); s->get_unsat_core(core); for (expr* a : core) { @@ -207,7 +221,6 @@ namespace polysat { deps.push_back(dep); } SASSERT(deps.size() > 0); - return deps; } rational model() override { diff --git a/src/math/polysat/univariate/univariate_solver.h b/src/math/polysat/univariate/univariate_solver.h index 904342a79..1d41c4075 100644 --- a/src/math/polysat/univariate/univariate_solver.h +++ b/src/math/polysat/univariate/univariate_solver.h @@ -39,13 +39,15 @@ namespace polysat { virtual void push() = 0; virtual void pop(unsigned n) = 0; + virtual unsigned scope_level() = 0; virtual lbool check() = 0; /** * Precondition: check() returned l_false */ - virtual dep_vector unsat_core() = 0; + dep_vector unsat_core(); + virtual void unsat_core(dep_vector& out_deps) = 0; /** * Precondition: check() returned l_true diff --git a/src/math/polysat/viable.cpp b/src/math/polysat/viable.cpp index 6369dba87..dcedec777 100644 --- a/src/math/polysat/viable.cpp +++ b/src/math/polysat/viable.cpp @@ -23,6 +23,10 @@ TODO: improve management of the fallback univariate solvers: - incrementally add/remove constraints - set resource limit of univariate solver +TODO: plan to fix the FI "pumping": + 1. simple looping detection and bitblasting fallback. + 2. intervals at multiple bit widths + --*/ @@ -33,6 +37,8 @@ TODO: improve management of the fallback univariate solvers: namespace polysat { + using namespace viable_query; + struct inf_fi : public inference { viable& v; pvar var; @@ -137,7 +143,7 @@ namespace polysat { prop = true; break; case find_t::empty: - s.set_conflict(v, false); + SASSERT(s.is_conflict()); return true; default: break; @@ -543,15 +549,22 @@ namespace polysat { return refine_viable(v, val); } + lbool viable::min_viable(pvar v, rational& lo) { + return query(v, lo); + } - rational viable::min_viable(pvar v) { - refined: - rational lo(0); - auto* e = m_units[v]; + lbool viable::max_viable(pvar v, rational& hi) { + return query(v, hi); + } + + bool viable::query_min(pvar v, rational& lo) { + // TODO: should be able to deal with UNSAT case; since also min_viable has to deal with it due to fallback solver + lo = 0; + entry* e = m_units[v]; if (!e && !refine_viable(v, lo)) - goto refined; + return false; if (!e) - return lo; + return true; entry* first = e; entry* last = first->prev(); if (last->interval.currently_contains(lo)) @@ -564,19 +577,19 @@ namespace polysat { } while (e != first); if (!refine_viable(v, lo)) - goto refined; + return false; SASSERT(is_viable(v, lo)); - return lo; + return true; } - rational viable::max_viable(pvar v) { - refined: - rational hi = s.var2pdd(v).max_value(); + bool viable::query_max(pvar v, rational& hi) { + // TODO: should be able to deal with UNSAT case; since also max_viable has to deal with it due to fallback solver + hi = s.var2pdd(v).max_value(); auto* e = m_units[v]; if (!e && !refine_viable(v, hi)) - goto refined; + return false; if (!e) - return hi; + return true; entry* last = e->prev(); e = last; do { @@ -587,17 +600,13 @@ namespace polysat { } while (e != last); if (!refine_viable(v, hi)) - goto refined; + return false; SASSERT(is_viable(v, hi)); - return hi; + return true; } - // template - find_t viable::query(query_t mode, pvar v, rational& lo, rational& hi) { - SASSERT(mode == query_t::find_viable); // other modes are TODO - - auto const& max_value = s.var2pdd(v).max_value(); - + template + lbool viable::query(pvar v, typename query_result::result_t& result) { // max number of interval refinements before falling back to the univariate solver unsigned const refinement_budget = 1000; unsigned refinements = refinement_budget; @@ -606,25 +615,152 @@ namespace polysat { if (!refinements) { LOG("Refinement budget exhausted! Fall back to univariate solver."); - return find_t::resource_out; + return query_fallback(v, result); } refinements--; + if constexpr (mode == query_t::find_viable) { + lbool res = query_find(v, result.first, result.second); + if (res == l_undef) + goto refined; + return res; + } + + if constexpr (mode == query_t::min_viable) { + if (!query_min(v, result)) + goto refined; + return l_true; + } + + if constexpr (mode == query_t::max_viable) { + if (!query_max(v, result)) + goto refined; + return l_true; + } + + if constexpr (mode == query_t::has_viable) { + NOT_IMPLEMENTED_YET(); + return l_undef; + } + + UNREACHABLE(); + return l_undef; + } + + template + lbool viable::query_fallback(pvar v, typename query_result::result_t& result) { + unsigned const bit_width = s.size(v); + univariate_solver* us = s.m_viable_fallback.usolver(bit_width); + sat::literal_set added; + + // First step: only query the looping constraints and see if they alone are already UNSAT. + // The constraints which caused the refinement loop will be reached from m_units. + entry const* first = m_units[v]; + entry const* e = first; + do { + entry const* origin = e; + while (origin->refined) + origin = origin->refined; + signed_constraint const c = origin->src; + sat::literal const lit = c.blit(); + if (!added.contains(lit)) { + added.insert(lit); + c.add_to_univariate_solver(s, *us, lit.to_uint()); + } + e = e->next(); + } + while (e != first); + + switch (us->check()) { + case l_false: + set_fallback_conflict(v, *us); + return l_false; + case l_true: + // At this point we don't know much because we did not add all relevant constraints + break; + default: + // resource limit + return l_undef; + } + + // Second step: looping constraints aren't UNSAT, so add the remaining relevant constraints + auto const& cs = s.m_viable_fallback.m_constraints[v]; + for (unsigned i = cs.size(); i-- > 0; ) { + sat::literal const lit = cs[i].blit(); + if (added.contains(lit)) + continue; + added.insert(lit); + cs[i].add_to_univariate_solver(s, *us, lit.to_uint()); + } + + switch (us->check()) { + case l_false: + set_fallback_conflict(v, *us); + return l_false; + case l_true: + // pass solver to mode-specific query + break; + default: + // resource limit + return l_undef; + } + + if constexpr (mode == query_t::find_viable) + return query_find_fallback(v, *us, result.first, result.second); + + if constexpr (mode == query_t::min_viable) + return query_min_fallback(v, *us, result); + + if constexpr (mode == query_t::max_viable) + return query_max_fallback(v, *us, result); + + if constexpr (mode == query_t::has_viable) { + NOT_IMPLEMENTED_YET(); + return l_undef; + } + + UNREACHABLE(); + return l_undef; + } + + lbool viable::query_find_fallback(pvar v, univariate_solver& us, rational& lo, rational& hi) { + if (!us.find_min(lo)) + return l_undef; + if (!us.find_max(hi)) + return l_undef; + return l_true; + } + + lbool viable::query_min_fallback(pvar v, univariate_solver& us, rational& lo) { + return us.find_min(lo) ? l_true : l_undef; + } + + lbool viable::query_max_fallback(pvar v, univariate_solver& us, rational& hi) { + return us.find_max(hi) ? l_true : l_undef; + } + + lbool viable::query_find(pvar v, rational& lo, rational& hi) { + auto const& max_value = s.var2pdd(v).max_value(); + lbool const refined = l_undef; + // After a refinement, any of the existing entries may have been replaced // (if it is subsumed by the new entry created during refinement). // For this reason, we start chasing the intervals from the start again. lo = 0; + hi = max_value; auto* e = m_units[v]; if (!e && !refine_viable(v, lo)) - goto refined; - if (!e && !refine_viable(v, rational::one())) - goto refined; + return refined; + if (!e && !refine_viable(v, hi)) + return refined; if (!e) - return find_t::multiple; - if (e->interval.is_full()) - return find_t::empty; + return l_true; + if (e->interval.is_full()) { + set_interval_conflict(v); + return l_false; + } entry* first = e; entry* last = first->prev(); @@ -635,10 +771,10 @@ namespace polysat { last->interval.hi_val() < max_value) { lo = last->interval.hi_val(); if (!refine_viable(v, lo)) - goto refined; + return refined; if (!refine_viable(v, max_value)) - goto refined; - return find_t::multiple; + return refined; + return l_true; } // find lower bound @@ -652,8 +788,10 @@ namespace polysat { } while (e != first); - if (e->interval.currently_contains(lo)) - return find_t::empty; + if (e->interval.currently_contains(lo)) { + set_interval_conflict(v); + return l_false; + } // find upper bound hi = max_value; @@ -666,83 +804,59 @@ namespace polysat { } while (e != last); if (!refine_viable(v, lo)) - goto refined; + return refined; if (!refine_viable(v, hi)) - goto refined; + return refined; + return l_true; + } - if (lo == hi) - return find_t::singleton; - else - return find_t::multiple; + lbool viable::find_viable(pvar v, rational& lo, rational& hi) { + std::pair args{lo, hi}; + return query(v, args); } find_t viable::find_viable(pvar v, rational& lo) { -#if 1 rational hi; - // return query(v, lo, hi); - return query(query_t::find_viable, v, lo, hi); -#else - refined: - lo = 0; - auto* e = m_units[v]; - if (!e && !refine_viable(v, lo)) - goto refined; - if (!e && !refine_viable(v, rational::one())) - goto refined; - if (!e) - return find_t::multiple; - if (e->interval.is_full()) + switch (find_viable(v, lo, hi)) { + case l_true: + return (lo == hi) ? find_t::singleton : find_t::multiple; + case l_false: return find_t::empty; - - entry* first = e; - entry* last = first->prev(); - - // quick check: last interval does not wrap around - // and has space for 2 unassigned values. - auto& max_value = s.var2pdd(v).max_value(); - if (last->interval.lo_val() < last->interval.hi_val() && - last->interval.hi_val() < max_value) { - lo = last->interval.hi_val(); - if (!refine_viable(v, lo)) - goto refined; - if (!refine_viable(v, max_value)) - goto refined; - return find_t::multiple; + default: + return find_t::resource_out; } + } - // find lower bound - if (last->interval.currently_contains(lo)) - lo = last->interval.hi_val(); - do { - if (!e->interval.currently_contains(lo)) - break; - lo = e->interval.hi_val(); - e = e->next(); + void viable::set_fallback_conflict(pvar v, univariate_solver& us) { + SASSERT(!s.is_assigned(v)); + conflict& core = s.m_conflict; + core.init_empty(); + core.logger().begin_conflict(); //header_with_var("unsat core from viable fallback for v", v)); // TODO: begin_conflict before or after adding constraints? + // The conflict is the unsat core of the univariate solver, + // and the current assignment (under which the constraints are univariate in v) + // TODO: + // - currently we add variables directly, which is sound: + // e.g.: v^2 + w^2 == 0; w := 1 + // - but we could use side constraints on the coefficients instead (coefficients when viewed as polynomial over v): + // e.g.: v^2 + w^2 == 0; w^2 == 1 + for (unsigned dep : us.unsat_core()) { + sat::literal lit = sat::to_literal(dep); + signed_constraint c = s.lit2cnstr(lit); + core.insert(c); + core.insert_vars(c); } - while (e != first); + SASSERT(!core.vars().contains(v)); + core.add_lemma("viable unsat core", core.build_lemma()); + core.revert_pvar(v); // at this point, v is not assigned + } - if (e->interval.currently_contains(lo)) - return find_t::empty; - - // find upper bound - rational hi = max_value; - e = last; - do { - if (!e->interval.currently_contains(hi)) - break; - hi = e->interval.lo_val() - 1; - e = e->prev(); - } - while (e != last); - if (!refine_viable(v, lo)) - goto refined; - if (!refine_viable(v, hi)) - goto refined; - if (lo == hi) - return find_t::singleton; - else - return find_t::multiple; -#endif + void viable::set_interval_conflict(pvar v) { + SASSERT(!s.is_assigned(v)); + conflict& core = s.m_conflict; + core.init_empty(); + core.logger().begin_conflict(); //header_with_var("forbidden interval lemma for v", v)); + VERIFY(resolve(v, core)); // TODO: merge? + core.revert_pvar(v); // at this point, v is not assigned } bool viable::resolve(pvar v, conflict& core) { @@ -960,6 +1074,7 @@ namespace polysat { m_usolver.insert(bit_width, mk_solver(bit_width)); us = m_usolver[bit_width].get(); } + SASSERT_EQ(us->scope_level(), 0); // push once on the empty solver so we can reset it before the next use us->push(); diff --git a/src/math/polysat/viable.h b/src/math/polysat/viable.h index c99c27104..c7fbcaf11 100644 --- a/src/math/polysat/viable.h +++ b/src/math/polysat/viable.h @@ -25,6 +25,7 @@ Author: #include "math/polysat/conflict.h" #include "math/polysat/constraint.h" #include "math/polysat/forbidden_intervals.h" +#include namespace polysat { @@ -39,6 +40,34 @@ namespace polysat { resource_out, }; + namespace viable_query { + enum class query_t { + has_viable, // currently only used internally in resolve_viable + min_viable, // currently unused + max_viable, // currently unused + find_viable, + }; + + template + struct query_result { + }; + + template <> + struct query_result { + using result_t = rational; + }; + + template <> + struct query_result { + using result_t = rational; + }; + + template <> + struct query_result { + using result_t = std::pair; + }; + } + std::ostream& operator<<(std::ostream& out, find_t x); class viable { @@ -76,15 +105,38 @@ namespace polysat { void propagate(pvar v, rational const& val); - enum class query_t { - has_viable, // currently only used internally in resolve_viable - min_viable, // currently unused - max_viable, // currently unused - find_viable, - }; + // return true if done, false if refined + bool query_min(pvar v, rational& out_lo); - // template - find_t query(query_t mode, pvar v, rational& out_lo, rational& out_hi); + // return true if done, false if refined + bool query_max(pvar v, rational& out_hi); + + // return true if done, false if resource out + lbool query_min_fallback(pvar v, univariate_solver& us, rational& out_lo); + lbool query_max_fallback(pvar v, univariate_solver& us, rational& out_hi); + + // return resource_out if refined + lbool query_find(pvar v, rational& out_lo, rational& out_hi); + lbool query_find_fallback(pvar v, univariate_solver& us, rational& out_lo, rational& out_hi); + + /** + * Interval query with bounded refinement and fallback to bitblasting. + * @return l_true on success, l_false on conflict, l_undef on resource limit + */ + template + lbool query(pvar v, typename viable_query::query_result::result_t& out_result); + + /** + * @return l_true on success, l_false on conflict, l_undef on resource limit + */ + template + lbool query_fallback(pvar v, typename viable_query::query_result::result_t& out_result); + + /** Set viable conflict due to interval cover */ + void set_interval_conflict(pvar v); + + /** Set viable conflict due to fallback solver */ + void set_fallback_conflict(pvar v, univariate_solver& us); public: viable(solver& s); @@ -122,17 +174,29 @@ namespace polysat { */ bool is_viable(pvar v, rational const& val); - /* - * Extract min and max viable values for v + /** + * Extract min viable value for v. + * @return l_true on success, l_false on conflict, l_undef on resource limit */ - rational min_viable(pvar v); - rational max_viable(pvar v); + lbool min_viable(pvar v, rational& out_lo); + + /** + * Extract max viable value for v. + * @return l_true on success, l_false on conflict, l_undef on resource limit + */ + lbool max_viable(pvar v, rational& out_hi); /** * Find a next viable value for variable. */ find_t find_viable(pvar v, rational& out_val); + /** + * Find a next viable value for variable by determining currently viable lower and upper bounds. + * @return l_true on success, l_false on conflict, l_undef on resource limit + */ + lbool find_viable(pvar v, rational& out_lo, rational& out_hi); + /** * Retrieve the unsat core for v, * and add the forbidden interval lemma for v (which eliminates v from the unsat core). @@ -251,6 +315,8 @@ namespace polysat { } class viable_fallback { + friend class viable; + solver& s; scoped_ptr m_usolver_factory; diff --git a/src/test/viable.cpp b/src/test/viable.cpp index c2614854d..ba68e377b 100644 --- a/src/test/viable.cpp +++ b/src/test/viable.cpp @@ -38,16 +38,19 @@ namespace polysat { auto c = s.ule(x + 3, x + 5); s.v.intersect(xv, c); std::cout << s.v << "\n"; - std::cout << "min-max " << s.v.min_viable(xv) << " " << s.v.max_viable(xv) << "\n"; + std::cout << "min " << s.v.min_viable(xv, val) << " " << val << "\n"; + std::cout << "max " << s.v.max_viable(xv, val) << " " << val << "\n"; s.v.intersect(xv, s.ule(x, 2)); std::cout << s.v << "\n"; s.v.intersect(xv, s.ule(1, x)); std::cout << s.v << "\n"; - std::cout << "min-max " << s.v.min_viable(xv) << " " << s.v.max_viable(xv) << "\n"; + std::cout << "min " << s.v.min_viable(xv, val) << " " << val << "\n"; + std::cout << "max " << s.v.max_viable(xv, val) << " " << val << "\n"; s.v.intersect(xv, s.ule(x, 3)); std::cout << s.v << "\n"; std::cout << s.v.find_viable(xv, val) << " " << val << "\n"; - std::cout << "min-max " << s.v.min_viable(xv) << " " << s.v.max_viable(xv) << "\n"; + std::cout << "min " << s.v.min_viable(xv, val) << " " << val << "\n"; + std::cout << "max " << s.v.max_viable(xv, val) << " " << val << "\n"; s.v.intersect(xv, s.ule(3, x)); std::cout << s.v << "\n"; std::cout << s.v.find_viable(xv, val) << " " << val << "\n";