From b43971bb4a7e8d4965b1d222bd65a22ab4ff52d9 Mon Sep 17 00:00:00 2001 From: Jakob Rath Date: Wed, 21 Sep 2022 12:12:57 +0200 Subject: [PATCH] Connect conflict2 --- src/math/polysat/CMakeLists.txt | 9 +- src/math/polysat/conflict.cpp | 205 +++++++++++++++++++++----- src/math/polysat/conflict.h | 104 +++++++++++-- src/math/polysat/inference_logger.cpp | 42 +++--- src/math/polysat/inference_logger.h | 34 +++-- src/math/polysat/solver.cpp | 124 ++++------------ src/math/polysat/solver.h | 20 +-- src/math/polysat/viable.cpp | 146 +++++++++--------- src/math/polysat/viable.h | 29 ++-- 9 files changed, 420 insertions(+), 293 deletions(-) diff --git a/src/math/polysat/CMakeLists.txt b/src/math/polysat/CMakeLists.txt index 8174eff59..0f184c7aa 100644 --- a/src/math/polysat/CMakeLists.txt +++ b/src/math/polysat/CMakeLists.txt @@ -4,10 +4,9 @@ z3_add_component(polysat clause.cpp clause_builder.cpp conflict.cpp - conflict2.cpp constraint.cpp - eq_explain.cpp - explain.cpp + # eq_explain.cpp + # explain.cpp forbidden_intervals.cpp inference_logger.cpp justification.cpp @@ -15,7 +14,7 @@ z3_add_component(polysat log.cpp op_constraint.cpp restart.cpp - saturation.cpp + # saturation.cpp search_state.cpp simplify.cpp simplify_clause.cpp @@ -23,7 +22,7 @@ z3_add_component(polysat solver.cpp ule_constraint.cpp umul_ovfl_constraint.cpp - variable_elimination.cpp + # variable_elimination.cpp viable.cpp COMPONENT_DEPENDENCIES util diff --git a/src/math/polysat/conflict.cpp b/src/math/polysat/conflict.cpp index f7a9acfff..bdecde349 100644 --- a/src/math/polysat/conflict.cpp +++ b/src/math/polysat/conflict.cpp @@ -14,7 +14,8 @@ Notes: --*/ -#include "math/polysat/conflict2.h" +#include "math/polysat/conflict.h" +#include "math/polysat/clause_builder.h" #include "math/polysat/solver.h" #include "math/polysat/inference_logger.h" #include "math/polysat/log.h" @@ -25,10 +26,17 @@ Notes: #include "math/polysat/saturation.h" #include "math/polysat/variable_elimination.h" #include -#include namespace polysat { + class header_with_var : public displayable { + char const* m_text; + pvar m_var; + public: + header_with_var(char const* text, pvar var) : m_text(text), m_var(var) { SASSERT(text); } + std::ostream& display(std::ostream& out) const override { return out << m_text << m_var; } + }; + struct inf_resolve_bool : public inference { sat::literal m_lit; clause const& m_clause; @@ -61,7 +69,7 @@ namespace polysat { } }; - conflict2::conflict2(solver& s) : s(s) { + conflict::conflict(solver& s) : s(s) { // TODO: m_log_conflicts is always false even if "polysat.log_conflicts=true" is given on the command line if (true || s.get_config().m_log_conflicts) m_logger = alloc(file_inference_logger, s); @@ -69,35 +77,73 @@ namespace polysat { m_logger = alloc(dummy_inference_logger); } - inference_logger& conflict2::logger() { + inference_logger& conflict::logger() { return *m_logger; } - bool conflict2::empty() const { - return m_literals.empty() && m_vars.empty() && m_lemmas.empty(); + conflict::const_iterator conflict::begin() const { + return conflict_iterator::begin(s.m_constraints, m_literals); } - void conflict2::reset() { + conflict::const_iterator conflict::end() const { + return conflict_iterator::end(s.m_constraints, m_literals); + } + + bool conflict::empty() const { + return m_literals.empty() + && m_vars.empty() + && m_bail_vars.empty() + && m_lemmas.empty(); + } + + void conflict::reset() { m_literals.reset(); m_vars.reset(); + m_bail_vars.reset(); + m_relevant_vars.reset(); m_var_occurrences.reset(); m_lemmas.reset(); - m_kind = conflict2_kind_t::ok; + m_kind = conflict_kind_t::ok; SASSERT(empty()); } - void conflict2::set_bailout() { - SASSERT(m_kind == conflict2_kind_t::ok); - m_kind = conflict2_kind_t::bailout; + void conflict::set_bailout() { + SASSERT(m_kind == conflict_kind_t::ok); + m_kind = conflict_kind_t::bailout; s.m_stats.m_num_bailouts++; } - void conflict2::set_backjump() { - SASSERT(m_kind == conflict2_kind_t::ok); - m_kind = conflict2_kind_t::backjump; + void conflict::set_backtrack() { + SASSERT(m_kind == conflict_kind_t::ok); + SASSERT(m_relevant_vars.empty()); + m_kind = conflict_kind_t::backtrack; + + } + void conflict::set_backjump() { + SASSERT(m_kind == conflict_kind_t::ok); + m_kind = conflict_kind_t::backjump; } - void conflict2::init(signed_constraint c) { + bool conflict::is_relevant_pvar(pvar v) const { + switch (m_kind) { + case conflict_kind_t::ok: + return contains_pvar(v); + case conflict_kind_t::bailout: + return true; + case conflict_kind_t::backtrack: + return pvar_occurs_in_constraints(v) || m_relevant_vars.contains(v); + // return m_relevant_vars.contains(v); + case conflict_kind_t::backjump: + UNREACHABLE(); // we don't follow the regular loop when backjumping + return false; + } + } + + bool conflict::is_relevant(sat::literal lit) const { + return contains(lit) || contains(~lit); + } + + void conflict::init(signed_constraint c) { SASSERT(empty()); if (c.bvalue(s) == l_false) { // boolean conflict @@ -110,34 +156,48 @@ namespace polysat { insert_vars(c); } SASSERT(!empty()); + logger().begin_conflict(); // TODO: we often call reset/set so doing this here doesn't really work... make subsequent begins a no-op? or separate init and set? (set could then do reset() internally ... and we only need set() for signed_constraint, not all three variations) + } + + void conflict::init(clause const& cl) { + // if (!empty()) + // return; + // LOG("Conflict: " << cl); + SASSERT(empty()); + for (auto lit : cl) { + auto c = s.lit2cnstr(lit); + SASSERT(c.bvalue(s) == l_false); + insert(~c); + } + SASSERT(!empty()); logger().begin_conflict(); } - void conflict2::init(pvar v, bool by_viable_fallback) { + void conflict::init(pvar v, bool by_viable_fallback) { if (by_viable_fallback) { + logger().begin_conflict(header_with_var("unsat core from viable fallback for v", v)); // Conflict detected by viable fallback: // initial conflict is the unsat core of the univariate solver signed_constraints unsat_core = s.m_viable_fallback.unsat_core(v); for (auto c : unsat_core) insert(c); - logger().begin_conflict("unsat core from viable fallback"); // TODO: apply conflict resolution plugins here too? } else { + logger().begin_conflict(header_with_var("forbidden interval lemma for v", v)); + set_backtrack(); VERIFY(s.m_viable.resolve(v, *this)); // TODO: in general the forbidden interval lemma is not asserting. // but each branch exclude the current assignment. // in those cases we will (additionally?) need an abstraction that is asserting to make sure viable is updated properly. - set_backjump(); - logger().begin_conflict("forbidden interval lemma"); } } - bool conflict2::contains(sat::literal lit) const { + bool conflict::contains(sat::literal lit) const { SASSERT(lit != sat::null_literal); return m_literals.contains(lit.index()); } - void conflict2::insert(signed_constraint c) { + void conflict::insert(signed_constraint c) { if (contains(c)) return; if (c.is_always_true()) @@ -153,7 +213,7 @@ namespace polysat { } } - void conflict2::insert_eval(signed_constraint c) { + void conflict::insert_eval(signed_constraint c) { switch (c.bvalue(s)) { case l_undef: s.assign_eval(c.blit()); @@ -166,20 +226,20 @@ namespace polysat { insert(c); } - void conflict2::insert_vars(signed_constraint c) { + void conflict::insert_vars(signed_constraint c) { for (pvar v : c->vars()) if (s.is_assigned(v)) m_vars.insert(v); } - void conflict2::remove(signed_constraint c) { + void conflict::remove(signed_constraint c) { SASSERT(contains(c)); m_literals.remove(c.blit().index()); for (pvar v : c->vars()) m_var_occurrences[v]--; } - void conflict2::resolve_bool(sat::literal lit, clause const& cl) { + void conflict::resolve_bool(sat::literal lit, clause const& cl) { // Note: core: x, y, z; corresponds to clause ~x \/ ~y \/ ~z // clause: x \/ u \/ v // resolvent: ~y \/ ~z \/ u \/ v; as core: y, z, ~u, ~v @@ -197,7 +257,7 @@ namespace polysat { logger().log(inf_resolve_bool(lit, cl)); } - void conflict2::resolve_with_assignment(sat::literal lit) { + void conflict::resolve_with_assignment(sat::literal lit) { // The reason for lit is conceptually: // x1 = v1 /\ ... /\ xn = vn ==> lit @@ -227,19 +287,21 @@ namespace polysat { logger().log(inf_resolve_with_assignment(s, lit, c)); } - bool conflict2::resolve_value(pvar v) { - SASSERT(contains_pvar(v)); - - if (is_backjumping()) { - for (auto const& c : s.m_viable.get_constraints(v)) - for (pvar v : c->vars()) - logger().log_var(v); - return false; - } + bool conflict::resolve_value(pvar v) { if (is_bailout()) return false; + if (is_backtracking()) { + for (auto const& c : s.m_viable.get_constraints(v)) + for (pvar v : c->vars()) { + m_relevant_vars.insert(v); + logger().log_var(v); + } + return false; + } + + SASSERT(contains_pvar(v)); auto const& j = s.m_justification[v]; if (j.is_decision() && m_bail_vars.contains(v)) // TODO: what if also m_vars.contains(v)? might have a chance at elimination @@ -265,12 +327,79 @@ namespace polysat { // Need to keep the variable in case of decision if (s.is_assigned(v) && j.is_decision()) m_vars.insert(v); - logger().log("bailout"); + logger().log("Bailout"); return false; } - std::ostream& conflict2::display(std::ostream& out) const { - out << "TODO\n"; + clause_ref conflict::build_lemma() { + LOG_H3("Build lemma from core"); + LOG("core: " << *this); + clause_builder lemma(s); + + // TODO: is this sound, doing it for each constraint separately? + // for (auto c : *this) + // minimize_vars(c); + + for (auto c : *this) + lemma.push(~c); + + for (unsigned v : m_vars) { + auto eq = s.eq(s.var(v), s.get_value(v)); + if (eq.bvalue(s) == l_undef) + s.assign_eval(eq.blit()); + lemma.push(~eq); + } + s.decay_activity(); + + logger().log_lemma(lemma); + logger().end_conflict(); + + return lemma.build(); + } + + bool conflict::minimize_vars(signed_constraint c) { + if (m_vars.empty()) + return false; + if (!c.is_currently_false(s)) + return false; + + assignment_t a; + for (auto v : m_vars) + a.push_back(std::make_pair(v, s.get_value(v))); + for (unsigned i = 0; i < a.size(); ++i) { + std::pair save = a[i]; + std::pair last = a.back(); + a[i] = last; + a.pop_back(); + if (c.is_currently_false(s, a)) + --i; + else { + a.push_back(last); + a[i] = save; + } + } + if (a.size() == m_vars.num_elems()) + return false; + m_vars.reset(); + for (auto const& [v, val] : a) + m_vars.insert(v); + logger().log("minimize vars"); + LOG("reduced " << m_vars); + return true; + } + + std::ostream& conflict::display(std::ostream& out) const { + char const* sep = ""; + for (auto c : *this) + out << sep << c->bvar2string() << " " << c, sep = " ; "; + if (!m_vars.empty()) + out << " vars"; + for (auto v : m_vars) + out << " v" << v; + if (!m_bail_vars.empty()) + out << " bail vars"; + for (auto v : m_bail_vars) + out << " v" << v; return out; } } diff --git a/src/math/polysat/conflict.h b/src/math/polysat/conflict.h index c99cc4e26..7d5a35fa2 100644 --- a/src/math/polysat/conflict.h +++ b/src/math/polysat/conflict.h @@ -77,42 +77,54 @@ TODO: - bailout lemma if no method applies (log these cases in particular because it indicates where we are missing something) - force a restart if we get a bailout lemma or non-asserting conflict? - consider case if v is both in vars and bail_vars (do we need to keep it in bail_vars even if we can eliminate it from vars?) +- Find a way to use resolve_value with forbidden interval lemmas. + Then get rid of conflict_kind_t::backtrack and m_relevant_vars. + Maybe: + x := a, y := b, z has no viable value + - assume y was propagated + - FI-Lemma C1 \/ ... \/ Cn without z. + - for each i, we should have x := a /\ Ci ==> y != b + - can we choose one of the Ci to cover the domain of y and extract an FI-Lemma D1 \/ ... \/ Dk without y,z? + - or try to find an L(x,y) such that C1 -> L, ..., Cn -> L, and L -> y != b (under x := a); worst case y != b can work as L +- minimize_vars... is it sound to do for each constraint separately, like we are doing now? --*/ #pragma once #include "math/polysat/constraint.h" -#include "math/polysat/clause_builder.h" #include "math/polysat/inference_logger.h" #include namespace polysat { class solver; - class explainer; - class inference_engine; - class variable_elimination_engine; class conflict_iterator; - class inference_logger; - enum class conflict2_kind_t { + enum class conflict_kind_t { // standard conflict resolution ok, // bailout lemma because no appropriate conflict resolution method applies bailout, + // conflict contains the final lemma; + // backtrack to and revert the last relevant decision + // NOTE: this is currently used for the forbidden intervals lemmas. + // we should find a way to use resolve_value with these lemmas, + // to properly eliminate value propagations. (see todo notes above) + backtrack, + // conflict contains the final lemma; // force backjumping without further conflict resolution because a good lemma has been found - // TODO: distinguish backtrack/revert of last decision from backjump to second-highest level in the lemma backjump, }; - class conflict2 { + class conflict { solver& s; scoped_ptr m_logger; // current conflict core consists of m_literals and m_vars indexed_uint_set m_literals; // set of boolean literals in the conflict uint_set m_vars; // variable assignments used as premises, shorthand for literals (x := v) - uint_set m_bail_vars; // tracked for cone of influence but not directly involved in conflict resolution + uint_set m_bail_vars; // decision variables that are only used to evaluate a constraint; see resolve_with_assignment. + uint_set m_relevant_vars; // tracked for cone of influence but not directly involved in conflict resolution unsigned_vector m_var_occurrences; // for each variable, the number of constraints in m_literals that contain it @@ -120,31 +132,47 @@ namespace polysat { // TODO: we might not need all of these in the end. add only the side lemmas which justify a constraint in the final lemma (recursively)? vector m_lemmas; - conflict2_kind_t m_kind = conflict2_kind_t::ok; + conflict_kind_t m_kind = conflict_kind_t::ok; + + bool minimize_vars(signed_constraint c); public: - conflict2(solver& s); + conflict(solver& s); inference_logger& logger(); bool empty() const; void reset(); - uint_set const& vars() const { return m_vars; } + using const_iterator = conflict_iterator; + const_iterator begin() const; + const_iterator end() const; - bool is_bailout() const { return m_kind == conflict2_kind_t::bailout; } - bool is_backjumping() const { return m_kind == conflict2_kind_t::backjump; } + uint_set const& vars() const { return m_vars; } + uint_set const& bail_vars() const { return m_bail_vars; } + + conflict_kind_t kind() const { return m_kind; } + bool is_bailout() const { return m_kind == conflict_kind_t::bailout; } + bool is_backtracking() const { return m_kind == conflict_kind_t::backtrack; } + bool is_backjumping() const { return m_kind == conflict_kind_t::backjump; } void set_bailout(); + void set_backtrack(); void set_backjump(); + bool is_relevant_pvar(pvar v) const; + bool is_relevant(sat::literal lit) const; + /** conflict because the constraint c is false under current variable assignment */ void init(signed_constraint c); + /** boolean conflict with the given clause */ + void init(clause const& cl); /** conflict because there is no viable value for the variable v */ - void init(pvar v, bool by_viable_fallback = false); + void init(pvar v, bool by_viable_fallback); bool contains(signed_constraint c) const { SASSERT(c); return contains(c.blit()); } bool contains(sat::literal lit) const; 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; } /** * Insert constraint c into conflict state. @@ -172,9 +200,53 @@ namespace polysat { /** Perform resolution with "v = value <- ..." */ bool resolve_value(pvar v); + /** Convert the core into a lemma to be learned. */ + clause_ref build_lemma(); + std::ostream& display(std::ostream& out) const; }; - inline std::ostream& operator<<(std::ostream& out, conflict2 const& c) { return c.display(out); } + inline std::ostream& operator<<(std::ostream& out, conflict const& c) { return c.display(out); } + class conflict_iterator { + friend class conflict; + + using inner_t = indexed_uint_set::iterator; + + constraint_manager* m_cm; + inner_t m_inner; + + conflict_iterator(constraint_manager& cm, inner_t inner): + m_cm(&cm), m_inner(inner) {} + + static conflict_iterator begin(constraint_manager& cm, indexed_uint_set const& lits) { + return {cm, lits.begin()}; + } + + static conflict_iterator end(constraint_manager& cm, indexed_uint_set const& lits) { + return {cm, lits.end()}; + } + + public: + using value_type = signed_constraint; + using difference_type = unsigned; + using pointer = signed_constraint const*; + using reference = signed_constraint const&; + using iterator_category = std::input_iterator_tag; + + conflict_iterator& operator++() { + ++m_inner; + return *this; + } + + signed_constraint operator*() const { + return m_cm->lookup(sat::to_literal(*m_inner)); + } + + bool operator==(conflict_iterator const& other) const { + return m_inner == other.m_inner; + } + + bool operator!=(conflict_iterator const& other) const { return !operator==(other); } + }; } diff --git a/src/math/polysat/inference_logger.cpp b/src/math/polysat/inference_logger.cpp index 62c130fa1..b0af8a8f2 100644 --- a/src/math/polysat/inference_logger.cpp +++ b/src/math/polysat/inference_logger.cpp @@ -40,48 +40,53 @@ namespace polysat { return std::string(70, '-'); } - void file_inference_logger::begin_conflict(char const* text) { + void file_inference_logger::begin_conflict(displayable const& header) { ++m_num_conflicts; - if (text) - LOG("Begin CONFLICT #" << m_num_conflicts << " (" << text << ")"); - else - LOG("Begin CONFLICT #" << m_num_conflicts); + LOG("Begin CONFLICT #" << m_num_conflicts << ": " << header); m_used_constraints.reset(); m_used_vars.reset(); if (!m_out) m_out = alloc(std::ofstream, "conflicts.txt"); else out() << "\n\n\n\n\n\n\n\n\n\n\n\n"; - out() << "CONFLICT #" << m_num_conflicts; - if (text) - out() << " (" << text << ")"; - out() << "\n"; + out() << "CONFLICT #" << m_num_conflicts << ": " << header << "\n"; // log initial conflict state out() << hline() << "\n"; log_conflict_state(); } void file_inference_logger::log_conflict_state() { - out() << "TODO"; - /* TODO: update for new conflict - conflict2 const& core = s.m_conflict2; + conflict const& core = s.m_conflict; for (auto const& c : core) { - out_indent() << c.blit() << ": " << c << '\n'; - m_used_constraints.insert(c.blit().index()); + sat::literal const lit = c.blit(); + out_indent() << lit << ": " << c << '\n'; + // TODO: if justified by a side lemma, print it here + // out_indent() << " justified by: " << lemma << '\n'; + m_used_constraints.insert(lit.index()); for (pvar v : c->vars()) m_used_vars.insert(v); } for (auto v : core.vars()) { - out_indent() << assignment_pp(core.s, v, core.s.get_value(v)) << "\n"; + out_indent() << assignment_pp(s, v, s.get_value(v)) << "\n"; m_used_vars.insert(v); } for (auto v : core.bail_vars()) { - out_indent() << assignment_pp(core.s, v, core.s.get_value(v)) << " (bail)\n"; + out_indent() << assignment_pp(s, v, s.get_value(v)) << " (bail)\n"; m_used_vars.insert(v); } - if (core.is_bailout()) + switch (core.kind()) { + case conflict_kind_t::ok: + break; + case conflict_kind_t::bailout: out_indent() << "(bailout)\n"; - */ + break; + case conflict_kind_t::backtrack: + out_indent() << "(backtrack)\n"; + break; + case conflict_kind_t::backjump: + out_indent() << "(backjump)\n"; + break; + } out().flush(); } @@ -102,7 +107,6 @@ namespace polysat { out() << "\n"; for (auto const& lit : cb) out_indent() << lit_pp(s, lit) << "\n"; - // out_indent() << lit << ": " << s.lit2cnstr(lit) << "\n"; out().flush(); } diff --git a/src/math/polysat/inference_logger.h b/src/math/polysat/inference_logger.h index b1931da53..6d97661c8 100644 --- a/src/math/polysat/inference_logger.h +++ b/src/math/polysat/inference_logger.h @@ -26,13 +26,26 @@ namespace polysat { class search_item; class solver; - class inference { + class displayable { public: - virtual ~inference() {} + virtual ~displayable() {} virtual std::ostream& display(std::ostream& out) const = 0; }; - inline std::ostream& operator<<(std::ostream& out, inference const& i) { return i.display(out); } + inline std::ostream& operator<<(std::ostream& out, displayable const& d) { return d.display(out); } + + class display_c_str : public displayable { + char const* m_str; + public: + display_c_str(char const* str) : m_str(str) { } + std::ostream& display(std::ostream& out) const override { + if (m_str) + out << m_str; + return out; + } + }; + + class inference : public displayable { }; class inference_named : public inference { char const* m_name; @@ -46,12 +59,14 @@ namespace polysat { virtual ~inference_logger() {} /// Begin next conflict - virtual void begin_conflict(char const* text = nullptr) = 0; + void begin_conflict(char const* text = nullptr) { begin_conflict(display_c_str(text)); } + virtual void begin_conflict(displayable const& header) = 0; /// Log inference and the current state. virtual void log(inference const& inf) = 0; virtual void log(char const* name) { log(inference_named(name)); } virtual void log_var(pvar v) = 0; /// Log relevant part of search state and viable. + /// Call end_conflict before backjumping in the solver. virtual void end_conflict() = 0; /// Log current conflict state (implicitly done by log_inference) @@ -62,7 +77,7 @@ namespace polysat { class dummy_inference_logger : public inference_logger { public: - virtual void begin_conflict(char const* text) override {} + virtual void begin_conflict(displayable const& header) override {} virtual void log(inference const& inf) override {} virtual void log_var(pvar v) override {} virtual void end_conflict() override {} @@ -85,18 +100,11 @@ namespace polysat { public: file_inference_logger(solver& s); - - /// Begin next conflict - void begin_conflict(char const* text) override; - /// Log inference and the current state. + void begin_conflict(displayable const& header) override; void log(inference const& inf) override; void log_var(pvar v) override; - /// Log relevant part of search state and viable. void end_conflict() override; - - /// Log current conflict state (implicitly done by log_inference) void log_conflict_state() override; - void log_lemma(clause_builder const& cb) override; }; diff --git a/src/math/polysat/solver.cpp b/src/math/polysat/solver.cpp index a552e5272..45869b0d5 100644 --- a/src/math/polysat/solver.cpp +++ b/src/math/polysat/solver.cpp @@ -33,7 +33,6 @@ namespace polysat { m_viable_fallback(*this), m_linear_solver(*this), m_conflict(*this), - m_conflict2(*this), m_simplify_clause(*this), m_simplify(*this), m_restart(*this), @@ -545,7 +544,7 @@ namespace polysat { // (fail here in debug mode so we notice if we miss some) DEBUG_CODE( UNREACHABLE(); ); m_free_pvars.unassign_var_eh(v); - set_conflict(v); + set_conflict(v, false); return; case dd::find_t::singleton: // NOTE: this case may happen legitimately if all other possibilities were excluded by brute force search @@ -578,8 +577,7 @@ namespace polysat { case dd::find_t::empty: LOG("Fallback solver: unsat"); m_free_pvars.unassign_var_eh(v); - auto core = m_viable_fallback.unsat_core(v); // TODO: add constraints from unsat_core to conflict - set_conflict(v); + set_conflict(v, true); return; } } @@ -620,17 +618,6 @@ namespace polysat { SASSERT(is_conflict()); - if (m_conflict.conflict_var() != null_var) { - m_conflict.begin_conflict("backtrack_fi"); - pvar v = m_conflict.conflict_var(); - // This case corresponds to a propagation of conflict_var, except it's not explicitly on the stack. - // TODO: use unsat core from m_viable_fallback if the conflict is from there - VERIFY(m_viable.resolve(v, m_conflict)); - backtrack_fi(); - return; - } - m_conflict.begin_conflict("resolve_conflict"); - search_iterator search_it(m_search); while (search_it.next()) { auto& item = *search_it; @@ -638,23 +625,21 @@ namespace polysat { if (item.is_assignment()) { // Resolve over variable assignment pvar v = item.var(); - if (!m_conflict.contains_pvar(v) && !m_conflict.is_bailout()) { + // if (!m_conflict.contains_pvar(v) && !m_conflict.is_bailout()) { + if (!m_conflict.is_relevant_pvar(v)) { m_search.pop_assignment(); continue; } LOG_H2("Working on " << search_item_pp(m_search, item)); LOG(m_justification[v]); LOG("Conflict: " << m_conflict); - // inc_activity(v); // done in resolve_value justification& j = m_justification[v]; if (j.level() > base_level() && !m_conflict.resolve_value(v) && j.is_decision()) { - m_conflict.end_conflict(); revert_decision(v); return; } - if (m_conflict.is_bailout_lemma()) { - m_conflict.end_conflict(); - backtrack_lemma(); + if (m_conflict.is_backjumping()) { + backjump_lemma(); return; } m_search.pop_assignment(); @@ -664,36 +649,37 @@ namespace polysat { SASSERT(item.is_boolean()); sat::literal const lit = item.lit(); sat::bool_var const var = lit.var(); - if (!m_conflict.is_marked(var)) + if (!m_conflict.is_relevant(lit)) continue; - LOG_H2("Working on " << search_item_pp(m_search, item)); LOG(bool_justification_pp(m_bvars, lit)); LOG("Literal " << lit << " is " << lit2cnstr(lit)); LOG("Conflict: " << m_conflict); - if (m_bvars.is_assumption(var)) // TODO: wouldn't this mean we're already at the base level? - continue; + if (m_bvars.is_assumption(var)) { + SASSERT(m_bvars.level(var) <= base_level()); + break; + } else if (m_bvars.is_bool_propagation(var)) - m_conflict.resolve(lit, *m_bvars.reason(lit)); + m_conflict.resolve_bool(lit, *m_bvars.reason(lit)); else { SASSERT(m_bvars.is_value_propagation(var)); - m_conflict.resolve_with_assignment(lit, m_bvars.level(lit)); + m_conflict.resolve_with_assignment(lit); } } } LOG("End of resolve_conflict loop"); - m_conflict.end_conflict(); + m_conflict.logger().end_conflict(); report_unsat(); } /** - * Simple backtracking for lemmas: + * Simple backjumping for lemmas: * jump to the level where the lemma can be (bool-)propagated, * even without reverting the last decision. */ - void solver::backtrack_lemma() { - clause_ref lemma = m_conflict.build_lemma().build(); - LOG_H2("backtrack_lemma: " << show_deref(lemma)); + void solver::backjump_lemma() { + clause_ref lemma = m_conflict.build_lemma(); + LOG_H2("backjump_lemma: " << show_deref(lemma)); SASSERT(lemma); LOG("Lemma: " << *lemma); for (sat::literal lit : *lemma) { @@ -715,6 +701,7 @@ namespace polysat { jump_level = lit_level; } } + SASSERT(max_level == m_level); // not required; see comment on max_level jump_level = std::max(jump_level, base_level()); @@ -728,69 +715,6 @@ namespace polysat { learn_lemma(*lemma); } - /** - * Simpler backtracking for forbidden interval lemmas: - * since forbidden intervals already gives us a lemma where the conflict variable has been eliminated, - * we can backtrack to the last relevant decision and learn this lemma. - */ - void solver::backtrack_fi() { - uint_set relevant_vars; - search_iterator search_it(m_search); - while (search_it.next()) { - auto& item = *search_it; - search_it.set_resolved(); - if (item.is_assignment()) { - // Resolve over variable assignment - pvar v = item.var(); - if (!m_conflict.pvar_occurs_in_constraints(v) && !relevant_vars.contains(v)) { - m_search.pop_assignment(); - continue; - } - LOG_H2("Working on " << search_item_pp(m_search, item)); - LOG(m_justification[v]); - LOG("Conflict: " << m_conflict); - inc_activity(v); - justification& j = m_justification[v]; - if (j.level() > base_level() && j.is_decision()) { - m_conflict.end_conflict(); - revert_decision(v); - return; - } - SASSERT(j.is_propagation()); - // If a variable was propagated: - // we don't really care about the constraints in this case, but just about the variables it depends on - for (auto const& c : m_viable.get_constraints(v)) - for (pvar v : c->vars()) { - relevant_vars.insert(v); - m_conflict.log_var(v); - } - m_search.pop_assignment(); - } - else { - // Resolve over boolean literal - SASSERT(item.is_boolean()); - sat::literal const lit = item.lit(); - sat::bool_var const var = lit.var(); - if (!m_conflict.is_marked(var)) - continue; - LOG_H2("Working on " << search_item_pp(m_search, item)); - LOG(bool_justification_pp(m_bvars, lit)); - LOG("Literal " << lit << " is " << lit2cnstr(lit)); - LOG("Conflict: " << m_conflict); - if (m_bvars.is_assumption(var)) // TODO: wouldn't this mean we're already at the base level? - continue; - else if (m_bvars.is_bool_propagation(var)) - m_conflict.resolve(lit, *m_bvars.reason(lit)); - else { - SASSERT(m_bvars.is_value_propagation(var)); - continue; - } - } - } - m_conflict.end_conflict(); - report_unsat(); - } - /** * Variable activity accounting. * As a placeholder we increment activity @@ -839,6 +763,7 @@ namespace polysat { LOG("Learning: "<< lemma); SASSERT(!lemma.empty()); m_simplify_clause.apply(lemma); + // TODO: print warning if the lemma is non-asserting? add_clause(lemma); } @@ -858,7 +783,7 @@ namespace polysat { LOG_H3("Reverting decision: pvar " << v << " := " << val); SASSERT(m_justification[v].is_decision()); - clause_ref lemma = m_conflict.build_lemma().build(); + clause_ref lemma = m_conflict.build_lemma(); if (lemma->empty()) report_unsat(); else { @@ -887,7 +812,7 @@ namespace polysat { } void solver::assign_eval(sat::literal lit) { - SASSERT(lit2cnstr(lit).is_currently_true(*this)); + // SASSERT(lit2cnstr(lit).is_currently_true(*this)); // "morally" this should hold, but currently fails because of pop_assignment during resolve_conflict unsigned level = 0; // NOTE: constraint may be evaluated even if some variables are still unassigned (e.g., 0*x doesn't depend on x). for (auto v : lit2cnstr(lit)->vars()) @@ -934,12 +859,13 @@ namespace polysat { void solver::add_clause(clause& clause) { LOG((clause.is_redundant() ? "Lemma: ": "Aux: ") << clause); for (sat::literal lit : clause) { - LOG(" Literal " << lit << " is: " << lit_pp(*this, lit)); + LOG(" " << lit_pp(*this, lit)); // SASSERT(m_bvars.value(lit) != l_true); // it could be that such a literal has been created previously but we don't detect it when e.g. narrowing a mul_ovfl_constraint if (m_bvars.value(lit) == l_true) { // in this case the clause is useless LOG(" Clause is already true, skipping..."); + // SASSERT(false); // should never happen (at least for redundant clauses) return; } } @@ -1106,12 +1032,14 @@ namespace polysat { * Check that two variables of each constraint are watched. */ bool solver::wlist_invariant() { +#if 0 for (pvar v = 0; v < m_value.size(); ++v) { std::stringstream s; for (constraint* c : m_pwatch[v]) s << " " << c->bvar(); LOG("Watch for v" << v << ": " << s.str()); } +#endif // Skip boolean variables that aren't active yet uint_set skip; for (unsigned i = m_qhead; i < m_search.size(); ++i) diff --git a/src/math/polysat/solver.h b/src/math/polysat/solver.h index 3f65fabcb..ae42f8861 100644 --- a/src/math/polysat/solver.h +++ b/src/math/polysat/solver.h @@ -22,7 +22,6 @@ Author: #include "util/params.h" #include "math/polysat/boolean.h" #include "math/polysat/conflict.h" -#include "math/polysat/conflict2.h" #include "math/polysat/constraint.h" #include "math/polysat/clause_builder.h" #include "math/polysat/simplify_clause.h" @@ -37,8 +36,6 @@ Author: #include "math/polysat/viable.h" #include "math/polysat/log.h" - - namespace polysat { struct config { @@ -70,14 +67,12 @@ namespace polysat { friend class clause; friend class clause_builder; friend class conflict; - friend class conflict2; friend class conflict_explainer; friend class simplify_clause; friend class simplify; friend class restart; friend class explainer; friend class inference_engine; - friend class old_inference_logger; friend class file_inference_logger; friend class forbidden_intervals; friend class linear_solver; @@ -94,7 +89,6 @@ namespace polysat { friend class scoped_solverv; friend class test_polysat; friend class test_fi; - friend struct inference_resolve_with_assignment; friend struct inf_resolve_with_assignment; reslimit& m_lim; @@ -105,7 +99,6 @@ namespace polysat { viable_fallback m_viable_fallback; // fallback for viable, using bitblasting over univariate constraints linear_solver m_linear_solver; conflict m_conflict; - conflict2 m_conflict2; simplify_clause m_simplify_clause; simplify m_simplify; restart m_restart; @@ -192,9 +185,9 @@ namespace polysat { void erase_pwatch(pvar v, constraint* c); void erase_pwatch(constraint* c); - void set_conflict(signed_constraint c) { m_conflict.set(c); } - void set_conflict(clause& cl) { m_conflict.set(cl); } - void set_conflict(pvar v) { m_conflict.set(v); } + void set_conflict(signed_constraint c) { m_conflict.init(c); } + void set_conflict(clause& cl) { m_conflict.init(cl); } + void set_conflict(pvar v, bool by_viable_fallback) { m_conflict.init(v, by_viable_fallback); } bool can_decide() const { return !m_free_pvars.empty(); } void decide(); @@ -202,14 +195,12 @@ namespace polysat { void linear_propagate(); - bool is_conflict() const { return !m_conflict.empty(); } bool at_base_level() const; unsigned base_level() const; void resolve_conflict(); - void backtrack_fi(); - void backtrack_lemma(); + void backjump_lemma(); void revert_decision(pvar v); void revert_bool_decision(sat::literal lit); @@ -461,7 +452,4 @@ namespace polysat { inline std::ostream& operator<<(std::ostream& out, assignments_pp const& a) { return a.display(out); } - } - - diff --git a/src/math/polysat/viable.cpp b/src/math/polysat/viable.cpp index d86b83ac3..90e5ff4a1 100644 --- a/src/math/polysat/viable.cpp +++ b/src/math/polysat/viable.cpp @@ -29,9 +29,19 @@ TODO: improve management of the fallback univariate solvers: #include "util/debug.h" #include "math/polysat/viable.h" #include "math/polysat/solver.h" +#include "math/polysat/univariate/univariate_solver.h" namespace polysat { + struct inf_fi : public inference { + viable& v; + pvar var; + inf_fi(viable& v, pvar var) : v(v), var(var) {} + std::ostream& display(std::ostream& out) const override { + return out << "Forbidden intervals for v" << var << ": " << viable::var_pp(v, var); + } + }; + viable::viable(solver& s): s(s), m_forbidden_intervals(s) { @@ -54,7 +64,7 @@ namespace polysat { m_diseq_lin.pop_back(); } - viable::entry* viable::alloc_entry() { + viable::entry* viable::alloc_entry() { if (m_alloc.empty()) return alloc(entry); auto* e = m_alloc.back(); @@ -68,21 +78,21 @@ namespace polysat { auto& [v, k, e] = m_trail.back(); SASSERT(well_formed(m_units[v])); switch (k) { - case entry_kind::unit_e: - e->remove_from(m_units[v], e); + case entry_kind::unit_e: + e->remove_from(m_units[v], e); SASSERT(well_formed(m_units[v])); break; - case entry_kind::equal_e: - e->remove_from(m_equal_lin[v], e); + case entry_kind::equal_e: + e->remove_from(m_equal_lin[v], e); break; case entry_kind::diseq_e: - e->remove_from(m_diseq_lin[v], e); + e->remove_from(m_diseq_lin[v], e); break; default: UNREACHABLE(); break; } - m_alloc.push_back(e); + m_alloc.push_back(e); m_trail.pop_back(); } @@ -98,12 +108,12 @@ namespace polysat { if (e->interval.lo_val() < m_units[v]->interval.lo_val()) m_units[v] = e; } - else - m_units[v] = e; + else + m_units[v] = e; SASSERT(well_formed(m_units[v])); m_trail.pop_back(); } - + bool viable::intersect(pdd const & p, pdd const & q, signed_constraint const& sc) { pvar v = null_var; bool first = true; @@ -124,7 +134,7 @@ namespace polysat { prop = true; break; case dd::find_t::empty: - s.set_conflict(v); + s.set_conflict(v, false); return true; default: break; @@ -136,7 +146,7 @@ namespace polysat { goto try_viable; } return prop; - } + } bool viable::intersect(pvar v, signed_constraint const& c) { entry* ne = alloc_entry(); @@ -184,12 +194,11 @@ namespace polysat { m_alloc.push_back(ne); return false; } - auto create_entry = [&]() { m_trail.push_back({ v, entry_kind::unit_e, ne }); s.m_trail.push_back(trail_instr_t::viable_add_i); - ne->init(ne); + ne->init(ne); return ne; }; @@ -200,13 +209,13 @@ namespace polysat { }; if (ne->interval.is_full()) { - while (m_units[v]) + while (m_units[v]) remove_entry(m_units[v]); m_units[v] = create_entry(); return true; } - if (!e) + if (!e) m_units[v] = create_entry(); else { entry* first = e; @@ -222,10 +231,10 @@ namespace polysat { m_units[v] = create_entry(); return true; } - if (e == first) - first = n; + if (e == first) + first = n; e = n; - } + } SASSERT(e->interval.lo_val() != ne->interval.lo_val()); if (e->interval.lo_val() > ne->interval.lo_val()) { if (first->prev()->interval.currently_contains(ne->interval)) { @@ -239,7 +248,7 @@ namespace polysat { return true; } e = e->next(); - } + } while (e != first); // otherwise, append to end of list first->insert_before(create_entry()); @@ -255,10 +264,10 @@ namespace polysat { /** * Traverse all interval constraints with coefficients to check whether current value 'val' for * 'v' is feasible. If not, extract a (maximal) interval to block 'v' from being assigned val. - * + * * To investigate: * - side conditions are stronger than for unit intervals. They constrain the lower and upper bounds to - * be precisely the assigned values. This is to ensure that lo/hi that are computed based on lo_val + * be precisely the assigned values. This is to ensure that lo/hi that are computed based on lo_val * and division with coeff are valid. Is there a more relaxed scheme? */ bool viable::refine_equal_lin(pvar v, rational const& val) { @@ -330,7 +339,7 @@ namespace polysat { if (e->interval.lo_val() < e->interval.hi_val()) { increase_hi(hi); - decrease_lo(lo); + decrease_lo(lo); } else if (e->interval.lo_val() <= coeff_val) { rational lambda_u = floor((max_value - coeff_val) / e->coeff); @@ -342,13 +351,13 @@ namespace polysat { else { SASSERT(coeff_val < e->interval.hi_val()); rational lambda_l = floor(coeff_val / e->coeff); - lo = val - lambda_l; + lo = val - lambda_l; increase_hi(hi); } LOG("forbidden interval v" << v << " " << val << " " << e->coeff << " * " << e->interval << " [" << lo << ", " << hi << "["); SASSERT(hi <= mod_value); - bool full = (lo == 0 && hi == mod_value); - if (hi == mod_value) + bool full = (lo == 0 && hi == mod_value); + if (hi == mod_value) hi = 0; pdd lop = s.var2pdd(v).mk_val(lo); pdd hip = s.var2pdd(v).mk_val(hi); @@ -358,13 +367,13 @@ namespace polysat { ne->coeff = 1; if (full) ne->interval = eval_interval::full(); - else + else ne->interval = eval_interval::proper(lop, lo, hip, hi); intersect(v, ne); return false; } e = e->next(); - } + } while (e != first); return true; } @@ -453,7 +462,7 @@ namespace polysat { return true; } - bool viable::has_viable(pvar v) { + bool viable::has_viable(pvar v) { refined: auto* e = m_units[v]; @@ -468,9 +477,9 @@ namespace polysat { return false; // quick check: last interval doesn't wrap around, so hi_val // has not been covered - if (last->interval.lo_val() < last->interval.hi_val()) + if (last->interval.lo_val() < last->interval.hi_val()) CHECK_RETURN(last->interval.hi_val()); - + do { if (e->interval.is_full()) return false; @@ -482,16 +491,16 @@ namespace polysat { if (n == first) { if (e->interval.lo_val() > e->interval.hi_val()) return false; - CHECK_RETURN(e->interval.hi_val()); + CHECK_RETURN(e->interval.hi_val()); } e = n; - } + } while (e != first); return false; #undef CHECK_RETURN } - bool viable::is_viable(pvar v, rational const& val) { + bool viable::is_viable(pvar v, rational const& val) { auto* e = m_units[v]; if (!e) return refine_viable(v, val); @@ -499,17 +508,17 @@ namespace polysat { entry* last = first->prev(); if (last->interval.currently_contains(val)) return false; - for (; e != last; e = e->next()) { + for (; e != last; e = e->next()) { if (e->interval.currently_contains(val)) return false; - if (val < e->interval.lo_val()) - return refine_viable(v, val); - } + if (val < e->interval.lo_val()) + return refine_viable(v, val); + } return refine_viable(v, val); } - rational viable::min_viable(pvar v) { + rational viable::min_viable(pvar v) { refined: rational lo(0); auto* e = m_units[v]; @@ -521,20 +530,20 @@ namespace polysat { entry* last = first->prev(); if (last->interval.currently_contains(lo)) lo = last->interval.hi_val(); - do { + do { if (!e->interval.currently_contains(lo)) break; lo = e->interval.hi_val(); e = e->next(); - } + } while (e != first); if (!refine_viable(v, lo)) goto refined; - SASSERT(is_viable(v, lo)); + SASSERT(is_viable(v, lo)); return lo; } - rational viable::max_viable(pvar v) { + rational viable::max_viable(pvar v) { refined: rational hi = s.var2pdd(v).max_value(); auto* e = m_units[v]; @@ -549,7 +558,7 @@ namespace polysat { break; hi = e->interval.lo_val() - 1; e = e->prev(); - } + } while (e != last); if (!refine_viable(v, hi)) goto refined; @@ -557,7 +566,7 @@ namespace polysat { return hi; } - dd::find_t viable::find_viable(pvar v, rational& lo) { + dd::find_t viable::find_viable(pvar v, rational& lo) { refined: lo = 0; auto* e = m_units[v]; @@ -594,7 +603,7 @@ namespace polysat { break; lo = e->interval.hi_val(); e = e->next(); - } + } while (e != first); if (e->interval.currently_contains(lo)) @@ -608,7 +617,7 @@ namespace polysat { break; hi = e->interval.lo_val() - 1; e = e->prev(); - } + } while (e != last); if (!refine_viable(v, lo)) goto refined; @@ -620,20 +629,6 @@ namespace polysat { return dd::find_t::multiple; } - struct inference_fi : public inference { - viable& v; - pvar var; - inference_fi(viable& v, pvar var) : v(v), var(var) {} - std::ostream& display(std::ostream& out) const override { - return out << "Forbidden intervals for v" << var << ": " << viable::var_pp(v, var); - } - }; - - bool viable::resolve(pvar v, conflict2& core) { - NOT_IMPLEMENTED_YET(); - return false; - } - bool viable::resolve(pvar v, conflict& core) { if (has_viable(v)) return false; @@ -652,7 +647,7 @@ namespace polysat { auto lhs = hi - next_lo; auto rhs = next_hi - next_lo; signed_constraint c = s.m_constraints.ult(lhs, rhs); - core.propagate(c); + core.insert_eval(c); #if 0 if (n != first) { while { @@ -666,21 +661,26 @@ namespace polysat { } #endif } - for (auto sc : e->side_cond) - core.propagate(sc); + for (auto sc : e->side_cond) + core.insert_eval(sc); core.insert(e->src); e = n; - } + } while (e != first); + core.logger().log(inf_fi(*this, v)); + // TODO: should not be here, too general + /* for (auto c : core) { if (c.bvalue(s) == l_false) { core.reset(); core.set(~c); + core.logger().log(""); break; } } - core.log_inference(inference_fi(*this, v)); + */ + return true; } @@ -694,7 +694,7 @@ namespace polysat { do { LOG("v" << v << ": " << e->interval << " " << e->side_cond << " " << e->src); e = e->next(); - } + } while (e != first); } @@ -712,7 +712,7 @@ namespace polysat { out << e->coeff << " * v" << v << " "; out << e->interval << " " << e->side_cond << " " << e->src << "; "; e = e->next(); - } + } while (e != first); return out; } @@ -732,7 +732,7 @@ namespace polysat { /* * Lower bounds are strictly ascending. - * intervals don't contain each-other (since lower bounds are ascending, + * intervals don't contain each-other (since lower bounds are ascending, * it suffices to check containment in one direction). */ bool viable::well_formed(entry* e) { @@ -742,15 +742,15 @@ namespace polysat { while (true) { if (e->interval.is_full()) return e->next() == e; - if (e->interval.is_currently_empty()) + if (e->interval.is_currently_empty()) return false; - + auto* n = e->next(); if (n != e && e->interval.currently_contains(n->interval)) return false; - + if (n == first) - break; + break; if (e->interval.lo_val() >= n->interval.lo_val()) return false; e = n; diff --git a/src/math/polysat/viable.h b/src/math/polysat/viable.h index f1928e5f1..4507323a8 100644 --- a/src/math/polysat/viable.h +++ b/src/math/polysat/viable.h @@ -5,7 +5,7 @@ Module Name: maintain viable domains It uses the interval extraction functions from forbidden intervals. - An empty viable set corresponds directly to a conflict that does not rely on + An empty viable set corresponds directly to a conflict that does not rely on the non-viable variable. Author: @@ -23,24 +23,24 @@ Author: #include "util/small_object_allocator.h" #include "math/polysat/types.h" #include "math/polysat/conflict.h" -#include "math/polysat/conflict2.h" #include "math/polysat/constraint.h" #include "math/polysat/forbidden_intervals.h" -#include "math/polysat/univariate/univariate_solver.h" namespace polysat { class solver; + class univariate_solver; + class univariate_solver_factory; class viable { friend class test_fi; solver& s; forbidden_intervals m_forbidden_intervals; - + struct entry : public dll_base, public fi_record {}; enum class entry_kind { unit_e, equal_e, diseq_e }; - + ptr_vector m_alloc; ptr_vector m_units; // set of viable values based on unit multipliers ptr_vector m_equal_lin; // entries that have non-unit multipliers, but are equal @@ -112,7 +112,6 @@ namespace polysat { * \pre there are no viable values for v */ bool resolve(pvar v, conflict& core); - bool resolve(pvar v, conflict2& core); /** Log all viable values for the given variable. * (Inefficient, but useful for debugging small instances.) @@ -129,11 +128,11 @@ namespace polysat { bool visited = false; unsigned idx = 0; public: - iterator(entry* curr, bool visited) : + iterator(entry* curr, bool visited) : curr(curr), visited(visited || !curr) {} iterator& operator++() { - if (idx < curr->side_cond.size()) + if (idx < curr->side_cond.size()) ++idx; else { idx = 0; @@ -143,7 +142,7 @@ namespace polysat { return *this; } - signed_constraint& operator*() { + signed_constraint& operator*() { return idx < curr->side_cond.size() ? curr->side_cond[idx] : curr->src; } @@ -165,8 +164,8 @@ namespace polysat { iterator end() const { return iterator(v.m_units[var], true); } }; - constraints get_constraints(pvar v) const { - return constraints(*this, v); + constraints get_constraints(pvar v) const { + return constraints(*this, v); } class int_iterator { @@ -181,8 +180,8 @@ namespace polysat { return *this; } - eval_interval const& operator*() { - return curr->interval; + eval_interval const& operator*() { + return curr->interval; } bool operator==(int_iterator const& other) const { @@ -210,10 +209,10 @@ namespace polysat { struct var_pp { viable const& v; - pvar var; + pvar var; var_pp(viable const& v, pvar var) : v(v), var(var) {} }; - + }; inline std::ostream& operator<<(std::ostream& out, viable const& v) {