diff --git a/src/math/polysat/polysat.cpp b/src/math/polysat/polysat.cpp index ed4b62025..06af89c4f 100644 --- a/src/math/polysat/polysat.cpp +++ b/src/math/polysat/polysat.cpp @@ -53,7 +53,24 @@ namespace polysat { } lbool solver::find_viable(unsigned var, rational & val) { - return l_false; + val = 0; + bdd viable = m_viable[var]; + if (viable.is_false()) + return l_false; + unsigned num_vars = 0; + while (!viable.is_true()) { + unsigned k = viable.var(); + if (viable.lo().is_false()) { + val += rational::power_of_two(k); + viable = viable.hi(); + } + else + viable = viable.lo(); + ++num_vars; + } + if (num_vars == size(var)) + return l_true; + return l_undef; } @@ -68,7 +85,7 @@ namespace polysat { m_trail(s), m_bdd(1000), m_dep_manager(m_value_manager, m_alloc), - m_lemma_dep(nullptr, m_dep_manager), + m_conflict_dep(nullptr, m_dep_manager), m_free_vars(m_activity) { } @@ -76,7 +93,7 @@ namespace polysat { lbool solver::check_sat() { while (true) { - if (is_conflict() && m_level == 0) return l_false; + if (is_conflict() && at_base_level()) return l_false; else if (is_conflict()) resolve_conflict(); else if (can_propagate()) propagate(); else if (!can_decide()) return l_true; @@ -116,7 +133,7 @@ namespace polysat { } void solver::add_eq(pdd const& p, unsigned dep) { - p_dependency_ref d(m_dep_manager.mk_leaf(dep), m_dep_manager); + p_dependency_ref d(mk_dep(dep), m_dep_manager); constraint* c = constraint::eq(m_level, p, d); m_constraints.push_back(c); add_watch(*c); @@ -242,7 +259,6 @@ namespace polysat { VERIFY(a.mult_inverse(sz, inv_a)); rational val = mod(inv_a * -b, rational::power_of_two(sz)); m_cjust[other_var].push_back(&c); - m_trail.push(push_back_vector(m_cjust[other_var])); propagate(other_var, val, justification::propagation(m_level)); return false; } @@ -290,6 +306,8 @@ namespace polysat { auto v = m_search.back(); m_justification[v] = justification::unassigned(); m_free_vars.unassign_var_eh(v); + m_cjust[v].reset(); + m_viable[v] = m_bdd.mk_true(); m_search.pop_back(); } } @@ -367,16 +385,23 @@ namespace polysat { * */ void solver::resolve_conflict() { - SASSERT(m_conflict); - constraint& c = *m_conflict; - m_conflict = nullptr; - pdd p = c.p(); - m_lemma_level = c.level(); - m_lemma_dep = c.dep(); - unsigned new_lemma_level = 0; + SASSERT(!m_conflict.empty()); reset_marks(); - for (auto v : c.vars()) - set_mark(v); + m_conflict_level = 0; + m_conflict_dep = nullptr; + pdd p = m_conflict[0]->p(); + for (constraint* c : m_conflict) { + for (auto v : c->vars()) + set_mark(v); + pdd p = c->p(); + m_conflict_level = std::max(m_conflict_level, c->level()); + m_conflict_dep = m_dep_manager.mk_join(m_conflict_dep, c->dep()); + } + // TBD: deal with case of multiple constaints + // to obtain single p or delay extracting p until resolution. + // + m_conflict.reset(); + unsigned new_lemma_level = 0; unsigned v = UINT_MAX; unsigned i = m_search.size(); vector> sub; @@ -392,16 +417,17 @@ namespace polysat { report_unsat(); return; } + if (j.is_decision()) { + learn_lemma(v, p); + revert_decision(i); + return; + } pdd r = resolve(v, p, new_lemma_level); pdd rval = r.subst_val(sub); if (r.is_val() && rval.is_non_zero()) { report_unsat(); return; } - if (j.is_decision()) { - revert_decision(p, i); - return; - } if (!rval.is_non_zero()) { backtrack(i); return; @@ -411,11 +437,17 @@ namespace polysat { for (auto w : r.free_vars()) set_mark(w); p = r; - m_lemma_level = new_lemma_level; + m_conflict_level = new_lemma_level; } report_unsat(); } + /** + * TBD: m_conflict_dep is a justification that m_value[v] is not viable. + * it is currently not yet being accounted for. + * A more general data-structure could be to maintain a p_dependency + * with each variable state. The dependencies are augmented on backtracking. + */ void solver::backtrack(unsigned i) { do { auto v = m_search[i]; @@ -423,72 +455,78 @@ namespace polysat { if (j.level() <= base_level()) break; if (j.is_decision()) { - // TBD: flip last decision. - // subtract value from viable - // m_viable[v] -= m_value[v]; - if (m_viable[v].is_false()) - continue; - // - // pop levels to i - // choose a new value for v as a decision. - // + revert_decision(i); + return; } } - while (i-- > 0); - + while (i-- > 0); report_unsat(); } void solver::report_unsat() { - // dependencies for variables that are currently marked and below base level - // are in the unsat core that is produced as a side-effect + backjump(base_level()); + m_conflict.push_back(nullptr); } + void solver::unsat_core(unsigned_vector& deps) { + deps.reset(); + for (auto* c : m_conflict) { + if (c) + m_conflict_dep = m_dep_manager.mk_join(c->dep(), m_conflict_dep); + } + m_dep_manager.linearize(m_conflict_dep, deps); + } + + /** - * variable v was assigned by a decision at position i in the search stack. * The polynomial p encodes an equality that the decision was infeasible. * The effect of this function is that the assignment to v is undone and replaced * by a new decision or unit propagation or conflict. * We add 'p == 0' as a lemma. The lemma depends on the dependencies used * to derive p, and the level of the lemma is the maximal level of the dependencies. */ - void solver::revert_decision(pdd const& p, unsigned i) { - auto v = m_search[i]; - SASSERT(m_justification[v].is_decision()); - SASSERT(m_lemma_level <= m_justification[v].level()); - constraint* c = constraint::eq(m_lemma_level, p, m_lemma_dep); + void solver::learn_lemma(unsigned v, pdd const& p) { + SASSERT(m_conflict_level <= m_justification[v].level()); + constraint* c = constraint::eq(m_conflict_level, p, m_conflict_dep); m_cjust[v].push_back(c); add_lemma(c); + } + + /** + * variable v was assigned by a decision at position i in the search stack. + */ + void solver::revert_decision(unsigned i) { + auto v = m_search[i]; + SASSERT(m_justification[v].is_decision()); add_non_viable(v, m_value[v]); - // TBD conditions for when backjumping applies to be clarified. + // TBD how much to backjump to be clarified + // everything before v is reverted, but not assignment + // to v. This is different from propositional CDCL + // where decision on v is also reverted. unsigned new_level = m_justification[v].level(); backjump(new_level); - // - // find a new decision if there is one, - // propagate if decision is singular, - // otherwise if there are no viable decisions, backjump - // and set a new conflict. - // rational value; + m_conflict_dep = nullptr; switch (find_viable(v, value)) { - case l_true: - // unit propagation + case l_true: + assign_core(v, value, justification::propagation(new_level)); break; case l_undef: - // branch + assign_core(v, value, justification::decision(new_level)); break; case l_false: - // no viable. + set_conflict(m_cjust[v]); break; } } void solver::backjump(unsigned new_level) { unsigned num_levels = m_level - new_level; - SASSERT(num_levels > 0); - pop_levels(num_levels); - m_trail.pop_scope(num_levels); + if (num_levels > 0) { + pop_levels(num_levels); + m_trail.pop_scope(num_levels); + } } /** @@ -522,7 +560,7 @@ namespace polysat { // add parity condition to presere falsification degree = r.degree(v); resolve_level = std::max(resolve_level, c->level()); - m_lemma_dep = m_dep_manager.mk_join(m_lemma_dep.get(), c->dep()); + m_conflict_dep = m_dep_manager.mk_join(m_conflict_dep.get(), c->dep()); } } } diff --git a/src/math/polysat/polysat.h b/src/math/polysat/polysat.h index ec714eaee..f2971d2aa 100644 --- a/src/math/polysat/polysat.h +++ b/src/math/polysat/polysat.h @@ -30,6 +30,8 @@ namespace polysat { typedef dd::pdd pdd; typedef dd::bdd bdd; + const unsigned null_dependency = UINT_MAX; + struct dep_value_manager { void inc_ref(unsigned) {} void dec_ref(unsigned) {} @@ -117,7 +119,7 @@ namespace polysat { dep_value_manager m_value_manager; small_object_allocator m_alloc; poly_dep_manager m_dep_manager; - p_dependency_ref m_lemma_dep; + p_dependency_ref m_conflict_dep; var_queue m_free_vars; // Per constraint state @@ -144,7 +146,7 @@ namespace polysat { // conflict state - constraint* m_conflict { nullptr }; + ptr_vector m_conflict; unsigned size(unsigned var) const { return m_size[var]; } /** @@ -193,8 +195,8 @@ namespace polysat { void erase_watch(constraint& c); void add_watch(constraint& c); - void set_conflict(constraint& c) { m_conflict = &c; } - void clear_conflict() { m_conflict = nullptr; } + void set_conflict(constraint& c) { m_conflict.push_back(&c); } + void set_conflict(ptr_vector& cs) { m_conflict.append(cs); } unsigned_vector m_marks; unsigned m_clock { 0 }; @@ -202,20 +204,23 @@ namespace polysat { bool is_marked(unsigned v) const { return m_clock == m_marks[v]; } void set_mark(unsigned v) { m_marks[v] = m_clock; } - unsigned m_lemma_level { 0 }; + unsigned m_conflict_level { 0 }; pdd isolate(unsigned v); pdd resolve(unsigned v, pdd const& p, unsigned& resolve_level); void decide(); - bool is_conflict() const { return nullptr != m_conflict; } + p_dependency* mk_dep(unsigned dep) { return dep == null_dependency ? nullptr : m_dep_manager.mk_leaf(dep); } + + bool is_conflict() const { return !m_conflict.empty(); } bool at_base_level() const; unsigned base_level() const; void resolve_conflict(); void backtrack(unsigned i); void report_unsat(); - void revert_decision(pdd const& p, unsigned i); + void revert_decision(unsigned i); + void learn_lemma(unsigned v, pdd const& p); void backjump(unsigned new_level); void add_lemma(constraint* c); @@ -241,6 +246,11 @@ namespace polysat { * End-game satisfiability checker. */ lbool check_sat(); + + /** + * retrieve unsat core dependencies + */ + void unsat_core(unsigned_vector& deps); /** * Add variable with bit-size. @@ -257,12 +267,12 @@ namespace polysat { * Each constraint is tracked by a dependency. * assign sets the 'index'th bit of var. */ - void add_eq(pdd const& p, unsigned dep = 0); - void add_diseq(pdd const& p, unsigned dep = 0); - void add_ule(pdd const& p, pdd const& q, unsigned dep = 0); - void add_ult(pdd const& p, pdd const& q, unsigned dep = 0); - void add_sle(pdd const& p, pdd const& q, unsigned dep = 0); - void add_slt(pdd const& p, pdd const& q, unsigned dep = 0); + void add_eq(pdd const& p, unsigned dep = null_dependency); + void add_diseq(pdd const& p, unsigned dep = null_dependency); + void add_ule(pdd const& p, pdd const& q, unsigned dep = null_dependency); + void add_ult(pdd const& p, pdd const& q, unsigned dep = null_dependency); + void add_sle(pdd const& p, pdd const& q, unsigned dep = null_dependency); + void add_slt(pdd const& p, pdd const& q, unsigned dep = null_dependency); void assign(unsigned var, unsigned index, bool value, unsigned dep);