From 7d58296ad21fbe1ee9170bd341c4489ae5780ba8 Mon Sep 17 00:00:00 2001 From: Jakob Rath Date: Tue, 7 Sep 2021 11:40:50 +0200 Subject: [PATCH] Begin reorganizing resolve_value --- src/math/polysat/conflict_core.cpp | 24 +++++++++++++ src/math/polysat/conflict_core.h | 5 +++ src/math/polysat/explain.cpp | 54 ++++++++++++++++++++++++++++++ src/math/polysat/explain.h | 26 +++++++++++++- src/math/polysat/solver.cpp | 28 +++------------- src/math/polysat/solver.h | 1 + 6 files changed, 113 insertions(+), 25 deletions(-) diff --git a/src/math/polysat/conflict_core.cpp b/src/math/polysat/conflict_core.cpp index 5173bb1d4..7ef2b87d1 100644 --- a/src/math/polysat/conflict_core.cpp +++ b/src/math/polysat/conflict_core.cpp @@ -165,6 +165,30 @@ namespace polysat { return clause::from_literals(lvl, std::move(dep), std::move(literals)); } + bool conflict_core::resolve_value(pvar v, vector const& cjust_v) { + // TODO: maybe don't do this automatically, because cjust-constraints are true and core constraints are false. + // issue: what if viable(v) is empty? then we only have cjust constraints and none of them is evaluable (at least not immediately because no value is set for this variable.) + // => think about what we want to do in this case (choose a value and evaluate? try all possible superpositions without caring about the value of the premises?) + // the last value_resolution method can then be the one that adds the cjusts and calls saturation and more general VE. + + // No value resolution method was successful => fall back to saturation and variable elimination + for (auto c : cjust_v) + insert(c); + + // Variable elimination + while (true) { // TODO: limit? + // TODO: maybe we shouldn't try to split up VE/Saturation in the implementation. + // it might be better to just have more general "core inferences" that may combine elimination/saturation steps that fit together... + // or even keep the whole "value resolution + VE/Saturation" as a single step. we might want to know which constraints come from the current cjusts? + // TODO: as a last resort, substitute v by m_value[v]? + if (!try_saturate(v)) + break; + if (try_eliminate(v)) + return true; + } + return false; + } + bool conflict_core::try_eliminate(pvar v) { // TODO: could be tracked incrementally when constraints are added/removed vector v_constraints; diff --git a/src/math/polysat/conflict_core.h b/src/math/polysat/conflict_core.h index 77af2c134..1c25b0d70 100644 --- a/src/math/polysat/conflict_core.h +++ b/src/math/polysat/conflict_core.h @@ -82,6 +82,11 @@ namespace polysat { */ void resolve(constraint_manager const& m, sat::bool_var var, clause const& cl); + /** Perform value resolution by applying various inference rules. + * Returns true if it was possible to eliminate the variable 'v'. + */ + bool resolve_value(pvar v, vector const& cjust_v); + /** Convert the core into a lemma to be learned. */ clause_ref build_lemma(); diff --git a/src/math/polysat/explain.cpp b/src/math/polysat/explain.cpp index 4dfe283b9..a035ffcd4 100644 --- a/src/math/polysat/explain.cpp +++ b/src/math/polysat/explain.cpp @@ -17,6 +17,60 @@ Author: namespace polysat { + constraint_manager& explainer::cm() { return s().m_constraints; } + + bool ex_polynomial_superposition::try_explain(pvar v, vector const& cjust_v, conflict_core& core) { + // TODO: check superposition into disequality again (see notes) + + // TODO: use indexing/marking for this instead of allocating a temporary vector + // TODO: core saturation premises are from \Gamma (i.e., has_bvar)... but here we further restrict to the core; might need to revise + // -- especially: should take into account results from previous saturations (they will be in \Gamma, but only if we use the constraint or one of its descendants for the lemma) + // actually: we want to take one from the current cjust (currently true) and one from the conflict (currently false) + vector candidates; + for (auto c : core) + if (c->has_bvar() && c.is_positive() && c->is_eq() && c->contains_var(v)) + candidates.push_back(c); + + // TODO: c1 should a currently true constraint, while c2 should take a currently false constraint. + // remove candidates vector (premature optimization) + // we may want to apply this multiple times (a single resolve might not eliminate the variable). + + LOG_H3("Trying polynomial superposition..."); + for (auto it1 = candidates.begin(); it1 != candidates.end(); ++it1) { + for (auto it2 = it1 + 1; it2 != candidates.end(); ++it2) { + signed_constraint c1 = *it1; + signed_constraint c2 = *it2; + SASSERT(c1 != c2); + LOG("c1: " << c1); + LOG("c2: " << c2); + + pdd a = c1->to_eq().p(); + pdd b = c2->to_eq().p(); + pdd r = a; + if (!a.resolve(v, b, r) && !b.resolve(v, a, r)) + continue; + unsigned const lvl = std::max(c1->level(), c2->level()); + signed_constraint c = cm().eq(lvl, r); + LOG("resolved: " << c << " currently false? " << c.is_currently_false(s())); + if (!c.is_currently_false(s())) + continue; + vector premises; + premises.push_back(c1); + premises.push_back(c2); + core.insert(c, std::move(premises)); + return true; + +// clause_builder clause(m_solver); +// clause.push_literal(~c1->blit()); +// clause.push_literal(~c2->blit()); +// clause.push_new_constraint(m_solver.m_constraints.eq(lvl, r)); +// return clause.build(); + } + } + + return false; + } + // LOG_H3("Attempting to explain conflict for v" << v); // m_var = v; // m_cjust_v = cjust; diff --git a/src/math/polysat/explain.h b/src/math/polysat/explain.h index 97e34b38c..07bfc22b9 100644 --- a/src/math/polysat/explain.h +++ b/src/math/polysat/explain.h @@ -19,6 +19,30 @@ Author: namespace polysat { + class solver; + class constraint_manager; + + class explainer { + friend class conflict_core; + solver* m_solver = nullptr; + void set_solver(solver& s) { m_solver = &s; } + protected: + solver& s() { return *m_solver; } + constraint_manager& cm(); + public: + virtual ~explainer() {} + virtual bool try_explain(pvar v, vector const& cjust_v, conflict_core& core) = 0; + }; + + class ex_polynomial_superposition : public explainer { + bool try_explain(pvar v, vector const& cjust_v, conflict_core& core) override; + }; + + + + + + #if 0 class conflict_explainer { @@ -45,7 +69,7 @@ namespace polysat { bool saturate(); /** resolve conflict state against assignment to v */ - void resolve(pvar v, ptr_vector const& cjust_v); // TODO: try variable elimination of 'v', if not possible, core saturation and core reduction. (actually reduction could be one specific VE method). + void resolve(pvar v, ptr_vector const& cjust_v); void resolve(sat::literal lit); // TODO: move conflict resolution from solver into this class. diff --git a/src/math/polysat/solver.cpp b/src/math/polysat/solver.cpp index bac2a1f5c..549e7bdc6 100644 --- a/src/math/polysat/solver.cpp +++ b/src/math/polysat/solver.cpp @@ -526,31 +526,11 @@ namespace polysat { } // Value Resolution - // TODO: maybe don't do this automatically, because cjust-constraints are true and core constraints are false. - // issue: what if viable(v) is empty? then we only have cjust constraints and none of them is evaluable (at least not immediately because no value is set for this variable.) - // => think about what we want to do in this case (choose a value and evaluate? try all possible superpositions without caring about the value of the premises?) - // the last value_resolution method can then be the one that adds the cjusts and calls saturation and more general VE. - for (auto c : m_cjust[v]) - m_conflict.insert(c); - - // Variable elimination - while (true) { - // TODO: - // 1. Try variable elimination of 'v' - // 2. If not possible, try saturation and core reduction (actually reduction could be one specific VE method?). - // 3. as a last resort, substitute v by m_value[v]? - // TODO: maybe we shouldn't try to split up VE/Saturation in the implementation. - // it might be better to just have more general "core inferences" that may combine elimination/saturation steps that fit together... - // or even keep the whole "value resolution + VE/Saturation" as a single step. we might want to know which constraints come from the current cjusts? - if (m_conflict.try_eliminate(v)) - return; - if (!m_conflict.try_saturate(v)) - break; + if (!m_conflict.resolve_value(v, m_cjust[v])) { + // Failed to resolve => bail out + ++m_stats.m_num_bailouts; + m_conflict.set_bailout(); } - - // Failed to resolve => bail out - ++m_stats.m_num_bailouts; - m_conflict.set_bailout(); } /** Conflict resolution case where boolean literal 'lit' is on top of the stack */ diff --git a/src/math/polysat/solver.h b/src/math/polysat/solver.h index 04555e630..1d66cfdb1 100644 --- a/src/math/polysat/solver.h +++ b/src/math/polysat/solver.h @@ -56,6 +56,7 @@ namespace polysat { friend class clause_builder; friend class conflict_core; friend class conflict_explainer; + friend class explainer; friend class inference_engine; friend class forbidden_intervals; friend class linear_solver;