diff --git a/src/math/polysat/conflict.cpp b/src/math/polysat/conflict.cpp index 07ef61247..f7a9acfff 100644 --- a/src/math/polysat/conflict.cpp +++ b/src/math/polysat/conflict.cpp @@ -8,21 +8,15 @@ Module Name: Author: Nikolaj Bjorner (nbjorner) 2021-03-19 - Jakob Rath 2021-04-6 + Jakob Rath 2021-04-06 Notes: - TODO: try a final core reduction step or other core minimization - - TODO: revert(pvar v) is too weak. - It should apply saturation rules currently only available for propagated values. - - TODO: dependency tracking for constraints evaluating to false should be minimized. - --*/ -#include "math/polysat/conflict.h" +#include "math/polysat/conflict2.h" #include "math/polysat/solver.h" +#include "math/polysat/inference_logger.h" #include "math/polysat/log.h" #include "math/polysat/log_helper.h" #include "math/polysat/explain.h" @@ -35,359 +29,20 @@ Notes: namespace polysat { - class old_inference_logger { - uint_set m_used_constraints; - uint_set m_used_vars; - scoped_ptr m_out = nullptr; - unsigned m_conflicts = 0; - - friend class conflict; - - std::ostream& out() { - SASSERT(m_out); - return *m_out; - } - - std::ostream& out_indent() { return out() << " "; } - - std::string hline() const { return std::string(70, '-'); } - - public: - void begin_conflict(char const* text) { - ++m_conflicts; - if (text) - LOG("Begin CONFLICT #" << m_conflicts << " (" << text << ")"); - else - LOG("Begin CONFLICT #" << m_conflicts); - 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_conflicts << " (" << text << ")" << "\n"; - } - - void log_inference(conflict const& core, inference const* inf) { - out() << hline() << "\n"; - if (inf) - out() << *inf << "\n"; - if (core.conflict_var() != null_var) { - out_indent() << "Conflict var: " << core.conflict_var() << "\n"; - m_used_vars.insert(core.conflict_var()); - } - for (auto const& c : core) { - out_indent() << c.blit() << ": " << c << '\n'; - m_used_constraints.insert(c.blit().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"; - 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"; - m_used_vars.insert(v); - } - if (core.is_bailout()) - out_indent() << "(bailout)\n"; - out().flush(); - } - - void log_lemma(solver const& s, clause_builder const& cb) { - out() << hline() << "\nLemma:"; - for (auto const& lit : cb) - out() << " " << lit; - out() << "\n"; - for (auto const& lit : cb) - out_indent() << lit << ": " << s.lit2cnstr(lit) << '\n'; - out().flush(); - } - - void end_conflict(search_state const& search, viable const& v) { - out() << "\n" << hline() << "\n\n"; - out() << "Search state (part):\n"; - for (auto const& item : search) - if (is_relevant(item)) - out_indent() << search_item_pp(search, item, true) << "\n"; - out() << hline() << "\nViable (part):\n"; - for (pvar var : m_used_vars) - out_indent() << "v" << std::setw(3) << std::left << var << ": " << viable::var_pp(v, var) << "\n"; - out().flush(); - LOG("End CONFLICT #" << m_conflicts); - } - - bool is_relevant(search_item const& item) const { - switch (item.kind()) { - case search_item_k::assignment: - return m_used_vars.contains(item.var()); - case search_item_k::boolean: - return m_used_constraints.contains(item.lit().index()); - } - UNREACHABLE(); - return false; - } - }; - - void conflict::log_var(pvar v) { - if (m_logger) - m_logger->m_used_vars.insert(v); - } - - conflict::conflict(solver& s): s(s) { - ex_engines.push_back(alloc(ex_polynomial_superposition, s)); - ex_engines.push_back(alloc(eq_explain, s)); - ve_engines.push_back(alloc(ve_reduction)); - inf_engines.push_back(alloc(inf_saturate, s)); - // TODO: how to set this on the CLI? "polysat.log_conflicts=true" doesn't seem to work although z3 accepts it - if (true || s.get_config().m_log_conflicts) - m_logger = alloc(old_inference_logger); - } - - conflict::~conflict() {} - - void conflict::begin_conflict(char const* text) { - if (m_logger) { - m_logger->begin_conflict(text); - // log initial conflict state - m_logger->log_inference(*this, nullptr); - } - } - - void conflict::log_inference(inference const& inf) { - if (m_logger) - m_logger->log_inference(*this, &inf); - } - - void conflict::end_conflict() { - if (m_logger) - m_logger->end_conflict(s.m_search, s.m_viable); - } - - constraint_manager& conflict::cm() const { return s.m_constraints; } - - 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; - } - - bool conflict::empty() const { - return m_literals.empty() - && m_vars.empty() - && m_bail_vars.empty() - && m_conflict_var == null_var; - } - - void conflict::reset() { - for (auto c : *this) - unset_mark(c); - m_literals.reset(); - m_vars.reset(); - m_var_occurrences.reset(); - m_bail_vars.reset(); - m_conflict_var = null_var; - m_kind = conflict_kind_t::ok; - SASSERT(empty()); - } - - /** - * The constraint is false under the current assignment of variables. - * The core is then the conjuction of this constraint and assigned variables. - */ - void conflict::set(signed_constraint c) { - LOG("Conflict: " << c << " " << c.bvalue(s)); - SASSERT(empty()); - if (c.bvalue(s) == l_false) { - auto* cl = s.m_bvars.reason(c.blit().var()); - if (cl) - set(*cl); - else - insert(c); - } - else { - SASSERT(c.is_currently_false(s)); - // TBD: fails with test_subst SASSERT(c.bvalue(s) == l_true); - insert_vars(c); - insert(c); - } - SASSERT(!empty()); - } - - /** - * The variable v cannot be assigned. - * The conflict is the set of justifications accumulated for the viable values for v. - * These constraints are (in the current form) not added to the core, but passed directly - * to the forbidden interval module. - * A consistent approach could be to add these constraints to the core and then also include the - * variable assignments. - */ - void conflict::set(pvar v) { - LOG("Conflict: v" << v); - SASSERT(empty()); - m_conflict_var = v; - SASSERT(!empty()); - } - - /** - * The clause is conflicting in the current search state. - */ - void conflict::set(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()); - } - - /** - * Insert constraint into conflict state - * Skip trivial constraints - * - e.g., constant ones such as "4 > 1"... only true ones - * should appear, otherwise the lemma would be a tautology - */ - void conflict::insert(signed_constraint c) { - if (c.is_always_true()) - return; - if (is_marked(c)) - return; - LOG("inserting: " << c); - SASSERT(!c->vars().empty()); - set_mark(c); - m_literals.insert(c.blit().index()); - for (pvar v : c->vars()) { - if (v >= m_var_occurrences.size()) - m_var_occurrences.resize(v + 1, 0); - m_var_occurrences[v]++; - } - } - - void conflict::propagate(signed_constraint c) { - switch (c.bvalue(s)) { - case l_undef: - s.assign_eval(c.blit()); - break; - case l_true: - break; - case l_false: - break; - } - insert(c); - } - - void conflict::insert_vars(signed_constraint c) { - for (pvar v : c->vars()) - if (s.is_assigned(v)) - m_vars.insert(v); - } - - /** - * Premises can either be justified by a Clause or by a value assignment. - * Premises that are justified by value assignments are not assigned (the bvalue is l_undef) - * The justification for those premises are based on the free assigned variables. - * - * NOTE: maybe we should skip intermediate steps and just collect the leaf premises for c? - * Ensure that c is assigned and justified - */ - // TODO: rename this; it pushes onto \Gamma and doesn't insert into the core - void conflict::insert(signed_constraint c, vector const& premises) { - // keep(c); - clause_builder c_lemma(s); - for (auto premise : premises) { - LOG_H3("premise: " << premise); - // keep(premise); - SASSERT(premise.bvalue(s) != l_false); - c_lemma.push(~premise.blit()); - } - c_lemma.push(c.blit()); - clause_ref lemma = c_lemma.build(); - SASSERT(lemma); - cm().store(lemma.get(), s, false); - if (c.bvalue(s) == l_undef) - s.assign_propagate(c.blit(), *lemma); - } - - void conflict::remove(signed_constraint c) { - unset_mark(c); - m_literals.remove(c.blit().index()); - for (pvar v : c->vars()) { - if (v < m_var_occurrences.size()) - m_var_occurrences[v]--; - } - } - - void conflict::replace(signed_constraint c_old, signed_constraint c_new, vector const& c_new_premises) { - remove(c_old); - insert(c_new, c_new_premises); - } - - bool conflict::contains(signed_constraint c) const { - return m_literals.contains(c.blit().index()); - } - - bool conflict::contains(sat::literal lit) const { - SASSERT(lit != sat::null_literal); - return m_literals.contains(lit.index()); - } - - void conflict::set_bailout_gave_up() { - SASSERT(m_kind == conflict_kind_t::ok); - m_kind = conflict_kind_t::bailout_gave_up; - s.m_stats.m_num_bailouts++; - } - - void conflict::set_bailout_lemma() { - SASSERT(m_kind == conflict_kind_t::ok); - m_kind = conflict_kind_t::bailout_lemma; - // s.m_stats.m_num_bailouts++; - } - - struct inference_resolve : public inference { + struct inf_resolve_bool : public inference { sat::literal m_lit; clause const& m_clause; - inference_resolve(sat::literal lit, clause const& cl) : m_lit(lit), m_clause(cl) {} + inf_resolve_bool(sat::literal lit, clause const& cl) : m_lit(lit), m_clause(cl) {} std::ostream& display(std::ostream& out) const override { return out << "Resolve upon " << m_lit << " with " << m_clause; } }; - void conflict::resolve(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 - - SASSERT(contains(lit)); - SASSERT(std::count(cl.begin(), cl.end(), lit) > 0); - SASSERT(!contains(~lit)); - SASSERT(std::count(cl.begin(), cl.end(), ~lit) == 0); - - remove(s.lit2cnstr(lit)); - for (sat::literal lit2 : cl) - if (lit2 != lit) - insert(s.lit2cnstr(~lit2)); - log_inference(inference_resolve(lit, cl)); - } - - struct inference_resolve_with_assignment : public inference { + struct inf_resolve_with_assignment : public inference { solver& s; sat::literal lit; signed_constraint c; - inference_resolve_with_assignment(solver& s, sat::literal lit, signed_constraint c) : s(s), lit(lit), c(c) {} + inf_resolve_with_assignment(solver& s, sat::literal lit, signed_constraint c) : s(s), lit(lit), c(c) {} std::ostream& display(std::ostream& out) const override { out << "Resolve upon " << lit << " with assignment:"; for (pvar v : c->vars()) @@ -397,207 +52,225 @@ namespace polysat { } }; - void conflict::resolve_with_assignment(sat::literal lit, unsigned lvl) { + struct inf_resolve_value : public inference { + solver& s; + pvar v; + inf_resolve_value(solver& s, pvar v) : s(s), v(v) {} + std::ostream& display(std::ostream& out) const override { + return out << "Value resolution with " << assignment_pp(s, v, s.get_value(v), true); + } + }; + + conflict2::conflict2(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); + else + m_logger = alloc(dummy_inference_logger); + } + + inference_logger& conflict2::logger() { + return *m_logger; + } + + bool conflict2::empty() const { + return m_literals.empty() && m_vars.empty() && m_lemmas.empty(); + } + + void conflict2::reset() { + m_literals.reset(); + m_vars.reset(); + m_var_occurrences.reset(); + m_lemmas.reset(); + m_kind = conflict2_kind_t::ok; + SASSERT(empty()); + } + + void conflict2::set_bailout() { + SASSERT(m_kind == conflict2_kind_t::ok); + m_kind = conflict2_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 conflict2::init(signed_constraint c) { + SASSERT(empty()); + if (c.bvalue(s) == l_false) { + // boolean conflict + NOT_IMPLEMENTED_YET(); + } else { + // conflict due to assignment + SASSERT(c.bvalue(s) == l_true); + SASSERT(c.is_currently_false(s)); + insert(c); + insert_vars(c); + } + SASSERT(!empty()); + logger().begin_conflict(); + } + + void conflict2::init(pvar v, bool by_viable_fallback) { + if (by_viable_fallback) { + // 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 { + 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 { + SASSERT(lit != sat::null_literal); + return m_literals.contains(lit.index()); + } + + void conflict2::insert(signed_constraint c) { + if (contains(c)) + return; + if (c.is_always_true()) + return; + LOG("Inserting: " << c); + SASSERT(!c.is_always_false()); // if we added c, the core would be a tautology + SASSERT(!c->vars().empty()); + m_literals.insert(c.blit().index()); + for (pvar v : c->vars()) { + if (v >= m_var_occurrences.size()) + m_var_occurrences.resize(v + 1, 0); + m_var_occurrences[v]++; + } + } + + void conflict2::insert_eval(signed_constraint c) { + switch (c.bvalue(s)) { + case l_undef: + s.assign_eval(c.blit()); + break; + case l_true: + break; + case l_false: + break; + } + insert(c); + } + + void conflict2::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) { + 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) { + // 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 + + SASSERT(contains(lit)); + SASSERT(std::count(cl.begin(), cl.end(), lit) > 0); + SASSERT(!contains(~lit)); + SASSERT(std::count(cl.begin(), cl.end(), ~lit) == 0); + + remove(s.lit2cnstr(lit)); + for (sat::literal other : cl) + if (other != lit) + insert(s.lit2cnstr(~other)); + + logger().log(inf_resolve_bool(lit, cl)); + } + + void conflict2::resolve_with_assignment(sat::literal lit) { // The reason for lit is conceptually: // x1 = v1 /\ ... /\ xn = vn ==> lit SASSERT(contains(lit)); SASSERT(!contains(~lit)); + if (is_backjumping()) + return; + + unsigned const lvl = s.m_bvars.level(lit); signed_constraint c = s.lit2cnstr(lit); + + // If evaluation depends on a decision, + // then we rather keep the more general constraint c instead of inserting "x = v" bool has_decision = false; - for (pvar v : c->vars()) - if (s.is_assigned(v) && s.m_justification[v].is_decision()) + for (pvar v : c->vars()) + if (s.is_assigned(v) && s.m_justification[v].is_decision()) m_bail_vars.insert(v), has_decision = true; if (!has_decision) { remove(c); - for (pvar v : c->vars()) - if (s.is_assigned(v)) { - // TODO: 'lit' was propagated at level 'lvl'; can we here ignore variables above that? - SASSERT(s.get_level(v) <= lvl); - m_vars.insert(v); - } + for (pvar v : c->vars()) + if (s.is_assigned(v) && s.get_level(v) <= lvl) + m_vars.insert(v); } - log_inference(inference_resolve_with_assignment(s, lit, c)); + + logger().log(inf_resolve_with_assignment(s, lit, c)); } - clause_builder conflict::build_lemma() { - LOG_H3("Build lemma from core"); - LOG("core: " << *this); - clause_builder lemma(s); + bool conflict2::resolve_value(pvar v) { + SASSERT(contains_pvar(v)); - 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(); - - if (m_logger) - m_logger->log_lemma(s, lemma); - - return lemma; - } - - void conflict::minimize_vars(signed_constraint c) { - if (m_vars.empty()) - return; - if (!c.is_currently_false(s)) - return; - - 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; - m_vars.reset(); - for (auto const& [v, val] : a) - m_vars.insert(v); - log_inference("minimize vars"); - LOG("reduced " << m_vars); - } - - - struct inference_resolve_value : public inference { - solver& s; - pvar v; - inference_resolve_value(solver& s, pvar v) : s(s), v(v) {} - std::ostream& display(std::ostream& out) const override { - return out << "Value resolution with " << assignment_pp(s, v, s.get_value(v), true); - } - }; - - bool conflict::resolve_value(pvar v) { - // NOTE: - // In the "standard" case where "v = val" is on the stack: - // forbidden interval projection is performed at top level - - SASSERT(v != conflict_var()); - - bool has_saturated = false; - - auto const& j = s.m_justification[v]; - - if (j.is_decision() && m_bail_vars.contains(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; - - s.inc_activity(v); - m_vars.remove(v); - - if (j.is_propagation()) { - for (auto const& c : s.m_viable.get_constraints(v)) - propagate(c); - for (auto const& i : s.m_viable.units(v)) { - propagate(s.eq(i.lo(), i.lo_val())); - propagate(s.eq(i.hi(), i.hi_val())); - } } if (is_bailout()) - goto bailout; + return false; - LOG("try-explain v" << v); - if (try_explain(v)) - return true; + auto const& j = s.m_justification[v]; - // No value resolution method was successful => fall back to saturation and variable elimination - while (s.inc()) { - LOG("try-eliminate v" << v); - // TODO: as a last resort, substitute v by m_value[v]? - if (try_eliminate(v)) - return true; - LOG("try-saturate v" << v); - if (try_saturate(v)) - has_saturated = true; - else - break; + if (j.is_decision() && m_bail_vars.contains(v)) // TODO: what if also m_vars.contains(v)? might have a chance at elimination + return false; + + s.inc_activity(v); + m_vars.remove(v); + + if (j.is_propagation()) { + for (auto const& c : s.m_viable.get_constraints(v)) + insert_eval(c); + for (auto const& i : s.m_viable.units(v)) { + insert_eval(s.eq(i.lo(), i.lo_val())); + insert_eval(s.eq(i.hi(), i.hi_val())); + } } - LOG("bailout v" << v); - if (has_saturated) { - // NOTE: current saturation rules create valid lemmas that do not depend on the variable assignment - set_bailout_lemma(); - return true; - } - else - set_bailout_gave_up(); - bailout: + logger().log(inf_resolve_value(s, v)); + + // TODO: call conflict resolution plugins here; "return true" if successful + + // No conflict resolution plugin succeeded => give up and bail out + set_bailout(); + // Need to keep the variable in case of decision if (s.is_assigned(v) && j.is_decision()) m_vars.insert(v); - log_inference(inference_resolve_value(s, v)); + logger().log("bailout"); return false; } - bool conflict::try_eliminate(pvar v) { - LOG("try v" << v << " contains " << m_vars.contains(v)); - if (m_vars.contains(v)) - return false; - bool has_v = false; - for (auto c : *this) - has_v |= c->contains_var(v); - if (!has_v) - return true; - for (auto* engine : ve_engines) - if (engine->perform(s, v, *this)) - return true; - return false; - } - - bool conflict::try_saturate(pvar v) { - for (auto* engine : inf_engines) - if (engine->perform(v, *this)) - return true; - return false; - } - - bool conflict::try_explain(pvar v) { - for (auto* engine : ex_engines) - if (engine->try_explain(v, *this)) - return true; - return false; - } - - void conflict::set_mark(signed_constraint c) { - sat::bool_var b = c->bvar(); - if (b >= m_bvar2mark.size()) - m_bvar2mark.resize(b + 1); - SASSERT(!m_bvar2mark[b]); - m_bvar2mark[b] = true; - } - - /** - * unset marking on the constraint, but keep variable dependencies. - */ - void conflict::unset_mark(signed_constraint c) { - sat::bool_var b = c->bvar(); - SASSERT(m_bvar2mark[b]); - m_bvar2mark[b] = false; - } - - bool conflict::is_marked(signed_constraint c) const { - return is_marked(c->bvar()); - } - - bool conflict::is_marked(sat::bool_var b) const { - return m_bvar2mark.get(b, false); + std::ostream& conflict2::display(std::ostream& out) const { + out << "TODO\n"; + return out; } } diff --git a/src/math/polysat/conflict.h b/src/math/polysat/conflict.h index ce54f97c5..c99cc4e26 100644 --- a/src/math/polysat/conflict.h +++ b/src/math/polysat/conflict.h @@ -8,30 +8,31 @@ Module Name: Author: Nikolaj Bjorner (nbjorner) 2021-03-19 - Jakob Rath 2021-04-6 + Jakob Rath 2021-04-06 Notes: - A conflict state is of the form - Where Vars are shorthand for the constraints v = value(v) for v in Vars and value(v) is the assignent. - + A conflict state is of the form + Where Vars are shorthand for the constraints v = value(v) for v in Vars and value(v) is the assignment. + Lemmas provide justifications for newly created constraints. + The conflict state is unsatisfiable under background clauses F. Dually, the negation is a consequence of F. Conflict resolution resolves an assignment in the search stack against the conflict state. Assignments are of the form: - + lit <- D => lit - lit is propagated by the clause D => lit - lit <- ? - lit is a decision literal. lit <- asserted - lit is asserted lit <- Vars - lit is propagated from variable evaluation. v = value <- D - v is assigned value by constraints D v = value <- ? - v is a decision literal. - - All literals should be assigned in the stack prior to their use. - + - All literals should be assigned in the stack prior to their use; + or justified by one of the side lemmas. + l <- D => l, < Vars, { l } u C > ===> < Vars, C u D > l <- ?, < Vars, { l } u C > ===> ~l <- (C & Vars = value(Vars) => ~l) l <- asserted, < Vars, { l } u C > ===> < Vars, { l } u C > @@ -40,15 +41,15 @@ Notes: v = value <- D, < Vars u { v }, C > ===> < Vars, D u C > v = value <- ?, < Vars u { v }, C > ===> v != value <- (C & Vars = value(Vars) => v != value) - - + + Example derivations: -Trail: z <= y <- asserted - xz > xy <- asserted - x = a <- ? - y = b <- ? - z = c <- ? +Trail: z <= y <- asserted + xz > xy <- asserted + x = a <- ? + y = b <- ? + z = c <- ? Conflict: < {x, y, z}, xz > xy > when ~O(a,b) and c <= b Append x <= a <- { x } Append y <= b <- { y } @@ -58,7 +59,7 @@ Resolve: y <= b <- { y }, y is a decision variable. Bailout: lemma ~(y >= z & xz > xy & x <= a & y <= b) at decision level of lemma With overflow predicate: -Append ~O(x, y) <- { x, y } +Append ~O(x, y) <- { x, y } Conflict: < {}, y >= z, xz > xy, ~O(x,y) > Based on z <= y & ~O(x,y) => xz <= xy Resolve: ~O(x, y) <- { x, y } both x, y are decision variables @@ -66,8 +67,18 @@ Lemma: y < z or xz <= xy or O(x,y) - - +TODO: +- update notes/example above +- question: if a side lemma justifies a constraint, then we resolve over one of the premises of the lemma; do we want to update the lemma or not? +- conflict resolution plugins + - may generate lemma + - post-processing/simplification on lemma (e.g., literal subsumption; can be done in solver) + - may force backjumping without further conflict resolution (e.g., if applicable lemma was found by global analysis of search state) + - 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?) + + --*/ #pragma once #include "math/polysat/constraint.h" @@ -82,170 +93,88 @@ namespace polysat { class inference_engine; class variable_elimination_engine; class conflict_iterator; - class old_inference_logger; + class inference_logger; - enum class conflict_kind_t { + enum class conflict2_kind_t { + // standard conflict resolution ok, - bailout_gave_up, - bailout_lemma, + // bailout lemma because no appropriate conflict resolution method applies + bailout, + // 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, }; - /** Conflict state, represented as core (~negation of clause). */ - class conflict { + class conflict2 { 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 + unsigned_vector m_var_occurrences; // for each variable, the number of constraints in m_literals that contain it - uint_set m_vars; // variable assignments used as premises - uint_set m_bail_vars; - // If this is not null_var, the conflict was due to empty viable set for this variable. - // Can be treated like "v = x" for any value x. - pvar m_conflict_var = null_var; + // additional lemmas generated during conflict resolution + // 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; - /** Whether we are in a bailout state. - * We enter a bailout state when we give up on proper conflict resolution, - * or want to learn a lemma without fine-grained backtracking. - */ - conflict_kind_t m_kind = conflict_kind_t::ok; - - friend class old_inference_logger; - scoped_ptr m_logger; - - bool_vector m_bvar2mark; // mark of Boolean variables - - void set_mark(signed_constraint c); - void unset_mark(signed_constraint c); - - void minimize_vars(signed_constraint c); - - constraint_manager& cm() const; - scoped_ptr_vector ex_engines; - scoped_ptr_vector ve_engines; - scoped_ptr_vector inf_engines; + conflict2_kind_t m_kind = conflict2_kind_t::ok; public: - conflict(solver& s); - ~conflict(); + conflict2(solver& s); - /// Begin next conflict - void begin_conflict(char const* text = nullptr); - /// Log inference at the current state. - void log_inference(inference const& inf); - void log_inference(char const* name) { log_inference(inference_named(name)); } - void log_var(pvar v); - /// Log relevant part of search state and viable. - void end_conflict(); - - pvar conflict_var() const { return m_conflict_var; } - - bool is_bailout() const { return m_kind != conflict_kind_t::ok; } - bool is_bailout_lemma() const { return m_kind == conflict_kind_t::bailout_lemma; } - void set_bailout_gave_up(); - void set_bailout_lemma(); + inference_logger& logger(); bool empty() const; void reset(); - bool pvar_occurs_in_constraints(pvar v) const { return v < m_var_occurrences.size() && m_var_occurrences[v] > 0; } + uint_set const& vars() const { return m_vars; } - bool contains_pvar(pvar v) const { return m_vars.contains(v) || m_bail_vars.contains(v); } - bool is_marked(signed_constraint c) const; - bool is_marked(sat::bool_var b) const; + bool is_bailout() const { return m_kind == conflict2_kind_t::bailout; } + bool is_backjumping() const { return m_kind == conflict2_kind_t::backjump; } + void set_bailout(); + void set_backjump(); /** conflict because the constraint c is false under current variable assignment */ - void set(signed_constraint c); + void init(signed_constraint c); /** conflict because there is no viable value for the variable v */ - void set(pvar v); - /** all literals in clause are false */ - void set(clause const& cl); + void init(pvar v, bool by_viable_fallback = false); - void propagate(signed_constraint c); - void insert(signed_constraint c); - void insert_vars(signed_constraint c); - void insert(signed_constraint c, vector const& premises); - void remove(signed_constraint c); - void replace(signed_constraint c_old, signed_constraint c_new, vector const& c_new_premises); - - bool contains(signed_constraint c) const; + 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); } - /** Perform boolean resolution with the clause upon variable 'var'. - * Precondition: core/clause contain complementary 'var'-literals. + /** + * Insert constraint c into conflict state. + * + * Skips trivial constraints: + * - e.g., constant constraints such as "4 > 1" */ - void resolve(sat::literal lit, clause const& cl); + void insert(signed_constraint c); - /** lit was fully evaluated under the assignment up to level 'lvl'. - */ - void resolve_with_assignment(sat::literal lit, unsigned lvl); + /** Insert assigned variables of c */ + void insert_vars(signed_constraint c); - /** Perform value resolution by applying various inference rules. - * Returns true if it was possible to eliminate the variable 'v'. - */ + /** Evaluate constraint under assignment and insert it into conflict state. */ + void insert_eval(signed_constraint c); + + /** Remove c from core */ + void remove(signed_constraint c); + + /** Perform boolean resolution with the clause upon the given literal. */ + void resolve_bool(sat::literal lit, clause const& cl); + + /** lit was fully evaluated under the assignment. */ + void resolve_with_assignment(sat::literal lit); + + /** Perform resolution with "v = value <- ..." */ bool resolve_value(pvar v); - /** Convert the core into a lemma to be learned. */ - clause_builder build_lemma(); - - bool try_eliminate(pvar v); - bool try_saturate(pvar v); - bool try_explain(pvar v); - - using const_iterator = conflict_iterator; - const_iterator begin() const; - const_iterator end() const; - - uint_set const& vars() const { return m_vars; } - uint_set const& bail_vars() const { return m_bail_vars; } - std::ostream& display(std::ostream& out) const; }; - inline std::ostream& operator<<(std::ostream& out, conflict const& c) { return c.display(out); } + inline std::ostream& operator<<(std::ostream& out, conflict2 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); } - }; - - - inline conflict::const_iterator conflict::begin() const { return conflict_iterator::begin(cm(), m_literals); } - inline conflict::const_iterator conflict::end() const { return conflict_iterator::end(cm(), m_literals); } } diff --git a/src/math/polysat/conflict2.cpp b/src/math/polysat/conflict2.cpp deleted file mode 100644 index f7a9acfff..000000000 --- a/src/math/polysat/conflict2.cpp +++ /dev/null @@ -1,276 +0,0 @@ -/*++ -Copyright (c) 2021 Microsoft Corporation - -Module Name: - - polysat conflict - -Author: - - Nikolaj Bjorner (nbjorner) 2021-03-19 - Jakob Rath 2021-04-06 - -Notes: - ---*/ - -#include "math/polysat/conflict2.h" -#include "math/polysat/solver.h" -#include "math/polysat/inference_logger.h" -#include "math/polysat/log.h" -#include "math/polysat/log_helper.h" -#include "math/polysat/explain.h" -#include "math/polysat/eq_explain.h" -#include "math/polysat/forbidden_intervals.h" -#include "math/polysat/saturation.h" -#include "math/polysat/variable_elimination.h" -#include -#include - -namespace polysat { - - struct inf_resolve_bool : public inference { - sat::literal m_lit; - clause const& m_clause; - inf_resolve_bool(sat::literal lit, clause const& cl) : m_lit(lit), m_clause(cl) {} - std::ostream& display(std::ostream& out) const override { - return out << "Resolve upon " << m_lit << " with " << m_clause; - } - }; - - struct inf_resolve_with_assignment : public inference { - solver& s; - sat::literal lit; - signed_constraint c; - inf_resolve_with_assignment(solver& s, sat::literal lit, signed_constraint c) : s(s), lit(lit), c(c) {} - std::ostream& display(std::ostream& out) const override { - out << "Resolve upon " << lit << " with assignment:"; - for (pvar v : c->vars()) - if (s.is_assigned(v)) - out << " " << assignment_pp(s, v, s.get_value(v), true); - return out; - } - }; - - struct inf_resolve_value : public inference { - solver& s; - pvar v; - inf_resolve_value(solver& s, pvar v) : s(s), v(v) {} - std::ostream& display(std::ostream& out) const override { - return out << "Value resolution with " << assignment_pp(s, v, s.get_value(v), true); - } - }; - - conflict2::conflict2(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); - else - m_logger = alloc(dummy_inference_logger); - } - - inference_logger& conflict2::logger() { - return *m_logger; - } - - bool conflict2::empty() const { - return m_literals.empty() && m_vars.empty() && m_lemmas.empty(); - } - - void conflict2::reset() { - m_literals.reset(); - m_vars.reset(); - m_var_occurrences.reset(); - m_lemmas.reset(); - m_kind = conflict2_kind_t::ok; - SASSERT(empty()); - } - - void conflict2::set_bailout() { - SASSERT(m_kind == conflict2_kind_t::ok); - m_kind = conflict2_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 conflict2::init(signed_constraint c) { - SASSERT(empty()); - if (c.bvalue(s) == l_false) { - // boolean conflict - NOT_IMPLEMENTED_YET(); - } else { - // conflict due to assignment - SASSERT(c.bvalue(s) == l_true); - SASSERT(c.is_currently_false(s)); - insert(c); - insert_vars(c); - } - SASSERT(!empty()); - logger().begin_conflict(); - } - - void conflict2::init(pvar v, bool by_viable_fallback) { - if (by_viable_fallback) { - // 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 { - 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 { - SASSERT(lit != sat::null_literal); - return m_literals.contains(lit.index()); - } - - void conflict2::insert(signed_constraint c) { - if (contains(c)) - return; - if (c.is_always_true()) - return; - LOG("Inserting: " << c); - SASSERT(!c.is_always_false()); // if we added c, the core would be a tautology - SASSERT(!c->vars().empty()); - m_literals.insert(c.blit().index()); - for (pvar v : c->vars()) { - if (v >= m_var_occurrences.size()) - m_var_occurrences.resize(v + 1, 0); - m_var_occurrences[v]++; - } - } - - void conflict2::insert_eval(signed_constraint c) { - switch (c.bvalue(s)) { - case l_undef: - s.assign_eval(c.blit()); - break; - case l_true: - break; - case l_false: - break; - } - insert(c); - } - - void conflict2::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) { - 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) { - // 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 - - SASSERT(contains(lit)); - SASSERT(std::count(cl.begin(), cl.end(), lit) > 0); - SASSERT(!contains(~lit)); - SASSERT(std::count(cl.begin(), cl.end(), ~lit) == 0); - - remove(s.lit2cnstr(lit)); - for (sat::literal other : cl) - if (other != lit) - insert(s.lit2cnstr(~other)); - - logger().log(inf_resolve_bool(lit, cl)); - } - - void conflict2::resolve_with_assignment(sat::literal lit) { - // The reason for lit is conceptually: - // x1 = v1 /\ ... /\ xn = vn ==> lit - - SASSERT(contains(lit)); - SASSERT(!contains(~lit)); - - if (is_backjumping()) - return; - - unsigned const lvl = s.m_bvars.level(lit); - signed_constraint c = s.lit2cnstr(lit); - - // If evaluation depends on a decision, - // then we rather keep the more general constraint c instead of inserting "x = v" - bool has_decision = false; - for (pvar v : c->vars()) - if (s.is_assigned(v) && s.m_justification[v].is_decision()) - m_bail_vars.insert(v), has_decision = true; - - if (!has_decision) { - remove(c); - for (pvar v : c->vars()) - if (s.is_assigned(v) && s.get_level(v) <= lvl) - m_vars.insert(v); - } - - 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; - } - - if (is_bailout()) - return false; - - 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 - return false; - - s.inc_activity(v); - m_vars.remove(v); - - if (j.is_propagation()) { - for (auto const& c : s.m_viable.get_constraints(v)) - insert_eval(c); - for (auto const& i : s.m_viable.units(v)) { - insert_eval(s.eq(i.lo(), i.lo_val())); - insert_eval(s.eq(i.hi(), i.hi_val())); - } - } - logger().log(inf_resolve_value(s, v)); - - // TODO: call conflict resolution plugins here; "return true" if successful - - // No conflict resolution plugin succeeded => give up and bail out - set_bailout(); - // Need to keep the variable in case of decision - if (s.is_assigned(v) && j.is_decision()) - m_vars.insert(v); - logger().log("bailout"); - return false; - } - - std::ostream& conflict2::display(std::ostream& out) const { - out << "TODO\n"; - return out; - } -} diff --git a/src/math/polysat/conflict2.h b/src/math/polysat/conflict2.h deleted file mode 100644 index c99cc4e26..000000000 --- a/src/math/polysat/conflict2.h +++ /dev/null @@ -1,180 +0,0 @@ -/*++ -Copyright (c) 2021 Microsoft Corporation - -Module Name: - - polysat conflict - -Author: - - Nikolaj Bjorner (nbjorner) 2021-03-19 - Jakob Rath 2021-04-06 - -Notes: - - A conflict state is of the form - Where Vars are shorthand for the constraints v = value(v) for v in Vars and value(v) is the assignment. - Lemmas provide justifications for newly created constraints. - - The conflict state is unsatisfiable under background clauses F. - Dually, the negation is a consequence of F. - - Conflict resolution resolves an assignment in the search stack against the conflict state. - - Assignments are of the form: - - lit <- D => lit - lit is propagated by the clause D => lit - lit <- asserted - lit is asserted - lit <- Vars - lit is propagated from variable evaluation. - - v = value <- D - v is assigned value by constraints D - v = value <- ? - v is a decision literal. - - - All literals should be assigned in the stack prior to their use; - or justified by one of the side lemmas. - - l <- D => l, < Vars, { l } u C > ===> < Vars, C u D > - l <- ?, < Vars, { l } u C > ===> ~l <- (C & Vars = value(Vars) => ~l) - l <- asserted, < Vars, { l } u C > ===> < Vars, { l } u C > - l <- Vars', < Vars, { l } u C > ===> < Vars u Vars', C > if all Vars' are propagated - l <- Vars', < Vars, { l } u C > ===> Mark < Vars, { l } u C > as bailout - - v = value <- D, < Vars u { v }, C > ===> < Vars, D u C > - v = value <- ?, < Vars u { v }, C > ===> v != value <- (C & Vars = value(Vars) => v != value) - - -Example derivations: - -Trail: z <= y <- asserted - xz > xy <- asserted - x = a <- ? - y = b <- ? - z = c <- ? -Conflict: < {x, y, z}, xz > xy > when ~O(a,b) and c <= b -Append x <= a <- { x } -Append y <= b <- { y } -Conflict: < {}, y >= z, xz > xy, x <= a, y <= b > -Based on: z <= y & x <= a & y <= b => xz <= xy -Resolve: y <= b <- { y }, y is a decision variable. -Bailout: lemma ~(y >= z & xz > xy & x <= a & y <= b) at decision level of lemma - -With overflow predicate: -Append ~O(x, y) <- { x, y } -Conflict: < {}, y >= z, xz > xy, ~O(x,y) > -Based on z <= y & ~O(x,y) => xz <= xy -Resolve: ~O(x, y) <- { x, y } both x, y are decision variables -Lemma: y < z or xz <= xy or O(x,y) - - - -TODO: -- update notes/example above -- question: if a side lemma justifies a constraint, then we resolve over one of the premises of the lemma; do we want to update the lemma or not? -- conflict resolution plugins - - may generate lemma - - post-processing/simplification on lemma (e.g., literal subsumption; can be done in solver) - - may force backjumping without further conflict resolution (e.g., if applicable lemma was found by global analysis of search state) - - 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?) - - ---*/ -#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 { - // standard conflict resolution - ok, - // bailout lemma because no appropriate conflict resolution method applies - bailout, - // 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 { - 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 - - unsigned_vector m_var_occurrences; // for each variable, the number of constraints in m_literals that contain it - - // additional lemmas generated during conflict resolution - // 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; - - public: - conflict2(solver& s); - - inference_logger& logger(); - - bool empty() const; - void reset(); - - uint_set const& vars() const { return m_vars; } - - bool is_bailout() const { return m_kind == conflict2_kind_t::bailout; } - bool is_backjumping() const { return m_kind == conflict2_kind_t::backjump; } - void set_bailout(); - void set_backjump(); - - /** conflict because the constraint c is false under current variable assignment */ - void init(signed_constraint c); - /** conflict because there is no viable value for the variable v */ - void init(pvar v, bool by_viable_fallback = false); - - 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); } - - /** - * Insert constraint c into conflict state. - * - * Skips trivial constraints: - * - e.g., constant constraints such as "4 > 1" - */ - void insert(signed_constraint c); - - /** 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); - - /** Remove c from core */ - void remove(signed_constraint c); - - /** Perform boolean resolution with the clause upon the given literal. */ - void resolve_bool(sat::literal lit, clause const& cl); - - /** lit was fully evaluated under the assignment. */ - void resolve_with_assignment(sat::literal lit); - - /** Perform resolution with "v = value <- ..." */ - bool resolve_value(pvar v); - - std::ostream& display(std::ostream& out) const; - }; - - inline std::ostream& operator<<(std::ostream& out, conflict2 const& c) { return c.display(out); } - -} diff --git a/src/math/polysat/conflict_old.cpp b/src/math/polysat/conflict_old.cpp new file mode 100644 index 000000000..07ef61247 --- /dev/null +++ b/src/math/polysat/conflict_old.cpp @@ -0,0 +1,603 @@ +/*++ +Copyright (c) 2021 Microsoft Corporation + +Module Name: + + polysat conflict + +Author: + + Nikolaj Bjorner (nbjorner) 2021-03-19 + Jakob Rath 2021-04-6 + +Notes: + + TODO: try a final core reduction step or other core minimization + + TODO: revert(pvar v) is too weak. + It should apply saturation rules currently only available for propagated values. + + TODO: dependency tracking for constraints evaluating to false should be minimized. + +--*/ + +#include "math/polysat/conflict.h" +#include "math/polysat/solver.h" +#include "math/polysat/log.h" +#include "math/polysat/log_helper.h" +#include "math/polysat/explain.h" +#include "math/polysat/eq_explain.h" +#include "math/polysat/forbidden_intervals.h" +#include "math/polysat/saturation.h" +#include "math/polysat/variable_elimination.h" +#include +#include + +namespace polysat { + + class old_inference_logger { + uint_set m_used_constraints; + uint_set m_used_vars; + scoped_ptr m_out = nullptr; + unsigned m_conflicts = 0; + + friend class conflict; + + std::ostream& out() { + SASSERT(m_out); + return *m_out; + } + + std::ostream& out_indent() { return out() << " "; } + + std::string hline() const { return std::string(70, '-'); } + + public: + void begin_conflict(char const* text) { + ++m_conflicts; + if (text) + LOG("Begin CONFLICT #" << m_conflicts << " (" << text << ")"); + else + LOG("Begin CONFLICT #" << m_conflicts); + 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_conflicts << " (" << text << ")" << "\n"; + } + + void log_inference(conflict const& core, inference const* inf) { + out() << hline() << "\n"; + if (inf) + out() << *inf << "\n"; + if (core.conflict_var() != null_var) { + out_indent() << "Conflict var: " << core.conflict_var() << "\n"; + m_used_vars.insert(core.conflict_var()); + } + for (auto const& c : core) { + out_indent() << c.blit() << ": " << c << '\n'; + m_used_constraints.insert(c.blit().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"; + 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"; + m_used_vars.insert(v); + } + if (core.is_bailout()) + out_indent() << "(bailout)\n"; + out().flush(); + } + + void log_lemma(solver const& s, clause_builder const& cb) { + out() << hline() << "\nLemma:"; + for (auto const& lit : cb) + out() << " " << lit; + out() << "\n"; + for (auto const& lit : cb) + out_indent() << lit << ": " << s.lit2cnstr(lit) << '\n'; + out().flush(); + } + + void end_conflict(search_state const& search, viable const& v) { + out() << "\n" << hline() << "\n\n"; + out() << "Search state (part):\n"; + for (auto const& item : search) + if (is_relevant(item)) + out_indent() << search_item_pp(search, item, true) << "\n"; + out() << hline() << "\nViable (part):\n"; + for (pvar var : m_used_vars) + out_indent() << "v" << std::setw(3) << std::left << var << ": " << viable::var_pp(v, var) << "\n"; + out().flush(); + LOG("End CONFLICT #" << m_conflicts); + } + + bool is_relevant(search_item const& item) const { + switch (item.kind()) { + case search_item_k::assignment: + return m_used_vars.contains(item.var()); + case search_item_k::boolean: + return m_used_constraints.contains(item.lit().index()); + } + UNREACHABLE(); + return false; + } + }; + + void conflict::log_var(pvar v) { + if (m_logger) + m_logger->m_used_vars.insert(v); + } + + conflict::conflict(solver& s): s(s) { + ex_engines.push_back(alloc(ex_polynomial_superposition, s)); + ex_engines.push_back(alloc(eq_explain, s)); + ve_engines.push_back(alloc(ve_reduction)); + inf_engines.push_back(alloc(inf_saturate, s)); + // TODO: how to set this on the CLI? "polysat.log_conflicts=true" doesn't seem to work although z3 accepts it + if (true || s.get_config().m_log_conflicts) + m_logger = alloc(old_inference_logger); + } + + conflict::~conflict() {} + + void conflict::begin_conflict(char const* text) { + if (m_logger) { + m_logger->begin_conflict(text); + // log initial conflict state + m_logger->log_inference(*this, nullptr); + } + } + + void conflict::log_inference(inference const& inf) { + if (m_logger) + m_logger->log_inference(*this, &inf); + } + + void conflict::end_conflict() { + if (m_logger) + m_logger->end_conflict(s.m_search, s.m_viable); + } + + constraint_manager& conflict::cm() const { return s.m_constraints; } + + 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; + } + + bool conflict::empty() const { + return m_literals.empty() + && m_vars.empty() + && m_bail_vars.empty() + && m_conflict_var == null_var; + } + + void conflict::reset() { + for (auto c : *this) + unset_mark(c); + m_literals.reset(); + m_vars.reset(); + m_var_occurrences.reset(); + m_bail_vars.reset(); + m_conflict_var = null_var; + m_kind = conflict_kind_t::ok; + SASSERT(empty()); + } + + /** + * The constraint is false under the current assignment of variables. + * The core is then the conjuction of this constraint and assigned variables. + */ + void conflict::set(signed_constraint c) { + LOG("Conflict: " << c << " " << c.bvalue(s)); + SASSERT(empty()); + if (c.bvalue(s) == l_false) { + auto* cl = s.m_bvars.reason(c.blit().var()); + if (cl) + set(*cl); + else + insert(c); + } + else { + SASSERT(c.is_currently_false(s)); + // TBD: fails with test_subst SASSERT(c.bvalue(s) == l_true); + insert_vars(c); + insert(c); + } + SASSERT(!empty()); + } + + /** + * The variable v cannot be assigned. + * The conflict is the set of justifications accumulated for the viable values for v. + * These constraints are (in the current form) not added to the core, but passed directly + * to the forbidden interval module. + * A consistent approach could be to add these constraints to the core and then also include the + * variable assignments. + */ + void conflict::set(pvar v) { + LOG("Conflict: v" << v); + SASSERT(empty()); + m_conflict_var = v; + SASSERT(!empty()); + } + + /** + * The clause is conflicting in the current search state. + */ + void conflict::set(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()); + } + + /** + * Insert constraint into conflict state + * Skip trivial constraints + * - e.g., constant ones such as "4 > 1"... only true ones + * should appear, otherwise the lemma would be a tautology + */ + void conflict::insert(signed_constraint c) { + if (c.is_always_true()) + return; + if (is_marked(c)) + return; + LOG("inserting: " << c); + SASSERT(!c->vars().empty()); + set_mark(c); + m_literals.insert(c.blit().index()); + for (pvar v : c->vars()) { + if (v >= m_var_occurrences.size()) + m_var_occurrences.resize(v + 1, 0); + m_var_occurrences[v]++; + } + } + + void conflict::propagate(signed_constraint c) { + switch (c.bvalue(s)) { + case l_undef: + s.assign_eval(c.blit()); + break; + case l_true: + break; + case l_false: + break; + } + insert(c); + } + + void conflict::insert_vars(signed_constraint c) { + for (pvar v : c->vars()) + if (s.is_assigned(v)) + m_vars.insert(v); + } + + /** + * Premises can either be justified by a Clause or by a value assignment. + * Premises that are justified by value assignments are not assigned (the bvalue is l_undef) + * The justification for those premises are based on the free assigned variables. + * + * NOTE: maybe we should skip intermediate steps and just collect the leaf premises for c? + * Ensure that c is assigned and justified + */ + // TODO: rename this; it pushes onto \Gamma and doesn't insert into the core + void conflict::insert(signed_constraint c, vector const& premises) { + // keep(c); + clause_builder c_lemma(s); + for (auto premise : premises) { + LOG_H3("premise: " << premise); + // keep(premise); + SASSERT(premise.bvalue(s) != l_false); + c_lemma.push(~premise.blit()); + } + c_lemma.push(c.blit()); + clause_ref lemma = c_lemma.build(); + SASSERT(lemma); + cm().store(lemma.get(), s, false); + if (c.bvalue(s) == l_undef) + s.assign_propagate(c.blit(), *lemma); + } + + void conflict::remove(signed_constraint c) { + unset_mark(c); + m_literals.remove(c.blit().index()); + for (pvar v : c->vars()) { + if (v < m_var_occurrences.size()) + m_var_occurrences[v]--; + } + } + + void conflict::replace(signed_constraint c_old, signed_constraint c_new, vector const& c_new_premises) { + remove(c_old); + insert(c_new, c_new_premises); + } + + bool conflict::contains(signed_constraint c) const { + return m_literals.contains(c.blit().index()); + } + + bool conflict::contains(sat::literal lit) const { + SASSERT(lit != sat::null_literal); + return m_literals.contains(lit.index()); + } + + void conflict::set_bailout_gave_up() { + SASSERT(m_kind == conflict_kind_t::ok); + m_kind = conflict_kind_t::bailout_gave_up; + s.m_stats.m_num_bailouts++; + } + + void conflict::set_bailout_lemma() { + SASSERT(m_kind == conflict_kind_t::ok); + m_kind = conflict_kind_t::bailout_lemma; + // s.m_stats.m_num_bailouts++; + } + + struct inference_resolve : public inference { + sat::literal m_lit; + clause const& m_clause; + inference_resolve(sat::literal lit, clause const& cl) : m_lit(lit), m_clause(cl) {} + std::ostream& display(std::ostream& out) const override { + return out << "Resolve upon " << m_lit << " with " << m_clause; + } + }; + + void conflict::resolve(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 + + SASSERT(contains(lit)); + SASSERT(std::count(cl.begin(), cl.end(), lit) > 0); + SASSERT(!contains(~lit)); + SASSERT(std::count(cl.begin(), cl.end(), ~lit) == 0); + + remove(s.lit2cnstr(lit)); + for (sat::literal lit2 : cl) + if (lit2 != lit) + insert(s.lit2cnstr(~lit2)); + log_inference(inference_resolve(lit, cl)); + } + + struct inference_resolve_with_assignment : public inference { + solver& s; + sat::literal lit; + signed_constraint c; + inference_resolve_with_assignment(solver& s, sat::literal lit, signed_constraint c) : s(s), lit(lit), c(c) {} + std::ostream& display(std::ostream& out) const override { + out << "Resolve upon " << lit << " with assignment:"; + for (pvar v : c->vars()) + if (s.is_assigned(v)) + out << " " << assignment_pp(s, v, s.get_value(v), true); + return out; + } + }; + + void conflict::resolve_with_assignment(sat::literal lit, unsigned lvl) { + // The reason for lit is conceptually: + // x1 = v1 /\ ... /\ xn = vn ==> lit + + SASSERT(contains(lit)); + SASSERT(!contains(~lit)); + + signed_constraint c = s.lit2cnstr(lit); + bool has_decision = false; + for (pvar v : c->vars()) + if (s.is_assigned(v) && s.m_justification[v].is_decision()) + m_bail_vars.insert(v), has_decision = true; + + if (!has_decision) { + remove(c); + for (pvar v : c->vars()) + if (s.is_assigned(v)) { + // TODO: 'lit' was propagated at level 'lvl'; can we here ignore variables above that? + SASSERT(s.get_level(v) <= lvl); + m_vars.insert(v); + } + } + log_inference(inference_resolve_with_assignment(s, lit, c)); + } + + clause_builder conflict::build_lemma() { + LOG_H3("Build lemma from core"); + LOG("core: " << *this); + clause_builder lemma(s); + + 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(); + + if (m_logger) + m_logger->log_lemma(s, lemma); + + return lemma; + } + + void conflict::minimize_vars(signed_constraint c) { + if (m_vars.empty()) + return; + if (!c.is_currently_false(s)) + return; + + 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; + m_vars.reset(); + for (auto const& [v, val] : a) + m_vars.insert(v); + log_inference("minimize vars"); + LOG("reduced " << m_vars); + } + + + struct inference_resolve_value : public inference { + solver& s; + pvar v; + inference_resolve_value(solver& s, pvar v) : s(s), v(v) {} + std::ostream& display(std::ostream& out) const override { + return out << "Value resolution with " << assignment_pp(s, v, s.get_value(v), true); + } + }; + + bool conflict::resolve_value(pvar v) { + // NOTE: + // In the "standard" case where "v = val" is on the stack: + // forbidden interval projection is performed at top level + + SASSERT(v != conflict_var()); + + bool has_saturated = false; + + auto const& j = s.m_justification[v]; + + if (j.is_decision() && m_bail_vars.contains(v)) + return false; + + s.inc_activity(v); + m_vars.remove(v); + + if (j.is_propagation()) { + for (auto const& c : s.m_viable.get_constraints(v)) + propagate(c); + for (auto const& i : s.m_viable.units(v)) { + propagate(s.eq(i.lo(), i.lo_val())); + propagate(s.eq(i.hi(), i.hi_val())); + } + } + + if (is_bailout()) + goto bailout; + + LOG("try-explain v" << v); + if (try_explain(v)) + return true; + + // No value resolution method was successful => fall back to saturation and variable elimination + while (s.inc()) { + LOG("try-eliminate v" << v); + // TODO: as a last resort, substitute v by m_value[v]? + if (try_eliminate(v)) + return true; + LOG("try-saturate v" << v); + if (try_saturate(v)) + has_saturated = true; + else + break; + } + LOG("bailout v" << v); + if (has_saturated) { + // NOTE: current saturation rules create valid lemmas that do not depend on the variable assignment + set_bailout_lemma(); + return true; + } + else + set_bailout_gave_up(); + bailout: + if (s.is_assigned(v) && j.is_decision()) + m_vars.insert(v); + log_inference(inference_resolve_value(s, v)); + return false; + } + + bool conflict::try_eliminate(pvar v) { + LOG("try v" << v << " contains " << m_vars.contains(v)); + if (m_vars.contains(v)) + return false; + bool has_v = false; + for (auto c : *this) + has_v |= c->contains_var(v); + if (!has_v) + return true; + for (auto* engine : ve_engines) + if (engine->perform(s, v, *this)) + return true; + return false; + } + + bool conflict::try_saturate(pvar v) { + for (auto* engine : inf_engines) + if (engine->perform(v, *this)) + return true; + return false; + } + + bool conflict::try_explain(pvar v) { + for (auto* engine : ex_engines) + if (engine->try_explain(v, *this)) + return true; + return false; + } + + void conflict::set_mark(signed_constraint c) { + sat::bool_var b = c->bvar(); + if (b >= m_bvar2mark.size()) + m_bvar2mark.resize(b + 1); + SASSERT(!m_bvar2mark[b]); + m_bvar2mark[b] = true; + } + + /** + * unset marking on the constraint, but keep variable dependencies. + */ + void conflict::unset_mark(signed_constraint c) { + sat::bool_var b = c->bvar(); + SASSERT(m_bvar2mark[b]); + m_bvar2mark[b] = false; + } + + bool conflict::is_marked(signed_constraint c) const { + return is_marked(c->bvar()); + } + + bool conflict::is_marked(sat::bool_var b) const { + return m_bvar2mark.get(b, false); + } +} diff --git a/src/math/polysat/conflict_old.h b/src/math/polysat/conflict_old.h new file mode 100644 index 000000000..ce54f97c5 --- /dev/null +++ b/src/math/polysat/conflict_old.h @@ -0,0 +1,251 @@ +/*++ +Copyright (c) 2021 Microsoft Corporation + +Module Name: + + polysat conflict + +Author: + + Nikolaj Bjorner (nbjorner) 2021-03-19 + Jakob Rath 2021-04-6 + +Notes: + + A conflict state is of the form + Where Vars are shorthand for the constraints v = value(v) for v in Vars and value(v) is the assignent. + + The conflict state is unsatisfiable under background clauses F. + Dually, the negation is a consequence of F. + + Conflict resolution resolves an assignment in the search stack against the conflict state. + + Assignments are of the form: + + lit <- D => lit - lit is propagated by the clause D => lit + lit <- ? - lit is a decision literal. + lit <- asserted - lit is asserted + lit <- Vars - lit is propagated from variable evaluation. + + v = value <- D - v is assigned value by constraints D + v = value <- ? - v is a decision literal. + + - All literals should be assigned in the stack prior to their use. + + l <- D => l, < Vars, { l } u C > ===> < Vars, C u D > + l <- ?, < Vars, { l } u C > ===> ~l <- (C & Vars = value(Vars) => ~l) + l <- asserted, < Vars, { l } u C > ===> < Vars, { l } u C > + l <- Vars', < Vars, { l } u C > ===> < Vars u Vars', C > if all Vars' are propagated + l <- Vars', < Vars, { l } u C > ===> Mark < Vars, { l } u C > as bailout + + v = value <- D, < Vars u { v }, C > ===> < Vars, D u C > + v = value <- ?, < Vars u { v }, C > ===> v != value <- (C & Vars = value(Vars) => v != value) + + +Example derivations: + +Trail: z <= y <- asserted + xz > xy <- asserted + x = a <- ? + y = b <- ? + z = c <- ? +Conflict: < {x, y, z}, xz > xy > when ~O(a,b) and c <= b +Append x <= a <- { x } +Append y <= b <- { y } +Conflict: < {}, y >= z, xz > xy, x <= a, y <= b > +Based on: z <= y & x <= a & y <= b => xz <= xy +Resolve: y <= b <- { y }, y is a decision variable. +Bailout: lemma ~(y >= z & xz > xy & x <= a & y <= b) at decision level of lemma + +With overflow predicate: +Append ~O(x, y) <- { x, y } +Conflict: < {}, y >= z, xz > xy, ~O(x,y) > +Based on z <= y & ~O(x,y) => xz <= xy +Resolve: ~O(x, y) <- { x, y } both x, y are decision variables +Lemma: y < z or xz <= xy or O(x,y) + + + + + +--*/ +#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 old_inference_logger; + + enum class conflict_kind_t { + ok, + bailout_gave_up, + bailout_lemma, + }; + + /** Conflict state, represented as core (~negation of clause). */ + class conflict { + solver& s; + indexed_uint_set m_literals; // set of boolean literals in the conflict + unsigned_vector m_var_occurrences; // for each variable, the number of constraints in m_literals that contain it + uint_set m_vars; // variable assignments used as premises + uint_set m_bail_vars; + + // If this is not null_var, the conflict was due to empty viable set for this variable. + // Can be treated like "v = x" for any value x. + pvar m_conflict_var = null_var; + + /** Whether we are in a bailout state. + * We enter a bailout state when we give up on proper conflict resolution, + * or want to learn a lemma without fine-grained backtracking. + */ + conflict_kind_t m_kind = conflict_kind_t::ok; + + friend class old_inference_logger; + scoped_ptr m_logger; + + bool_vector m_bvar2mark; // mark of Boolean variables + + void set_mark(signed_constraint c); + void unset_mark(signed_constraint c); + + void minimize_vars(signed_constraint c); + + constraint_manager& cm() const; + scoped_ptr_vector ex_engines; + scoped_ptr_vector ve_engines; + scoped_ptr_vector inf_engines; + + public: + conflict(solver& s); + ~conflict(); + + /// Begin next conflict + void begin_conflict(char const* text = nullptr); + /// Log inference at the current state. + void log_inference(inference const& inf); + void log_inference(char const* name) { log_inference(inference_named(name)); } + void log_var(pvar v); + /// Log relevant part of search state and viable. + void end_conflict(); + + pvar conflict_var() const { return m_conflict_var; } + + bool is_bailout() const { return m_kind != conflict_kind_t::ok; } + bool is_bailout_lemma() const { return m_kind == conflict_kind_t::bailout_lemma; } + void set_bailout_gave_up(); + void set_bailout_lemma(); + + bool empty() const; + void reset(); + + bool pvar_occurs_in_constraints(pvar v) const { return v < m_var_occurrences.size() && m_var_occurrences[v] > 0; } + + bool contains_pvar(pvar v) const { return m_vars.contains(v) || m_bail_vars.contains(v); } + bool is_marked(signed_constraint c) const; + bool is_marked(sat::bool_var b) const; + + /** conflict because the constraint c is false under current variable assignment */ + void set(signed_constraint c); + /** conflict because there is no viable value for the variable v */ + void set(pvar v); + /** all literals in clause are false */ + void set(clause const& cl); + + void propagate(signed_constraint c); + void insert(signed_constraint c); + void insert_vars(signed_constraint c); + void insert(signed_constraint c, vector const& premises); + void remove(signed_constraint c); + void replace(signed_constraint c_old, signed_constraint c_new, vector const& c_new_premises); + + bool contains(signed_constraint c) const; + bool contains(sat::literal lit) const; + + /** Perform boolean resolution with the clause upon variable 'var'. + * Precondition: core/clause contain complementary 'var'-literals. + */ + void resolve(sat::literal lit, clause const& cl); + + /** lit was fully evaluated under the assignment up to level 'lvl'. + */ + void resolve_with_assignment(sat::literal lit, unsigned lvl); + + /** Perform value resolution by applying various inference rules. + * Returns true if it was possible to eliminate the variable 'v'. + */ + bool resolve_value(pvar v); + + /** Convert the core into a lemma to be learned. */ + clause_builder build_lemma(); + + bool try_eliminate(pvar v); + bool try_saturate(pvar v); + bool try_explain(pvar v); + + using const_iterator = conflict_iterator; + const_iterator begin() const; + const_iterator end() const; + + uint_set const& vars() const { return m_vars; } + uint_set const& bail_vars() const { return m_bail_vars; } + + std::ostream& display(std::ostream& out) const; + }; + + 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); } + }; + + + inline conflict::const_iterator conflict::begin() const { return conflict_iterator::begin(cm(), m_literals); } + inline conflict::const_iterator conflict::end() const { return conflict_iterator::end(cm(), m_literals); } +}