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

move files (conflict2 -> conflict)

Browse source
This commit is contained in:
Jakob Rath 2022-09-20 10:26:38 +02:00
parent 48d5a98edc
commit a978604a7e
6 changed files with 1134 additions and 1134 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -8,21 +8,15 @@ Module Name:
Author:
Nikolaj Bjorner (nbjorner) 2021-03-19
Jakob Rath 2021-04-6
Jakob Rath 2021-04-06
Notes:
TODO: try a final core reduction step or other core minimization
TODO: revert(pvar v) is too weak.
It should apply saturation rules currently only available for propagated values.
TODO: dependency tracking for constraints evaluating to false should be minimized.
--*/
#include "math/polysat/conflict.h"
#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"
@ -35,359 +29,20 @@ Notes:
namespace polysat {
class old_inference_logger {
uint_set m_used_constraints;
uint_set m_used_vars;
scoped_ptr<std::ostream> m_out = nullptr;
unsigned m_conflicts = 0;
friend class conflict;
std::ostream& out() {
SASSERT(m_out);
return *m_out;
}
std::ostream& out_indent() { return out() << " "; }
std::string hline() const { return std::string(70, '-'); }
public:
void begin_conflict(char const* text) {
++m_conflicts;
if (text)
LOG("Begin CONFLICT #" << m_conflicts << " (" << text << ")");
else
LOG("Begin CONFLICT #" << m_conflicts);
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_conflicts << " (" << text << ")" << "\n";
}
void log_inference(conflict const& core, inference const* inf) {
out() << hline() << "\n";
if (inf)
out() << *inf << "\n";
if (core.conflict_var() != null_var) {
out_indent() << "Conflict var: " << core.conflict_var() << "\n";
m_used_vars.insert(core.conflict_var());
}
for (auto const& c : core) {
out_indent() << c.blit() << ": " << c << '\n';
m_used_constraints.insert(c.blit().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";
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";
m_used_vars.insert(v);
}
if (core.is_bailout())
out_indent() << "(bailout)\n";
out().flush();
}
void log_lemma(solver const& s, clause_builder const& cb) {
out() << hline() << "\nLemma:";
for (auto const& lit : cb)
out() << " " << lit;
out() << "\n";
for (auto const& lit : cb)
out_indent() << lit << ": " << s.lit2cnstr(lit) << '\n';
out().flush();
}
void end_conflict(search_state const& search, viable const& v) {
out() << "\n" << hline() << "\n\n";
out() << "Search state (part):\n";
for (auto const& item : search)
if (is_relevant(item))
out_indent() << search_item_pp(search, item, true) << "\n";
out() << hline() << "\nViable (part):\n";
for (pvar var : m_used_vars)
out_indent() << "v" << std::setw(3) << std::left << var << ": " << viable::var_pp(v, var) << "\n";
out().flush();
LOG("End CONFLICT #" << m_conflicts);
}
bool is_relevant(search_item const& item) const {
switch (item.kind()) {
case search_item_k::assignment:
return m_used_vars.contains(item.var());
case search_item_k::boolean:
return m_used_constraints.contains(item.lit().index());
}
UNREACHABLE();
return false;
}
};
void conflict::log_var(pvar v) {
if (m_logger)
m_logger->m_used_vars.insert(v);
}
conflict::conflict(solver& s): s(s) {
ex_engines.push_back(alloc(ex_polynomial_superposition, s));
ex_engines.push_back(alloc(eq_explain, s));
ve_engines.push_back(alloc(ve_reduction));
inf_engines.push_back(alloc(inf_saturate, s));
// TODO: how to set this on the CLI? "polysat.log_conflicts=true" doesn't seem to work although z3 accepts it
if (true || s.get_config().m_log_conflicts)
m_logger = alloc(old_inference_logger);
}
conflict::~conflict() {}
void conflict::begin_conflict(char const* text) {
if (m_logger) {
m_logger->begin_conflict(text);
// log initial conflict state
m_logger->log_inference(*this, nullptr);
}
}
void conflict::log_inference(inference const& inf) {
if (m_logger)
m_logger->log_inference(*this, &inf);
}
void conflict::end_conflict() {
if (m_logger)
m_logger->end_conflict(s.m_search, s.m_viable);
}
constraint_manager& conflict::cm() const { return s.m_constraints; }
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;
}
bool conflict::empty() const {
return m_literals.empty()
&& m_vars.empty()
&& m_bail_vars.empty()
&& m_conflict_var == null_var;
}
void conflict::reset() {
for (auto c : *this)
unset_mark(c);
m_literals.reset();
m_vars.reset();
m_var_occurrences.reset();
m_bail_vars.reset();
m_conflict_var = null_var;
m_kind = conflict_kind_t::ok;
SASSERT(empty());
}
/**
* The constraint is false under the current assignment of variables.
* The core is then the conjuction of this constraint and assigned variables.
*/
void conflict::set(signed_constraint c) {
LOG("Conflict: " << c << " " << c.bvalue(s));
SASSERT(empty());
if (c.bvalue(s) == l_false) {
auto* cl = s.m_bvars.reason(c.blit().var());
if (cl)
set(*cl);
else
insert(c);
}
else {
SASSERT(c.is_currently_false(s));
// TBD: fails with test_subst SASSERT(c.bvalue(s) == l_true);
insert_vars(c);
insert(c);
}
SASSERT(!empty());
}
/**
* The variable v cannot be assigned.
* The conflict is the set of justifications accumulated for the viable values for v.
* These constraints are (in the current form) not added to the core, but passed directly
* to the forbidden interval module.
* A consistent approach could be to add these constraints to the core and then also include the
* variable assignments.
*/
void conflict::set(pvar v) {
LOG("Conflict: v" << v);
SASSERT(empty());
m_conflict_var = v;
SASSERT(!empty());
}
/**
* The clause is conflicting in the current search state.
*/
void conflict::set(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());
}
/**
* Insert constraint into conflict state
* Skip trivial constraints
* - e.g., constant ones such as "4 > 1"... only true ones
* should appear, otherwise the lemma would be a tautology
*/
void conflict::insert(signed_constraint c) {
if (c.is_always_true())
return;
if (is_marked(c))
return;
LOG("inserting: " << c);
SASSERT(!c->vars().empty());
set_mark(c);
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 conflict::propagate(signed_constraint c) {
switch (c.bvalue(s)) {
case l_undef:
s.assign_eval(c.blit());
break;
case l_true:
break;
case l_false:
break;
}
insert(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.
* Premises that are justified by value assignments are not assigned (the bvalue is l_undef)
* The justification for those premises are based on the free assigned variables.
*
* NOTE: maybe we should skip intermediate steps and just collect the leaf premises for c?
* Ensure that c is assigned and justified
*/
// TODO: rename this; it pushes onto \Gamma and doesn't insert into the core
void conflict::insert(signed_constraint c, vector<signed_constraint> const& premises) {
// keep(c);
clause_builder c_lemma(s);
for (auto premise : premises) {
LOG_H3("premise: " << premise);
// keep(premise);
SASSERT(premise.bvalue(s) != l_false);
c_lemma.push(~premise.blit());
}
c_lemma.push(c.blit());
clause_ref lemma = c_lemma.build();
SASSERT(lemma);
cm().store(lemma.get(), s, false);
if (c.bvalue(s) == l_undef)
s.assign_propagate(c.blit(), *lemma);
}
void conflict::remove(signed_constraint c) {
unset_mark(c);
m_literals.remove(c.blit().index());
for (pvar v : c->vars()) {
if (v < m_var_occurrences.size())
m_var_occurrences[v]--;
}
}
void conflict::replace(signed_constraint c_old, signed_constraint c_new, vector<signed_constraint> const& c_new_premises) {
remove(c_old);
insert(c_new, c_new_premises);
}
bool conflict::contains(signed_constraint c) const {
return m_literals.contains(c.blit().index());
}
bool conflict::contains(sat::literal lit) const {
SASSERT(lit != sat::null_literal);
return m_literals.contains(lit.index());
}
void conflict::set_bailout_gave_up() {
SASSERT(m_kind == conflict_kind_t::ok);
m_kind = conflict_kind_t::bailout_gave_up;
s.m_stats.m_num_bailouts++;
}
void conflict::set_bailout_lemma() {
SASSERT(m_kind == conflict_kind_t::ok);
m_kind = conflict_kind_t::bailout_lemma;
// s.m_stats.m_num_bailouts++;
}
struct inference_resolve : public inference {
struct inf_resolve_bool : public inference {
sat::literal m_lit;
clause const& m_clause;
inference_resolve(sat::literal lit, clause const& cl) : m_lit(lit), m_clause(cl) {}
inf_resolve_bool(sat::literal lit, clause const& cl) : m_lit(lit), m_clause(cl) {}
std::ostream& display(std::ostream& out) const override {
return out << "Resolve upon " << m_lit << " with " << m_clause;
}
};
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
SASSERT(contains(lit));
SASSERT(std::count(cl.begin(), cl.end(), lit) > 0);
SASSERT(!contains(~lit));
SASSERT(std::count(cl.begin(), cl.end(), ~lit) == 0);
remove(s.lit2cnstr(lit));
for (sat::literal lit2 : cl)
if (lit2 != lit)
insert(s.lit2cnstr(~lit2));
log_inference(inference_resolve(lit, cl));
}
struct inference_resolve_with_assignment : public inference {
struct inf_resolve_with_assignment : public inference {
solver& s;
sat::literal lit;
signed_constraint c;
inference_resolve_with_assignment(solver& s, sat::literal lit, signed_constraint c) : s(s), lit(lit), c(c) {}
inf_resolve_with_assignment(solver& s, sat::literal lit, signed_constraint c) : s(s), lit(lit), c(c) {}
std::ostream& display(std::ostream& out) const override {
out << "Resolve upon " << lit << " with assignment:";
for (pvar v : c->vars())
@ -397,207 +52,225 @@ namespace polysat {
}
};
void conflict::resolve_with_assignment(sat::literal lit, unsigned lvl) {
struct inf_resolve_value : public inference {
solver& s;
pvar v;
inf_resolve_value(solver& s, pvar v) : s(s), v(v) {}
std::ostream& display(std::ostream& out) const override {
return out << "Value resolution with " << assignment_pp(s, v, s.get_value(v), true);
}
};
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();
m_kind = conflict2_kind_t::ok;
SASSERT(empty());
}
void conflict2::set_bailout() {
SASSERT(m_kind == conflict2_kind_t::ok);
m_kind = conflict2_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 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());
logger().begin_conflict();
}
void conflict2::init(pvar v, bool by_viable_fallback) {
if (by_viable_fallback) {
// 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 {
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 {
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 added 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::insert_eval(signed_constraint c) {
switch (c.bvalue(s)) {
case l_undef:
s.assign_eval(c.blit());
break;
case l_true:
break;
case l_false:
break;
}
insert(c);
}
void conflict2::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) {
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) {
// 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
SASSERT(contains(lit));
SASSERT(std::count(cl.begin(), cl.end(), lit) > 0);
SASSERT(!contains(~lit));
SASSERT(std::count(cl.begin(), cl.end(), ~lit) == 0);
remove(s.lit2cnstr(lit));
for (sat::literal other : cl)
if (other != lit)
insert(s.lit2cnstr(~other));
logger().log(inf_resolve_bool(lit, cl));
}
void conflict2::resolve_with_assignment(sat::literal lit) {
// The reason for lit is conceptually:
// x1 = v1 /\ ... /\ xn = vn ==> lit
SASSERT(contains(lit));
SASSERT(!contains(~lit));
if (is_backjumping())
return;
unsigned const lvl = s.m_bvars.level(lit);
signed_constraint c = s.lit2cnstr(lit);
// If evaluation depends on a decision,
// then we rather keep the more general constraint c instead of inserting "x = v"
bool has_decision = false;
for (pvar v : c->vars())
if (s.is_assigned(v) && s.m_justification[v].is_decision())
for (pvar v : c->vars())
if (s.is_assigned(v) && s.m_justification[v].is_decision())
m_bail_vars.insert(v), has_decision = true;
if (!has_decision) {
remove(c);
for (pvar v : c->vars())
if (s.is_assigned(v)) {
// TODO: 'lit' was propagated at level 'lvl'; can we here ignore variables above that?
SASSERT(s.get_level(v) <= lvl);
m_vars.insert(v);
}
for (pvar v : c->vars())
if (s.is_assigned(v) && s.get_level(v) <= lvl)
m_vars.insert(v);
}
log_inference(inference_resolve_with_assignment(s, lit, c));
logger().log(inf_resolve_with_assignment(s, lit, c));
}
clause_builder conflict::build_lemma() {
LOG_H3("Build lemma from core");
LOG("core: " << *this);
clause_builder lemma(s);
bool conflict2::resolve_value(pvar v) {
SASSERT(contains_pvar(v));
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();
if (m_logger)
m_logger->log_lemma(s, lemma);
return lemma;
}
void conflict::minimize_vars(signed_constraint c) {
if (m_vars.empty())
return;
if (!c.is_currently_false(s))
return;
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;
m_vars.reset();
for (auto const& [v, val] : a)
m_vars.insert(v);
log_inference("minimize vars");
LOG("reduced " << m_vars);
}
struct inference_resolve_value : public inference {
solver& s;
pvar v;
inference_resolve_value(solver& s, pvar v) : s(s), v(v) {}
std::ostream& display(std::ostream& out) const override {
return out << "Value resolution with " << assignment_pp(s, v, s.get_value(v), true);
}
};
bool conflict::resolve_value(pvar v) {
// NOTE:
// In the "standard" case where "v = val" is on the stack:
// forbidden interval projection is performed at top level
SASSERT(v != conflict_var());
bool has_saturated = false;
auto const& j = s.m_justification[v];
if (j.is_decision() && m_bail_vars.contains(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;
s.inc_activity(v);
m_vars.remove(v);
if (j.is_propagation()) {
for (auto const& c : s.m_viable.get_constraints(v))
propagate(c);
for (auto const& i : s.m_viable.units(v)) {
propagate(s.eq(i.lo(), i.lo_val()));
propagate(s.eq(i.hi(), i.hi_val()));
}
}
if (is_bailout())
goto bailout;
return false;
LOG("try-explain v" << v);
if (try_explain(v))
return true;
auto const& j = s.m_justification[v];
// No value resolution method was successful => fall back to saturation and variable elimination
while (s.inc()) {
LOG("try-eliminate v" << v);
// TODO: as a last resort, substitute v by m_value[v]?
if (try_eliminate(v))
return true;
LOG("try-saturate v" << v);
if (try_saturate(v))
has_saturated = true;
else
break;
if (j.is_decision() && m_bail_vars.contains(v)) // TODO: what if also m_vars.contains(v)? might have a chance at elimination
return false;
s.inc_activity(v);
m_vars.remove(v);
if (j.is_propagation()) {
for (auto const& c : s.m_viable.get_constraints(v))
insert_eval(c);
for (auto const& i : s.m_viable.units(v)) {
insert_eval(s.eq(i.lo(), i.lo_val()));
insert_eval(s.eq(i.hi(), i.hi_val()));
}
}
LOG("bailout v" << v);
if (has_saturated) {
// NOTE: current saturation rules create valid lemmas that do not depend on the variable assignment
set_bailout_lemma();
return true;
}
else
set_bailout_gave_up();
bailout:
logger().log(inf_resolve_value(s, v));
// TODO: call conflict resolution plugins here; "return true" if successful
// No conflict resolution plugin succeeded => give up and bail out
set_bailout();
// Need to keep the variable in case of decision
if (s.is_assigned(v) && j.is_decision())
m_vars.insert(v);
log_inference(inference_resolve_value(s, v));
logger().log("bailout");
return false;
}
bool conflict::try_eliminate(pvar v) {
LOG("try v" << v << " contains " << m_vars.contains(v));
if (m_vars.contains(v))
return false;
bool has_v = false;
for (auto c : *this)
has_v |= c->contains_var(v);
if (!has_v)
return true;
for (auto* engine : ve_engines)
if (engine->perform(s, v, *this))
return true;
return false;
}
bool conflict::try_saturate(pvar v) {
for (auto* engine : inf_engines)
if (engine->perform(v, *this))
return true;
return false;
}
bool conflict::try_explain(pvar v) {
for (auto* engine : ex_engines)
if (engine->try_explain(v, *this))
return true;
return false;
}
void conflict::set_mark(signed_constraint c) {
sat::bool_var b = c->bvar();
if (b >= m_bvar2mark.size())
m_bvar2mark.resize(b + 1);
SASSERT(!m_bvar2mark[b]);
m_bvar2mark[b] = true;
}
/**
* unset marking on the constraint, but keep variable dependencies.
*/
void conflict::unset_mark(signed_constraint c) {
sat::bool_var b = c->bvar();
SASSERT(m_bvar2mark[b]);
m_bvar2mark[b] = false;
}
bool conflict::is_marked(signed_constraint c) const {
return is_marked(c->bvar());
}
bool conflict::is_marked(sat::bool_var b) const {
return m_bvar2mark.get(b, false);
std::ostream& conflict2::display(std::ostream& out) const {
out << "TODO\n";
return out;
}
}

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

@ -8,30 +8,31 @@ Module Name:
Author:
Nikolaj Bjorner (nbjorner) 2021-03-19
Jakob Rath 2021-04-6
Jakob Rath 2021-04-06
Notes:
A conflict state is of the form <Vars, Constraints>
Where Vars are shorthand for the constraints v = value(v) for v in Vars and value(v) is the assignent.
A conflict state is of the form <Vars, Constraints, Lemmas>
Where Vars are shorthand for the constraints v = value(v) for v in Vars and value(v) is the assignment.
Lemmas provide justifications for newly created constraints.
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.
- All literals should be assigned in the stack prior to their use;
or justified by one of the side lemmas.
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 >
@ -40,15 +41,15 @@ Notes:
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 <- ?
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 }
@ -58,7 +59,7 @@ 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 }
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
@ -66,8 +67,18 @@ Lemma: y < z or xz <= xy or O(x,y)
TODO:
- update notes/example above
- question: if a side lemma justifies a constraint, then we resolve over one of the premises of the lemma; do we want to update the lemma or not?
- conflict resolution plugins
- may generate lemma
- post-processing/simplification on lemma (e.g., literal subsumption; can be done in solver)
- may force backjumping without further conflict resolution (e.g., if applicable lemma was found by global analysis of search state)
- 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?)
--*/
#pragma once
#include "math/polysat/constraint.h"
@ -82,170 +93,88 @@ namespace polysat {
class inference_engine;
class variable_elimination_engine;
class conflict_iterator;
class old_inference_logger;
class inference_logger;
enum class conflict_kind_t {
enum class conflict2_kind_t {
// standard conflict resolution
ok,
bailout_gave_up,
bailout_lemma,
// bailout lemma because no appropriate conflict resolution method applies
bailout,
// 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,
};
/** Conflict state, represented as core (~negation of clause). */
class conflict {
class conflict2 {
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
unsigned_vector m_var_occurrences; // for each variable, the number of constraints in m_literals that contain it
uint_set m_vars; // variable assignments used as premises
uint_set m_bail_vars;
// If this is not null_var, the conflict was due to empty viable set for this variable.
// Can be treated like "v = x" for any value x.
pvar m_conflict_var = null_var;
// additional lemmas generated during conflict resolution
// 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;
/** Whether we are in a bailout state.
* We enter a bailout state when we give up on proper conflict resolution,
* or want to learn a lemma without fine-grained backtracking.
*/
conflict_kind_t m_kind = conflict_kind_t::ok;
friend class old_inference_logger;
scoped_ptr<old_inference_logger> m_logger;
bool_vector m_bvar2mark; // mark of Boolean variables
void set_mark(signed_constraint c);
void unset_mark(signed_constraint c);
void minimize_vars(signed_constraint c);
constraint_manager& cm() const;
scoped_ptr_vector<explainer> ex_engines;
scoped_ptr_vector<variable_elimination_engine> ve_engines;
scoped_ptr_vector<inference_engine> inf_engines;
conflict2_kind_t m_kind = conflict2_kind_t::ok;
public:
conflict(solver& s);
~conflict();
conflict2(solver& s);
/// Begin next conflict
void begin_conflict(char const* text = nullptr);
/// Log inference at the current state.
void log_inference(inference const& inf);
void log_inference(char const* name) { log_inference(inference_named(name)); }
void log_var(pvar v);
/// Log relevant part of search state and viable.
void end_conflict();
pvar conflict_var() const { return m_conflict_var; }
bool is_bailout() const { return m_kind != conflict_kind_t::ok; }
bool is_bailout_lemma() const { return m_kind == conflict_kind_t::bailout_lemma; }
void set_bailout_gave_up();
void set_bailout_lemma();
inference_logger& logger();
bool empty() const;
void reset();
bool pvar_occurs_in_constraints(pvar v) const { return v < m_var_occurrences.size() && m_var_occurrences[v] > 0; }
uint_set const& vars() const { return m_vars; }
bool contains_pvar(pvar v) const { return m_vars.contains(v) || m_bail_vars.contains(v); }
bool is_marked(signed_constraint c) const;
bool is_marked(sat::bool_var b) const;
bool is_bailout() const { return m_kind == conflict2_kind_t::bailout; }
bool is_backjumping() const { return m_kind == conflict2_kind_t::backjump; }
void set_bailout();
void set_backjump();
/** conflict because the constraint c is false under current variable assignment */
void set(signed_constraint c);
void init(signed_constraint c);
/** conflict because there is no viable value for the variable v */
void set(pvar v);
/** all literals in clause are false */
void set(clause const& cl);
void init(pvar v, bool by_viable_fallback = false);
void propagate(signed_constraint c);
void insert(signed_constraint c);
void insert_vars(signed_constraint c);
void insert(signed_constraint c, vector<signed_constraint> const& premises);
void remove(signed_constraint c);
void replace(signed_constraint c_old, signed_constraint c_new, vector<signed_constraint> const& c_new_premises);
bool contains(signed_constraint c) const;
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); }
/** Perform boolean resolution with the clause upon variable 'var'.
* Precondition: core/clause contain complementary 'var'-literals.
/**
* Insert constraint c into conflict state.
*
* Skips trivial constraints:
* - e.g., constant constraints such as "4 > 1"
*/
void resolve(sat::literal lit, clause const& cl);
void insert(signed_constraint c);
/** lit was fully evaluated under the assignment up to level 'lvl'.
*/
void resolve_with_assignment(sat::literal lit, unsigned lvl);
/** Insert assigned variables of c */
void insert_vars(signed_constraint c);
/** Perform value resolution by applying various inference rules.
* Returns true if it was possible to eliminate the variable 'v'.
*/
/** Evaluate constraint under assignment and insert it into conflict state. */
void insert_eval(signed_constraint c);
/** Remove c from core */
void remove(signed_constraint c);
/** Perform boolean resolution with the clause upon the given literal. */
void resolve_bool(sat::literal lit, clause const& cl);
/** lit was fully evaluated under the assignment. */
void resolve_with_assignment(sat::literal lit);
/** Perform resolution with "v = value <- ..." */
bool resolve_value(pvar v);
/** Convert the core into a lemma to be learned. */
clause_builder build_lemma();
bool try_eliminate(pvar v);
bool try_saturate(pvar v);
bool try_explain(pvar v);
using const_iterator = conflict_iterator;
const_iterator begin() const;
const_iterator end() const;
uint_set const& vars() const { return m_vars; }
uint_set const& bail_vars() const { return m_bail_vars; }
std::ostream& display(std::ostream& out) const;
};
inline std::ostream& operator<<(std::ostream& out, conflict const& c) { return c.display(out); }
inline std::ostream& operator<<(std::ostream& out, conflict2 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); }
};
inline conflict::const_iterator conflict::begin() const { return conflict_iterator::begin(cm(), m_literals); }
inline conflict::const_iterator conflict::end() const { return conflict_iterator::end(cm(), m_literals); }
}

276
src/math/polysat/conflict2.cpp
View file

@ -1,276 +0,0 @@
/*++
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 <algorithm>
#include <fstream>
namespace polysat {
struct inf_resolve_bool : public inference {
sat::literal m_lit;
clause const& m_clause;
inf_resolve_bool(sat::literal lit, clause const& cl) : m_lit(lit), m_clause(cl) {}
std::ostream& display(std::ostream& out) const override {
return out << "Resolve upon " << m_lit << " with " << m_clause;
}
};
struct inf_resolve_with_assignment : public inference {
solver& s;
sat::literal lit;
signed_constraint c;
inf_resolve_with_assignment(solver& s, sat::literal lit, signed_constraint c) : s(s), lit(lit), c(c) {}
std::ostream& display(std::ostream& out) const override {
out << "Resolve upon " << lit << " with assignment:";
for (pvar v : c->vars())
if (s.is_assigned(v))
out << " " << assignment_pp(s, v, s.get_value(v), true);
return out;
}
};
struct inf_resolve_value : public inference {
solver& s;
pvar v;
inf_resolve_value(solver& s, pvar v) : s(s), v(v) {}
std::ostream& display(std::ostream& out) const override {
return out << "Value resolution with " << assignment_pp(s, v, s.get_value(v), true);
}
};
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();
m_kind = conflict2_kind_t::ok;
SASSERT(empty());
}
void conflict2::set_bailout() {
SASSERT(m_kind == conflict2_kind_t::ok);
m_kind = conflict2_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 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());
logger().begin_conflict();
}
void conflict2::init(pvar v, bool by_viable_fallback) {
if (by_viable_fallback) {
// 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 {
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 {
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 added 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::insert_eval(signed_constraint c) {
switch (c.bvalue(s)) {
case l_undef:
s.assign_eval(c.blit());
break;
case l_true:
break;
case l_false:
break;
}
insert(c);
}
void conflict2::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) {
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) {
// 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
SASSERT(contains(lit));
SASSERT(std::count(cl.begin(), cl.end(), lit) > 0);
SASSERT(!contains(~lit));
SASSERT(std::count(cl.begin(), cl.end(), ~lit) == 0);
remove(s.lit2cnstr(lit));
for (sat::literal other : cl)
if (other != lit)
insert(s.lit2cnstr(~other));
logger().log(inf_resolve_bool(lit, cl));
}
void conflict2::resolve_with_assignment(sat::literal lit) {
// The reason for lit is conceptually:
// x1 = v1 /\ ... /\ xn = vn ==> lit
SASSERT(contains(lit));
SASSERT(!contains(~lit));
if (is_backjumping())
return;
unsigned const lvl = s.m_bvars.level(lit);
signed_constraint c = s.lit2cnstr(lit);
// If evaluation depends on a decision,
// then we rather keep the more general constraint c instead of inserting "x = v"
bool has_decision = false;
for (pvar v : c->vars())
if (s.is_assigned(v) && s.m_justification[v].is_decision())
m_bail_vars.insert(v), has_decision = true;
if (!has_decision) {
remove(c);
for (pvar v : c->vars())
if (s.is_assigned(v) && s.get_level(v) <= lvl)
m_vars.insert(v);
}
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;
}
if (is_bailout())
return false;
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
return false;
s.inc_activity(v);
m_vars.remove(v);
if (j.is_propagation()) {
for (auto const& c : s.m_viable.get_constraints(v))
insert_eval(c);
for (auto const& i : s.m_viable.units(v)) {
insert_eval(s.eq(i.lo(), i.lo_val()));
insert_eval(s.eq(i.hi(), i.hi_val()));
}
}
logger().log(inf_resolve_value(s, v));
// TODO: call conflict resolution plugins here; "return true" if successful
// No conflict resolution plugin succeeded => give up and bail out
set_bailout();
// Need to keep the variable in case of decision
if (s.is_assigned(v) && j.is_decision())
m_vars.insert(v);
logger().log("bailout");
return false;
}
std::ostream& conflict2::display(std::ostream& out) const {
out << "TODO\n";
return out;
}
}

180
src/math/polysat/conflict2.h
View file

@ -1,180 +0,0 @@
/*++
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 <Vars, Constraints, Lemmas>
Where Vars are shorthand for the constraints v = value(v) for v in Vars and value(v) is the assignment.
Lemmas provide justifications for newly created constraints.
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 <- 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;
or justified by one of the side lemmas.
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)
TODO:
- update notes/example above
- question: if a side lemma justifies a constraint, then we resolve over one of the premises of the lemma; do we want to update the lemma or not?
- conflict resolution plugins
- may generate lemma
- post-processing/simplification on lemma (e.g., literal subsumption; can be done in solver)
- may force backjumping without further conflict resolution (e.g., if applicable lemma was found by global analysis of search state)
- 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?)
--*/
#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 {
// standard conflict resolution
ok,
// bailout lemma because no appropriate conflict resolution method applies
bailout,
// 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 {
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
unsigned_vector m_var_occurrences; // for each variable, the number of constraints in m_literals that contain it
// additional lemmas generated during conflict resolution
// 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;
public:
conflict2(solver& s);
inference_logger& logger();
bool empty() const;
void reset();
uint_set const& vars() const { return m_vars; }
bool is_bailout() const { return m_kind == conflict2_kind_t::bailout; }
bool is_backjumping() const { return m_kind == conflict2_kind_t::backjump; }
void set_bailout();
void set_backjump();
/** 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 by_viable_fallback = false);
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); }
/**
* 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);
/** Evaluate constraint under assignment and insert it into conflict state. */
void insert_eval(signed_constraint c);
/** Remove c from core */
void remove(signed_constraint c);
/** Perform boolean resolution with the clause upon the given literal. */
void resolve_bool(sat::literal lit, clause const& cl);
/** lit was fully evaluated under the assignment. */
void resolve_with_assignment(sat::literal lit);
/** Perform resolution with "v = value <- ..." */
bool resolve_value(pvar v);
std::ostream& display(std::ostream& out) const;
};
inline std::ostream& operator<<(std::ostream& out, conflict2 const& c) { return c.display(out); }
}

603
src/math/polysat/conflict_old.cpp Normal file
View file

@ -0,0 +1,603 @@
/*++
Copyright (c) 2021 Microsoft Corporation
Module Name:
polysat conflict
Author:
Nikolaj Bjorner (nbjorner) 2021-03-19
Jakob Rath 2021-04-6
Notes:
TODO: try a final core reduction step or other core minimization
TODO: revert(pvar v) is too weak.
It should apply saturation rules currently only available for propagated values.
TODO: dependency tracking for constraints evaluating to false should be minimized.
--*/
#include "math/polysat/conflict.h"
#include "math/polysat/solver.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 <algorithm>
#include <fstream>
namespace polysat {
class old_inference_logger {
uint_set m_used_constraints;
uint_set m_used_vars;
scoped_ptr<std::ostream> m_out = nullptr;
unsigned m_conflicts = 0;
friend class conflict;
std::ostream& out() {
SASSERT(m_out);
return *m_out;
}
std::ostream& out_indent() { return out() << " "; }
std::string hline() const { return std::string(70, '-'); }
public:
void begin_conflict(char const* text) {
++m_conflicts;
if (text)
LOG("Begin CONFLICT #" << m_conflicts << " (" << text << ")");
else
LOG("Begin CONFLICT #" << m_conflicts);
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_conflicts << " (" << text << ")" << "\n";
}
void log_inference(conflict const& core, inference const* inf) {
out() << hline() << "\n";
if (inf)
out() << *inf << "\n";
if (core.conflict_var() != null_var) {
out_indent() << "Conflict var: " << core.conflict_var() << "\n";
m_used_vars.insert(core.conflict_var());
}
for (auto const& c : core) {
out_indent() << c.blit() << ": " << c << '\n';
m_used_constraints.insert(c.blit().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";
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";
m_used_vars.insert(v);
}
if (core.is_bailout())
out_indent() << "(bailout)\n";
out().flush();
}
void log_lemma(solver const& s, clause_builder const& cb) {
out() << hline() << "\nLemma:";
for (auto const& lit : cb)
out() << " " << lit;
out() << "\n";
for (auto const& lit : cb)
out_indent() << lit << ": " << s.lit2cnstr(lit) << '\n';
out().flush();
}
void end_conflict(search_state const& search, viable const& v) {
out() << "\n" << hline() << "\n\n";
out() << "Search state (part):\n";
for (auto const& item : search)
if (is_relevant(item))
out_indent() << search_item_pp(search, item, true) << "\n";
out() << hline() << "\nViable (part):\n";
for (pvar var : m_used_vars)
out_indent() << "v" << std::setw(3) << std::left << var << ": " << viable::var_pp(v, var) << "\n";
out().flush();
LOG("End CONFLICT #" << m_conflicts);
}
bool is_relevant(search_item const& item) const {
switch (item.kind()) {
case search_item_k::assignment:
return m_used_vars.contains(item.var());
case search_item_k::boolean:
return m_used_constraints.contains(item.lit().index());
}
UNREACHABLE();
return false;
}
};
void conflict::log_var(pvar v) {
if (m_logger)
m_logger->m_used_vars.insert(v);
}
conflict::conflict(solver& s): s(s) {
ex_engines.push_back(alloc(ex_polynomial_superposition, s));
ex_engines.push_back(alloc(eq_explain, s));
ve_engines.push_back(alloc(ve_reduction));
inf_engines.push_back(alloc(inf_saturate, s));
// TODO: how to set this on the CLI? "polysat.log_conflicts=true" doesn't seem to work although z3 accepts it
if (true || s.get_config().m_log_conflicts)
m_logger = alloc(old_inference_logger);
}
conflict::~conflict() {}
void conflict::begin_conflict(char const* text) {
if (m_logger) {
m_logger->begin_conflict(text);
// log initial conflict state
m_logger->log_inference(*this, nullptr);
}
}
void conflict::log_inference(inference const& inf) {
if (m_logger)
m_logger->log_inference(*this, &inf);
}
void conflict::end_conflict() {
if (m_logger)
m_logger->end_conflict(s.m_search, s.m_viable);
}
constraint_manager& conflict::cm() const { return s.m_constraints; }
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;
}
bool conflict::empty() const {
return m_literals.empty()
&& m_vars.empty()
&& m_bail_vars.empty()
&& m_conflict_var == null_var;
}
void conflict::reset() {
for (auto c : *this)
unset_mark(c);
m_literals.reset();
m_vars.reset();
m_var_occurrences.reset();
m_bail_vars.reset();
m_conflict_var = null_var;
m_kind = conflict_kind_t::ok;
SASSERT(empty());
}
/**
* The constraint is false under the current assignment of variables.
* The core is then the conjuction of this constraint and assigned variables.
*/
void conflict::set(signed_constraint c) {
LOG("Conflict: " << c << " " << c.bvalue(s));
SASSERT(empty());
if (c.bvalue(s) == l_false) {
auto* cl = s.m_bvars.reason(c.blit().var());
if (cl)
set(*cl);
else
insert(c);
}
else {
SASSERT(c.is_currently_false(s));
// TBD: fails with test_subst SASSERT(c.bvalue(s) == l_true);
insert_vars(c);
insert(c);
}
SASSERT(!empty());
}
/**
* The variable v cannot be assigned.
* The conflict is the set of justifications accumulated for the viable values for v.
* These constraints are (in the current form) not added to the core, but passed directly
* to the forbidden interval module.
* A consistent approach could be to add these constraints to the core and then also include the
* variable assignments.
*/
void conflict::set(pvar v) {
LOG("Conflict: v" << v);
SASSERT(empty());
m_conflict_var = v;
SASSERT(!empty());
}
/**
* The clause is conflicting in the current search state.
*/
void conflict::set(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());
}
/**
* Insert constraint into conflict state
* Skip trivial constraints
* - e.g., constant ones such as "4 > 1"... only true ones
* should appear, otherwise the lemma would be a tautology
*/
void conflict::insert(signed_constraint c) {
if (c.is_always_true())
return;
if (is_marked(c))
return;
LOG("inserting: " << c);
SASSERT(!c->vars().empty());
set_mark(c);
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 conflict::propagate(signed_constraint c) {
switch (c.bvalue(s)) {
case l_undef:
s.assign_eval(c.blit());
break;
case l_true:
break;
case l_false:
break;
}
insert(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.
* Premises that are justified by value assignments are not assigned (the bvalue is l_undef)
* The justification for those premises are based on the free assigned variables.
*
* NOTE: maybe we should skip intermediate steps and just collect the leaf premises for c?
* Ensure that c is assigned and justified
*/
// TODO: rename this; it pushes onto \Gamma and doesn't insert into the core
void conflict::insert(signed_constraint c, vector<signed_constraint> const& premises) {
// keep(c);
clause_builder c_lemma(s);
for (auto premise : premises) {
LOG_H3("premise: " << premise);
// keep(premise);
SASSERT(premise.bvalue(s) != l_false);
c_lemma.push(~premise.blit());
}
c_lemma.push(c.blit());
clause_ref lemma = c_lemma.build();
SASSERT(lemma);
cm().store(lemma.get(), s, false);
if (c.bvalue(s) == l_undef)
s.assign_propagate(c.blit(), *lemma);
}
void conflict::remove(signed_constraint c) {
unset_mark(c);
m_literals.remove(c.blit().index());
for (pvar v : c->vars()) {
if (v < m_var_occurrences.size())
m_var_occurrences[v]--;
}
}
void conflict::replace(signed_constraint c_old, signed_constraint c_new, vector<signed_constraint> const& c_new_premises) {
remove(c_old);
insert(c_new, c_new_premises);
}
bool conflict::contains(signed_constraint c) const {
return m_literals.contains(c.blit().index());
}
bool conflict::contains(sat::literal lit) const {
SASSERT(lit != sat::null_literal);
return m_literals.contains(lit.index());
}
void conflict::set_bailout_gave_up() {
SASSERT(m_kind == conflict_kind_t::ok);
m_kind = conflict_kind_t::bailout_gave_up;
s.m_stats.m_num_bailouts++;
}
void conflict::set_bailout_lemma() {
SASSERT(m_kind == conflict_kind_t::ok);
m_kind = conflict_kind_t::bailout_lemma;
// s.m_stats.m_num_bailouts++;
}
struct inference_resolve : public inference {
sat::literal m_lit;
clause const& m_clause;
inference_resolve(sat::literal lit, clause const& cl) : m_lit(lit), m_clause(cl) {}
std::ostream& display(std::ostream& out) const override {
return out << "Resolve upon " << m_lit << " with " << m_clause;
}
};
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
SASSERT(contains(lit));
SASSERT(std::count(cl.begin(), cl.end(), lit) > 0);
SASSERT(!contains(~lit));
SASSERT(std::count(cl.begin(), cl.end(), ~lit) == 0);
remove(s.lit2cnstr(lit));
for (sat::literal lit2 : cl)
if (lit2 != lit)
insert(s.lit2cnstr(~lit2));
log_inference(inference_resolve(lit, cl));
}
struct inference_resolve_with_assignment : public inference {
solver& s;
sat::literal lit;
signed_constraint c;
inference_resolve_with_assignment(solver& s, sat::literal lit, signed_constraint c) : s(s), lit(lit), c(c) {}
std::ostream& display(std::ostream& out) const override {
out << "Resolve upon " << lit << " with assignment:";
for (pvar v : c->vars())
if (s.is_assigned(v))
out << " " << assignment_pp(s, v, s.get_value(v), true);
return out;
}
};
void conflict::resolve_with_assignment(sat::literal lit, unsigned lvl) {
// The reason for lit is conceptually:
// x1 = v1 /\ ... /\ xn = vn ==> lit
SASSERT(contains(lit));
SASSERT(!contains(~lit));
signed_constraint c = s.lit2cnstr(lit);
bool has_decision = false;
for (pvar v : c->vars())
if (s.is_assigned(v) && s.m_justification[v].is_decision())
m_bail_vars.insert(v), has_decision = true;
if (!has_decision) {
remove(c);
for (pvar v : c->vars())
if (s.is_assigned(v)) {
// TODO: 'lit' was propagated at level 'lvl'; can we here ignore variables above that?
SASSERT(s.get_level(v) <= lvl);
m_vars.insert(v);
}
}
log_inference(inference_resolve_with_assignment(s, lit, c));
}
clause_builder conflict::build_lemma() {
LOG_H3("Build lemma from core");
LOG("core: " << *this);
clause_builder lemma(s);
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();
if (m_logger)
m_logger->log_lemma(s, lemma);
return lemma;
}
void conflict::minimize_vars(signed_constraint c) {
if (m_vars.empty())
return;
if (!c.is_currently_false(s))
return;
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;
m_vars.reset();
for (auto const& [v, val] : a)
m_vars.insert(v);
log_inference("minimize vars");
LOG("reduced " << m_vars);
}
struct inference_resolve_value : public inference {
solver& s;
pvar v;
inference_resolve_value(solver& s, pvar v) : s(s), v(v) {}
std::ostream& display(std::ostream& out) const override {
return out << "Value resolution with " << assignment_pp(s, v, s.get_value(v), true);
}
};
bool conflict::resolve_value(pvar v) {
// NOTE:
// In the "standard" case where "v = val" is on the stack:
// forbidden interval projection is performed at top level
SASSERT(v != conflict_var());
bool has_saturated = false;
auto const& j = s.m_justification[v];
if (j.is_decision() && m_bail_vars.contains(v))
return false;
s.inc_activity(v);
m_vars.remove(v);
if (j.is_propagation()) {
for (auto const& c : s.m_viable.get_constraints(v))
propagate(c);
for (auto const& i : s.m_viable.units(v)) {
propagate(s.eq(i.lo(), i.lo_val()));
propagate(s.eq(i.hi(), i.hi_val()));
}
}
if (is_bailout())
goto bailout;
LOG("try-explain v" << v);
if (try_explain(v))
return true;
// No value resolution method was successful => fall back to saturation and variable elimination
while (s.inc()) {
LOG("try-eliminate v" << v);
// TODO: as a last resort, substitute v by m_value[v]?
if (try_eliminate(v))
return true;
LOG("try-saturate v" << v);
if (try_saturate(v))
has_saturated = true;
else
break;
}
LOG("bailout v" << v);
if (has_saturated) {
// NOTE: current saturation rules create valid lemmas that do not depend on the variable assignment
set_bailout_lemma();
return true;
}
else
set_bailout_gave_up();
bailout:
if (s.is_assigned(v) && j.is_decision())
m_vars.insert(v);
log_inference(inference_resolve_value(s, v));
return false;
}
bool conflict::try_eliminate(pvar v) {
LOG("try v" << v << " contains " << m_vars.contains(v));
if (m_vars.contains(v))
return false;
bool has_v = false;
for (auto c : *this)
has_v |= c->contains_var(v);
if (!has_v)
return true;
for (auto* engine : ve_engines)
if (engine->perform(s, v, *this))
return true;
return false;
}
bool conflict::try_saturate(pvar v) {
for (auto* engine : inf_engines)
if (engine->perform(v, *this))
return true;
return false;
}
bool conflict::try_explain(pvar v) {
for (auto* engine : ex_engines)
if (engine->try_explain(v, *this))
return true;
return false;
}
void conflict::set_mark(signed_constraint c) {
sat::bool_var b = c->bvar();
if (b >= m_bvar2mark.size())
m_bvar2mark.resize(b + 1);
SASSERT(!m_bvar2mark[b]);
m_bvar2mark[b] = true;
}
/**
* unset marking on the constraint, but keep variable dependencies.
*/
void conflict::unset_mark(signed_constraint c) {
sat::bool_var b = c->bvar();
SASSERT(m_bvar2mark[b]);
m_bvar2mark[b] = false;
}
bool conflict::is_marked(signed_constraint c) const {
return is_marked(c->bvar());
}
bool conflict::is_marked(sat::bool_var b) const {
return m_bvar2mark.get(b, false);
}
}

251
src/math/polysat/conflict_old.h Normal file
View file

@ -0,0 +1,251 @@
/*++
Copyright (c) 2021 Microsoft Corporation
Module Name:
polysat conflict
Author:
Nikolaj Bjorner (nbjorner) 2021-03-19
Jakob Rath 2021-04-6
Notes:
A conflict state is of the form <Vars, Constraints>
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 "math/polysat/inference_logger.h"
#include <optional>
namespace polysat {
class solver;
class explainer;
class inference_engine;
class variable_elimination_engine;
class conflict_iterator;
class old_inference_logger;
enum class conflict_kind_t {
ok,
bailout_gave_up,
bailout_lemma,
};
/** Conflict state, represented as core (~negation of clause). */
class conflict {
solver& s;
indexed_uint_set m_literals; // set of boolean literals in the conflict
unsigned_vector m_var_occurrences; // for each variable, the number of constraints in m_literals that contain it
uint_set m_vars; // variable assignments used as premises
uint_set m_bail_vars;
// If this is not null_var, the conflict was due to empty viable set for this variable.
// Can be treated like "v = x" for any value x.
pvar m_conflict_var = null_var;
/** Whether we are in a bailout state.
* We enter a bailout state when we give up on proper conflict resolution,
* or want to learn a lemma without fine-grained backtracking.
*/
conflict_kind_t m_kind = conflict_kind_t::ok;
friend class old_inference_logger;
scoped_ptr<old_inference_logger> m_logger;
bool_vector m_bvar2mark; // mark of Boolean variables
void set_mark(signed_constraint c);
void unset_mark(signed_constraint c);
void minimize_vars(signed_constraint c);
constraint_manager& cm() const;
scoped_ptr_vector<explainer> ex_engines;
scoped_ptr_vector<variable_elimination_engine> ve_engines;
scoped_ptr_vector<inference_engine> inf_engines;
public:
conflict(solver& s);
~conflict();
/// Begin next conflict
void begin_conflict(char const* text = nullptr);
/// Log inference at the current state.
void log_inference(inference const& inf);
void log_inference(char const* name) { log_inference(inference_named(name)); }
void log_var(pvar v);
/// Log relevant part of search state and viable.
void end_conflict();
pvar conflict_var() const { return m_conflict_var; }
bool is_bailout() const { return m_kind != conflict_kind_t::ok; }
bool is_bailout_lemma() const { return m_kind == conflict_kind_t::bailout_lemma; }
void set_bailout_gave_up();
void set_bailout_lemma();
bool empty() const;
void reset();
bool pvar_occurs_in_constraints(pvar v) const { return v < m_var_occurrences.size() && m_var_occurrences[v] > 0; }
bool contains_pvar(pvar v) const { return m_vars.contains(v) || m_bail_vars.contains(v); }
bool is_marked(signed_constraint c) const;
bool is_marked(sat::bool_var b) const;
/** conflict because the constraint c is false under current variable assignment */
void set(signed_constraint c);
/** conflict because there is no viable value for the variable v */
void set(pvar v);
/** all literals in clause are false */
void set(clause const& cl);
void propagate(signed_constraint c);
void insert(signed_constraint c);
void insert_vars(signed_constraint c);
void insert(signed_constraint c, vector<signed_constraint> const& premises);
void remove(signed_constraint c);
void replace(signed_constraint c_old, signed_constraint c_new, vector<signed_constraint> const& c_new_premises);
bool contains(signed_constraint c) const;
bool contains(sat::literal lit) const;
/** Perform boolean resolution with the clause upon variable 'var'.
* Precondition: core/clause contain complementary 'var'-literals.
*/
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'.
*/
bool resolve_value(pvar v);
/** Convert the core into a lemma to be learned. */
clause_builder build_lemma();
bool try_eliminate(pvar v);
bool try_saturate(pvar v);
bool try_explain(pvar v);
using const_iterator = conflict_iterator;
const_iterator begin() const;
const_iterator end() const;
uint_set const& vars() const { return m_vars; }
uint_set const& bail_vars() const { return m_bail_vars; }
std::ostream& display(std::ostream& out) const;
};
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); }
};
inline conflict::const_iterator conflict::begin() const { return conflict_iterator::begin(cm(), m_literals); }
inline conflict::const_iterator conflict::end() const { return conflict_iterator::end(cm(), m_literals); }
}