From b488a1fadd856a9150aa1079652384a49708b637 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 29 Jan 2022 16:17:58 -0800 Subject: [PATCH] WIP revamp conflict state Signed-off-by: Nikolaj Bjorner --- src/math/polysat/conflict.cpp | 58 +++++++-------------------------- src/math/polysat/conflict.h | 34 ++++++++++++++++++- src/math/polysat/constraint.h | 4 --- src/math/polysat/saturation.cpp | 2 +- src/math/polysat/solver.cpp | 2 +- src/math/polysat/viable.cpp | 5 +-- 6 files changed, 50 insertions(+), 55 deletions(-) diff --git a/src/math/polysat/conflict.cpp b/src/math/polysat/conflict.cpp index f7c4d26de..67042ae51 100644 --- a/src/math/polysat/conflict.cpp +++ b/src/math/polysat/conflict.cpp @@ -50,8 +50,7 @@ namespace polysat { if (!m_vars.empty()) out << " vars"; for (auto v : m_vars) - if (is_pmarked(v)) - out << " v" << v; + out << " v" << v; return out; } @@ -83,7 +82,7 @@ namespace polysat { else { SASSERT(c.is_currently_false(s)); // TBD: fails with test_subst SASSERT(c.bvalue(s) == l_true); - c->set_var_dependent(); + insert_vars(c); insert(c); } SASSERT(!empty()); @@ -140,6 +139,13 @@ namespace polysat { m_constraints.push_back(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. @@ -210,7 +216,7 @@ namespace polysat { SASSERT(std::count(cl.begin(), cl.end(), ~lit) == 0); remove_literal(lit); - unset_bmark(s.lit2cnstr(lit)); + unset_mark(s.lit2cnstr(lit)); for (sat::literal lit2 : cl) if (lit2 != lit) insert(s.lit2cnstr(~lit2)); @@ -229,12 +235,7 @@ namespace polysat { 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); - inc_pref(v); - } - } + insert_vars(c); } /** @@ -268,8 +269,6 @@ namespace polysat { lemma.push(~c); for (unsigned v : m_vars) { - if (!is_pmarked(v)) - continue; auto eq = s.eq(s.var(v), s.get_value(v)); cm().ensure_bvar(eq.get()); if (eq.bvalue(s) == l_undef) @@ -406,19 +405,12 @@ namespace polysat { c->set_mark(); if (c->has_bvar()) set_bmark(c->bvar()); - if (c->is_var_dependent()) { - for (auto v : c->vars()) { - if (s.is_assigned(v)) - m_vars.insert(v); - inc_pref(v); - } - } } /** * unset marking on the constraint, but keep variable dependencies. */ - void conflict::unset_bmark(signed_constraint c) { + void conflict::unset_mark(signed_constraint c) { if (!c->is_marked()) return; c->unset_mark(); @@ -426,32 +418,6 @@ namespace polysat { unset_bmark(c->bvar()); } - void conflict::unset_mark(signed_constraint c) { - if (!c->is_marked()) - return; - unset_bmark(c); - if (!c->is_var_dependent()) - return; - c->unset_var_dependent(); - for (auto v : c->vars()) - dec_pref(v); - } - - void conflict::inc_pref(pvar v) { - if (v >= m_pvar2count.size()) - m_pvar2count.resize(v + 1); - m_pvar2count[v]++; - } - - void conflict::dec_pref(pvar v) { - SASSERT(m_pvar2count[v] > 0); - m_pvar2count[v]--; - } - - bool conflict::is_pmarked(pvar v) const { - return m_pvar2count.get(v, 0) > 0; - } - void conflict::set_bmark(sat::bool_var b) { if (b >= m_bvar2mark.size()) m_bvar2mark.resize(b + 1); diff --git a/src/math/polysat/conflict.h b/src/math/polysat/conflict.h index 38a7a6c17..4a14fa350 100644 --- a/src/math/polysat/conflict.h +++ b/src/math/polysat/conflict.h @@ -10,6 +10,37 @@ 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 <- Cs - v is assigned value by constraints Cs + v = value <- ? - v is a decision literal. + + - All literals should be assigned in the stack prior to their use. + + lit <- D => lit, < Vars, { lit } u Cs > ===> < Vars, Cs u D > + lit <- ?, < Vars, { lit } u Cs > ===> ~lit <- (Cs & Vars = value(Vars) => ~lit) + lit <- asserted, < Vars, { lit } u Cs > ===> accumulate lit for a core + lit <- Vars', < Vars, { lit } u Cs > ===> ~lit <- (Cs & Vars = value(Vars) => ~lit) + + v = value <- Cs, < Vars u { v }, Cs > ===> + + + --*/ #pragma once #include "math/polysat/constraint.h" @@ -77,7 +108,7 @@ namespace polysat { void reset(); - bool is_pmarked(pvar v) const; + bool contains_pvar(pvar v) const { return m_vars.contains(v); } bool is_bmarked(sat::bool_var b) const; /** conflict because the constraint c is false under current variable assignment */ @@ -88,6 +119,7 @@ namespace polysat { void set(clause const& cl); 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); diff --git a/src/math/polysat/constraint.h b/src/math/polysat/constraint.h index e1f385208..db131acba 100644 --- a/src/math/polysat/constraint.h +++ b/src/math/polysat/constraint.h @@ -146,7 +146,6 @@ namespace polysat { unsigned_vector m_vars; lbool m_external_sign = l_undef; bool m_is_marked = false; - bool m_is_var_dependent = false; bool m_is_active = false; /** The boolean variable associated to this constraint, if any. * If this is not null_bool_var, then the constraint corresponds to a literal on the assignment stack. @@ -207,9 +206,6 @@ namespace polysat { void unset_mark() { m_is_marked = false; } bool is_marked() const { return m_is_marked; } - void set_var_dependent() { m_is_var_dependent = true; } - void unset_var_dependent() { m_is_var_dependent = false; } - bool is_var_dependent() const { return m_is_var_dependent; } bool is_active() const { return m_is_active; } void set_active(bool f) { m_is_active = f; } diff --git a/src/math/polysat/saturation.cpp b/src/math/polysat/saturation.cpp index e68d87a75..564afd238 100644 --- a/src/math/polysat/saturation.cpp +++ b/src/math/polysat/saturation.cpp @@ -88,7 +88,7 @@ namespace polysat { for (auto d : m_new_constraints) core.insert(d); if (c.bvalue(s) != l_false) - c->set_var_dependent(); + core.insert_vars(c); core.insert(~c); LOG("Core " << core); return true; diff --git a/src/math/polysat/solver.cpp b/src/math/polysat/solver.cpp index 49cc4ba18..5405a0024 100644 --- a/src/math/polysat/solver.cpp +++ b/src/math/polysat/solver.cpp @@ -534,7 +534,7 @@ namespace polysat { if (item.is_assignment()) { // Resolve over variable assignment pvar v = item.var(); - if (!m_conflict.is_pmarked(v) && !m_conflict.is_bailout()) { + if (!m_conflict.contains_pvar(v) && !m_conflict.is_bailout()) { m_search.pop_assignment(); continue; } diff --git a/src/math/polysat/viable.cpp b/src/math/polysat/viable.cpp index 7aef1cbf3..4b33d6b75 100644 --- a/src/math/polysat/viable.cpp +++ b/src/math/polysat/viable.cpp @@ -557,9 +557,10 @@ namespace polysat { signed_constraint c = s.m_constraints.ult(lhs, rhs); core.insert(c); } - for (auto sc : e->side_cond) + for (auto sc : e->side_cond) { core.insert(sc); - e->src->set_var_dependent(); + core.insert_vars(sc); + } core.insert(e->src); e = n; }