From 3e1cfcd538352cc85bd24d3aa2ebf0b1e6cc6262 Mon Sep 17 00:00:00 2001 From: Jakob Rath Date: Thu, 17 Jun 2021 17:35:32 +0200 Subject: [PATCH] Polysat: conflict explanation prototype (#5353) * display constraint's extra info in one place * Add stub for conflict explainer * Add helper functions to check whether constraint is active at base level * Add helper class tmp_assign * Add clause_builder; it skips unnecessary literals during clause creation * some fixes * Use clause_builder for forbidden intervals * remove old comments * fixes/comments in solver * print redundant clauses * First pass at conflict_explainer * remove unused model class * Choose value for k * also print min/max k --- src/math/polysat/CMakeLists.txt | 1 + src/math/polysat/constraint.cpp | 40 ++++- src/math/polysat/constraint.h | 72 ++++++++- src/math/polysat/eq_constraint.cpp | 6 +- src/math/polysat/explain.cpp | 186 +++++++++++++++++++++++ src/math/polysat/explain.h | 43 ++++++ src/math/polysat/forbidden_intervals.cpp | 36 ++--- src/math/polysat/solver.cpp | 108 +++++++++---- src/math/polysat/solver.h | 8 + src/math/polysat/ule_constraint.cpp | 6 +- src/math/polysat/var_constraint.cpp | 3 +- 11 files changed, 449 insertions(+), 60 deletions(-) create mode 100644 src/math/polysat/explain.cpp create mode 100644 src/math/polysat/explain.h diff --git a/src/math/polysat/CMakeLists.txt b/src/math/polysat/CMakeLists.txt index abff51f65..f2d774ecc 100644 --- a/src/math/polysat/CMakeLists.txt +++ b/src/math/polysat/CMakeLists.txt @@ -3,6 +3,7 @@ z3_add_component(polysat boolean.cpp constraint.cpp eq_constraint.cpp + explain.cpp forbidden_intervals.cpp justification.cpp linear_solver.cpp diff --git a/src/math/polysat/constraint.cpp b/src/math/polysat/constraint.cpp index 9ec8ca6bc..83a252953 100644 --- a/src/math/polysat/constraint.cpp +++ b/src/math/polysat/constraint.cpp @@ -154,6 +154,13 @@ namespace polysat { return ult(lvl, sign, a + shift, b + shift, d); } + std::ostream& constraint::display_extra(std::ostream& out) const { + out << " @" << level() << " (b" << bvar() << ")"; + if (is_undef()) + out << " [inactive]"; + return out; + } + bool constraint::propagate(solver& s, pvar v) { LOG_H3("Propagate " << s.m_vars[v] << " in " << *this); SASSERT(!vars().empty()); @@ -194,12 +201,13 @@ namespace polysat { } clause_ref clause::from_literals(unsigned lvl, p_dependency_ref const& d, sat::literal_vector literals, constraint_ref_vector constraints) { - return alloc(clause, lvl, d, literals, constraints); + return alloc(clause, lvl, d, std::move(literals), std::move(constraints)); } bool clause::is_always_false(solver& s) const { return std::all_of(m_literals.begin(), m_literals.end(), [&s](sat::literal lit) { constraint *c = s.m_constraints.lookup(lit.var()); + tmp_assign _t(c, lit); return c->is_always_false(); }); } @@ -207,6 +215,7 @@ namespace polysat { bool clause::is_currently_false(solver& s) const { return std::all_of(m_literals.begin(), m_literals.end(), [&s](sat::literal lit) { constraint *c = s.m_constraints.lookup(lit.var()); + tmp_assign _t(c, lit); return c->is_currently_false(s); }); } @@ -247,6 +256,35 @@ namespace polysat { return out; } + void clause_builder::reset() { + m_literals.reset(); + m_new_constraints.reset(); + SASSERT(empty()); + } + + clause_ref clause_builder::build(unsigned lvl, p_dependency_ref const& d) { + clause_ref cl = clause::from_literals(lvl, d, std::move(m_literals), std::move(m_new_constraints)); + SASSERT(empty()); + return cl; + } + + void clause_builder::push_literal(sat::literal lit) { + if (m_solver.active_at_base_level(lit)) + return; + m_literals.push_back(lit); + } + + void clause_builder::push_new_constraint(constraint_ref c) { + SASSERT(c); + SASSERT(c->is_undef()); + sat::literal lit{c->bvar()}; + tmp_assign _t(c, lit); + if (c->is_always_false()) + return; + m_literals.push_back(lit); + m_new_constraints.push_back(std::move(c)); + } + std::ostream& constraints_and_clauses::display(std::ostream& out) const { bool first = true; for (auto c : units()) { diff --git a/src/math/polysat/constraint.h b/src/math/polysat/constraint.h index 18ab2da4d..0a315f50d 100644 --- a/src/math/polysat/constraint.h +++ b/src/math/polysat/constraint.h @@ -93,7 +93,7 @@ namespace polysat { unsigned m_ref_count = 0; // bool m_stored = false; ///< Whether it has been inserted into the constraint_manager to be tracked by level unsigned m_storage_level; ///< Controls lifetime of the constraint object. Always a base level (for external dependencies the level at which it was created, and for others the maximum storage level of its external dependencies). - unsigned m_active_level = UINT_MAX; ///< Level at which the constraint was activated. Possibly different from m_storage_level because constraints in lemmas may become activated only at a higher level. + // unsigned m_active_level = UINT_MAX; ///< Level at which the constraint was activated. Possibly different from m_storage_level because constraints in lemmas may become activated only at a higher level. NOTE: this is actually the level of the corresponding bool_var. ckind_t m_kind; p_dependency_ref m_dep; unsigned_vector m_vars; @@ -108,6 +108,9 @@ namespace polysat { m_manager->insert_bv2c(bvar(), this); } + protected: + std::ostream& display_extra(std::ostream& out) const; + public: void inc_ref() { m_ref_count++; } void dec_ref() { SASSERT(m_ref_count > 0); m_ref_count--; if (!m_ref_count) dealloc(this); } @@ -138,6 +141,13 @@ namespace polysat { unsigned_vector& vars() { return m_vars; } unsigned_vector const& vars() const { return m_vars; } unsigned level() const { return m_storage_level; } + // unsigned active_level() const { + // SASSERT(!is_undef()); + // return m_manager->m_bvars.level(bvar()); + // } + // unsigned active_at_base_level(solver& s) const { + // return !is_undef() && active_level() <= s.base_level(); + // } sat::bool_var bvar() const { return m_bvar; } sat::literal blit() const { SASSERT(m_bvalue != l_undef); return m_bvalue == l_true ? sat::literal(m_bvar) : ~sat::literal(m_bvar); } bool sign() const { return m_sign; } @@ -230,6 +240,33 @@ namespace polysat { inline std::ostream& operator<<(std::ostream& out, clause const& c) { return c.display(out); } + /// Builds a clause from literals and constraints. + /// Takes care to + /// - skip literals that are active at the base level, + /// - skip trivial new constraints such as "4 <= 1". + class clause_builder { + solver& m_solver; + sat::literal_vector m_literals; + constraint_ref_vector m_new_constraints; + + public: + clause_builder(solver& s): m_solver(s) {} + + bool empty() const { return m_literals.empty() && m_new_constraints.empty(); } + void reset(); + + /// Build the clause. This will reset the clause builder so it can be reused. + clause_ref build(unsigned lvl, p_dependency_ref const& d); + + /// Add a literal to the clause. + /// Intended to be used for literals representing a constraint that already exists. + void push_literal(sat::literal lit); + /// Add a constraint to the clause that does not yet exist in the solver so far. + /// By convention, this will add the positive literal for this constraint. + /// (TODO: we might need to change this later; but then we will add a second argument for the literal or the sign.) + void push_new_constraint(constraint_ref c); + }; + // Container for unit constraints and clauses. class constraints_and_clauses { constraint_ref_vector m_units; @@ -289,4 +326,37 @@ namespace polysat { inline std::ostream& operator<<(std::ostream& out, constraints_and_clauses const& c) { return c.display(out); } + + /// Temporarily assign a constraint according to the sign of the given literal. + class tmp_assign final { + constraint* m_constraint; + bool m_should_unassign = false; + public: + tmp_assign(constraint* c, sat::literal lit): + m_constraint(c) { + SASSERT(c); + SASSERT(c->bvar() == lit.var()); + if (c->is_undef()) { + c->assign(!lit.sign()); + m_should_unassign = true; + } + else + SASSERT(c->blit() == lit); + } + tmp_assign(constraint_ref const& c, sat::literal lit): tmp_assign(c.get(), lit) {} + void revert() { + if (m_should_unassign) { + m_constraint->unassign(); + m_should_unassign = false; + } + } + ~tmp_assign() { + revert(); + } + tmp_assign(tmp_assign&) = delete; + tmp_assign(tmp_assign&&) = delete; + tmp_assign& operator=(tmp_assign&) = delete; + tmp_assign& operator=(tmp_assign&&) = delete; + }; + } diff --git a/src/math/polysat/eq_constraint.cpp b/src/math/polysat/eq_constraint.cpp index d946d1262..661aa1c63 100644 --- a/src/math/polysat/eq_constraint.cpp +++ b/src/math/polysat/eq_constraint.cpp @@ -19,10 +19,8 @@ Author: namespace polysat { std::ostream& eq_constraint::display(std::ostream& out) const { - out << p() << (sign() == pos_t ? " == 0" : " != 0") << " @" << level() << " b" << bvar(); - if (is_undef()) - out << " [inactive]"; - return out; + out << p() << (sign() == pos_t ? " == 0" : " != 0"); + return display_extra(out); } constraint_ref eq_constraint::resolve(solver& s, pvar v) { diff --git a/src/math/polysat/explain.cpp b/src/math/polysat/explain.cpp new file mode 100644 index 000000000..01866fd5a --- /dev/null +++ b/src/math/polysat/explain.cpp @@ -0,0 +1,186 @@ +/*++ +Copyright (c) 2021 Microsoft Corporation + +Module Name: + + Conflict explanation / resolution + +Author: + + Nikolaj Bjorner (nbjorner) 2021-03-19 + Jakob Rath 2021-04-6 + +--*/ +#include "math/polysat/explain.h" +#include "math/polysat/log.h" + +namespace polysat { + + conflict_explainer::conflict_explainer(solver& s, constraints_and_clauses const& conflict): + m_solver(s), m_conflict(conflict) {} + + clause_ref conflict_explainer::resolve(pvar v, ptr_vector const& cjust) { + LOG_H3("Attempting to explain conflict for v" << v); + m_var = v; + m_cjust_v = cjust; + + for (auto* c : cjust) + m_conflict.push_back(c); + + // TODO: we should share work done for examining constraints between different resolution methods + clause_ref lemma; + if (!lemma) lemma = by_polynomial_superposition(); + if (!lemma) lemma = by_ugt_x(); + if (!lemma) lemma = by_ugt_y(); + if (!lemma) lemma = by_ugt_z(); + + if (lemma) { + LOG("New lemma: " << *lemma); + for (auto* c : lemma->new_constraints()) { + LOG("New constraint: " << show_deref(c)); + } + } + + m_var = null_var; + m_cjust_v.reset(); + return lemma; + } + + clause_ref conflict_explainer::by_polynomial_superposition() { + if (m_conflict.units().size() != 2 || m_conflict.clauses().size() > 0) + return nullptr; + constraint* c1 = m_conflict.units()[0]; + constraint* c2 = m_conflict.units()[1]; + if (c1 == c2) + return nullptr; + if (!c1->is_eq() || !c2->is_eq()) + return nullptr; + if (c1->is_positive() && c2->is_positive()) { + pdd a = c1->to_eq().p(); + pdd b = c2->to_eq().p(); + pdd r = a; + if (!a.resolve(m_var, b, r) && !b.resolve(m_var, a, r)) + return nullptr; + p_dependency_ref d(m_solver.m_dm.mk_join(c1->dep(), c2->dep()), m_solver.m_dm); + unsigned lvl = std::max(c1->level(), c2->level()); + constraint_ref c = m_solver.m_constraints.eq(lvl, pos_t, r, d); + c->assign(true); + return clause::from_unit(c); + } + return nullptr; + } + + /// [x] zx > yx ==> ... + clause_ref conflict_explainer::by_ugt_x() { + LOG_H3("Try zx > yx"); + for (auto* c : m_conflict.units()) + LOG("Constraint: " << show_deref(c)); + for (auto* c : m_conflict.clauses()) + LOG("Clause: " << show_deref(c)); + + // Find constraint of desired shape + for (auto* c : m_conflict.units()) { + if (!c->is_ule()) + continue; + pdd lhs = c->to_ule().lhs(); + pdd rhs = c->to_ule().rhs(); + if (lhs.degree(m_var) != 1) + continue; + if (rhs.degree(m_var) != 1) + continue; + pdd y = lhs; + pdd rest = lhs; + rhs.factor(m_var, 1, y, rest); + if (!rest.is_zero()) + continue; + pdd z = lhs; + lhs.factor(m_var, 1, z, rest); + if (!rest.is_zero()) + continue; + + if (c->is_positive()) { + // zx <= yx + NOT_IMPLEMENTED_YET(); + } + else { + SASSERT(c->is_negative()); + // zx > yx + + unsigned const lvl = c->level(); + + pdd x = m_solver.var(m_var); + unsigned const p = m_solver.size(m_var); + + clause_builder clause(m_solver); + // Omega^*(x, y) + push_omega_mul(clause, lvl, p, x, y); + // z > y + constraint_ref z_gt_y = m_solver.m_constraints.ult(lvl, pos_t, y, z, null_dep()); + LOG("z>y: " << show_deref(z_gt_y)); + clause.push_new_constraint(std::move(z_gt_y)); + + p_dependency_ref d(c->dep(), m_solver.m_dm); + return clause.build(lvl, d); + } + + } + return nullptr; + } + + /// [y] y >= z' /\ zx > yx ==> ... + clause_ref conflict_explainer::by_ugt_y() { + return nullptr; + } + + /// [z] y' >= z /\ zx > yx ==> ... + clause_ref conflict_explainer::by_ugt_z() { + return nullptr; + } + + /// Add Ω*(x, y) to the clause. + /// + /// @param[in] p bit width + void conflict_explainer::push_omega_mul(clause_builder& clause, unsigned level, unsigned p, pdd const& x, pdd const& y) { + LOG_H3("Omega^*(x, y)"); + LOG("x = " << x); + LOG("y = " << y); + auto& pddm = m_solver.sz2pdd(p); + unsigned min_k = 0; + unsigned max_k = p - 1; + unsigned k = p/2; + + rational x_val; + if (m_solver.try_eval(x, x_val)) { + unsigned x_bits = x_val.bitsize(); + LOG("eval x: " << x << " := " << x_val << " (x_bits: " << x_bits << ")"); + SASSERT(x_val < rational::power_of_two(x_bits)); + min_k = x_bits; + } + + rational y_val; + if (m_solver.try_eval(y, y_val)) { + unsigned y_bits = y_val.bitsize(); + LOG("eval y: " << y << " := " << y_val << " (y_bits: " << y_bits << ")"); + SASSERT(y_val < rational::power_of_two(y_bits)); + max_k = p - y_bits; + } + + SASSERT(min_k <= max_k); // in this case, cannot choose k s.t. both literals are false + + // TODO: could also choose other value for k (but between the bounds) + if (min_k == 0) + k = max_k; + else + k = min_k; + + LOG("k = " << k << "; min_k = " << min_k << "; max_k = " << max_k << "; p = " << p); + SASSERT(min_k <= k && k <= max_k); + + // x >= 2^k + constraint_ref c1 = m_solver.m_constraints.ult(level, pos_t, pddm.mk_val(rational::power_of_two(k)), x, null_dep()); + // y > 2^{p-k} + constraint_ref c2 = m_solver.m_constraints.ule(level, pos_t, pddm.mk_val(rational::power_of_two(p-k)), y, null_dep()); + clause.push_new_constraint(std::move(c1)); + clause.push_new_constraint(std::move(c2)); + } +} diff --git a/src/math/polysat/explain.h b/src/math/polysat/explain.h new file mode 100644 index 000000000..d542c8759 --- /dev/null +++ b/src/math/polysat/explain.h @@ -0,0 +1,43 @@ +/*++ +Copyright (c) 2021 Microsoft Corporation + +Module Name: + + Conflict explanation / resolution + +Author: + + Nikolaj Bjorner (nbjorner) 2021-03-19 + Jakob Rath 2021-04-6 + +--*/ +#pragma once +#include "math/polysat/constraint.h" +#include "math/polysat/interval.h" +#include "math/polysat/solver.h" + +namespace polysat { + + // TODO: later, we probably want to update this class incrementally (adding/removing constraints as we go back through the trail) + // TODO: indexing of constraints/clauses? + class conflict_explainer { + solver& m_solver; + constraints_and_clauses m_conflict; + pvar m_var = null_var; + ptr_vector m_cjust_v; + + + clause_ref by_polynomial_superposition(); + + clause_ref by_ugt_x(); + clause_ref by_ugt_y(); + clause_ref by_ugt_z(); + + p_dependency_ref null_dep() const { return m_solver.mk_dep_ref(null_dependency); } + void push_omega_mul(clause_builder& clause, unsigned level, unsigned p, pdd const& x, pdd const& y); + public: + conflict_explainer(solver& s, constraints_and_clauses const& conflict); + + clause_ref resolve(pvar v, ptr_vector const& cjust_v); + }; +} diff --git a/src/math/polysat/forbidden_intervals.cpp b/src/math/polysat/forbidden_intervals.cpp index 38e672088..4efdc2980 100644 --- a/src/math/polysat/forbidden_intervals.cpp +++ b/src/math/polysat/forbidden_intervals.cpp @@ -99,21 +99,20 @@ namespace polysat { // => the side conditions of that interval are enough to produce a conflict auto& full_record = records.back(); SASSERT(full_record.interval.is_full()); - sat::literal_vector literals; - constraint_ref_vector new_constraints; - literals.push_back(~full_record.src->blit()); // TODO: only do this if it's not a base-level constraint! (from unit clauses, e.g., external constraints) - if (full_record.neg_cond) { - literals.push_back(sat::literal(full_record.neg_cond.get()->bvar())); - new_constraints.push_back(std::move(full_record.neg_cond)); - } + clause_builder clause(s); + clause.push_literal(~full_record.src->blit()); + if (full_record.neg_cond) + clause.push_new_constraint(std::move(full_record.neg_cond)); unsigned lemma_lvl = full_record.src->level(); p_dependency_ref lemma_dep(full_record.src->dep(), s.m_dm); - out_lemma = clause::from_literals(lemma_lvl, lemma_dep, std::move(literals), std::move(new_constraints)); + out_lemma = clause.build(lemma_lvl, lemma_dep); return true; } - if (records.empty()) + if (records.empty()) { + LOG("aborted (no intervals)"); return false; + } SASSERT(longest_i != UINT_MAX); LOG("longest: i=" << longest_i << "; " << records[longest_i].interval); @@ -123,6 +122,7 @@ namespace polysat { // Select a sequence of covering intervals unsigned_vector seq; if (!find_covering_sequence(records, longest_i, modulus, seq)) { + LOG("aborted (intervals do not cover domain)"); return false; } LOG("seq: " << seq); @@ -145,14 +145,11 @@ namespace polysat { // then the forbidden intervals cover the whole domain and we have a conflict. // We learn the negation of this conjunction. - sat::literal_vector literals; - constraint_ref_vector new_constraints; + clause_builder clause(s); // Add negation of src constraints as antecedents (may be resolved during backtracking) for (unsigned const i : seq) { - // TODO: don't add base-level constraints! (from unit clauses, e.g., external constraints) - // (maybe extract that into a helper function on 'clause'... it could sort out base-level and other constraints; add the first to lemma_dep and the other to antecedents) sat::literal src_lit = records[i].src->blit(); - literals.push_back(~src_lit); + clause.push_literal(~src_lit); } // Add side conditions and interval constraints for (unsigned seq_i = seq.size(); seq_i-- > 0; ) { @@ -167,17 +164,14 @@ namespace polysat { auto const& rhs = next_hi - next_lo; constraint_ref c = s.m_constraints.ult(lemma_lvl, neg_t, lhs, rhs, s.mk_dep_ref(null_dependency)); LOG("constraint: " << *c); - literals.push_back(sat::literal(c->bvar())); - new_constraints.push_back(std::move(c)); + clause.push_new_constraint(std::move(c)); // Side conditions // TODO: check whether the condition is subsumed by c? maybe at the end do a "lemma reduction" step, to try and reduce branching? constraint_ref& neg_cond = records[i].neg_cond; - if (neg_cond) { - literals.push_back(sat::literal(neg_cond->bvar())); - new_constraints.push_back(std::move(neg_cond)); - } + if (neg_cond) + clause.push_new_constraint(std::move(neg_cond)); } - out_lemma = clause::from_literals(lemma_lvl, lemma_dep, std::move(literals), std::move(new_constraints)); + out_lemma = clause.build(lemma_lvl, lemma_dep); return true; } diff --git a/src/math/polysat/solver.cpp b/src/math/polysat/solver.cpp index f5ab84e75..8203a0737 100644 --- a/src/math/polysat/solver.cpp +++ b/src/math/polysat/solver.cpp @@ -17,6 +17,7 @@ Author: --*/ #include "math/polysat/solver.h" +#include "math/polysat/explain.h" #include "math/polysat/log.h" #include "math/polysat/forbidden_intervals.h" @@ -550,6 +551,13 @@ namespace polysat { m_bvars.reset_marks(); set_marks(*lemma.get()); } + else { + // lemma = resolve(conflict_var); + conflict_explainer cx(*this, m_conflict); + lemma = cx.resolve(conflict_var, {}); + LOG("resolved: " << show_deref(lemma)); + // std::abort(); + } } for (unsigned i = m_search.size(); i-- > 0; ) { @@ -615,6 +623,8 @@ namespace polysat { SASSERT(m_bvars.is_propagation(var)); clause_ref new_lemma = resolve_bool(lit); SASSERT(new_lemma); + LOG("new_lemma: " << show_deref(new_lemma)); + LOG("new_lemma is always false: " << new_lemma->is_always_false(*this)); if (new_lemma->is_always_false(*this)) { // learn_lemma(v, new_lemma); m_conflict.reset(); @@ -622,10 +632,11 @@ namespace polysat { report_unsat(); return; } - if (!new_lemma->is_currently_false(*this)) { - backtrack(i, lemma); - return; - } + LOG("new_lemma is currently false: " << new_lemma->is_currently_false(*this)); + // if (!new_lemma->is_currently_false(*this)) { + // backtrack(i, lemma); + // return; + // } lemma = std::move(new_lemma); reset_marks(); m_bvars.reset_marks(); @@ -642,12 +653,26 @@ namespace polysat { return nullptr; if (m_conflict.clauses().size() != 1) return nullptr; + LOG_H3("resolve_bool"); clause* lemma = m_conflict.clauses()[0]; SASSERT(lemma); SASSERT(m_bvars.is_propagation(lit.var())); clause* other = m_bvars.reason(lit.var()); SASSERT(other); + LOG("lemma: " << show_deref(lemma)); + LOG("other: " << show_deref(other)); VERIFY(lemma->resolve(lit.var(), *other)); + LOG("resolved: " << show_deref(lemma)); + + // unassign constraints whose current value does not agree with their occurrence in the lemma + for (sat::literal lit : *lemma) { + constraint *c = m_constraints.lookup(lit.var()); + if (!c->is_undef() && c ->blit() != lit) { + LOG("unassigning: " << show_deref(c)); + c->unassign(); + } + } + return lemma; // currently modified in-place } @@ -764,17 +789,14 @@ namespace polysat { IF_LOGGING(log_viable()); LOG("Boolean assignment: " << m_bvars); + // To make a guess, we need to find an unassigned literal that is not false in the current model. auto is_suitable = [this](sat::literal lit) -> bool { if (m_bvars.value(lit) == l_false) // already assigned => cannot decide on this (comes from either lemma LHS or previously decided literals that are now changed to propagation) return false; SASSERT(m_bvars.value(lit) != l_true); // cannot happen in a valid lemma constraint* c = m_constraints.lookup(lit.var()); - c->assign(!lit.sign()); - bool result = true; - if (c->is_currently_false(*this)) - result = false; - c->unassign(); - return result; + tmp_assign _t(c, lit); + return !c->is_currently_false(*this); }; // constraint *choice = nullptr; @@ -782,19 +804,15 @@ namespace polysat { unsigned num_choices = 0; // TODO: should probably cache this? for (sat::literal lit : lemma) { - IF_LOGGING({ - auto value = m_bvars.value(lit); - auto c = m_constraints.lookup(lit.var()); - bool is_false; - if (value == l_undef) { - c->assign(!lit.sign()); - is_false = c->is_currently_false(*this); - c->unassign(); - } - else - is_false = c->is_currently_false(*this); - LOG_V("Checking: lit=" << lit << ", value=" << value << ", constraint=" << show_deref(c) << ", currently_false=" << is_false); - }); + // IF_LOGGING({ + // auto value = m_bvars.value(lit); + // auto c = m_constraints.lookup(lit.var()); + // bool is_false; + // LOG_V("Checking: lit=" << lit << ", value=" << value << ", constraint=" << show_deref(c)); + // tmp_assign _t(c, lit); + // is_false = c->is_currently_false(*this); + // LOG_V("Checking: lit=" << lit << ", value=" << value << ", constraint=" << show_deref(c) << ", currently_false=" << is_false); + // }); if (is_suitable(lit)) { num_choices++; if (choice == sat::null_literal) @@ -886,7 +904,9 @@ namespace polysat { // - Guess x = 0. // - We have a conflict but we don't know. It will be discovered when y and z are assigned, // and then may lead to an assertion failure through this call to narrow. - c->narrow(*this); + // TODO: what to do with "unassigned" constraints at this point? (we probably should have resolved those away, even in the 'backtrack' case.) + if (!c->is_undef()) // TODO: this check to be removed once this is fixed properly. + c->narrow(*this); if (is_conflict()) { LOG_H1("Conflict during revert_decision/narrow!"); return; @@ -1048,10 +1068,19 @@ namespace polysat { * Return residue of superposing p and q with respect to v. */ clause_ref solver::resolve(pvar v) { + LOG_H3("Resolve v" << v); SASSERT(!m_cjust[v].empty()); SASSERT(m_justification[v].is_propagation()); - LOG("resolve pvar " << v); - if (m_cjust[v].size() != 1) + LOG("Conflict: " << m_conflict); + LOG("cjust[v" << v << "]: " << m_cjust[v]); + + conflict_explainer cx(*this, m_conflict); + clause_ref res = cx.resolve(v, m_cjust[v]); + LOG("resolved: " << show_deref(res)); + // std::abort(); + return res; +/* + if (m_cjust[v].size() != 1) return nullptr; constraint* d = m_cjust[v].back(); constraint_ref res = d->resolve(*this, v); @@ -1062,6 +1091,7 @@ namespace polysat { } else return nullptr; +*/ } /** @@ -1085,7 +1115,10 @@ namespace polysat { if (!lemma) return; LOG("Lemma: " << show_deref(lemma)); - SASSERT(lemma->size() > 1); + // SASSERT(lemma->size() > 1); + if (lemma->size() < 2) { + LOG_H1("TODO: this should be treated as unit constraint and asserted at the base level!"); + } clause* cl = m_constraints.insert(lemma); m_redundant_clauses.push_back(cl); } @@ -1132,7 +1165,18 @@ namespace polysat { unsigned solver::base_level() const { return m_base_levels.empty() ? 0 : m_base_levels.back(); } - + + bool solver::active_at_base_level(sat::bool_var bvar) const { + return m_bvars.is_assigned(bvar) && m_bvars.level(bvar) <= base_level(); + } + + bool solver::try_eval(pdd const& p, rational& out_value) const { + pdd r = p.subst_val(assignment()); + if (r.is_val()) + out_value = r.val(); + return r.is_val(); + } + std::ostream& solver::display(std::ostream& out) const { for (auto p : assignment()) { auto v = p.first; @@ -1146,6 +1190,14 @@ namespace polysat { out << "Redundant:\n"; for (auto* c : m_redundant) out << "\t" << *c << "\n"; + out << "Redundant clauses:\n"; + for (auto* cl : m_redundant_clauses) { + out << "\t" << *cl << "\n"; + for (auto lit : *cl) { + auto c = m_constraints.lookup(lit.var()); + out << "\t\t" << lit.var() << ": " << *c << "\n"; + } + } return out; } diff --git a/src/math/polysat/solver.h b/src/math/polysat/solver.h index 3c505e1d2..11042f764 100644 --- a/src/math/polysat/solver.h +++ b/src/math/polysat/solver.h @@ -47,6 +47,8 @@ namespace polysat { friend class var_constraint; friend class ule_constraint; friend class clause; + friend class clause_builder; + friend class conflict_explainer; friend class forbidden_intervals; friend class linear_solver; @@ -244,9 +246,15 @@ namespace polysat { p_dependency* mk_dep(unsigned dep) { return dep == null_dependency ? nullptr : m_dm.mk_leaf(dep); } p_dependency_ref mk_dep_ref(unsigned dep) { return p_dependency_ref(mk_dep(dep), m_dm); } + /// Evaluate term under the current assignment. + bool try_eval(pdd const& p, rational& out_value) const; + bool is_conflict() const { return !m_conflict.empty(); } bool at_base_level() const; unsigned base_level() const; + bool active_at_base_level(sat::bool_var bvar) const; + bool active_at_base_level(sat::literal lit) const { return active_at_base_level(lit.var()); } + bool active_at_base_level(constraint& c) const { return active_at_base_level(c.bvar()); } void resolve_conflict(); void backtrack(unsigned i, clause_ref lemma); diff --git a/src/math/polysat/ule_constraint.cpp b/src/math/polysat/ule_constraint.cpp index c86fe496d..d73d73c57 100644 --- a/src/math/polysat/ule_constraint.cpp +++ b/src/math/polysat/ule_constraint.cpp @@ -19,10 +19,8 @@ Author: namespace polysat { std::ostream& ule_constraint::display(std::ostream& out) const { - out << m_lhs << (sign() == pos_t ? " <=u " : " >u ") << m_rhs << " @" << level() << " b" << bvar(); - if (is_undef()) - out << " [inactive]"; - return out; + out << m_lhs << (sign() == pos_t ? " <= " : " > ") << m_rhs; + return display_extra(out); } constraint_ref ule_constraint::resolve(solver& s, pvar v) { diff --git a/src/math/polysat/var_constraint.cpp b/src/math/polysat/var_constraint.cpp index 6f6b7d7c5..cfc5ff739 100644 --- a/src/math/polysat/var_constraint.cpp +++ b/src/math/polysat/var_constraint.cpp @@ -18,7 +18,8 @@ Author: namespace polysat { std::ostream& var_constraint::display(std::ostream& out) const { - return out << "v" << m_var << ": " << m_viable << "\n"; + out << "v" << m_var << ": " << m_viable << "\n"; + return display_extra(out); } constraint_ref var_constraint::resolve(solver& s, pvar v) {