diff --git a/src/math/polysat/boolean.cpp b/src/math/polysat/boolean.cpp index 249a19987..253be8fad 100644 --- a/src/math/polysat/boolean.cpp +++ b/src/math/polysat/boolean.cpp @@ -24,8 +24,8 @@ namespace polysat { m_value.push_back(l_undef); m_level.push_back(UINT_MAX); m_deps.push_back(null_dependency); - m_reason.push_back(nullptr); - m_lemma.push_back(nullptr); + m_kind.push_back(kind_t::unassigned); + m_clause.push_back(nullptr); m_watch.push_back({}); m_watch.push_back({}); m_activity.push_back(0); @@ -36,8 +36,8 @@ namespace polysat { SASSERT_EQ(m_level[var], UINT_MAX); SASSERT_EQ(m_value[2*var], l_undef); SASSERT_EQ(m_value[2*var+1], l_undef); - SASSERT_EQ(m_reason[var], nullptr); - SASSERT_EQ(m_lemma[var], nullptr); + SASSERT_EQ(m_kind[var], kind_t::unassigned); + SASSERT_EQ(m_clause[var], nullptr); SASSERT_EQ(m_deps[var], null_dependency); } m_free_vars.mk_var_eh(var); @@ -50,8 +50,8 @@ namespace polysat { m_value[lit.index()] = l_undef; m_value[(~lit).index()] = l_undef; m_level[var] = UINT_MAX; - m_reason[var] = nullptr; - m_lemma[var] = nullptr; + m_kind[var] = kind_t::unassigned; + m_clause[var] = nullptr; m_deps[var] = null_dependency; m_watch[lit.index()].reset(); m_watch[(~lit).index()].reset(); @@ -62,31 +62,36 @@ namespace polysat { void bool_var_manager::propagate(sat::literal lit, unsigned lvl, clause& reason) { LOG("Propagate literal " << lit << " @ " << lvl << " by " << reason); - assign(lit, lvl, &reason, nullptr, null_dependency); + assign(kind_t::propagation, lit, lvl, &reason); + SASSERT(is_propagation(lit)); } - void bool_var_manager::decide(sat::literal lit, unsigned lvl, clause* lemma) { + void bool_var_manager::decide(sat::literal lit, unsigned lvl, clause& lemma) { LOG("Decide literal " << lit << " @ " << lvl); - assign(lit, lvl, nullptr, lemma); + assign(kind_t::decision, lit, lvl, &lemma); + SASSERT(is_decision(lit)); } void bool_var_manager::eval(sat::literal lit, unsigned lvl) { LOG("Eval literal " << lit << " @ " << lvl); - assign(lit, lvl, nullptr, nullptr); + assign(kind_t::propagation, lit, lvl, nullptr); + SASSERT(is_propagation(lit)); } void bool_var_manager::asserted(sat::literal lit, unsigned lvl, unsigned dep) { LOG("Asserted " << lit << " @ " << lvl); - assign(lit, lvl, nullptr, nullptr, dep); + assign(kind_t::decision, lit, lvl, nullptr, dep); + SASSERT(is_decision(lit)); } - void bool_var_manager::assign(sat::literal lit, unsigned lvl, clause* reason, clause* lemma, unsigned dep) { + void bool_var_manager::assign(kind_t k, sat::literal lit, unsigned lvl, clause* reason, unsigned dep) { SASSERT(!is_assigned(lit)); + SASSERT(k != kind_t::unassigned); m_value[lit.index()] = l_true; m_value[(~lit).index()] = l_false; m_level[lit.var()] = lvl; - m_reason[lit.var()] = reason; - m_lemma[lit.var()] = lemma; + m_kind[lit.var()] = k; + m_clause[lit.var()] = reason; m_deps[lit.var()] = dep; m_free_vars.del_var_eh(lit.var()); } @@ -96,8 +101,8 @@ namespace polysat { m_value[lit.index()] = l_undef; m_value[(~lit).index()] = l_undef; m_level[lit.var()] = UINT_MAX; - m_reason[lit.var()] = nullptr; - m_lemma[lit.var()] = nullptr; + m_kind[lit.var()] = kind_t::unassigned; + m_clause[lit.var()] = nullptr; m_deps[lit.var()] = null_dependency; m_free_vars.unassign_var_eh(lit.var()); } diff --git a/src/math/polysat/boolean.h b/src/math/polysat/boolean.h index be333bf6e..a0a8b8bf6 100644 --- a/src/math/polysat/boolean.h +++ b/src/math/polysat/boolean.h @@ -19,20 +19,28 @@ namespace polysat { class clause; class bool_var_manager { + + enum class kind_t { + unassigned, + propagation, + decision, + }; + svector m_unused; // previously deleted variables that can be reused by new_var(); svector m_value; // current value (indexed by literal) unsigned_vector m_level; // level of assignment (indexed by variable) unsigned_vector m_deps; // dependencies of external asserts - unsigned_vector m_activity; // - ptr_vector m_reason; // propagation reason, NULL for decisions and external asserts (indexed by variable) - - // For enumerative backtracking we store the lemma we're handling with a certain decision - ptr_vector m_lemma; + unsigned_vector m_activity; // + svector m_kind; // decision or propagation? + // Clause associated with the assignment (indexed by variable): + // - for propagations: the reason (or NULL for eval'd literals) + // - for decisions: the lemma (or NULL for externally asserted literals) + ptr_vector m_clause; var_queue m_free_vars; // free Boolean variables vector> m_watch; // watch list for literals into clauses - void assign(sat::literal lit, unsigned lvl, clause* reason, clause* lemma, unsigned dep = null_dependency); + void assign(kind_t k, sat::literal lit, unsigned lvl, clause* reason, unsigned dep = null_dependency); public: @@ -46,19 +54,21 @@ namespace polysat { bool is_assigned(sat::bool_var var) const { return value(var) != l_undef; } bool is_assigned(sat::literal lit) const { return value(lit) != l_undef; } - bool is_decision(sat::bool_var var) const { return is_assigned(var) && !reason(var); } + bool is_decision(sat::bool_var var) const { return is_assigned(var) && m_kind[var] == kind_t::decision; } bool is_decision(sat::literal lit) const { return is_decision(lit.var()); } - bool is_propagation(sat::bool_var var) const { return is_assigned(var) && reason(var); } + bool is_propagation(sat::bool_var var) const { return is_assigned(var) && m_kind[var] == kind_t::propagation; } + bool is_propagation(sat::literal lit) const { return is_propagation(lit.var()); } lbool value(sat::bool_var var) const { return value(sat::literal(var)); } lbool value(sat::literal lit) const { return m_value[lit.index()]; } bool is_true(sat::literal lit) const { return value(lit) == l_true; } bool is_false(sat::literal lit) const { return value(lit) == l_false; } unsigned level(sat::bool_var var) const { SASSERT(is_assigned(var)); return m_level[var]; } unsigned level(sat::literal lit) const { return level(lit.var()); } - clause* reason(sat::bool_var var) const { SASSERT(is_assigned(var)); return m_reason[var]; } + clause* reason(sat::bool_var var) const { SASSERT(is_assigned(var)); return is_propagation(var) ? m_clause[var] : nullptr; } + clause* reason(sat::literal lit) const { return reason(lit.var()); } unsigned dep(sat::literal lit) const { return lit == sat::null_literal ? null_dependency : m_deps[lit.var()]; } - clause* lemma(sat::bool_var var) const { SASSERT(is_decision(var)); return m_lemma[var]; } + clause* lemma(sat::bool_var var) const { SASSERT(is_decision(var)); return m_clause[var]; } ptr_vector& watch(sat::literal lit) { return m_watch[lit.index()]; } unsigned_vector& activity() { return m_activity; } @@ -71,12 +81,21 @@ namespace polysat { /// Set the given literal to true void propagate(sat::literal lit, unsigned lvl, clause& reason); - void decide(sat::literal lit, unsigned lvl, clause* lemma); + void decide(sat::literal lit, unsigned lvl, clause& lemma); void eval(sat::literal lit, unsigned lvl); void asserted(sat::literal lit, unsigned lvl, unsigned dep); void unassign(sat::literal lit); std::ostream& display(std::ostream& out) const; + + friend std::ostream& operator<<(std::ostream& out, kind_t const& k) { + switch (k) { + case kind_t::unassigned: return out << "unassigned"; break; + case kind_t::propagation: return out << "propagation"; break; + case kind_t::decision: return out << "decision"; break; + default: UNREACHABLE(); + } + } }; inline std::ostream& operator<<(std::ostream& out, bool_var_manager const& m) { return m.display(out); } diff --git a/src/math/polysat/conflict.cpp b/src/math/polysat/conflict.cpp index b415fa9a7..70cd1703b 100644 --- a/src/math/polysat/conflict.cpp +++ b/src/math/polysat/conflict.cpp @@ -194,7 +194,7 @@ namespace polysat { s.m_stats.m_num_bailouts++; } - void conflict::resolve(constraint_manager const& m, sat::literal lit, clause const& cl) { + 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 @@ -208,10 +208,28 @@ namespace polysat { SASSERT(std::count(cl.begin(), cl.end(), ~lit) == 0); remove_literal(lit); - unset_mark(m.lookup(lit)); + unset_mark(s.lit2cnstr(lit)); for (sat::literal lit2 : cl) if (lit2 != lit) - insert(m.lookup(~lit2)); + insert(s.lit2cnstr(~lit2)); + } + + void conflict::resolve_with_assignment(sat::literal lit, unsigned lvl) { + // The reason for lit is conceptually: + // x1 = v1 /\ ... /\ xn = vn ==> lit + + SASSERT(lit != sat::null_literal); + SASSERT(~lit != sat::null_literal); + SASSERT(std::all_of(m_constraints.begin(), m_constraints.end(), [](signed_constraint const& c){ return !c->has_bvar(); })); + SASSERT(contains_literal(lit)); + SASSERT(!contains_literal(~lit)); + + remove_literal(lit); + signed_constraint c = s.lit2cnstr(lit); + unset_mark(c); + for (pvar v : c->vars()) + if (s.is_assigned(v) && s.get_level(v) <= lvl) + m_vars.insert(v); // TODO: check this } /** diff --git a/src/math/polysat/conflict.h b/src/math/polysat/conflict.h index 302bd837e..d34da7370 100644 --- a/src/math/polysat/conflict.h +++ b/src/math/polysat/conflict.h @@ -98,7 +98,11 @@ namespace polysat { /** Perform boolean resolution with the clause upon variable 'var'. * Precondition: core/clause contain complementary 'var'-literals. */ - void resolve(constraint_manager const& m, sat::literal lit, clause const& cl); + 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'. diff --git a/src/math/polysat/solver.cpp b/src/math/polysat/solver.cpp index d28d2a7a3..7cc6f66fd 100644 --- a/src/math/polysat/solver.cpp +++ b/src/math/polysat/solver.cpp @@ -250,14 +250,12 @@ namespace polysat { DEBUG_CODE(m_locked_wlist = v;); auto& wlist = m_pwatch[v]; unsigned i = 0, j = 0, sz = wlist.size(); - LOG("wlist old: " << wlist); for (; i < sz && !is_conflict(); ++i) if (!wlist[i].propagate(*this, v)) wlist[j++] = wlist[i]; for (; i < sz; ++i) wlist[j++] = wlist[i]; wlist.shrink(j); - LOG("wlist new: " << wlist); DEBUG_CODE(m_locked_wlist = std::nullopt;); } @@ -578,10 +576,13 @@ namespace polysat { * NOTE: boolean resolution should work normally even in bailout mode. */ void solver::resolve_bool(sat::literal lit) { - SASSERT(m_bvars.is_propagation(lit.var())); - clause const& other = *m_bvars.reason(lit.var()); - LOG_H3("resolve_bool: " << lit << " " << other); - m_conflict.resolve(m_constraints, lit, other); + SASSERT(m_bvars.is_propagation(lit)); + clause const* other = m_bvars.reason(lit); + LOG_H3("resolve_bool: " << lit << " " << show_deref(other)); + if (other) + m_conflict.resolve(lit, *other); + else + m_conflict.resolve_with_assignment(lit, m_bvars.level(lit)); } void solver::report_unsat() { @@ -664,7 +665,7 @@ namespace polysat { break; default: push_level(); - assign_decision(choice, &lemma); + assign_decision(choice, lemma); break; } } @@ -740,14 +741,16 @@ namespace polysat { // The lemma where 'lit' comes from. // Currently, boolean decisions always come from guessing a literal of a learned non-unit lemma. clause* lemma = m_bvars.lemma(var); // need to grab this while 'lit' is still assigned + // We only revert decisions that come from lemmas, so lemma must not be NULL here. + // (Externally asserted literals are at a base level, so we would return UNSAT instead of reverting.) + SASSERT(lemma); backjump(m_bvars.level(var) - 1); // reason should force ~lit after propagation add_clause(*reason); - if (lemma) // TODO: can (should) this ever be NULL? - enqueue_decision_on_lemma(*lemma); + enqueue_decision_on_lemma(*lemma); } unsigned solver::level(sat::literal lit0, clause const& cl) { @@ -768,7 +771,7 @@ namespace polysat { m_search.push_boolean(lit); } - void solver::assign_decision(sat::literal lit, clause* lemma) { + void solver::assign_decision(sat::literal lit, clause& lemma) { m_bvars.decide(lit, m_level, lemma); m_trail.push_back(trail_instr_t::assign_bool_i); m_search.push_boolean(lit); diff --git a/src/math/polysat/solver.h b/src/math/polysat/solver.h index f7ec8583a..0681ea4c1 100644 --- a/src/math/polysat/solver.h +++ b/src/math/polysat/solver.h @@ -152,7 +152,7 @@ namespace polysat { void pop_levels(unsigned num_levels); void assign_propagate(sat::literal lit, clause& reason); - void assign_decision(sat::literal lit, clause* lemma); + void assign_decision(sat::literal lit, clause& lemma); void assign_eval(sat::literal lit); void activate_constraint(signed_constraint c); void deactivate_constraint(signed_constraint c); diff --git a/src/test/polysat.cpp b/src/test/polysat.cpp index bf9154170..cbc7672e6 100644 --- a/src/test/polysat.cpp +++ b/src/test/polysat.cpp @@ -1310,9 +1310,6 @@ void tst_polysat() { test_fi::randomized(); return; - test_polysat::test_ineq_axiom1(32, 2); // crashes - return; - // looks like a fishy conflict lemma? test_polysat::test_monot_bounds(); return; @@ -1433,6 +1430,7 @@ void tst_polysat_argv(char** argv, int argc, int& i) { VERIFY(parse_smt2_commands(ctx, is)); ptr_vector fmls = ctx.assertions(); polysat::scoped_solver s("polysat"); + s.set_max_conflicts(1000); g_solver = &s; polysat::internalize(m, s, fmls); std::cout << "checking\n";