diff --git a/src/math/polysat/clause.h b/src/math/polysat/clause.h index abef08d53..1e8fdf44a 100644 --- a/src/math/polysat/clause.h +++ b/src/math/polysat/clause.h @@ -33,7 +33,6 @@ namespace polysat { friend class constraint_manager; unsigned m_ref_count = 0; // TODO: remove refcount once we confirm it's not needed anymore - pvar m_justified_var = null_var; // The variable that was restricted by learning this lemma. bool m_redundant = false; sat::literal_vector m_literals; @@ -60,9 +59,6 @@ namespace polysat { static clause_ref from_literals(sat::literal_vector literals); - pvar justified_var() const { return m_justified_var; } - void set_justified_var(pvar v) { SASSERT(m_justified_var == null_var); m_justified_var = v; } - bool empty() const { return m_literals.empty(); } unsigned size() const { return m_literals.size(); } sat::literal operator[](unsigned idx) const { return m_literals[idx]; } diff --git a/src/math/polysat/solver.cpp b/src/math/polysat/solver.cpp index 196ea8705..4147cbce2 100644 --- a/src/math/polysat/solver.cpp +++ b/src/math/polysat/solver.cpp @@ -20,18 +20,14 @@ Author: #include "math/polysat/explain.h" #include "math/polysat/log.h" #include "math/polysat/variable_elimination.h" +#include "util/luby.h" // For development; to be removed once the linear solver works well enough #define ENABLE_LINEAR_SOLVER 0 namespace polysat { - dd::pdd_manager& solver::sz2pdd(unsigned sz) { - m_pdd.reserve(sz + 1); - if (!m_pdd[sz]) - m_pdd.set(sz, alloc(dd::pdd_manager, 1000, dd::pdd_manager::semantics::mod2N_e, sz)); - return *m_pdd[sz]; - } + solver::solver(reslimit& lim): m_lim(lim), @@ -73,16 +69,29 @@ namespace polysat { LOG("Assignment: " << assignments_pp(*this)); if (is_conflict()) LOG("Conflict: " << m_conflict); IF_LOGGING(m_viable.log()); - if (!is_conflict() && m_constraints.should_gc()) m_constraints.gc(*this); - else if (is_conflict() && at_base_level()) { LOG_H2("UNSAT"); return l_false; } + if (is_conflict() && at_base_level()) { LOG_H2("UNSAT"); return l_false; } else if (is_conflict()) resolve_conflict(); else if (can_propagate()) propagate(); else if (!can_decide()) { LOG_H2("SAT"); SASSERT(verify_sat()); return l_true; } + else if (m_constraints.should_gc()) m_constraints.gc(*this); + else if (should_simplify()) simplify(); + else if (should_restart()) restart(); else decide(); } LOG_H2("UNDEF (resource limit)"); return l_undef; } + + dd::pdd_manager& solver::sz2pdd(unsigned sz) { + m_pdd.reserve(sz + 1); + if (!m_pdd[sz]) + m_pdd.set(sz, alloc(dd::pdd_manager, 1000, dd::pdd_manager::semantics::mod2N_e, sz)); + return *m_pdd[sz]; + } + + dd::pdd_manager& solver::var2pdd(pvar v) { + return sz2pdd(size(v)); + } unsigned solver::add_var(unsigned sz) { pvar v = m_value.size(); @@ -136,7 +145,6 @@ namespace polysat { #if ENABLE_LINEAR_SOLVER m_linear_solver.new_constraint(*c.get()); #endif - } @@ -243,6 +251,37 @@ namespace polysat { #endif } + /* + * This is a place holder for in-processing simplification + */ + bool solver::should_simplify() { + return false; + } + + void solver::simplify() { + + } + + /* + * Basic restart functionality. + * restarts make more sense when the order of variable + * assignments and the values assigned to variables can be diversified. + */ + bool solver::should_restart() { + if (m_stats.m_num_conflicts - m_conflicts_at_restart < m_restart_threshold) + return false; + if (base_level() + 2 > m_level) + return false; + return true; + } + + void solver::restart() { + ++m_stats.m_num_restarts; + pop_levels(m_level - base_level()); + m_conflicts_at_restart = m_stats.m_num_conflicts; + m_restart_threshold = m_restart_init * get_luby(++m_luby_idx); + } + void solver::pop_levels(unsigned num_levels) { if (num_levels == 0) return; @@ -518,10 +557,9 @@ namespace polysat { */ } - void solver::learn_lemma(pvar v, clause& lemma) { + void solver::learn_lemma(clause& lemma) { LOG("Learning: "<< lemma); SASSERT(!lemma.empty()); - lemma.set_justified_var(v); add_lemma(lemma); if (!is_conflict()) decide_bool(lemma); @@ -566,7 +604,6 @@ namespace polysat { signed_constraint c = lit2cnstr(choice); if (num_choices > 1) push_level(); - push_cjust(lemma.justified_var(), c); if (num_choices == 1) assign_propagate(choice, lemma); @@ -594,8 +631,8 @@ namespace polysat { // The justification for this restriction is the guessed constraint from the lemma. // cjust[v] will be updated accordingly by decide_bool. - m_viable.add_non_viable(v, val); - learn_lemma(v, *lemma); + // m_viable.add_non_viable(v, val); + learn_lemma(*lemma); if (!is_conflict()) narrow(v); @@ -831,6 +868,7 @@ namespace polysat { st.update("polysat conflicts", m_stats.m_num_conflicts); st.update("polysat bailouts", m_stats.m_num_bailouts); st.update("polysat propagations", m_stats.m_num_propagations); + st.update("polysat restarts", m_stats.m_num_restarts); } bool solver::invariant() { diff --git a/src/math/polysat/solver.h b/src/math/polysat/solver.h index 784fc6601..0dd223533 100644 --- a/src/math/polysat/solver.h +++ b/src/math/polysat/solver.h @@ -44,6 +44,7 @@ namespace polysat { unsigned m_num_propagations; unsigned m_num_conflicts; unsigned m_num_bailouts; + unsigned m_num_restarts; void reset() { memset(this, 0, sizeof(*this)); } stats() { reset(); } }; @@ -140,6 +141,7 @@ namespace polysat { void del_var(); dd::pdd_manager& sz2pdd(unsigned sz); + dd::pdd_manager& var2pdd(pvar v); void push_level(); void pop_levels(unsigned num_levels); @@ -195,10 +197,20 @@ namespace polysat { void revert_bool_decision(sat::literal lit); void report_unsat(); - void learn_lemma(pvar v, clause& lemma); + void learn_lemma(clause& lemma); void backjump(unsigned new_level); void add_lemma(clause& lemma); + bool should_simplify(); + void simplify(); + + unsigned m_conflicts_at_restart = 0; + unsigned m_restart_threshold = UINT_MAX; + unsigned m_restart_init = 100; + unsigned m_luby_idx = 0; + bool should_restart(); + void restart(); + signed_constraint lit2cnstr(sat::literal lit) const { return m_constraints.lookup(lit); } void assert_constraint(signed_constraint c, unsigned dep); static void insert_constraint(signed_constraints& cs, signed_constraint c); diff --git a/src/math/polysat/viable2.cpp b/src/math/polysat/viable2.cpp index f6d625671..f218246d5 100644 --- a/src/math/polysat/viable2.cpp +++ b/src/math/polysat/viable2.cpp @@ -138,7 +138,7 @@ namespace polysat { if (!e) return true; entry* first = e; - auto const& max_value = s.m_pdd[v]->max_value(); + auto const& max_value = s.var2pdd(v).max_value(); do { if (e->interval.is_full()) return false; @@ -174,10 +174,10 @@ namespace polysat { void viable2::add_non_viable(pvar v, rational const& lo_val, signed_constraint const& c) { entry* ne = alloc_entry(); - rational const& max_value = s.m_pdd[v]->max_value(); + rational const& max_value = s.var2pdd(v).max_value(); rational hi_val = (lo_val == max_value) ? rational::zero() : lo_val + 1; - pdd lo = s.m_pdd[v]->mk_val(lo_val); - pdd hi = s.m_pdd[v]->mk_val(hi_val); + pdd lo = s.var2pdd(v).mk_val(lo_val); + pdd hi = s.var2pdd(v).mk_val(hi_val); ne->interval = eval_interval::proper(lo, lo_val, hi, hi_val); ne->src = c; intersect(v, ne); @@ -204,7 +204,7 @@ namespace polysat { } rational viable2::max_viable(pvar v) { - rational hi = s.m_pdd[s.size(v)]->max_value(); + rational hi = s.var2pdd(v).max_value(); auto* e = m_viable[v]; if (!e) return hi; @@ -244,7 +244,7 @@ namespace polysat { if (e->interval.currently_contains(lo)) return dd::find_t::empty; - rational hi = s.m_pdd[s.size(v)]->max_value(); + rational hi = s.var2pdd(v).max_value(); e = last; do { if (!e->interval.currently_contains(hi))