From 1a733a3a5056a98d232cb2b4786d6564fce94ae2 Mon Sep 17 00:00:00 2001 From: Jakob Rath Date: Fri, 3 Feb 2023 17:37:09 +0100 Subject: [PATCH] compute polysat unsat core --- src/math/polysat/conflict.cpp | 84 ++++++++++++++++++++++++++++++----- src/math/polysat/solver.cpp | 30 +++++++++++-- src/math/polysat/solver.h | 4 ++ 3 files changed, 105 insertions(+), 13 deletions(-) diff --git a/src/math/polysat/conflict.cpp b/src/math/polysat/conflict.cpp index 8298b16ff..c599ddcbf 100644 --- a/src/math/polysat/conflict.cpp +++ b/src/math/polysat/conflict.cpp @@ -412,7 +412,7 @@ namespace polysat { s.inc_activity(v); m_vars.remove(v); - for (auto const& c : s.m_viable.get_constraints(v)) + for (signed_constraint const c : s.m_viable.get_constraints(v)) insert(c); for (auto const& i : s.m_viable.units(v)) { insert(s.eq(i.lo(), i.lo_val())); @@ -500,18 +500,82 @@ namespace polysat { #endif void conflict::find_deps(dependency_vector& out_deps) const { - sat::literal_vector todo; - sat::literal_set done; + sat::literal_vector todo_lits; + sat::literal_set done_lits; + unsigned_vector todo_vars; + uint_set done_vars; indexed_uint_set deps; - LOG("conflict: " << *this); + LOG("Conflict: " << *this); - // TODO: starting at literals/variables in the conflict, chase propagations backwards and accumulate dependencies. - verbose_stream() << "WARNING: unsat_core requested but dependency tracking in polysat is TODO\n"; - for (signed_constraint c : *this) { - dependency d = s.m_bvars.dep(c.blit()); - if (!d.is_null()) - deps.insert(d.val()); + auto const enqueue_lit = [&](sat::literal lit) { + if (done_lits.contains(lit)) + return; + // verbose_stream() << "enqueue " << lit_pp(s, lit) << "\n"; + todo_lits.push_back(lit); + done_lits.insert(lit); + }; + + auto const enqueue_var = [&](pvar v) { + if (done_vars.contains(v)) + return; + // verbose_stream() << "enqueue v" << v << "\n"; + todo_vars.push_back(v); + done_vars.insert(v); + }; + + // Starting at literals/variables in the conflict, chase propagations backwards and accumulate dependencies. + for (signed_constraint c : *this) + enqueue_lit(c.blit()); + for (pvar v : m_vars) + enqueue_var(v); + + while (!todo_vars.empty() || !todo_lits.empty()) { + while (!todo_vars.empty()) { + pvar const v = todo_vars.back(); + todo_vars.pop_back(); + + if (s.m_justification[v].is_decision()) + continue; + SASSERT(s.m_justification[v].is_propagation()); + + for (signed_constraint c : s.m_viable.get_constraints(v)) + enqueue_lit(c.blit()); + for (auto const& i : s.m_viable.units(v)) { + enqueue_lit(s.try_eval(s.eq(i.lo(), i.lo_val()))); + enqueue_lit(s.try_eval(s.eq(i.hi(), i.hi_val()))); + } + } + while (!todo_lits.empty()) { + sat::literal const lit = todo_lits.back(); + todo_lits.pop_back(); + + dependency const d = s.m_bvars.dep(lit); + if (!d.is_null()) + deps.insert(d.val()); + + if (s.m_bvars.is_decision(lit)) + continue; + else if (s.m_bvars.is_assumption(lit)) + continue; + else if (s.m_bvars.is_bool_propagation(lit)) { + for (sat::literal other : *s.m_bvars.reason(lit)) + enqueue_lit(other); + } + else if (s.m_bvars.is_evaluation(lit)) { + unsigned const lvl = s.m_bvars.level(lit); + for (pvar v : s.lit2cnstr(lit).vars()) { + if (!s.is_assigned(v)) + continue; + if (s.get_level(v) > lvl) + continue; + enqueue_var(v); + } + } + else { + UNREACHABLE(); + } + } } for (unsigned d : deps) diff --git a/src/math/polysat/solver.cpp b/src/math/polysat/solver.cpp index 3717f1427..fe9770861 100644 --- a/src/math/polysat/solver.cpp +++ b/src/math/polysat/solver.cpp @@ -153,7 +153,7 @@ namespace polysat { if (is_conflict()) return; // no need to do anything if we already have a conflict at base level sat::literal lit = c.blit(); - LOG("New constraint: " << c); + LOG("New constraint: " << lit_pp(*this, c)); switch (m_bvars.value(lit)) { case l_false: // Input literal contradicts current boolean state (e.g., opposite literals in the input) @@ -1085,6 +1085,21 @@ namespace polysat { assign_eval(lit); } + sat::literal solver::try_eval(sat::literal lit) { + signed_constraint const c = lit2cnstr(lit); + switch (c.eval(*this)) { + case l_true: + assign_eval(lit); + break; + case l_false: + assign_eval(~lit); + break; + default: + break; + } + return lit; + } + /** * Activate constraint immediately * Activation and de-activation of constraints follows the scope controlled by push/pop. @@ -1282,13 +1297,19 @@ namespace polysat { void solver::report_unsat() { backjump(base_level()); - SASSERT(!m_conflict.empty()); + VERIFY(!m_conflict.empty()); } void solver::unsat_core(dependency_vector& deps) { VERIFY(is_conflict()); deps.reset(); m_conflict.find_deps(deps); + IF_VERBOSE(10, + verbose_stream() << "polysat unsat_core"; + for (auto d : deps) + verbose_stream() << " " << d; + verbose_stream() << "\n"; + ); } std::ostream& solver::display(std::ostream& out) const { @@ -1335,7 +1356,7 @@ namespace polysat { } std::ostream& lit_pp::display(std::ostream& out) const { - auto c = s.lit2cnstr(lit); + signed_constraint const c = s.lit2cnstr(lit); out << lpad(5, lit) << ": " << rpad(30, c); if (!c) return out; @@ -1357,6 +1378,9 @@ namespace polysat { out << " pwatched"; if (c->is_external()) out << " ext"; + dependency const d = s.m_bvars.dep(lit); + if (!d.is_null()) + out << " dep:" << d.val(); out << " ]"; return out; } diff --git a/src/math/polysat/solver.h b/src/math/polysat/solver.h index 1c85e3bd7..a22c14915 100644 --- a/src/math/polysat/solver.h +++ b/src/math/polysat/solver.h @@ -307,6 +307,10 @@ namespace polysat { clause_ref mk_clause(std::initializer_list cs, bool is_redundant); clause_ref mk_clause(unsigned n, signed_constraint const* cs, bool is_redundant); + // Evaluate constraint under the current assignment. + sat::literal try_eval(sat::literal lit); + sat::literal try_eval(signed_constraint c) { return try_eval(c.blit()); } + signed_constraint lit2cnstr(sat::literal lit) const { return m_constraints.lookup(lit); } bool inc() { return m_lim.inc(); }