From f819c2bad8fdf6169a84bfb8418abb543c1fc027 Mon Sep 17 00:00:00 2001 From: Jakob Rath Date: Thu, 25 Aug 2022 17:04:07 +0200 Subject: [PATCH] conflict2 stub --- src/math/polysat/CMakeLists.txt | 1 + src/math/polysat/conflict2.cpp | 122 ++++++++++++++++++++++++++++ src/math/polysat/conflict2.h | 140 ++++++++++++++++++++++++++++++++ 3 files changed, 263 insertions(+) create mode 100644 src/math/polysat/conflict2.cpp create mode 100644 src/math/polysat/conflict2.h diff --git a/src/math/polysat/CMakeLists.txt b/src/math/polysat/CMakeLists.txt index 353dd4a22..8174eff59 100644 --- a/src/math/polysat/CMakeLists.txt +++ b/src/math/polysat/CMakeLists.txt @@ -4,6 +4,7 @@ z3_add_component(polysat clause.cpp clause_builder.cpp conflict.cpp + conflict2.cpp constraint.cpp eq_explain.cpp explain.cpp diff --git a/src/math/polysat/conflict2.cpp b/src/math/polysat/conflict2.cpp new file mode 100644 index 000000000..694c253b3 --- /dev/null +++ b/src/math/polysat/conflict2.cpp @@ -0,0 +1,122 @@ +/*++ +Copyright (c) 2021 Microsoft Corporation + +Module Name: + + polysat conflict + +Author: + + Nikolaj Bjorner (nbjorner) 2021-03-19 + Jakob Rath 2021-04-06 + +Notes: + +--*/ + +#include "math/polysat/conflict2.h" +#include "math/polysat/solver.h" +#include "math/polysat/inference_logger.h" +#include "math/polysat/log.h" +#include "math/polysat/log_helper.h" +#include "math/polysat/explain.h" +#include "math/polysat/eq_explain.h" +#include "math/polysat/forbidden_intervals.h" +#include "math/polysat/saturation.h" +#include "math/polysat/variable_elimination.h" +#include +#include + +namespace polysat { + + conflict2::conflict2(solver& s) : s(s) { + // TODO: m_log_conflicts is always false even if "polysat.log_conflicts=true" is given on the command line + if (true || s.get_config().m_log_conflicts) + m_logger = alloc(file_inference_logger, s); + else + m_logger = alloc(dummy_inference_logger); + } + + inference_logger& conflict2::logger() { + return *m_logger; + } + + bool conflict2::empty() const { + return m_literals.empty() && m_vars.empty() && m_lemmas.empty(); + } + + void conflict2::reset() { + m_literals.reset(); + m_vars.reset(); + m_var_occurrences.reset(); + m_lemmas.reset(); + SASSERT(empty()); + } + + void conflict2::init(signed_constraint c) { + SASSERT(empty()); + if (c.bvalue(s) == l_false) { + // boolean conflict + NOT_IMPLEMENTED_YET(); + } else { + // conflict due to assignment + SASSERT(c.bvalue(s) == l_true); + SASSERT(c.is_currently_false(s)); + insert(c); + insert_vars(c); + } + SASSERT(!empty()); + } + + void conflict2::init(pvar v) { + // NOTE: do forbidden interval projection in this method (rather than keeping a separate state like we did before) + // Option 1: forbidden interval projection + // Option 2: add all constraints from m_viable + dependent variables + + // TODO: we need to know whether the conflict is from m_viable for m_viable_fallback + // - m_viable: standard forbidden interval lemma + // - m_viable_fallback: initial conflict is the unsat core of the univariate solver + // (a flag on this method might be good enough) + + // VERIFY(s.m_viable.resolve(v, *this)); + // log_inference(inf_fi_lemma(v)); + } + + bool conflict2::contains(sat::literal lit) const { + SASSERT(lit != sat::null_literal); + return m_literals.contains(lit.index()); + } + + void conflict2::insert(signed_constraint c) { + if (contains(c)) + return; + if (c.is_always_true()) + return; + LOG("Inserting: " << c); + SASSERT(!c.is_always_false()); // if we add c, the core would be a tautology + SASSERT(!c->vars().empty()); + m_literals.insert(c.blit().index()); + for (pvar v : c->vars()) { + if (v >= m_var_occurrences.size()) + m_var_occurrences.resize(v + 1, 0); + m_var_occurrences[v]++; + } + } + + void conflict2::remove(signed_constraint c) { + SASSERT(contains(c)); + m_literals.remove(c.blit().index()); + for (pvar v : c->vars()) + m_var_occurrences[v]--; + } + + void conflict2::insert_vars(signed_constraint c) { + for (pvar v : c->vars()) + if (s.is_assigned(v)) + m_vars.insert(v); + } + + std::ostream& conflict2::display(std::ostream& out) const { + out << "TODO\n"; + } +} diff --git a/src/math/polysat/conflict2.h b/src/math/polysat/conflict2.h new file mode 100644 index 000000000..6cec7714c --- /dev/null +++ b/src/math/polysat/conflict2.h @@ -0,0 +1,140 @@ +/*++ +Copyright (c) 2021 Microsoft Corporation + +Module Name: + + polysat conflict + +Author: + + Nikolaj Bjorner (nbjorner) 2021-03-19 + Jakob Rath 2021-04-06 + +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 <- D - v is assigned value by constraints D + v = value <- ? - v is a decision literal. + + - All literals should be assigned in the stack prior to their use. + + l <- D => l, < Vars, { l } u C > ===> < Vars, C u D > + l <- ?, < Vars, { l } u C > ===> ~l <- (C & Vars = value(Vars) => ~l) + l <- asserted, < Vars, { l } u C > ===> < Vars, { l } u C > + l <- Vars', < Vars, { l } u C > ===> < Vars u Vars', C > if all Vars' are propagated + l <- Vars', < Vars, { l } u C > ===> Mark < Vars, { l } u C > as bailout + + v = value <- D, < Vars u { v }, C > ===> < Vars, D u C > + v = value <- ?, < Vars u { v }, C > ===> v != value <- (C & Vars = value(Vars) => v != value) + + +Example derivations: + +Trail: z <= y <- asserted + xz > xy <- asserted + x = a <- ? + y = b <- ? + z = c <- ? +Conflict: < {x, y, z}, xz > xy > when ~O(a,b) and c <= b +Append x <= a <- { x } +Append y <= b <- { y } +Conflict: < {}, y >= z, xz > xy, x <= a, y <= b > +Based on: z <= y & x <= a & y <= b => xz <= xy +Resolve: y <= b <- { y }, y is a decision variable. +Bailout: lemma ~(y >= z & xz > xy & x <= a & y <= b) at decision level of lemma + +With overflow predicate: +Append ~O(x, y) <- { x, y } +Conflict: < {}, y >= z, xz > xy, ~O(x,y) > +Based on z <= y & ~O(x,y) => xz <= xy +Resolve: ~O(x, y) <- { x, y } both x, y are decision variables +Lemma: y < z or xz <= xy or O(x,y) + + + + + +--*/ +#pragma once +#include "math/polysat/constraint.h" +#include "math/polysat/clause_builder.h" +#include + +namespace polysat { + + class solver; + class explainer; + class inference_engine; + class variable_elimination_engine; + class conflict_iterator; + class inference_logger; + + class conflict2 { + solver& s; + scoped_ptr m_logger; + + // current conflict core consists of m_literals and m_vars + indexed_uint_set m_literals; // set of boolean literals in the conflict + uint_set m_vars; // variable assignments used as premises, shorthand for literals (x := v) + + unsigned_vector m_var_occurrences; // for each variable, the number of constraints in m_literals that contain it + + // additional lemmas generated during conflict resolution + vector m_lemmas; + + // TODO: + // conflict resolution plugins + // - may generate lemma + // - may force backjumping without further conflict resolution + // - bailout lemma if no method applies (log these cases in particular because it indicates where we are missing something) + + public: + conflict2(solver& s); + + inference_logger& logger(); + + bool empty() const; + void reset(); + + /** conflict because the constraint c is false under current variable assignment */ + void init(signed_constraint c); + /** conflict because there is no viable value for the variable v */ + void init(pvar v); + + bool contains(signed_constraint c) const { SASSERT(c); return contains(c.blit()); } + bool contains(sat::literal lit) const; + + /** + * Insert constraint c into conflict state. + * + * Skips trivial constraints: + * - e.g., constant constraints such as "4 > 1" + */ + void insert(signed_constraint c); + + /** Insert assigned variables of c */ + void insert_vars(signed_constraint c); + + /** Remove c from core */ + void remove(signed_constraint c); + + std::ostream& display(std::ostream& out) const; + }; + + inline std::ostream& operator<<(std::ostream& out, conflict2 const& c) { return c.display(out); } + +}