mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-22 16:45:31 +00:00
Code Activity

Connect conflict2

Browse source
This commit is contained in:
Jakob Rath 2022-09-21 12:12:57 +02:00
parent a978604a7e
commit b43971bb4a
9 changed files with 420 additions and 293 deletions
Download patch file Download diff file Expand all files Collapse all files

9
src/math/polysat/CMakeLists.txt
View file

@ -4,10 +4,9 @@ z3_add_component(polysat
clause.cpp
clause_builder.cpp
conflict.cpp
conflict2.cpp
constraint.cpp
eq_explain.cpp
explain.cpp
# eq_explain.cpp
# explain.cpp
forbidden_intervals.cpp
inference_logger.cpp
justification.cpp
@ -15,7 +14,7 @@ z3_add_component(polysat
log.cpp
op_constraint.cpp
restart.cpp
saturation.cpp
# saturation.cpp
search_state.cpp
simplify.cpp
simplify_clause.cpp
@ -23,7 +22,7 @@ z3_add_component(polysat
solver.cpp
ule_constraint.cpp
umul_ovfl_constraint.cpp
variable_elimination.cpp
# variable_elimination.cpp
viable.cpp
COMPONENT_DEPENDENCIES
util

205
src/math/polysat/conflict.cpp
View file

@ -14,7 +14,8 @@ Notes:
--*/
#include "math/polysat/conflict2.h"
#include "math/polysat/conflict.h"
#include "math/polysat/clause_builder.h"
#include "math/polysat/solver.h"
#include "math/polysat/inference_logger.h"
#include "math/polysat/log.h"
@ -25,10 +26,17 @@ Notes:
#include "math/polysat/saturation.h"
#include "math/polysat/variable_elimination.h"
#include <algorithm>
#include <fstream>
namespace polysat {
class header_with_var : public displayable {
char const* m_text;
pvar m_var;
public:
header_with_var(char const* text, pvar var) : m_text(text), m_var(var) { SASSERT(text); }
std::ostream& display(std::ostream& out) const override { return out << m_text << m_var; }
};
struct inf_resolve_bool : public inference {
sat::literal m_lit;
clause const& m_clause;
@ -61,7 +69,7 @@ namespace polysat {
}
};
conflict2::conflict2(solver& s) : s(s) {
conflict::conflict(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);
@ -69,35 +77,73 @@ namespace polysat {
m_logger = alloc(dummy_inference_logger);
}
inference_logger& conflict2::logger() {
inference_logger& conflict::logger() {
return *m_logger;
}
bool conflict2::empty() const {
return m_literals.empty() && m_vars.empty() && m_lemmas.empty();
conflict::const_iterator conflict::begin() const {
return conflict_iterator::begin(s.m_constraints, m_literals);
}
void conflict2::reset() {
conflict::const_iterator conflict::end() const {
return conflict_iterator::end(s.m_constraints, m_literals);
}
bool conflict::empty() const {
return m_literals.empty()
&& m_vars.empty()
&& m_bail_vars.empty()
&& m_lemmas.empty();
}
void conflict::reset() {
m_literals.reset();
m_vars.reset();
m_bail_vars.reset();
m_relevant_vars.reset();
m_var_occurrences.reset();
m_lemmas.reset();
m_kind = conflict2_kind_t::ok;
m_kind = conflict_kind_t::ok;
SASSERT(empty());
}
void conflict2::set_bailout() {
SASSERT(m_kind == conflict2_kind_t::ok);
m_kind = conflict2_kind_t::bailout;
void conflict::set_bailout() {
SASSERT(m_kind == conflict_kind_t::ok);
m_kind = conflict_kind_t::bailout;
s.m_stats.m_num_bailouts++;
}
void conflict2::set_backjump() {
SASSERT(m_kind == conflict2_kind_t::ok);
m_kind = conflict2_kind_t::backjump;
void conflict::set_backtrack() {
SASSERT(m_kind == conflict_kind_t::ok);
SASSERT(m_relevant_vars.empty());
m_kind = conflict_kind_t::backtrack;
}
void conflict::set_backjump() {
SASSERT(m_kind == conflict_kind_t::ok);
m_kind = conflict_kind_t::backjump;
}
void conflict2::init(signed_constraint c) {
bool conflict::is_relevant_pvar(pvar v) const {
switch (m_kind) {
case conflict_kind_t::ok:
return contains_pvar(v);
case conflict_kind_t::bailout:
return true;
case conflict_kind_t::backtrack:
return pvar_occurs_in_constraints(v) || m_relevant_vars.contains(v);
// return m_relevant_vars.contains(v);
case conflict_kind_t::backjump:
UNREACHABLE(); // we don't follow the regular loop when backjumping
return false;
}
}
bool conflict::is_relevant(sat::literal lit) const {
return contains(lit) || contains(~lit);
}
void conflict::init(signed_constraint c) {
SASSERT(empty());
if (c.bvalue(s) == l_false) {
// boolean conflict
@ -110,34 +156,48 @@ namespace polysat {
insert_vars(c);
}
SASSERT(!empty());
logger().begin_conflict(); // TODO: we often call reset/set so doing this here doesn't really work... make subsequent begins a no-op? or separate init and set? (set could then do reset() internally ... and we only need set() for signed_constraint, not all three variations)
}
void conflict::init(clause const& cl) {
// if (!empty())
// return;
// LOG("Conflict: " << cl);
SASSERT(empty());
for (auto lit : cl) {
auto c = s.lit2cnstr(lit);
SASSERT(c.bvalue(s) == l_false);
insert(~c);
}
SASSERT(!empty());
logger().begin_conflict();
}
void conflict2::init(pvar v, bool by_viable_fallback) {
void conflict::init(pvar v, bool by_viable_fallback) {
if (by_viable_fallback) {
logger().begin_conflict(header_with_var("unsat core from viable fallback for v", v));
// Conflict detected by viable fallback:
// initial conflict is the unsat core of the univariate solver
signed_constraints unsat_core = s.m_viable_fallback.unsat_core(v);
for (auto c : unsat_core)
insert(c);
logger().begin_conflict("unsat core from viable fallback");
// TODO: apply conflict resolution plugins here too?
} else {
logger().begin_conflict(header_with_var("forbidden interval lemma for v", v));
set_backtrack();
VERIFY(s.m_viable.resolve(v, *this));
// TODO: in general the forbidden interval lemma is not asserting.
// but each branch exclude the current assignment.
// in those cases we will (additionally?) need an abstraction that is asserting to make sure viable is updated properly.
set_backjump();
logger().begin_conflict("forbidden interval lemma");
}
}
bool conflict2::contains(sat::literal lit) const {
bool conflict::contains(sat::literal lit) const {
SASSERT(lit != sat::null_literal);
return m_literals.contains(lit.index());
}
void conflict2::insert(signed_constraint c) {
void conflict::insert(signed_constraint c) {
if (contains(c))
return;
if (c.is_always_true())
@ -153,7 +213,7 @@ namespace polysat {
}
}
void conflict2::insert_eval(signed_constraint c) {
void conflict::insert_eval(signed_constraint c) {
switch (c.bvalue(s)) {
case l_undef:
s.assign_eval(c.blit());
@ -166,20 +226,20 @@ namespace polysat {
insert(c);
}
void conflict2::insert_vars(signed_constraint c) {
void conflict::insert_vars(signed_constraint c) {
for (pvar v : c->vars())
if (s.is_assigned(v))
m_vars.insert(v);
}
void conflict2::remove(signed_constraint c) {
void conflict::remove(signed_constraint c) {
SASSERT(contains(c));
m_literals.remove(c.blit().index());
for (pvar v : c->vars())
m_var_occurrences[v]--;
}
void conflict2::resolve_bool(sat::literal lit, clause const& cl) {
void conflict::resolve_bool(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
@ -197,7 +257,7 @@ namespace polysat {
logger().log(inf_resolve_bool(lit, cl));
}
void conflict2::resolve_with_assignment(sat::literal lit) {
void conflict::resolve_with_assignment(sat::literal lit) {
// The reason for lit is conceptually:
// x1 = v1 /\ ... /\ xn = vn ==> lit
@ -227,19 +287,21 @@ namespace polysat {
logger().log(inf_resolve_with_assignment(s, lit, c));
}
bool conflict2::resolve_value(pvar v) {
SASSERT(contains_pvar(v));
if (is_backjumping()) {
for (auto const& c : s.m_viable.get_constraints(v))
for (pvar v : c->vars())
logger().log_var(v);
return false;
}
bool conflict::resolve_value(pvar v) {
if (is_bailout())
return false;
if (is_backtracking()) {
for (auto const& c : s.m_viable.get_constraints(v))
for (pvar v : c->vars()) {
m_relevant_vars.insert(v);
logger().log_var(v);
}
return false;
}
SASSERT(contains_pvar(v));
auto const& j = s.m_justification[v];
if (j.is_decision() && m_bail_vars.contains(v)) // TODO: what if also m_vars.contains(v)? might have a chance at elimination
@ -265,12 +327,79 @@ namespace polysat {
// Need to keep the variable in case of decision
if (s.is_assigned(v) && j.is_decision())
m_vars.insert(v);
logger().log("bailout");
logger().log("Bailout");
return false;
}
std::ostream& conflict2::display(std::ostream& out) const {
out << "TODO\n";
clause_ref conflict::build_lemma() {
LOG_H3("Build lemma from core");
LOG("core: " << *this);
clause_builder lemma(s);
// TODO: is this sound, doing it for each constraint separately?
// for (auto c : *this)
// minimize_vars(c);
for (auto c : *this)
lemma.push(~c);
for (unsigned v : m_vars) {
auto eq = s.eq(s.var(v), s.get_value(v));
if (eq.bvalue(s) == l_undef)
s.assign_eval(eq.blit());
lemma.push(~eq);
}
s.decay_activity();
logger().log_lemma(lemma);
logger().end_conflict();
return lemma.build();
}
bool conflict::minimize_vars(signed_constraint c) {
if (m_vars.empty())
return false;
if (!c.is_currently_false(s))
return false;
assignment_t a;
for (auto v : m_vars)
a.push_back(std::make_pair(v, s.get_value(v)));
for (unsigned i = 0; i < a.size(); ++i) {
std::pair<pvar, rational> save = a[i];
std::pair<pvar, rational> last = a.back();
a[i] = last;
a.pop_back();
if (c.is_currently_false(s, a))
--i;
else {
a.push_back(last);
a[i] = save;
}
}
if (a.size() == m_vars.num_elems())
return false;
m_vars.reset();
for (auto const& [v, val] : a)
m_vars.insert(v);
logger().log("minimize vars");
LOG("reduced " << m_vars);
return true;
}
std::ostream& conflict::display(std::ostream& out) const {
char const* sep = "";
for (auto c : *this)
out << sep << c->bvar2string() << " " << c, sep = " ; ";
if (!m_vars.empty())
out << " vars";
for (auto v : m_vars)
out << " v" << v;
if (!m_bail_vars.empty())
out << " bail vars";
for (auto v : m_bail_vars)
out << " v" << v;
return out;
}
}

104
src/math/polysat/conflict.h
View file

@ -77,42 +77,54 @@ TODO:
- bailout lemma if no method applies (log these cases in particular because it indicates where we are missing something)
- force a restart if we get a bailout lemma or non-asserting conflict?
- consider case if v is both in vars and bail_vars (do we need to keep it in bail_vars even if we can eliminate it from vars?)
- Find a way to use resolve_value with forbidden interval lemmas.
Then get rid of conflict_kind_t::backtrack and m_relevant_vars.
Maybe:
x := a, y := b, z has no viable value
- assume y was propagated
- FI-Lemma C1 \/ ... \/ Cn without z.
- for each i, we should have x := a /\ Ci ==> y != b
- can we choose one of the Ci to cover the domain of y and extract an FI-Lemma D1 \/ ... \/ Dk without y,z?
- or try to find an L(x,y) such that C1 -> L, ..., Cn -> L, and L -> y != b (under x := a); worst case y != b can work as L
- minimize_vars... is it sound to do for each constraint separately, like we are doing now?
--*/
#pragma once
#include "math/polysat/constraint.h"
#include "math/polysat/clause_builder.h"
#include "math/polysat/inference_logger.h"
#include <optional>
namespace polysat {
class solver;
class explainer;
class inference_engine;
class variable_elimination_engine;
class conflict_iterator;
class inference_logger;
enum class conflict2_kind_t {
enum class conflict_kind_t {
// standard conflict resolution
ok,
// bailout lemma because no appropriate conflict resolution method applies
bailout,
// conflict contains the final lemma;
// backtrack to and revert the last relevant decision
// NOTE: this is currently used for the forbidden intervals lemmas.
// we should find a way to use resolve_value with these lemmas,
// to properly eliminate value propagations. (see todo notes above)
backtrack,
// conflict contains the final lemma;
// force backjumping without further conflict resolution because a good lemma has been found
// TODO: distinguish backtrack/revert of last decision from backjump to second-highest level in the lemma
backjump,
};
class conflict2 {
class conflict {
solver& s;
scoped_ptr<inference_logger> 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)
uint_set m_bail_vars; // tracked for cone of influence but not directly involved in conflict resolution
uint_set m_bail_vars; // decision variables that are only used to evaluate a constraint; see resolve_with_assignment.
uint_set m_relevant_vars; // tracked for cone of influence but not directly involved in conflict resolution
unsigned_vector m_var_occurrences; // for each variable, the number of constraints in m_literals that contain it
@ -120,31 +132,47 @@ namespace polysat {
// TODO: we might not need all of these in the end. add only the side lemmas which justify a constraint in the final lemma (recursively)?
vector<clause_ref> m_lemmas;
conflict2_kind_t m_kind = conflict2_kind_t::ok;
conflict_kind_t m_kind = conflict_kind_t::ok;
bool minimize_vars(signed_constraint c);
public:
conflict2(solver& s);
conflict(solver& s);
inference_logger& logger();
bool empty() const;
void reset();
uint_set const& vars() const { return m_vars; }
using const_iterator = conflict_iterator;
const_iterator begin() const;
const_iterator end() const;
bool is_bailout() const { return m_kind == conflict2_kind_t::bailout; }
bool is_backjumping() const { return m_kind == conflict2_kind_t::backjump; }
uint_set const& vars() const { return m_vars; }
uint_set const& bail_vars() const { return m_bail_vars; }
conflict_kind_t kind() const { return m_kind; }
bool is_bailout() const { return m_kind == conflict_kind_t::bailout; }
bool is_backtracking() const { return m_kind == conflict_kind_t::backtrack; }
bool is_backjumping() const { return m_kind == conflict_kind_t::backjump; }
void set_bailout();
void set_backtrack();
void set_backjump();
bool is_relevant_pvar(pvar v) const;
bool is_relevant(sat::literal lit) const;
/** conflict because the constraint c is false under current variable assignment */
void init(signed_constraint c);
/** boolean conflict with the given clause */
void init(clause const& cl);
/** conflict because there is no viable value for the variable v */
void init(pvar v, bool by_viable_fallback = false);
void init(pvar v, bool by_viable_fallback);
bool contains(signed_constraint c) const { SASSERT(c); return contains(c.blit()); }
bool contains(sat::literal lit) const;
bool contains_pvar(pvar v) const { return m_vars.contains(v) || m_bail_vars.contains(v); }
bool pvar_occurs_in_constraints(pvar v) const { return v < m_var_occurrences.size() && m_var_occurrences[v] > 0; }
/**
* Insert constraint c into conflict state.
@ -172,9 +200,53 @@ namespace polysat {
/** Perform resolution with "v = value <- ..." */
bool resolve_value(pvar v);
/** Convert the core into a lemma to be learned. */
clause_ref build_lemma();
std::ostream& display(std::ostream& out) const;
};
inline std::ostream& operator<<(std::ostream& out, conflict2 const& c) { return c.display(out); }
inline std::ostream& operator<<(std::ostream& out, conflict const& c) { return c.display(out); }
class conflict_iterator {
friend class conflict;
using inner_t = indexed_uint_set::iterator;
constraint_manager* m_cm;
inner_t m_inner;
conflict_iterator(constraint_manager& cm, inner_t inner):
m_cm(&cm), m_inner(inner) {}
static conflict_iterator begin(constraint_manager& cm, indexed_uint_set const& lits) {
return {cm, lits.begin()};
}
static conflict_iterator end(constraint_manager& cm, indexed_uint_set const& lits) {
return {cm, lits.end()};
}
public:
using value_type = signed_constraint;
using difference_type = unsigned;
using pointer = signed_constraint const*;
using reference = signed_constraint const&;
using iterator_category = std::input_iterator_tag;
conflict_iterator& operator++() {
++m_inner;
return *this;
}
signed_constraint operator*() const {
return m_cm->lookup(sat::to_literal(*m_inner));
}
bool operator==(conflict_iterator const& other) const {
return m_inner == other.m_inner;
}
bool operator!=(conflict_iterator const& other) const { return !operator==(other); }
};
}

42
src/math/polysat/inference_logger.cpp
View file

@ -40,48 +40,53 @@ namespace polysat {
return std::string(70, '-');
}
void file_inference_logger::begin_conflict(char const* text) {
void file_inference_logger::begin_conflict(displayable const& header) {
++m_num_conflicts;
if (text)
LOG("Begin CONFLICT #" << m_num_conflicts << " (" << text << ")");
else
LOG("Begin CONFLICT #" << m_num_conflicts);
LOG("Begin CONFLICT #" << m_num_conflicts << ": " << header);
m_used_constraints.reset();
m_used_vars.reset();
if (!m_out)
m_out = alloc(std::ofstream, "conflicts.txt");
else
out() << "\n\n\n\n\n\n\n\n\n\n\n\n";
out() << "CONFLICT #" << m_num_conflicts;
if (text)
out() << " (" << text << ")";
out() << "\n";
out() << "CONFLICT #" << m_num_conflicts << ": " << header << "\n";
// log initial conflict state
out() << hline() << "\n";
log_conflict_state();
}
void file_inference_logger::log_conflict_state() {
out() << "TODO";
/* TODO: update for new conflict
conflict2 const& core = s.m_conflict2;
conflict const& core = s.m_conflict;
for (auto const& c : core) {
out_indent() << c.blit() << ": " << c << '\n';
m_used_constraints.insert(c.blit().index());
sat::literal const lit = c.blit();
out_indent() << lit << ": " << c << '\n';
// TODO: if justified by a side lemma, print it here
// out_indent() << " justified by: " << lemma << '\n';
m_used_constraints.insert(lit.index());
for (pvar v : c->vars())
m_used_vars.insert(v);
}
for (auto v : core.vars()) {
out_indent() << assignment_pp(core.s, v, core.s.get_value(v)) << "\n";
out_indent() << assignment_pp(s, v, s.get_value(v)) << "\n";
m_used_vars.insert(v);
}
for (auto v : core.bail_vars()) {
out_indent() << assignment_pp(core.s, v, core.s.get_value(v)) << " (bail)\n";
out_indent() << assignment_pp(s, v, s.get_value(v)) << " (bail)\n";
m_used_vars.insert(v);
}
if (core.is_bailout())
switch (core.kind()) {
case conflict_kind_t::ok:
break;
case conflict_kind_t::bailout:
out_indent() << "(bailout)\n";
*/
break;
case conflict_kind_t::backtrack:
out_indent() << "(backtrack)\n";
break;
case conflict_kind_t::backjump:
out_indent() << "(backjump)\n";
break;
}
out().flush();
}
@ -102,7 +107,6 @@ namespace polysat {
out() << "\n";
for (auto const& lit : cb)
out_indent() << lit_pp(s, lit) << "\n";
// out_indent() << lit << ": " << s.lit2cnstr(lit) << "\n";
out().flush();
}

34
src/math/polysat/inference_logger.h
View file

@ -26,13 +26,26 @@ namespace polysat {
class search_item;
class solver;
class inference {
class displayable {
public:
virtual ~inference() {}
virtual ~displayable() {}
virtual std::ostream& display(std::ostream& out) const = 0;
};
inline std::ostream& operator<<(std::ostream& out, inference const& i) { return i.display(out); }
inline std::ostream& operator<<(std::ostream& out, displayable const& d) { return d.display(out); }
class display_c_str : public displayable {
char const* m_str;
public:
display_c_str(char const* str) : m_str(str) { }
std::ostream& display(std::ostream& out) const override {
if (m_str)
out << m_str;
return out;
}
};
class inference : public displayable { };
class inference_named : public inference {
char const* m_name;
@ -46,12 +59,14 @@ namespace polysat {
virtual ~inference_logger() {}
/// Begin next conflict
virtual void begin_conflict(char const* text = nullptr) = 0;
void begin_conflict(char const* text = nullptr) { begin_conflict(display_c_str(text)); }
virtual void begin_conflict(displayable const& header) = 0;
/// Log inference and the current state.
virtual void log(inference const& inf) = 0;
virtual void log(char const* name) { log(inference_named(name)); }
virtual void log_var(pvar v) = 0;
/// Log relevant part of search state and viable.
/// Call end_conflict before backjumping in the solver.
virtual void end_conflict() = 0;
/// Log current conflict state (implicitly done by log_inference)
@ -62,7 +77,7 @@ namespace polysat {
class dummy_inference_logger : public inference_logger {
public:
virtual void begin_conflict(char const* text) override {}
virtual void begin_conflict(displayable const& header) override {}
virtual void log(inference const& inf) override {}
virtual void log_var(pvar v) override {}
virtual void end_conflict() override {}
@ -85,18 +100,11 @@ namespace polysat {
public:
file_inference_logger(solver& s);
/// Begin next conflict
void begin_conflict(char const* text) override;
/// Log inference and the current state.
void begin_conflict(displayable const& header) override;
void log(inference const& inf) override;
void log_var(pvar v) override;
/// Log relevant part of search state and viable.
void end_conflict() override;
/// Log current conflict state (implicitly done by log_inference)
void log_conflict_state() override;
void log_lemma(clause_builder const& cb) override;
};

124
src/math/polysat/solver.cpp
View file

@ -33,7 +33,6 @@ namespace polysat {
m_viable_fallback(*this),
m_linear_solver(*this),
m_conflict(*this),
m_conflict2(*this),
m_simplify_clause(*this),
m_simplify(*this),
m_restart(*this),
@ -545,7 +544,7 @@ namespace polysat {
// (fail here in debug mode so we notice if we miss some)
DEBUG_CODE( UNREACHABLE(); );
m_free_pvars.unassign_var_eh(v);
set_conflict(v);
set_conflict(v, false);
return;
case dd::find_t::singleton:
// NOTE: this case may happen legitimately if all other possibilities were excluded by brute force search
@ -578,8 +577,7 @@ namespace polysat {
case dd::find_t::empty:
LOG("Fallback solver: unsat");
m_free_pvars.unassign_var_eh(v);
auto core = m_viable_fallback.unsat_core(v); // TODO: add constraints from unsat_core to conflict
set_conflict(v);
set_conflict(v, true);
return;
}
}
@ -620,17 +618,6 @@ namespace polysat {
SASSERT(is_conflict());
if (m_conflict.conflict_var() != null_var) {
m_conflict.begin_conflict("backtrack_fi");
pvar v = m_conflict.conflict_var();
// This case corresponds to a propagation of conflict_var, except it's not explicitly on the stack.
// TODO: use unsat core from m_viable_fallback if the conflict is from there
VERIFY(m_viable.resolve(v, m_conflict));
backtrack_fi();
return;
}
m_conflict.begin_conflict("resolve_conflict");
search_iterator search_it(m_search);
while (search_it.next()) {
auto& item = *search_it;
@ -638,23 +625,21 @@ namespace polysat {
if (item.is_assignment()) {
// Resolve over variable assignment
pvar v = item.var();
if (!m_conflict.contains_pvar(v) && !m_conflict.is_bailout()) {
// if (!m_conflict.contains_pvar(v) && !m_conflict.is_bailout()) {
if (!m_conflict.is_relevant_pvar(v)) {
m_search.pop_assignment();
continue;
}
LOG_H2("Working on " << search_item_pp(m_search, item));
LOG(m_justification[v]);
LOG("Conflict: " << m_conflict);
// inc_activity(v); // done in resolve_value
justification& j = m_justification[v];
if (j.level() > base_level() && !m_conflict.resolve_value(v) && j.is_decision()) {
m_conflict.end_conflict();
revert_decision(v);
return;
}
if (m_conflict.is_bailout_lemma()) {
m_conflict.end_conflict();
backtrack_lemma();
if (m_conflict.is_backjumping()) {
backjump_lemma();
return;
}
m_search.pop_assignment();
@ -664,36 +649,37 @@ namespace polysat {
SASSERT(item.is_boolean());
sat::literal const lit = item.lit();
sat::bool_var const var = lit.var();
if (!m_conflict.is_marked(var))
if (!m_conflict.is_relevant(lit))
continue;
LOG_H2("Working on " << search_item_pp(m_search, item));
LOG(bool_justification_pp(m_bvars, lit));
LOG("Literal " << lit << " is " << lit2cnstr(lit));
LOG("Conflict: " << m_conflict);
if (m_bvars.is_assumption(var)) // TODO: wouldn't this mean we're already at the base level?
continue;
if (m_bvars.is_assumption(var)) {
SASSERT(m_bvars.level(var) <= base_level());
break;
}
else if (m_bvars.is_bool_propagation(var))
m_conflict.resolve(lit, *m_bvars.reason(lit));
m_conflict.resolve_bool(lit, *m_bvars.reason(lit));
else {
SASSERT(m_bvars.is_value_propagation(var));
m_conflict.resolve_with_assignment(lit, m_bvars.level(lit));
m_conflict.resolve_with_assignment(lit);
}
}
}
LOG("End of resolve_conflict loop");
m_conflict.end_conflict();
m_conflict.logger().end_conflict();
report_unsat();
}
/**
* Simple backtracking for lemmas:
* Simple backjumping for lemmas:
* jump to the level where the lemma can be (bool-)propagated,
* even without reverting the last decision.
*/
void solver::backtrack_lemma() {
clause_ref lemma = m_conflict.build_lemma().build();
LOG_H2("backtrack_lemma: " << show_deref(lemma));
void solver::backjump_lemma() {
clause_ref lemma = m_conflict.build_lemma();
LOG_H2("backjump_lemma: " << show_deref(lemma));
SASSERT(lemma);
LOG("Lemma: " << *lemma);
for (sat::literal lit : *lemma) {
@ -715,6 +701,7 @@ namespace polysat {
jump_level = lit_level;
}
}
SASSERT(max_level == m_level); // not required; see comment on max_level
jump_level = std::max(jump_level, base_level());
@ -728,69 +715,6 @@ namespace polysat {
learn_lemma(*lemma);
}
/**
* Simpler backtracking for forbidden interval lemmas:
* since forbidden intervals already gives us a lemma where the conflict variable has been eliminated,
* we can backtrack to the last relevant decision and learn this lemma.
*/
void solver::backtrack_fi() {
uint_set relevant_vars;
search_iterator search_it(m_search);
while (search_it.next()) {
auto& item = *search_it;
search_it.set_resolved();
if (item.is_assignment()) {
// Resolve over variable assignment
pvar v = item.var();
if (!m_conflict.pvar_occurs_in_constraints(v) && !relevant_vars.contains(v)) {
m_search.pop_assignment();
continue;
}
LOG_H2("Working on " << search_item_pp(m_search, item));
LOG(m_justification[v]);
LOG("Conflict: " << m_conflict);
inc_activity(v);
justification& j = m_justification[v];
if (j.level() > base_level() && j.is_decision()) {
m_conflict.end_conflict();
revert_decision(v);
return;
}
SASSERT(j.is_propagation());
// If a variable was propagated:
// we don't really care about the constraints in this case, but just about the variables it depends on
for (auto const& c : m_viable.get_constraints(v))
for (pvar v : c->vars()) {
relevant_vars.insert(v);
m_conflict.log_var(v);
}
m_search.pop_assignment();
}
else {
// Resolve over boolean literal
SASSERT(item.is_boolean());
sat::literal const lit = item.lit();
sat::bool_var const var = lit.var();
if (!m_conflict.is_marked(var))
continue;
LOG_H2("Working on " << search_item_pp(m_search, item));
LOG(bool_justification_pp(m_bvars, lit));
LOG("Literal " << lit << " is " << lit2cnstr(lit));
LOG("Conflict: " << m_conflict);
if (m_bvars.is_assumption(var)) // TODO: wouldn't this mean we're already at the base level?
continue;
else if (m_bvars.is_bool_propagation(var))
m_conflict.resolve(lit, *m_bvars.reason(lit));
else {
SASSERT(m_bvars.is_value_propagation(var));
continue;
}
}
}
m_conflict.end_conflict();
report_unsat();
}
/**
* Variable activity accounting.
* As a placeholder we increment activity
@ -839,6 +763,7 @@ namespace polysat {
LOG("Learning: "<< lemma);
SASSERT(!lemma.empty());
m_simplify_clause.apply(lemma);
// TODO: print warning if the lemma is non-asserting?
add_clause(lemma);
}
@ -858,7 +783,7 @@ namespace polysat {
LOG_H3("Reverting decision: pvar " << v << " := " << val);
SASSERT(m_justification[v].is_decision());
clause_ref lemma = m_conflict.build_lemma().build();
clause_ref lemma = m_conflict.build_lemma();
if (lemma->empty())
report_unsat();
else {
@ -887,7 +812,7 @@ namespace polysat {
}
void solver::assign_eval(sat::literal lit) {
SASSERT(lit2cnstr(lit).is_currently_true(*this));
// SASSERT(lit2cnstr(lit).is_currently_true(*this)); // "morally" this should hold, but currently fails because of pop_assignment during resolve_conflict
unsigned level = 0;
// NOTE: constraint may be evaluated even if some variables are still unassigned (e.g., 0*x doesn't depend on x).
for (auto v : lit2cnstr(lit)->vars())
@ -934,12 +859,13 @@ namespace polysat {
void solver::add_clause(clause& clause) {
LOG((clause.is_redundant() ? "Lemma: ": "Aux: ") << clause);
for (sat::literal lit : clause) {
LOG(" Literal " << lit << " is: " << lit_pp(*this, lit));
LOG(" " << lit_pp(*this, lit));
// SASSERT(m_bvars.value(lit) != l_true);
// it could be that such a literal has been created previously but we don't detect it when e.g. narrowing a mul_ovfl_constraint
if (m_bvars.value(lit) == l_true) {
// in this case the clause is useless
LOG(" Clause is already true, skipping...");
// SASSERT(false); // should never happen (at least for redundant clauses)
return;
}
}
@ -1106,12 +1032,14 @@ namespace polysat {
* Check that two variables of each constraint are watched.
*/
bool solver::wlist_invariant() {
#if 0
for (pvar v = 0; v < m_value.size(); ++v) {
std::stringstream s;
for (constraint* c : m_pwatch[v])
s << " " << c->bvar();
LOG("Watch for v" << v << ": " << s.str());
}
#endif
// Skip boolean variables that aren't active yet
uint_set skip;
for (unsigned i = m_qhead; i < m_search.size(); ++i)

20
src/math/polysat/solver.h
View file

@ -22,7 +22,6 @@ Author:
#include "util/params.h"
#include "math/polysat/boolean.h"
#include "math/polysat/conflict.h"
#include "math/polysat/conflict2.h"
#include "math/polysat/constraint.h"
#include "math/polysat/clause_builder.h"
#include "math/polysat/simplify_clause.h"
@ -37,8 +36,6 @@ Author:
#include "math/polysat/viable.h"
#include "math/polysat/log.h"
namespace polysat {
struct config {
@ -70,14 +67,12 @@ namespace polysat {
friend class clause;
friend class clause_builder;
friend class conflict;
friend class conflict2;
friend class conflict_explainer;
friend class simplify_clause;
friend class simplify;
friend class restart;
friend class explainer;
friend class inference_engine;
friend class old_inference_logger;
friend class file_inference_logger;
friend class forbidden_intervals;
friend class linear_solver;
@ -94,7 +89,6 @@ namespace polysat {
friend class scoped_solverv;
friend class test_polysat;
friend class test_fi;
friend struct inference_resolve_with_assignment;
friend struct inf_resolve_with_assignment;
reslimit& m_lim;
@ -105,7 +99,6 @@ namespace polysat {
viable_fallback m_viable_fallback; // fallback for viable, using bitblasting over univariate constraints
linear_solver m_linear_solver;
conflict m_conflict;
conflict2 m_conflict2;
simplify_clause m_simplify_clause;
simplify m_simplify;
restart m_restart;
@ -192,9 +185,9 @@ namespace polysat {
void erase_pwatch(pvar v, constraint* c);
void erase_pwatch(constraint* c);
void set_conflict(signed_constraint c) { m_conflict.set(c); }
void set_conflict(clause& cl) { m_conflict.set(cl); }
void set_conflict(pvar v) { m_conflict.set(v); }
void set_conflict(signed_constraint c) { m_conflict.init(c); }
void set_conflict(clause& cl) { m_conflict.init(cl); }
void set_conflict(pvar v, bool by_viable_fallback) { m_conflict.init(v, by_viable_fallback); }
bool can_decide() const { return !m_free_pvars.empty(); }
void decide();
@ -202,14 +195,12 @@ namespace polysat {
void linear_propagate();
bool is_conflict() const { return !m_conflict.empty(); }
bool at_base_level() const;
unsigned base_level() const;
void resolve_conflict();
void backtrack_fi();
void backtrack_lemma();
void backjump_lemma();
void revert_decision(pvar v);
void revert_bool_decision(sat::literal lit);
@ -461,7 +452,4 @@ namespace polysat {
inline std::ostream& operator<<(std::ostream& out, assignments_pp const& a) { return a.display(out); }
}

146
src/math/polysat/viable.cpp
View file

@ -29,9 +29,19 @@ TODO: improve management of the fallback univariate solvers:
#include "util/debug.h"
#include "math/polysat/viable.h"
#include "math/polysat/solver.h"
#include "math/polysat/univariate/univariate_solver.h"
namespace polysat {
struct inf_fi : public inference {
viable& v;
pvar var;
inf_fi(viable& v, pvar var) : v(v), var(var) {}
std::ostream& display(std::ostream& out) const override {
return out << "Forbidden intervals for v" << var << ": " << viable::var_pp(v, var);
}
};
viable::viable(solver& s):
s(s),
m_forbidden_intervals(s) {
@ -54,7 +64,7 @@ namespace polysat {
m_diseq_lin.pop_back();
}
viable::entry* viable::alloc_entry() {
viable::entry* viable::alloc_entry() {
if (m_alloc.empty())
return alloc(entry);
auto* e = m_alloc.back();
@ -68,21 +78,21 @@ namespace polysat {
auto& [v, k, e] = m_trail.back();
SASSERT(well_formed(m_units[v]));
switch (k) {
case entry_kind::unit_e:
e->remove_from(m_units[v], e);
case entry_kind::unit_e:
e->remove_from(m_units[v], e);
SASSERT(well_formed(m_units[v]));
break;
case entry_kind::equal_e:
e->remove_from(m_equal_lin[v], e);
case entry_kind::equal_e:
e->remove_from(m_equal_lin[v], e);
break;
case entry_kind::diseq_e:
e->remove_from(m_diseq_lin[v], e);
e->remove_from(m_diseq_lin[v], e);
break;
default:
UNREACHABLE();
break;
}
m_alloc.push_back(e);
m_alloc.push_back(e);
m_trail.pop_back();
}
@ -98,12 +108,12 @@ namespace polysat {
if (e->interval.lo_val() < m_units[v]->interval.lo_val())
m_units[v] = e;
}
else
m_units[v] = e;
else
m_units[v] = e;
SASSERT(well_formed(m_units[v]));
m_trail.pop_back();
}
bool viable::intersect(pdd const & p, pdd const & q, signed_constraint const& sc) {
pvar v = null_var;
bool first = true;
@ -124,7 +134,7 @@ namespace polysat {
prop = true;
break;
case dd::find_t::empty:
s.set_conflict(v);
s.set_conflict(v, false);
return true;
default:
break;
@ -136,7 +146,7 @@ namespace polysat {
goto try_viable;
}
return prop;
}
}
bool viable::intersect(pvar v, signed_constraint const& c) {
entry* ne = alloc_entry();
@ -184,12 +194,11 @@ namespace polysat {
m_alloc.push_back(ne);
return false;
}
auto create_entry = [&]() {
m_trail.push_back({ v, entry_kind::unit_e, ne });
s.m_trail.push_back(trail_instr_t::viable_add_i);
ne->init(ne);
ne->init(ne);
return ne;
};
@ -200,13 +209,13 @@ namespace polysat {
};
if (ne->interval.is_full()) {
while (m_units[v])
while (m_units[v])
remove_entry(m_units[v]);
m_units[v] = create_entry();
return true;
}
if (!e)
if (!e)
m_units[v] = create_entry();
else {
entry* first = e;
@ -222,10 +231,10 @@ namespace polysat {
m_units[v] = create_entry();
return true;
}
if (e == first)
first = n;
if (e == first)
first = n;
e = n;
}
}
SASSERT(e->interval.lo_val() != ne->interval.lo_val());
if (e->interval.lo_val() > ne->interval.lo_val()) {
if (first->prev()->interval.currently_contains(ne->interval)) {
@ -239,7 +248,7 @@ namespace polysat {
return true;
}
e = e->next();
}
}
while (e != first);
// otherwise, append to end of list
first->insert_before(create_entry());
@ -255,10 +264,10 @@ namespace polysat {
/**
* Traverse all interval constraints with coefficients to check whether current value 'val' for
* 'v' is feasible. If not, extract a (maximal) interval to block 'v' from being assigned val.
*
*
* To investigate:
* - side conditions are stronger than for unit intervals. They constrain the lower and upper bounds to
* be precisely the assigned values. This is to ensure that lo/hi that are computed based on lo_val
* be precisely the assigned values. This is to ensure that lo/hi that are computed based on lo_val
* and division with coeff are valid. Is there a more relaxed scheme?
*/
bool viable::refine_equal_lin(pvar v, rational const& val) {
@ -330,7 +339,7 @@ namespace polysat {
if (e->interval.lo_val() < e->interval.hi_val()) {
increase_hi(hi);
decrease_lo(lo);
decrease_lo(lo);
}
else if (e->interval.lo_val() <= coeff_val) {
rational lambda_u = floor((max_value - coeff_val) / e->coeff);
@ -342,13 +351,13 @@ namespace polysat {
else {
SASSERT(coeff_val < e->interval.hi_val());
rational lambda_l = floor(coeff_val / e->coeff);
lo = val - lambda_l;
lo = val - lambda_l;
increase_hi(hi);
}
LOG("forbidden interval v" << v << " " << val << " " << e->coeff << " * " << e->interval << " [" << lo << ", " << hi << "[");
SASSERT(hi <= mod_value);
bool full = (lo == 0 && hi == mod_value);
if (hi == mod_value)
bool full = (lo == 0 && hi == mod_value);
if (hi == mod_value)
hi = 0;
pdd lop = s.var2pdd(v).mk_val(lo);
pdd hip = s.var2pdd(v).mk_val(hi);
@ -358,13 +367,13 @@ namespace polysat {
ne->coeff = 1;
if (full)
ne->interval = eval_interval::full();
else
else
ne->interval = eval_interval::proper(lop, lo, hip, hi);
intersect(v, ne);
return false;
}
e = e->next();
}
}
while (e != first);
return true;
}
@ -453,7 +462,7 @@ namespace polysat {
return true;
}
bool viable::has_viable(pvar v) {
bool viable::has_viable(pvar v) {
refined:
auto* e = m_units[v];
@ -468,9 +477,9 @@ namespace polysat {
return false;
// quick check: last interval doesn't wrap around, so hi_val
// has not been covered
if (last->interval.lo_val() < last->interval.hi_val())
if (last->interval.lo_val() < last->interval.hi_val())
CHECK_RETURN(last->interval.hi_val());
do {
if (e->interval.is_full())
return false;
@ -482,16 +491,16 @@ namespace polysat {
if (n == first) {
if (e->interval.lo_val() > e->interval.hi_val())
return false;
CHECK_RETURN(e->interval.hi_val());
CHECK_RETURN(e->interval.hi_val());
}
e = n;
}
}
while (e != first);
return false;
#undef CHECK_RETURN
}
bool viable::is_viable(pvar v, rational const& val) {
bool viable::is_viable(pvar v, rational const& val) {
auto* e = m_units[v];
if (!e)
return refine_viable(v, val);
@ -499,17 +508,17 @@ namespace polysat {
entry* last = first->prev();
if (last->interval.currently_contains(val))
return false;
for (; e != last; e = e->next()) {
for (; e != last; e = e->next()) {
if (e->interval.currently_contains(val))
return false;
if (val < e->interval.lo_val())
return refine_viable(v, val);
}
if (val < e->interval.lo_val())
return refine_viable(v, val);
}
return refine_viable(v, val);
}
rational viable::min_viable(pvar v) {
rational viable::min_viable(pvar v) {
refined:
rational lo(0);
auto* e = m_units[v];
@ -521,20 +530,20 @@ namespace polysat {
entry* last = first->prev();
if (last->interval.currently_contains(lo))
lo = last->interval.hi_val();
do {
do {
if (!e->interval.currently_contains(lo))
break;
lo = e->interval.hi_val();
e = e->next();
}
}
while (e != first);
if (!refine_viable(v, lo))
goto refined;
SASSERT(is_viable(v, lo));
SASSERT(is_viable(v, lo));
return lo;
}
rational viable::max_viable(pvar v) {
rational viable::max_viable(pvar v) {
refined:
rational hi = s.var2pdd(v).max_value();
auto* e = m_units[v];
@ -549,7 +558,7 @@ namespace polysat {
break;
hi = e->interval.lo_val() - 1;
e = e->prev();
}
}
while (e != last);
if (!refine_viable(v, hi))
goto refined;
@ -557,7 +566,7 @@ namespace polysat {
return hi;
}
dd::find_t viable::find_viable(pvar v, rational& lo) {
dd::find_t viable::find_viable(pvar v, rational& lo) {
refined:
lo = 0;
auto* e = m_units[v];
@ -594,7 +603,7 @@ namespace polysat {
break;
lo = e->interval.hi_val();
e = e->next();
}
}
while (e != first);
if (e->interval.currently_contains(lo))
@ -608,7 +617,7 @@ namespace polysat {
break;
hi = e->interval.lo_val() - 1;
e = e->prev();
}
}
while (e != last);
if (!refine_viable(v, lo))
goto refined;
@ -620,20 +629,6 @@ namespace polysat {
return dd::find_t::multiple;
}
struct inference_fi : public inference {
viable& v;
pvar var;
inference_fi(viable& v, pvar var) : v(v), var(var) {}
std::ostream& display(std::ostream& out) const override {
return out << "Forbidden intervals for v" << var << ": " << viable::var_pp(v, var);
}
};
bool viable::resolve(pvar v, conflict2& core) {
NOT_IMPLEMENTED_YET();
return false;
}
bool viable::resolve(pvar v, conflict& core) {
if (has_viable(v))
return false;
@ -652,7 +647,7 @@ namespace polysat {
auto lhs = hi - next_lo;
auto rhs = next_hi - next_lo;
signed_constraint c = s.m_constraints.ult(lhs, rhs);
core.propagate(c);
core.insert_eval(c);
#if 0
if (n != first) {
while {
@ -666,21 +661,26 @@ namespace polysat {
}
#endif
}
for (auto sc : e->side_cond)
core.propagate(sc);
for (auto sc : e->side_cond)
core.insert_eval(sc);
core.insert(e->src);
e = n;
}
}
while (e != first);
core.logger().log(inf_fi(*this, v));
// TODO: should not be here, too general
/*
for (auto c : core) {
if (c.bvalue(s) == l_false) {
core.reset();
core.set(~c);
core.logger().log("");
break;
}
}
core.log_inference(inference_fi(*this, v));
*/
return true;
}
@ -694,7 +694,7 @@ namespace polysat {
do {
LOG("v" << v << ": " << e->interval << " " << e->side_cond << " " << e->src);
e = e->next();
}
}
while (e != first);
}
@ -712,7 +712,7 @@ namespace polysat {
out << e->coeff << " * v" << v << " ";
out << e->interval << " " << e->side_cond << " " << e->src << "; ";
e = e->next();
}
}
while (e != first);
return out;
}
@ -732,7 +732,7 @@ namespace polysat {
/*
* Lower bounds are strictly ascending.
* intervals don't contain each-other (since lower bounds are ascending,
* intervals don't contain each-other (since lower bounds are ascending,
* it suffices to check containment in one direction).
*/
bool viable::well_formed(entry* e) {
@ -742,15 +742,15 @@ namespace polysat {
while (true) {
if (e->interval.is_full())
return e->next() == e;
if (e->interval.is_currently_empty())
if (e->interval.is_currently_empty())
return false;
auto* n = e->next();
if (n != e && e->interval.currently_contains(n->interval))
return false;
if (n == first)
break;
break;
if (e->interval.lo_val() >= n->interval.lo_val())
return false;
e = n;

29
src/math/polysat/viable.h
View file

@ -5,7 +5,7 @@ Module Name:
maintain viable domains
It uses the interval extraction functions from forbidden intervals.
An empty viable set corresponds directly to a conflict that does not rely on
An empty viable set corresponds directly to a conflict that does not rely on
the non-viable variable.
Author:
@ -23,24 +23,24 @@ Author:
#include "util/small_object_allocator.h"
#include "math/polysat/types.h"
#include "math/polysat/conflict.h"
#include "math/polysat/conflict2.h"
#include "math/polysat/constraint.h"
#include "math/polysat/forbidden_intervals.h"
#include "math/polysat/univariate/univariate_solver.h"
namespace polysat {
class solver;
class univariate_solver;
class univariate_solver_factory;
class viable {
friend class test_fi;
solver& s;
forbidden_intervals m_forbidden_intervals;
struct entry : public dll_base<entry>, public fi_record {};
enum class entry_kind { unit_e, equal_e, diseq_e };
ptr_vector<entry> m_alloc;
ptr_vector<entry> m_units; // set of viable values based on unit multipliers
ptr_vector<entry> m_equal_lin; // entries that have non-unit multipliers, but are equal
@ -112,7 +112,6 @@ namespace polysat {
* \pre there are no viable values for v
*/
bool resolve(pvar v, conflict& core);
bool resolve(pvar v, conflict2& core);
/** Log all viable values for the given variable.
* (Inefficient, but useful for debugging small instances.)
@ -129,11 +128,11 @@ namespace polysat {
bool visited = false;
unsigned idx = 0;
public:
iterator(entry* curr, bool visited) :
iterator(entry* curr, bool visited) :
curr(curr), visited(visited || !curr) {}
iterator& operator++() {
if (idx < curr->side_cond.size())
if (idx < curr->side_cond.size())
++idx;
else {
idx = 0;
@ -143,7 +142,7 @@ namespace polysat {
return *this;
}
signed_constraint& operator*() {
signed_constraint& operator*() {
return idx < curr->side_cond.size() ? curr->side_cond[idx] : curr->src;
}
@ -165,8 +164,8 @@ namespace polysat {
iterator end() const { return iterator(v.m_units[var], true); }
};
constraints get_constraints(pvar v) const {
return constraints(*this, v);
constraints get_constraints(pvar v) const {
return constraints(*this, v);
}
class int_iterator {
@ -181,8 +180,8 @@ namespace polysat {
return *this;
}
eval_interval const& operator*() {
return curr->interval;
eval_interval const& operator*() {
return curr->interval;
}
bool operator==(int_iterator const& other) const {
@ -210,10 +209,10 @@ namespace polysat {
struct var_pp {
viable const& v;
pvar var;
pvar var;
var_pp(viable const& v, pvar var) : v(v), var(var) {}
};
};
inline std::ostream& operator<<(std::ostream& out, viable const& v) {