From aa81f6c9fbb5d341150caa590914295b2f3b9a08 Mon Sep 17 00:00:00 2001 From: Jakob Rath Date: Mon, 7 Aug 2023 15:19:39 +0200 Subject: [PATCH] Propagate value assignments discovered by the slicing e-graph --- src/math/polysat/conflict.cpp | 48 +++++++++++++++++++++++------- src/math/polysat/conflict.h | 4 ++- src/math/polysat/justification.cpp | 8 +++-- src/math/polysat/justification.h | 15 +++++++--- src/math/polysat/search_state.cpp | 4 ++- src/math/polysat/slicing.cpp | 35 ++++++++++++++++++++-- src/math/polysat/slicing.h | 3 ++ src/math/polysat/solver.cpp | 46 +++++++++++++++++----------- src/math/polysat/solver.h | 6 ++-- src/math/polysat/types.h | 8 +++-- src/math/polysat/viable.cpp | 2 +- 11 files changed, 136 insertions(+), 43 deletions(-) diff --git a/src/math/polysat/conflict.cpp b/src/math/polysat/conflict.cpp index dea317bea..0ecf7699b 100644 --- a/src/math/polysat/conflict.cpp +++ b/src/math/polysat/conflict.cpp @@ -468,9 +468,9 @@ namespace polysat { m_resolver->infer_lemmas_for_value(v, *this); } - void conflict::resolve_value(pvar v) { + void conflict::resolve_value_by_viable(pvar v) { SASSERT(contains_pvar(v)); - SASSERT(s.m_justification[v].is_propagation()); + SASSERT(s.m_justification[v].is_propagation_by_viable()); s.inc_activity(v); @@ -489,6 +489,26 @@ namespace polysat { revert_pvar(v); } + void conflict::resolve_value_by_slicing(pvar v) { + SASSERT(contains_pvar(v)); + SASSERT(s.m_justification[v].is_propagation_by_slicing()); + + s.inc_activity(v); + + m_vars.remove(v); + s.m_slicing.explain_value(v, + [this](sat::literal lit) { + insert_or_replace(s.lit2cnstr(lit)); + }, + [this](pvar w) { + SASSERT(s.is_assigned(w)); + m_vars.insert(w); + }); + // logger().log(inf_resolve_value(s, v)); TODO + + revert_pvar(v); + } + clause_ref conflict::build_lemma() { LOG_H3("Build lemma from core"); LOG("core: " << *this); @@ -619,13 +639,21 @@ namespace polysat { todo_vars.pop_back(); IF_VERBOSE(11, verbose_stream() << "Handling v" << v << "\n";); - SASSERT(s.m_justification[v].is_propagation()); // no decisions at base level - - for (signed_constraint c : s.m_viable.get_constraints(v)) - enqueue_constraint(c); - for (auto const& i : s.m_viable.units(v)) { - enqueue_constraint(s.eq(i.lo(), i.lo_val())); - enqueue_constraint(s.eq(i.hi(), i.hi_val())); + auto const& j = s.m_justification[v]; + if (j.is_propagation_by_viable()) { + for (signed_constraint c : s.m_viable.get_constraints(v)) + enqueue_constraint(c); + for (auto const& i : s.m_viable.units(v)) { + enqueue_constraint(s.eq(i.lo(), i.lo_val())); + enqueue_constraint(s.eq(i.hi(), i.hi_val())); + } + } + else if (j.is_propagation_by_slicing()) { + s.m_slicing.explain_value(v, enqueue_lit, enqueue_var); + } + else { + // no decisions at base level + UNREACHABLE(); } } while (!todo_lits.empty()) { @@ -670,7 +698,7 @@ namespace polysat { std::ostream& conflict::display(std::ostream& out) const { out << "lvl " << m_level; if (!m_dep.is_null()) - out << "dep " << m_dep; + out << " dep " << m_dep; char const* sep = " "; for (auto c : *this) out << sep << c->bvar2string() << " " << c, sep = " ; "; diff --git a/src/math/polysat/conflict.h b/src/math/polysat/conflict.h index 49de153ac..1e2aaf107 100644 --- a/src/math/polysat/conflict.h +++ b/src/math/polysat/conflict.h @@ -191,7 +191,9 @@ namespace polysat { void resolve_evaluated(sat::literal lit); /** Perform resolution with "v = value <- ..." */ - void resolve_value(pvar v); + void resolve_value_by_viable(pvar v); + + void resolve_value_by_slicing(pvar v); /** Revert variable assignment, add auxiliary lemmas for the reverted variable */ void revert_pvar(pvar v); diff --git a/src/math/polysat/justification.cpp b/src/math/polysat/justification.cpp index 8054ce851..725223f97 100644 --- a/src/math/polysat/justification.cpp +++ b/src/math/polysat/justification.cpp @@ -8,7 +8,7 @@ Module Name: Author: Nikolaj Bjorner (nbjorner) 2021-03-19 - Jakob Rath 2021-04-6 + Jakob Rath 2021-04-06 --*/ @@ -22,8 +22,10 @@ namespace polysat { return out << "unassigned"; case justification_k::decision: return out << "decision @ " << level(); - case justification_k::propagation: - return out << "propagation @ " << level(); + case justification_k::propagation_by_viable: + return out << "propagation by viable @ " << level(); + case justification_k::propagation_by_slicing: + return out << "propagation by slicing @ " << level(); } UNREACHABLE(); return out; diff --git a/src/math/polysat/justification.h b/src/math/polysat/justification.h index 336b58f52..1d2fbe1a0 100644 --- a/src/math/polysat/justification.h +++ b/src/math/polysat/justification.h @@ -8,7 +8,7 @@ Module Name: Author: Nikolaj Bjorner (nbjorner) 2021-03-19 - Jakob Rath 2021-04-6 + Jakob Rath 2021-04-06 --*/ #pragma once @@ -21,7 +21,12 @@ namespace polysat { /** * Justification kind for a variable assignment. */ - enum justification_k { unassigned, decision, propagation }; + enum class justification_k { + unassigned, + decision, + propagation_by_viable, + propagation_by_slicing, + }; class justification { justification_k m_kind; @@ -31,10 +36,12 @@ namespace polysat { justification(): m_kind(justification_k::unassigned) {} static justification unassigned() { return justification(justification_k::unassigned, 0); } static justification decision(unsigned lvl) { return justification(justification_k::decision, lvl); } - static justification propagation(unsigned lvl) { return justification(justification_k::propagation, lvl); } + static justification propagation_by_viable(unsigned lvl) { return justification(justification_k::propagation_by_viable, lvl); } + static justification propagation_by_slicing(unsigned lvl) { return justification(justification_k::propagation_by_slicing, lvl); } bool is_decision() const { return m_kind == justification_k::decision; } bool is_unassigned() const { return m_kind == justification_k::unassigned; } - bool is_propagation() const { return m_kind == justification_k::propagation; } + bool is_propagation_by_viable() const { return m_kind == justification_k::propagation_by_viable; } + bool is_propagation_by_slicing() const { return m_kind == justification_k::propagation_by_slicing; } justification_k kind() const { return m_kind; } unsigned level() const { /* SASSERT(!is_unassigned()); */ return m_level; } // TODO: check why this assertion triggers... std::ostream& display(std::ostream& out) const; diff --git a/src/math/polysat/search_state.cpp b/src/math/polysat/search_state.cpp index 742941a9d..018e4777d 100644 --- a/src/math/polysat/search_state.cpp +++ b/src/math/polysat/search_state.cpp @@ -30,8 +30,10 @@ namespace polysat { switch (j.kind()) { case justification_k::decision: return out << " by decision"; - case justification_k::propagation: + case justification_k::propagation_by_viable: return out << " by " << viable::var_pp(s.m_viable, var); + case justification_k::propagation_by_slicing: + return out << " by slicing (detailed output is TODO)"; case justification_k::unassigned: return out << " unassigned"; } diff --git a/src/math/polysat/slicing.cpp b/src/math/polysat/slicing.cpp index 11c9ca368..a861b3230 100644 --- a/src/math/polysat/slicing.cpp +++ b/src/math/polysat/slicing.cpp @@ -718,6 +718,35 @@ namespace polysat { return cb.build(); } + void slicing::explain_value(pvar v, std::function const& on_lit, std::function const& on_var) { + SASSERT(m_solver.m_justification[v].is_propagation_by_slicing()); + SASSERT(invariant()); + SASSERT(m_marked_lits.empty()); + + enode* sv = var2slice(v); + enode* rv = sv->get_root(); + SASSERT(is_value(rv)); // by convention, value slices are always the root; and this method may only be called if v is equivalent to a value in the egraph. + + SASSERT(m_tmp_deps.empty()); + explain_equal(sv, rv, m_tmp_deps); + + for (void* dp : m_tmp_deps) { + dep_t const d = dep_t::decode(dp); + if (d.is_null()) + continue; + if (d.is_lit()) + on_lit(d.lit()); + else { + SASSERT(d.is_value()); + if (get_dep_lit(d) == sat::null_literal) + on_var(get_dep_var(d)); + else + on_lit(get_dep_lit(d)); + } + } + m_tmp_deps.reset(); + } + bool slicing::find_range_in_ancestor(enode* s, enode* a, unsigned& out_hi, unsigned& out_lo) { out_hi = width(s) - 1; out_lo = 0; @@ -747,10 +776,12 @@ namespace polysat { pvar const v = slice2var(n); if (v == null_var) continue; + if (m_solver.is_assigned(v)) + continue; LOG("on_merge: v" << v << " := " << get_value(root)); - // TODO: notify solver about value + m_solver.assign_propagate_by_slicing(v, get_value(root)); // TODO: congruence? what if all base slices of a variable are equivalent to values? - // -> could track, for each slice, how many of its base slices are (not) equivalent to values. (update on split and merge) + // -> could track, for each variable, how many of its base slices are (not) equivalent to values. (update on split and merge) } } } diff --git a/src/math/polysat/slicing.h b/src/math/polysat/slicing.h index 9e8d641f0..17c3aa37f 100644 --- a/src/math/polysat/slicing.h +++ b/src/math/polysat/slicing.h @@ -313,6 +313,9 @@ namespace polysat { /** Extract conflict clause */ clause_ref build_conflict_clause(); + /** Explain why slicing has propagated the value assignment for v */ + void explain_value(pvar v, std::function const& on_lit, std::function const& on_var); + /** For a given variable v, find the set of variables w such that w = v[|w|:0]. */ void collect_simple_overlaps(pvar v, pvar_vector& out); diff --git a/src/math/polysat/solver.cpp b/src/math/polysat/solver.cpp index 2319db247..b373e733a 100644 --- a/src/math/polysat/solver.cpp +++ b/src/math/polysat/solver.cpp @@ -863,7 +863,7 @@ namespace polysat { // The fallback solver currently does not detect propagations, because we would need to handle justifications differently. // However, this case may still occur if during viable::intersect, we run into the refinement budget, // but here, we continue refinement and actually succeed until propagation. - assign_propagate(v, val); + assign_propagate_by_viable(v, val); return; case find_t::multiple: j = justification::decision(m_level + 1); @@ -882,11 +882,7 @@ namespace polysat { assign_core(v, val, j); } - void solver::assign_propagate(pvar v, rational const& val) { - LOG("Propagation: " << assignment_pp(*this, v, val)); - SASSERT(!is_assigned(v)); - SASSERT(m_viable.is_viable(v, val)); - m_free_pvars.del_var_eh(v); + void solver::assign_propagate_by_viable(pvar v, rational const& val) { // NOTE: // The propagation v := val might depend on a lower level than the current level (m_level). // This can happen if the constraints that cause the propagation have been bool-propagated at an earlier level, @@ -901,14 +897,23 @@ namespace polysat { if (is_assigned(w)) // TODO: question of which variables are relevant. e.g., v1 > v0 implies v1 > 0 without dependency on v0. maybe add a lemma v1 > v0 --> v1 > 0 on the top level to reduce false variable dependencies? instead of handling such special cases separately everywhere. lvl = std::max(lvl, get_level(w)); } - // NOTE: we do not have to check the univariate solver here. - // Since we propagate, this means at most the single value 'val' is viable. - // If it is not actually viable, the propagation loop will find out and enter the conflict state. - // (However, if we do check here, we might find the conflict earlier. Might be worth a try.) - assign_core(v, val, justification::propagation(lvl)); + assign_propagate(v, val, justification::propagation_by_viable(lvl)); } - void solver::assign_core(pvar v, rational const& val, justification const& j) { + void solver::assign_propagate_by_slicing(pvar v, rational const& val) { + unsigned lvl = m_level; // TODO: can the actual level be lower? + assign_propagate(v, val, justification::propagation_by_slicing(lvl)); + } + + void solver::assign_propagate(pvar v, rational const& val, justification j) { + LOG("Propagation: " << assignment_pp(*this, v, val)); + SASSERT(!is_assigned(v)); + SASSERT(j.is_propagation_by_viable() || j.is_propagation_by_slicing()); + m_free_pvars.del_var_eh(v); + assign_core(v, val, j); + } + + void solver::assign_core(pvar v, rational const& val, justification j) { VERIFY(!is_assigned(v)); if (j.is_decision()) ++m_stats.m_num_decisions; @@ -916,7 +921,7 @@ namespace polysat { ++m_stats.m_num_propagations; LOG(assignment_pp(*this, v, val) << " by " << j); SASSERT(m_viable.is_viable(v, val)); - SASSERT(j.is_decision() || j.is_propagation()); + SASSERT(j.is_decision() || j.is_propagation_by_viable() || j.is_propagation_by_slicing()); SASSERT(j.level() <= m_level); SASSERT(!is_assigned(v)); SASSERT(all_of(get_assignment(), [v](auto p) { return p.first != v; })); @@ -956,8 +961,13 @@ namespace polysat { revert_decision(v); return; } - SASSERT(j.is_propagation()); - m_conflict.resolve_value(v); + if (j.is_propagation_by_viable()) + m_conflict.resolve_value_by_viable(v); + else if (j.is_propagation_by_slicing()) + m_conflict.resolve_value_by_slicing(v); + else { + UNREACHABLE(); + } } else { // Resolve over boolean literal @@ -1102,6 +1112,7 @@ namespace polysat { appraise_lemma(lemmas.back()); } if (!best_lemma) { + verbose_stream() << "ERROR: no best_lemma\n"; display(verbose_stream()); verbose_stream() << "conflict: " << m_conflict << "\n"; verbose_stream() << "no lemma\n"; @@ -1110,7 +1121,6 @@ namespace polysat { for (sat::literal lit : *cl) verbose_stream() << " " << lit_pp(*this, lit) << "\n"; } - } SASSERT(best_score < lemma_score::max()); VERIFY(best_lemma); @@ -1581,9 +1591,11 @@ namespace polysat { pvar v = item.var(); auto const& j = m_justification[v]; out << "\t" << assignment_pp(*this, v, get_value(v)) << " @" << j.level() << " "; - if (j.is_propagation()) + if (j.is_propagation_by_viable()) for (auto const& c : m_viable.get_constraints(v)) out << c << " "; + if (j.is_propagation_by_slicing()) + out << "by slicing (detailed output is TODO)"; out << "\n"; } else { diff --git a/src/math/polysat/solver.h b/src/math/polysat/solver.h index 530168cae..6c623957c 100644 --- a/src/math/polysat/solver.h +++ b/src/math/polysat/solver.h @@ -262,8 +262,10 @@ namespace polysat { void activate_constraint(signed_constraint c); unsigned level(sat::literal lit, clause const& cl); - void assign_propagate(pvar v, rational const& val); - void assign_core(pvar v, rational const& val, justification const& j); + void assign_propagate_by_viable(pvar v, rational const& val); + void assign_propagate_by_slicing(pvar v, rational const& val); + void assign_propagate(pvar v, rational const& val, justification j); + void assign_core(pvar v, rational const& val, justification j); bool is_assigned(pvar v) const { return !m_justification[v].is_unassigned(); } bool is_decision(pvar v) const { return m_justification[v].is_decision(); } diff --git a/src/math/polysat/types.h b/src/math/polysat/types.h index 756565070..a19db8cb8 100644 --- a/src/math/polysat/types.h +++ b/src/math/polysat/types.h @@ -67,8 +67,12 @@ namespace polysat { inline bool operator!=(dependency const& d1, dependency const& d2) { return d1.val() != d2.val(); } inline std::ostream& operator<<(std::ostream& out, dependency const& d) { - out << "dep(" << d.val() << ")"; - return out; + out << "dep("; + if (d.is_null()) + out << ""; + else + out << d.val(); + return out << ")"; } } diff --git a/src/math/polysat/viable.cpp b/src/math/polysat/viable.cpp index 6ed1cdca2..164357f60 100644 --- a/src/math/polysat/viable.cpp +++ b/src/math/polysat/viable.cpp @@ -227,7 +227,7 @@ namespace polysat { s.try_assign_eval(s.eq(i.lo(), i.lo_val())); s.try_assign_eval(s.eq(i.hi(), i.hi_val())); } - s.assign_propagate(v, val); + s.assign_propagate_by_viable(v, val); } bool viable::intersect(pvar v, signed_constraint const& c) {