From 5de0007157c7ac02f4b2bfba27f21a2aa1f8bc5d Mon Sep 17 00:00:00 2001 From: Jakob Rath Date: Thu, 15 Dec 2022 13:39:48 +0100 Subject: [PATCH] very basic refinement loop breaking --- src/math/polysat/solver.cpp | 23 ++++-- src/math/polysat/viable.cpp | 138 +++++++++++++++++++++++++++++++----- src/math/polysat/viable.h | 23 +++++- 3 files changed, 158 insertions(+), 26 deletions(-) diff --git a/src/math/polysat/solver.cpp b/src/math/polysat/solver.cpp index def600bad..dba5ba363 100644 --- a/src/math/polysat/solver.cpp +++ b/src/math/polysat/solver.cpp @@ -647,22 +647,29 @@ namespace polysat { rational val; justification j; switch (m_viable.find_viable(v, val)) { - case dd::find_t::empty: + case find_t::empty: // NOTE: all such cases should be discovered elsewhere (e.g., during propagation/narrowing) // (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); return; - case dd::find_t::singleton: + case find_t::singleton: // NOTE: this case may happen legitimately if all other possibilities were excluded by brute force search // NOTE 2: probably not true anymore; viable::intersect should trigger all propagations now DEBUG_CODE( UNREACHABLE(); ); j = justification::propagation(m_level); break; - case dd::find_t::multiple: + case find_t::multiple: j = justification::decision(m_level + 1); break; + case find_t::resource_out: + // the value is not viable, so assign_verify will call the univariate solver. + j = justification::decision(m_level + 1); + break; + default: + UNREACHABLE(); + break; } assign_verify(v, val, j); } @@ -731,20 +738,24 @@ namespace polysat { } if (c) { LOG_H2("Chosen assignment " << assignment_pp(*this, v, val) << " is not actually viable!"); + LOG("Current assignment: " << assignments_pp(*this)); ++m_stats.m_num_viable_fallback; // 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: + case find_t::singleton: + case find_t::multiple: LOG("Fallback solver: " << assignment_pp(*this, v, val)); SASSERT(!j.is_propagation()); // all excluded values are true negatives, so if j.is_propagation() the univariate solver must return unsat j = justification::decision(m_level + 1); break; - case dd::find_t::empty: + case find_t::empty: LOG("Fallback solver: unsat"); m_free_pvars.unassign_var_eh(v); set_conflict(v, true); return; + case find_t::resource_out: + UNREACHABLE(); // TODO: abort solving + return; } } if (j.is_decision()) diff --git a/src/math/polysat/viable.cpp b/src/math/polysat/viable.cpp index ae8fea496..3b832b7cf 100644 --- a/src/math/polysat/viable.cpp +++ b/src/math/polysat/viable.cpp @@ -132,11 +132,11 @@ namespace polysat { if (intersect(v, sc)) { rational val; switch (find_viable(v, val)) { - case dd::find_t::singleton: + case find_t::singleton: propagate(v, val); prop = true; break; - case dd::find_t::empty: + case find_t::empty: s.set_conflict(v, false); return true; default: @@ -592,25 +592,45 @@ namespace polysat { return hi; } - dd::find_t viable::find_viable(pvar v, rational& lo) { - refined: + // 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(); + + // max number of interval refinements before falling back to the univariate solver + unsigned const refinement_budget = 1000; + unsigned refinements = refinement_budget; + + refined: + + if (!refinements) { + LOG("Refinement budget exhausted! Fall back to univariate solver."); + return find_t::resource_out; + } + + refinements--; + + // 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; + 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 dd::find_t::multiple; + return find_t::multiple; if (e->interval.is_full()) - return dd::find_t::empty; + 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(); @@ -618,7 +638,7 @@ namespace polysat { goto refined; if (!refine_viable(v, max_value)) goto refined; - return dd::find_t::multiple; + return find_t::multiple; } // find lower bound @@ -633,7 +653,76 @@ namespace polysat { while (e != first); if (e->interval.currently_contains(lo)) - return dd::find_t::empty; + return find_t::empty; + + // find upper bound + 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; + } + + 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()) + 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; + } + + // 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(); + } + while (e != first); + + if (e->interval.currently_contains(lo)) + return find_t::empty; // find upper bound rational hi = max_value; @@ -650,9 +739,10 @@ namespace polysat { if (!refine_viable(v, hi)) goto refined; if (lo == hi) - return dd::find_t::singleton; + return find_t::singleton; else - return dd::find_t::multiple; + return find_t::multiple; +#endif } bool viable::resolve(pvar v, conflict& core) { @@ -857,7 +947,7 @@ namespace polysat { return {}; } - dd::find_t viable_fallback::find_viable(pvar v, rational& out_val) { + find_t viable_fallback::find_viable(pvar v, rational& out_val) { unsigned bit_width = s.m_size[v]; univariate_solver* us; @@ -884,14 +974,11 @@ namespace polysat { case l_true: out_val = us->model(); // we don't know whether the SMT instance has a unique solution - return dd::find_t::multiple; + return find_t::multiple; case l_false: - return dd::find_t::empty; + return find_t::empty; default: - // TODO: what should we do here? (SMT solver had resource-out ==> polysat should abort too?) - // can we pass polysat's resource limit to the univariate solver? - UNREACHABLE(); - return dd::find_t::empty; + return find_t::resource_out; } } @@ -905,5 +992,20 @@ namespace polysat { return cs; } + std::ostream& operator<<(std::ostream& out, find_t x) { + switch (x) { + case find_t::empty: + return out << "empty"; + case find_t::singleton: + return out << "singleton"; + case find_t::multiple: + return out << "multiple"; + case find_t::resource_out: + return out << "resource_out"; + } + UNREACHABLE(); + return out; + } + } diff --git a/src/math/polysat/viable.h b/src/math/polysat/viable.h index 544082d34..6588dcc18 100644 --- a/src/math/polysat/viable.h +++ b/src/math/polysat/viable.h @@ -32,6 +32,15 @@ namespace polysat { class univariate_solver; class univariate_solver_factory; + enum class find_t { + empty, + singleton, + multiple, + resource_out, + }; + + std::ostream& operator<<(std::ostream& out, find_t x); + class viable { friend class test_fi; @@ -67,6 +76,16 @@ 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, + }; + + // template + find_t query(query_t mode, pvar v, rational& out_lo, rational& out_hi); + public: viable(solver& s); @@ -112,7 +131,7 @@ namespace polysat { /** * Find a next viable value for variable. */ - dd::find_t find_viable(pvar v, rational & val); + find_t find_viable(pvar v, rational& out_val); /** * Retrieve the unsat core for v, @@ -255,7 +274,7 @@ namespace polysat { bool check_constraints(assignment const& a, pvar v) { return !find_violated_constraint(a, v); } signed_constraint find_violated_constraint(assignment const& a, pvar v); - dd::find_t find_viable(pvar v, rational& out_val); + find_t find_viable(pvar v, rational& out_val); signed_constraints unsat_core(pvar v); };