From 833366443313376858d424520ea0a54b83eb7241 Mon Sep 17 00:00:00 2001 From: Jakob Rath Date: Fri, 7 Oct 2022 16:19:41 +0200 Subject: [PATCH] Simplify handling of side lemmas in conflict --- src/math/polysat/conflict.cpp | 40 ++++++++++++++++------ src/math/polysat/conflict.h | 25 +++++++++----- src/math/polysat/explain.cpp | 48 ++++++--------------------- src/math/polysat/inference_logger.cpp | 11 ++++-- src/math/polysat/solver.cpp | 23 +++++++++++++ src/math/polysat/solver.h | 1 + 6 files changed, 90 insertions(+), 58 deletions(-) diff --git a/src/math/polysat/conflict.cpp b/src/math/polysat/conflict.cpp index b9ca97169..af045faec 100644 --- a/src/math/polysat/conflict.cpp +++ b/src/math/polysat/conflict.cpp @@ -321,6 +321,21 @@ namespace polysat { m_vars.insert(v); } + void conflict::add_lemma(signed_constraint const* cs, unsigned cs_len) { + clause_builder cb(s); + for (unsigned i = 0; i < cs_len; ++i) + cb.push(cs[i]); + clause_ref lemma = cb.build(); + SASSERT(lemma); + lemma->set_redundant(true); + m_lemmas.push_back(std::move(lemma)); + } + + void conflict::add_lemma(std::initializer_list cs) { + add_lemma(std::data(cs), cs.size()); + } + +#if 0 void conflict::bool_propagate(signed_constraint c, signed_constraint const* premises, unsigned premises_len) { if (c.is_always_false()) { VERIFY(false); // TODO: this case can probably happen, but needs special attention @@ -347,6 +362,7 @@ namespace polysat { void conflict::bool_propagate(signed_constraint c, std::initializer_list premises) { bool_propagate(c, std::data(premises), premises.size()); } +#endif void conflict::remove(signed_constraint c) { SASSERT(contains(c)); @@ -365,14 +381,7 @@ namespace polysat { m_kind = conflict_kind_t::ok; } - void conflict::insert(signed_constraint c, clause_ref lemma) { - unsigned const idx = c.blit().to_uint(); - SASSERT(!contains(c)); // not required, but this case should be checked - SASSERT(!m_lemmas.contains(idx)); // not required, but this case should be checked - insert(c); - m_lemmas.insert(idx, lemma); - } - +#if 0 clause* conflict::side_lemma(sat::literal lit) const { unsigned const idx = lit.to_uint(); return m_lemmas.get(idx, {}).get(); @@ -383,6 +392,7 @@ namespace polysat { unsigned const idx = lit.to_uint(); m_lemmas.insert(idx, std::move(lemma)); } +#endif void conflict::resolve_bool(sat::literal lit, clause const& cl) { // Note: core: x, y, z; corresponds to clause ~x \/ ~y \/ ~z @@ -503,11 +513,19 @@ namespace polysat { logger().log_lemma(lemma); logger().end_conflict(); - learn_side_lemmas(); - return lemma.build(); } + clause_ref_vector conflict::take_side_lemmas() { +#ifndef NDEBUG + on_scope_exit check_empty([this]() { + SASSERT(m_lemmas.empty()); + }); +#endif + return std::move(m_lemmas); + } + +#if 0 void conflict::learn_side_lemmas() { auto needs_side_lemma = [this](sat::literal lit) -> bool { return s.m_bvars.value(lit) == l_undef && side_lemma(lit); @@ -529,9 +547,11 @@ namespace polysat { todo.push_back(lit2); // Store and bool-propagate the lemma s.m_constraints.store(lemma, s, false); + SASSERT(s.m_bvars.value(lit) != l_undef); } m_lemmas.reset(); } +#endif bool conflict::minimize_vars(signed_constraint c) { if (m_vars.empty()) diff --git a/src/math/polysat/conflict.h b/src/math/polysat/conflict.h index fc5fa06f4..d0d9786d1 100644 --- a/src/math/polysat/conflict.h +++ b/src/math/polysat/conflict.h @@ -109,7 +109,7 @@ namespace polysat { unsigned_vector m_var_occurrences; // for each variable, the number of constraints in m_literals that contain it // Additional lemmas that justify new constraints generated during conflict resolution - u_map m_lemmas; + clause_ref_vector m_lemmas; conflict_kind_t m_kind = conflict_kind_t::ok; @@ -119,11 +119,10 @@ namespace polysat { void set_impl(signed_constraint c); bool minimize_vars(signed_constraint c); +#if 0 void set_side_lemma(signed_constraint c, clause_ref lemma) { SASSERT(c); set_side_lemma(c.blit(), std::move(lemma)); } void set_side_lemma(sat::literal lit, clause_ref lemma); - - /** Store relevant side lemmas */ - void learn_side_lemmas(); +#endif public: conflict(solver& s); @@ -174,8 +173,10 @@ namespace polysat { bool contains_pvar(pvar v) const { return m_vars.contains(v) || m_bail_vars.contains(v); } bool pvar_occurs_in_constraints(pvar v) const { return v < m_var_occurrences.size() && m_var_occurrences[v] > 0; } +#if 0 clause* side_lemma(signed_constraint c) const { SASSERT(c); return side_lemma(c.blit()); } clause* side_lemma(sat::literal lit) const; +#endif /** * Insert constraint c into conflict state. @@ -185,17 +186,17 @@ namespace polysat { */ void insert(signed_constraint c); - /** - * Insert constraint c that is justified by the given lemma. - */ - void insert(signed_constraint c, clause_ref lemma); - /** Insert assigned variables of c */ void insert_vars(signed_constraint c); /** Evaluate constraint under assignment and insert it into conflict state. */ void insert_eval(signed_constraint c); + /** Add a side lemma to the conflict; to be learned in addition to the main lemma after conflict resolution finishes. */ + void add_lemma(std::initializer_list cs); + void add_lemma(signed_constraint const* cs, unsigned cs_len); + +#if 0 /** * Derive new constraint c by bool-propagation from premises c1, ..., cn; * as if c was unit-propagated by the lemma c1 /\ ... /\ cn ==> c. @@ -203,6 +204,7 @@ namespace polysat { */ void bool_propagate(signed_constraint c, signed_constraint const* premises, unsigned premises_len); void bool_propagate(signed_constraint c, std::initializer_list premises); +#endif /** Remove c from core */ void remove(signed_constraint c); @@ -226,6 +228,11 @@ namespace polysat { /** Convert the core into a lemma to be learned. */ clause_ref build_lemma(); + /** Move the accumulated side lemmas out of the conflict */ + clause_ref_vector take_side_lemmas(); + + clause_ref_vector const& side_lemmas() const { return m_lemmas; } + std::ostream& display(std::ostream& out) const; }; diff --git a/src/math/polysat/explain.cpp b/src/math/polysat/explain.cpp index 5a31be587..136e45c81 100644 --- a/src/math/polysat/explain.cpp +++ b/src/math/polysat/explain.cpp @@ -15,24 +15,9 @@ Author: #include "math/polysat/log.h" #include "math/polysat/solver.h" -namespace polysat { +// TODO: rename file -/* - struct post_propagate2 : public inference { - const char* name; - signed_constraint conclusion; - signed_constraint premise1; - signed_constraint premise2; - post_propagate2(const char* name, signed_constraint conclusion, signed_constraint premise1, signed_constraint premise2) - : name(name), conclusion(conclusion), premise1(premise1), premise2(premise2) {} - std::ostream& display(std::ostream& out) const override { - return out << "Post-propagate (by " << name << "), " - << "conclusion " << conclusion.blit() << ": " << conclusion - << " from " << premise1.blit() << ": " << premise1 - << " and " << premise2.blit() << ": " << premise2; - } - }; -*/ +namespace polysat { struct inference_sup : public inference { const char* name; @@ -76,33 +61,22 @@ namespace polysat { // c2 ... constraint that is currently false // Try to replace it with a new false constraint (derived from superposition with a true constraint) lbool ex_polynomial_superposition::find_replacement(signed_constraint c2, pvar v, conflict& core) { - vector premises; - -#if 0 - for (auto si : s.m_search) { - if (!si.is_boolean()) - continue; - if (si.is_resolved()) - continue; - auto c1 = s.lit2cnstr(si.lit()); - if (!c1->contains_var(v)) - continue; - if (!c1.is_eq()) - continue; - if (!c1.is_currently_true(s)) - continue; -#else for (auto c1 : s.m_viable.get_constraints(v)) { if (!c1->contains_var(v)) // side conditions do not contain v; skip them here continue; if (!c1.is_eq()) continue; SASSERT(c1.is_currently_true(s)); -#endif + SASSERT(c2.is_currently_false(s)); + SASSERT_EQ(c1.bvalue(s), l_true); + SASSERT_EQ(c2.bvalue(s), l_true); + signed_constraint c = resolve1(v, c1, c2); if (!c) continue; + SASSERT(c.is_currently_false(s)); + // TODO: move this case distinction into conflict::add_lemma? char const* inf_name = "?"; switch (c.bvalue(s)) { case l_false: @@ -117,12 +91,12 @@ namespace polysat { inf_name = "l_undef"; // c evaluates to false, // c should be unit-propagated to l_true by c1 /\ c2 ==> c - core.bool_propagate(c, {c1, c2}); - // TODO: log inference? + core.add_lemma({c, ~c1, ~c2}); + core.log_inference(inference_sup("l_undef lemma", v, c2, c1)); SASSERT_EQ(l_true, c.bvalue(s)); - SASSERT(c.is_currently_false(s)); break; case l_true: + // c is just another constraint on the search stack; could be equivalent or better inf_name = "l_true"; break; default: diff --git a/src/math/polysat/inference_logger.cpp b/src/math/polysat/inference_logger.cpp index d3bfba069..c7b6affb7 100644 --- a/src/math/polysat/inference_logger.cpp +++ b/src/math/polysat/inference_logger.cpp @@ -60,9 +60,11 @@ namespace polysat { for (auto const& c : core) { sat::literal const lit = c.blit(); out_indent() << lit << ": " << c << '\n'; +#if 0 clause* lemma = core.side_lemma(lit); if (lemma) out_indent() << " justified by: " << lemma << '\n'; +#endif m_used_constraints.insert(lit.index()); for (pvar v : c->vars()) m_used_vars.insert(v); @@ -88,6 +90,11 @@ namespace polysat { out_indent() << "(backjump)\n"; break; } + for (clause* lemma : core.side_lemmas()) { + out_indent() << "Side lemma: " << *lemma << "\n"; + for (sat::literal lit : *lemma) + out_indent() << " " << lit_pp(s, lit) << "\n"; + } out().flush(); } @@ -103,10 +110,10 @@ namespace polysat { void file_inference_logger::log_lemma(clause_builder const& cb) { out() << hline() << "\nLemma:"; - for (auto const& lit : cb) + for (sat::literal lit : cb) out() << " " << lit; out() << "\n"; - for (auto const& lit : cb) + for (sat::literal lit : cb) out_indent() << lit_pp(s, lit) << "\n"; out().flush(); } diff --git a/src/math/polysat/solver.cpp b/src/math/polysat/solver.cpp index afbd0234a..3ba1d6dc7 100644 --- a/src/math/polysat/solver.cpp +++ b/src/math/polysat/solver.cpp @@ -801,9 +801,12 @@ namespace polysat { // LOG("max_level: " << max_level); // LOG("jump_level: " << jump_level); + backjump_and_learn(jump_level, *lemma); + /* m_conflict.reset(); backjump(jump_level); learn_lemma(*lemma); + */ } /** @@ -898,9 +901,16 @@ namespace polysat { return; } + unsigned jump_level = get_level(v) - 1; + backjump_and_learn(jump_level, *lemma); + /* + clause_ref_vector side_lemmas = m_conflict.take_side_lemmas(); m_conflict.reset(); backjump(get_level(v) - 1); + for (auto cl : side_lemmas) + add_clause(*cl); learn_lemma(*lemma); + */ } void solver::revert_bool_decision(sat::literal const lit) { @@ -917,9 +927,13 @@ namespace polysat { SASSERT(all_of(lemma, [this](sat::literal lit1) { return m_bvars.is_false(lit1); })); SASSERT(all_of(lemma, [this, var](sat::literal lit1) { return var == lit1.var() || m_bvars.level(lit1) < m_bvars.level(var); })); + unsigned jump_level = m_bvars.level(var) - 1; + backjump_and_learn(jump_level, lemma); + /* m_conflict.reset(); backjump(m_bvars.level(var) - 1); learn_lemma(lemma); + */ // At this point, the lemma is asserting for ~lit, // and has been propagated by learn_lemma/add_clause. SASSERT(all_of(lemma, [this](sat::literal lit1) { return m_bvars.is_assigned(lit1); })); @@ -930,6 +944,15 @@ namespace polysat { SASSERT(can_bdecide()); } + void solver::backjump_and_learn(unsigned jump_level, clause& lemma) { + clause_ref_vector side_lemmas = m_conflict.take_side_lemmas(); + m_conflict.reset(); + backjump(jump_level); + for (auto cl : side_lemmas) + add_clause(*cl); + learn_lemma(lemma); + } + bool solver::lemma_invariant(clause const* lemma) { SASSERT(lemma); LOG("Lemma: " << *lemma); diff --git a/src/math/polysat/solver.h b/src/math/polysat/solver.h index 3ddb95ccb..db271d942 100644 --- a/src/math/polysat/solver.h +++ b/src/math/polysat/solver.h @@ -212,6 +212,7 @@ namespace polysat { void backjump_lemma(); void revert_decision(pvar v); void revert_bool_decision(sat::literal lit); + void backjump_and_learn(unsigned jump_level, clause& lemma); // activity of variables based on standard VSIDS unsigned m_activity_inc = 128;