diff --git a/src/math/polysat/conflict.cpp b/src/math/polysat/conflict.cpp index db6a53271..05e699a22 100644 --- a/src/math/polysat/conflict.cpp +++ b/src/math/polysat/conflict.cpp @@ -100,9 +100,6 @@ namespace polysat { for (auto const& lit : cb) out_indent() << lit << ": " << s.lit2cnstr(lit) << '\n'; out().flush(); - - // if (m_conflicts == 9) - // std::exit(0); } void end_conflict(search_state const& search, viable const& v) { @@ -197,7 +194,7 @@ namespace polysat { m_var_occurrences.reset(); m_bail_vars.reset(); m_conflict_var = null_var; - m_bailout = false; + m_kind = conflict_kind_t::ok; SASSERT(empty()); } @@ -345,12 +342,18 @@ namespace polysat { return m_literals.contains(lit.index()); } - void conflict::set_bailout() { - SASSERT(!is_bailout()); - m_bailout = true; + 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; @@ -487,6 +490,8 @@ namespace polysat { SASSERT(v != conflict_var()); + bool has_saturated = false; + auto const& j = s.m_justification[v]; if (j.is_decision() && m_bail_vars.contains(v)) @@ -517,11 +522,20 @@ namespace polysat { // TODO: as a last resort, substitute v by m_value[v]? if (try_eliminate(v)) return true; - if (!try_saturate(v)) + LOG("try-saturate v" << v); + if (try_saturate(v)) + has_saturated = true; + else break; } LOG("bailout v" << v); - set_bailout(); + 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); diff --git a/src/math/polysat/conflict.h b/src/math/polysat/conflict.h index e11afb79f..5cc314a47 100644 --- a/src/math/polysat/conflict.h +++ b/src/math/polysat/conflict.h @@ -98,6 +98,12 @@ namespace polysat { std::ostream& display(std::ostream& out) const override { return out << m_name; } }; + enum class conflict_kind_t { + ok, + bailout_gave_up, + bailout_lemma, + }; + /** Conflict state, represented as core (~negation of clause). */ class conflict { solver& s; @@ -106,13 +112,19 @@ namespace polysat { uint_set m_vars; // variable assignments used as premises uint_set m_bail_vars; - friend class inference_logger; - scoped_ptr m_logger; - // 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 inference_logger; + scoped_ptr m_logger; + bool_vector m_bvar2mark; // mark of Boolean variables void set_mark(signed_constraint c); @@ -120,9 +132,6 @@ namespace polysat { void minimize_vars(signed_constraint c); - /** Whether we are in a bailout state. We enter a bailout state when we give up on proper conflict resolution. */ - bool m_bailout = false; - constraint_manager& cm() const; scoped_ptr_vector ex_engines; scoped_ptr_vector ve_engines; @@ -143,9 +152,10 @@ namespace polysat { pvar conflict_var() const { return m_conflict_var; } - bool is_bailout() const { return m_bailout; } - - void set_bailout(); + 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(); diff --git a/src/math/polysat/saturation.cpp b/src/math/polysat/saturation.cpp index e85202bb6..96869bbe9 100644 --- a/src/math/polysat/saturation.cpp +++ b/src/math/polysat/saturation.cpp @@ -73,6 +73,7 @@ namespace polysat { LOG("consequent " << c << " value: " << c.bvalue(s) << " is-false: " << c.is_currently_false(s) << " " << core.contains(~c)); // ensure new core is a conflict + // TODO: don't we need to check the m_new_constraints too? or maybe that is implicit in the rules (should check it) if (!c.is_currently_false(s) && c.bvalue(s) != l_false) return false; @@ -99,7 +100,7 @@ namespace polysat { core.reset(); for (auto d : m_new_constraints) core.insert(d); - if (c.bvalue(s) != l_false) + if (c.bvalue(s) != l_false) // conflict is due to the evaluation of c, so it depends on the variable values core.insert_vars(c); core.insert(~c); core.log_inference(inf_name); diff --git a/src/math/polysat/solver.cpp b/src/math/polysat/solver.cpp index 575a1dd98..f0b47065b 100644 --- a/src/math/polysat/solver.cpp +++ b/src/math/polysat/solver.cpp @@ -27,8 +27,6 @@ Author: namespace polysat { - - solver::solver(reslimit& lim): m_lim(lim), m_viable(*this), @@ -93,7 +91,6 @@ namespace polysat { return check_sat(); } - dd::pdd_manager& solver::sz2pdd(unsigned sz) const { m_pdd.reserve(sz + 1); if (!m_pdd[sz]) @@ -643,6 +640,11 @@ namespace polysat { revert_decision(v); return; } + if (m_conflict.is_bailout_lemma()) { + m_conflict.end_conflict(); + backtrack_lemma(); + return; + } m_search.pop_assignment(); } else { @@ -677,7 +679,44 @@ namespace polysat { } /** - * Simpler backracking for forbidden interval lemmas: + * Simple backtracking 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)); + SASSERT(lemma); + + // find second-highest level of the literals in the lemma + unsigned max_level = 0; // could be simplified if we're sure that always max_level == m_level + unsigned jump_level = 0; + for (auto lit : *lemma) { + if (!m_bvars.is_assigned(lit)) + continue; + unsigned lit_level = m_bvars.level(lit); + if (lit_level > max_level) { + jump_level = max_level; + max_level = lit_level; + } else if (max_level > lit_level && lit_level > jump_level) { + jump_level = lit_level; + } + } + + jump_level = std::max(jump_level, base_level()); + + // LOG("current lvl: " << m_level); + // LOG("base level: " << base_level()); + // LOG("max_level: " << max_level); + // LOG("jump_level: " << jump_level); + + m_conflict.reset(); + backjump(jump_level); + 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. */ @@ -914,7 +953,7 @@ namespace polysat { LOG_H3("Reverting boolean decision: " << lit << " " << m_conflict); SASSERT(m_bvars.is_decision(var)); - clause_builder reason_builder = m_conflict.build_lemma(); + clause_builder reason_builder = m_conflict.build_lemma(); SASSERT(std::find(reason_builder.begin(), reason_builder.end(), ~lit)); clause_ref reason = reason_builder.build(); diff --git a/src/math/polysat/solver.h b/src/math/polysat/solver.h index ee2920473..5192cf4bd 100644 --- a/src/math/polysat/solver.h +++ b/src/math/polysat/solver.h @@ -205,6 +205,7 @@ namespace polysat { void resolve_conflict(); void backtrack_fi(); + void backtrack_lemma(); void revert_decision(pvar v); void revert_bool_decision(sat::literal lit);