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

Polysat: conflict resolution updates (#5534)

Browse source 
* variable elimination / saturation sketch

* conflict resolution updates
This commit is contained in:
Jakob Rath 2021-09-03 19:17:06 +02:00 • committed by GitHub
parent dc547510db
commit 9f387f5738
No known key found for this signature in database
GPG key ID: 4AEE18F83AFDEB23
14 changed files with 343 additions and 294 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -11,6 +11,7 @@ z3_add_component(polysat
justification.cpp
linear_solver.cpp
log.cpp
saturation.cpp
search_state.cpp
solver.cpp
ule_constraint.cpp

96
src/math/polysat/conflict_core.cpp
View file

@ -16,10 +16,25 @@ Author:
#include "math/polysat/solver.h"
#include "math/polysat/log.h"
#include "math/polysat/log_helper.h"
#include "math/polysat/saturation.h"
#include "math/polysat/variable_elimination.h"
#include <algorithm>
namespace polysat {
conflict_core::conflict_core(solver& s) {
m_solver = &s;
ve_engines.push_back(alloc(ve_reduction));
// ve_engines.push_back(alloc(ve_forbidden_intervals));
inf_engines.push_back(alloc(inf_polynomial_superposition));
for (auto* engine : inf_engines)
engine->set_solver(s);
}
conflict_core::~conflict_core() {}
constraint_manager& conflict_core::cm() { return m_solver->m_constraints; }
std::ostream& conflict_core::display(std::ostream& out) const {
bool first = true;
for (auto c : m_constraints) {
@ -43,8 +58,8 @@ namespace polysat {
void conflict_core::set(signed_constraint c) {
LOG("Conflict: " << c);
SASSERT(empty());
m_constraints.push_back(std::move(c));
m_needs_model = true;
insert(c);
}
void conflict_core::set(pvar v) {
@ -54,7 +69,7 @@ namespace polysat {
m_needs_model = true;
}
void conflict_core::push(signed_constraint c) {
void conflict_core::insert(signed_constraint c) {
SASSERT(!empty()); // should use set() to enter 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)
@ -64,11 +79,17 @@ namespace polysat {
m_constraints.push_back(c);
}
void conflict_core::insert(signed_constraint c, vector<signed_constraint> premises) {
insert(c);
m_saturation_premises.insert(c, std::move(premises)); // TODO: map doesn't have move-insertion, so this still copies the vector. Maybe we want a clause_ref (but this doesn't work either since c doesn't have a boolean variable yet).
}
void conflict_core::resolve(constraint_manager const& m, sat::bool_var var, 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(!is_bailout());
SASSERT(var != sat::null_bool_var);
DEBUG_CODE({
bool core_has_pos = std::count_if(begin(), end(), [var](auto c){ return c.blit() == sat::literal(var); }) > 0;
@ -80,6 +101,9 @@ namespace polysat {
SASSERT((core_has_pos && clause_has_pos) || (core_has_neg && clause_has_neg));
});
// TODO: maybe implement by marking literals instead (like SAT solvers are doing); if we need to iterate, keep an indexed_uint_set (from util/uint_set.h)
// (i.e., instead of keeping an explicit list of constraints as core, we just mark them.)
// (we still need the list though, for new/temporary constraints.)
int j = 0;
for (auto c : m_constraints)
if (c->bvar() == var)
@ -91,27 +115,83 @@ namespace polysat {
m_constraints.push_back(m.lookup(~lit));
}
clause_ref conflict_core::build_lemma(solver& s, unsigned trail_idx) {
clause_ref conflict_core::build_lemma() {
sat::literal_vector literals;
p_dependency_ref dep = s.mk_dep_ref(null_dependency);
p_dependency_ref dep = m_solver->mk_dep_ref(null_dependency);
unsigned lvl = 0;
// TODO: another core reduction step?
// TODO: try a final core reduction step?
for (auto c : m_constraints) {
if (!c->has_bvar()) {
// temporary constraint -> keep it
cm().ensure_bvar(c.get());
// Insert the temporary constraint from saturation into \Gamma.
auto it = m_saturation_premises.find_iterator(c);
if (it != m_saturation_premises.end()) {
auto& premises = it->m_value;
clause_builder c_lemma(*m_solver);
for (auto premise : premises)
c_lemma.push_literal(~premise.blit());
c_lemma.push_literal(c.blit());
clause* cl = cm().store(c_lemma.build());
if (cl->size() == 1)
c->set_unit_clause(cl);
// TODO: actually, this should be backtrackable (unless clause is unit). But currently we cannot insert in the middle of the stack!
// (or do it like MCSAT... they keep "theory-propagated" literals also at the end and restore them on backtracking)
m_solver->assign_bool_core(c.blit(), cl, nullptr);
m_solver->activate_constraint(c);
}
}
if (c->unit_clause()) {
dep = s.m_dm.mk_join(dep, c->unit_dep());
dep = m_solver->m_dm.mk_join(dep, c->unit_dep());
continue;
}
lvl = std::max(lvl, c->level());
s.m_constraints.ensure_bvar(c.get());
literals.push_back(~c.blit());
}
if (m_needs_model) {
// TODO: add equalities corresponding to model up to trail_idx
// TODO: add equalities corresponding to current model.
// until we properly track variables (use marks from solver?), we just use all of them (reverted decision and the following ones should have been popped from the stack)
uint_set vars;
for (auto c : m_constraints)
for (pvar v : c->vars())
vars.insert(v);
// Add v != val for each variable
for (pvar v : vars) {
auto diseq = ~cm().eq(lvl, m_solver->var(v) - m_solver->m_value[v]);
cm().ensure_bvar(diseq.get());
literals.push_back(diseq.blit());
}
}
return clause::from_literals(lvl, std::move(dep), std::move(literals));
}
bool conflict_core::try_eliminate(pvar v) {
// TODO: could be tracked incrementally when constraints are added/removed
vector<signed_constraint> v_constraints;
for (auto c : *this)
if (c->contains_var(v)) {
v_constraints.push_back(c);
break;
}
// Variable already eliminated trivially (does this ever happen?)
if (v_constraints.empty())
return true;
for (auto* engine : ve_engines)
if (engine->perform(*m_solver, v, *this))
return true;
return false;
}
bool conflict_core::try_saturate(pvar v) {
for (auto* engine : inf_engines)
if (engine->perform(v, *this))
return true;
return false;
}
}

23
src/math/polysat/conflict_core.h
View file

@ -17,6 +17,8 @@ Author:
namespace polysat {
class solver;
class inference_engine;
class variable_elimination_engine;
/** Conflict state, represented as core (~negation of clause). */
class conflict_core {
@ -24,6 +26,7 @@ namespace polysat {
// 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.
// TODO: we could always set this to the variable we're currently focusing on.
pvar m_conflict_var = null_var;
/** True iff the conflict depends on the current variable assignment. (If so, additional constraints must be added to the final learned clause.) */
@ -32,7 +35,17 @@ namespace polysat {
// The drawback is that we may get weaker lemmas in some cases (but they are still correct).
// For example: if we have 4x+y=2 and y=0, then we have a conflict no matter the value of x, so we should drop x=? from the core.
solver* m_solver = nullptr;
constraint_manager& cm();
scoped_ptr_vector<variable_elimination_engine> ve_engines;
scoped_ptr_vector<inference_engine> inf_engines;
// ptr_addr_map<constraint, vector<signed_constraint>> m_saturation_premises;
map<signed_constraint, vector<signed_constraint>, obj_hash<signed_constraint>, default_eq<signed_constraint>> m_saturation_premises;
public:
conflict_core(solver& s);
~conflict_core();
vector<signed_constraint> const& constraints() const { return m_constraints; }
bool needs_model() const { return m_needs_model; }
pvar conflict_var() const { return m_conflict_var; }
@ -47,6 +60,7 @@ namespace polysat {
m_constraints.reset();
m_needs_model = false;
m_conflict_var = null_var;
m_saturation_premises.reset();
SASSERT(empty());
}
@ -57,7 +71,9 @@ namespace polysat {
/** conflict because there is no viable value for the variable v */
void set(pvar v);
void push(signed_constraint c);
void insert(signed_constraint c);
void insert(signed_constraint c, vector<signed_constraint> premises);
void remove(signed_constraint c);
/** Perform boolean resolution with the clause upon variable 'var'.
* Precondition: core/clause contain complementary 'var'-literals.
@ -65,7 +81,10 @@ namespace polysat {
void resolve(constraint_manager const& m, sat::bool_var var, clause const& cl);
/** Convert the core into a lemma to be learned. */
clause_ref build_lemma(solver& s, unsigned trail_idx);
clause_ref build_lemma();
bool try_eliminate(pvar v);
bool try_saturate(pvar v);
using const_iterator = decltype(m_constraints)::const_iterator;
const_iterator begin() { return constraints().begin(); }

5
src/math/polysat/constraint.cpp
View file

@ -269,4 +269,9 @@ namespace polysat {
narrow(s, is_positive);
}
void constraint::set_unit_clause(clause *cl) {
// can be seen as a cache... store the lowest-level unit clause for this constraint.
if (!cl || !m_unit_clause || m_unit_clause->level() > cl->level())
m_unit_clause = cl;
}
}

13
src/math/polysat/constraint.h
View file

@ -26,7 +26,9 @@ namespace polysat {
class ule_constraint;
class signed_constraint;
using constraint_table = ptr_hashtable<constraint, obj_ptr_hash<constraint>, deref_eq<constraint>>;
using constraint_hash = obj_ptr_hash<constraint>;
using constraint_eq = deref_eq<constraint>;
using constraint_table = ptr_hashtable<constraint, constraint_hash, constraint_eq>;
// Manage constraint lifetime, deduplication, and connection to boolean variables/literals.
class constraint_manager {
@ -134,6 +136,7 @@ namespace polysat {
virtual unsigned hash() const = 0;
virtual bool operator==(constraint const& other) const = 0;
bool operator!=(constraint const& other) const { return !operator==(other); }
bool is_eq() const { return m_kind == ckind_t::eq_t; }
bool is_ule() const { return m_kind == ckind_t::ule_t; }
@ -155,12 +158,13 @@ namespace polysat {
unsigned_vector& vars() { return m_vars; }
unsigned_vector const& vars() const { return m_vars; }
unsigned var(unsigned idx) const { return m_vars[idx]; }
bool contains_var(pvar v) const { return m_vars.contains(v); }
unsigned level() const { return m_level; }
bool has_bvar() const { return m_bvar != sat::null_bool_var; }
sat::bool_var bvar() const { return m_bvar; }
clause* unit_clause() const { return m_unit_clause; }
void set_unit_clause(clause* cl) { SASSERT(cl); SASSERT(!m_unit_clause || m_unit_clause == cl); m_unit_clause = cl; }
void set_unit_clause(clause* cl);
p_dependency* unit_dep() const { return m_unit_clause ? m_unit_clause->dep() : nullptr; }
/** Precondition: all variables other than v are assigned.
@ -175,6 +179,7 @@ namespace polysat {
inline std::ostream& operator<<(std::ostream& out, constraint const& c) { return c.display(out); }
class signed_constraint final {
public:
using ptr_t = constraint*;
@ -219,9 +224,13 @@ namespace polysat {
signed_constraint& operator=(std::nullptr_t) { m_constraint = nullptr; return *this; }
unsigned hash() const {
return combine_hash(get_ptr_hash(get()), bool_hash()(is_positive()));
}
bool operator==(signed_constraint const& other) const {
return get() == other.get() && is_positive() == other.is_positive();
}
bool operator!=(signed_constraint const& other) const { return !operator==(other); }
std::ostream& display(std::ostream& out) const {
if (m_constraint)

168
src/math/polysat/explain.cpp
View file

@ -17,32 +17,6 @@ Author:
namespace polysat {
bool inf_polynomial_superposition:: perform(conflict_explainer& ce) {
// TODO
return false;
}
#if 0
conflict_explainer::conflict_explainer(solver& s): m_solver(s) {
inference_engines.push_back(alloc(inf_polynomial_superposition));
}
bool conflict_explainer::saturate() {
for (auto* engine : inference_engines)
if (engine->perform(*this))
return true;
return false;
}
#endif
// clause_ref conflict_explainer::resolve(pvar v, ptr_vector<constraint> const& cjust) {
// LOG_H3("Attempting to explain conflict for v" << v);
// m_var = v;
// m_cjust_v = cjust;
@ -128,148 +102,6 @@ namespace polysat {
// return lemma;
// }
// /**
// * Polynomial superposition.
// * So far between two equalities.
// * TODO: Also handle =, != superposition here?
// * TODO: handle case when m_conflict.units().size() > 2
// * TODO: handle super-position into a clause?
// */
// clause_ref conflict_explainer::by_polynomial_superposition() {
// LOG_H3("units-size: " << m_conflict.units().size() << " conflict-clauses " << m_conflict.clauses().size());
// #if 0
// constraint* c1 = nullptr, *c2 = nullptr;
// if (m_conflict.units().size() == 2 && m_conflict.clauses().size() == 0) {
// c1 = m_conflict.units()[0];
// c2 = m_conflict.units()[1];
// }
// else {
// // other combinations?
// #if 1
// // A clause can also be a unit.
// // Even if a clause is not a unit, we could still resolve a propagation
// // into some literal in the current conflict clause.
// // Selecting resolvents should not be specific to superposition.
// for (auto clause : m_conflict.clauses()) {
// LOG("clause " << *clause << " size " << clause->size());
// if (clause->size() == 1) {
// sat::literal lit = (*clause)[0];
// // if (lit.sign())
// // continue;
// constraint* c = m_solver.m_constraints.lookup(lit.var());
// // Morally, a derived unit clause is always asserted at the base level.
// // (Even if we don't want to keep this one around. But maybe we should? Do we want to reconstruct proofs?)
// c->set_unit_clause(clause);
// c->assign(!lit.sign());
// // this clause is really a unit.
// LOG("unit clause: " << *c);
// if (c->is_eq()) { // && c->is_positive()) {
// c1 = c;
// break;
// }
// }
// }
// if (!c1)
// return nullptr;
// for (constraint* c : m_conflict.units()) {
// if (c->is_eq() && c->is_positive()) {
// c2 = c;
// break;
// }
// }
// #endif
// }
// if (!c1 || !c2 || c1 == c2)
// return nullptr;
// LOG("c1: " << show_deref(c1));
// LOG("c2: " << show_deref(c2));
// if (c1->is_eq() && c2->is_eq() && c1->is_positive() && c2->is_positive()) {
// pdd a = c1->to_eq().p();
// pdd b = c2->to_eq().p();
// pdd r = a;
// if (!a.resolve(m_var, b, r) && !b.resolve(m_var, a, r))
// return nullptr;
// unsigned const lvl = std::max(c1->level(), c2->level());
// clause_builder clause(m_solver);
// clause.push_literal(~c1->blit());
// clause.push_literal(~c2->blit());
// clause.push_new_constraint(m_solver.m_constraints.eq(lvl, r));
// return clause.build();
// }
// if (c1->is_eq() && c2->is_eq() && c1->is_negative() && c2->is_positive()) {
// pdd a = c1->to_eq().p();
// pdd b = c2->to_eq().p();
// pdd r = a;
// // TODO: only holds if the factor for 'a' is non-zero
// if (!a.resolve(m_var, b, r))
// return nullptr;
// unsigned const lvl = std::max(c1->level(), c2->level());
// clause_builder clause(m_solver);
// clause.push_literal(~c1->blit());
// clause.push_literal(~c2->blit());
// clause.push_new_constraint(~m_solver.m_constraints.eq(lvl, r));
// SASSERT(false); // TODO "breakpoint" for debugging
// return clause.build();
// }
// #else
// for (constraint* c1 : m_conflict_units) {
// if (!c1->is_eq())
// continue;
// for (constraint* c2 : m_conflict_units) { // TODO: can start iteration at index(c1)+1
// if (c1 == c2)
// continue;
// if (!c2->is_eq())
// continue;
// if (c1->is_negative() && c2->is_negative())
// continue;
// LOG("c1: " << show_deref(c1));
// LOG("c2: " << show_deref(c2));
// if (c1->is_positive() && c2->is_negative()) {
// std::swap(c1, c2);
// }
// pdd a = c1->to_eq().p();
// pdd b = c2->to_eq().p();
// pdd r = a;
// unsigned const lvl = std::max(c1->level(), c2->level());
// if (c1->is_positive() && c2->is_positive()) {
// if (!a.resolve(m_var, b, r) && !b.resolve(m_var, a, r))
// continue;
// clause_builder clause(m_solver);
// clause.push_literal(~c1->blit());
// clause.push_literal(~c2->blit());
// clause.push_new_constraint(m_solver.m_constraints.eq(lvl, r));
// auto cl = clause.build();
// LOG("r: " << show_deref(cl->new_constraints()[0]));
// LOG("result: " << show_deref(cl));
// // SASSERT(false); // NOTE: this is a simple "breakpoint" for debugging
// return cl;
// }
// if (c1->is_negative() && c2->is_positive()) {
// // TODO: only holds if the factor for 'a' is non-zero
// if (!a.resolve(m_var, b, r))
// continue;
// clause_builder clause(m_solver);
// clause.push_literal(~c1->blit());
// clause.push_literal(~c2->blit());
// clause.push_new_constraint(~m_solver.m_constraints.eq(lvl, r));
// auto cl = clause.build();
// LOG("r: " << show_deref(cl->new_constraints()[0]));
// LOG("result: " << show_deref(cl));
// // SASSERT(false); // NOTE: this is a simple "breakpoint" for debugging
// return cl;
// }
// }
// }
// #endif
// return nullptr;
// }
// /// [x] zx > yx ==> Ω*(x,y) \/ z > y
// /// [x] yx <= zx ==> Ω*(x,y) \/ y <= z
// clause_ref conflict_explainer::by_ugt_x() {

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

@ -19,40 +19,6 @@ Author:
namespace polysat {
class solver;
class conflict_explainer;
class inference_engine {
public:
virtual ~inference_engine() {}
/** Try to apply an inference rule. Returns true if a new constraint was added to the core. */
virtual bool perform(conflict_explainer& ce) = 0;
};
class inf_polynomial_superposition final : public inference_engine {
public:
bool perform(conflict_explainer& ce) override;
};
// TODO: other rules
// clause_ref by_ugt_x();
// clause_ref by_ugt_y();
// clause_ref by_ugt_z();
// clause_ref y_ule_ax_and_x_ule_z();
class core_saturation final {
scoped_ptr_vector<inference_engine> inference_engines;
public:
/// Derive new constraints from constraints containing the variable v (i.e., at least one premise must contain v)
bool saturate(pvar v, conflict_core& core) { NOT_IMPLEMENTED_YET(); return false; }
};
#if 0
class conflict_explainer {

1
src/math/polysat/linear_solver.h
View file

@ -127,6 +127,7 @@ namespace polysat {
void set_value(pvar v, rational const& value, unsigned dep);
void set_bound(pvar v, rational const& lo, rational const& hi, unsigned dep);
void activate_constraint(bool is_positive, constraint& c);
void activate_constraint(signed_constraint c) { activate_constraint(c.is_positive(), *c.get()); }
// check integer modular feasibility under current bounds.
lbool check();

71
src/math/polysat/saturation.cpp Normal file
View file

@ -0,0 +1,71 @@
/*++
Copyright (c) 2021 Microsoft Corporation
Module Name:
Polysat core saturation
Author:
Nikolaj Bjorner (nbjorner) 2021-03-19
Jakob Rath 2021-04-6
--*/
#include "math/polysat/saturation.h"
#include "math/polysat/solver.h"
#include "math/polysat/log.h"
namespace polysat {
constraint_manager& inference_engine::cm() { return s().m_constraints; }
/** Polynomial superposition between two equalities that contain v.
*/
bool inf_polynomial_superposition::perform(pvar v, conflict_core& core) {
// TODO: check superposition into disequality again (see notes)
// TODO: use indexing/marking for this instead of allocating a temporary vector
// TODO: core saturation premises are from \Gamma (i.e., has_bvar)... but here we further restrict to the core; might need to revise
// -- especially: should take into account results from previous saturations (they will be in \Gamma, but only if we use the constraint or one of its descendants for the lemma)
// actually: we want to take one from the current cjust (currently true) and one from the conflict (currently false)
vector<signed_constraint> candidates;
for (auto c : core)
if (c->has_bvar() && c.is_positive() && c->is_eq() && c->contains_var(v))
candidates.push_back(c);
for (auto it1 = candidates.begin(); it1 != candidates.end(); ++it1) {
for (auto it2 = it1 + 1; it2 != candidates.end(); ++it2) {
signed_constraint c1 = *it1;
signed_constraint c2 = *it2;
SASSERT(c1 != c2);
LOG("c1: " << c1);
LOG("c2: " << c2);
pdd a = c1->to_eq().p();
pdd b = c2->to_eq().p();
pdd r = a;
if (!a.resolve(v, b, r) && !b.resolve(v, a, r))
continue;
unsigned const lvl = std::max(c1->level(), c2->level());
signed_constraint c = cm().eq(lvl, r);
if (!c.is_currently_false(s()))
continue;
// TODO: we need to track the premises somewhere. also that we need to patch \Gamma if the constraint is used in the lemma.
// TODO: post-check to make sure r is false under current assignment. otherwise the rule makes no sense.
vector<signed_constraint> premises;
premises.push_back(c1);
premises.push_back(c2);
core.insert(c, std::move(premises));
// clause_builder clause(m_solver);
// clause.push_literal(~c1->blit());
// clause.push_literal(~c2->blit());
// clause.push_new_constraint(m_solver.m_constraints.eq(lvl, r));
// return clause.build();
}
}
return false;
}
}

58
src/math/polysat/saturation.h Normal file
View file

@ -0,0 +1,58 @@
/*++
Copyright (c) 2021 Microsoft Corporation
Module Name:
Polysat core saturation
Author:
Nikolaj Bjorner (nbjorner) 2021-03-19
Jakob Rath 2021-04-6
--*/
#pragma once
#include "math/polysat/conflict_core.h"
namespace polysat {
class solver;
class constraint_manager;
class inference_engine {
friend class conflict_core;
solver* m_solver = nullptr;
void set_solver(solver& s) { m_solver = &s; }
protected:
solver& s() { return *m_solver; }
constraint_manager& cm();
public:
virtual ~inference_engine() {}
/** Try to apply an inference rule.
* Derive new constraints from constraints containing the variable v (i.e., at least one premise must contain v).
* Returns true if a new constraint was added to the core.
*/
virtual bool perform(pvar v, conflict_core& core) = 0;
};
class inf_polynomial_superposition : public inference_engine {
public:
bool perform(pvar v, conflict_core& core) override;
};
// TODO: other rules
// clause_ref by_ugt_x();
// clause_ref by_ugt_y();
// clause_ref by_ugt_z();
// clause_ref y_ule_ax_and_x_ule_z();
/*
* TODO: we could resolve constraints in cjust[v] against each other to
* obtain stronger propagation. Example:
* (x + 1)*P = 0 and (x + 1)*Q = 0, where gcd(P,Q) = 1, then we have x + 1 = 0.
* We refer to this process as narrowing.
* In general form it can rely on factoring.
* Root finding can further prune viable.
*/
}

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

@ -39,6 +39,7 @@ namespace polysat {
m_viable(*this),
m_dm(m_value_manager, m_alloc),
m_linear_solver(*this),
m_conflict(*this),
m_free_vars(m_activity),
m_bvars(),
m_constraints(m_bvars) {
@ -449,14 +450,19 @@ namespace polysat {
return;
}
if (m_conflict.conflict_var() != null_var) {
// This case corresponds to a propagation of conflict_var, except it's not explicitly on the stack.
resolve_value(m_conflict.conflict_var());
}
reset_marks();
set_marks(m_conflict);
if (m_conflict.conflict_var() != null_var) {
// This case corresponds to a propagation of conflict_var, except it's not explicitly on the stack.
if (!resolve_value(m_conflict.conflict_var())) {
resolve_bailout(m_search.size() - 1);
return;
}
reset_marks();
set_marks(m_conflict);
}
for (unsigned i = m_search.size(); i-- > 0; ) {
LOG("Conflict: " << m_conflict);
auto const& item = m_search[i];
@ -507,15 +513,17 @@ namespace polysat {
/** Conflict resolution case where propagation 'v := ...' is on top of the stack */
bool solver::resolve_value(pvar v) {
SASSERT(m_justification[v].is_propagation());
// SASSERT(m_justification[v].is_propagation()); // doesn't hold if we enter because of conflict_var
// Conceptually:
// - Value Resolution
// - Variable Elimination
// - if VE isn't possible, try to derive new constraints using core saturation
// m_conflict.set_var(v);
// Value Resolution
for (auto c : m_cjust[v])
m_conflict.push(c);
m_conflict.insert(c);
// Variable elimination
while (true) {
@ -524,12 +532,12 @@ namespace polysat {
// 2. If not possible, try saturation and core reduction (actually reduction could be one specific VE method?).
// 3. as a last resort, substitute v by m_value[v]?
variable_elimination ve;
if (ve.perform(v, m_conflict))
// TODO: maybe we shouldn't try to split up VE/Saturation in the implementation.
// it might be better to just have more general "core inferences" that may combine elimination/saturation steps that fit together...
// or even keep the whole "value resolution + VE/Saturation" as a single step. we might want to know which constraints come from the current cjusts?
if (m_conflict.try_eliminate(v))
return true;
core_saturation cs;
if (!cs.saturate(v, m_conflict))
if (!m_conflict.try_saturate(v))
return false;
}
@ -548,6 +556,8 @@ namespace polysat {
void solver::resolve_bailout(unsigned i) {
// TODO: conflict resolution failed or was aborted. what to do with the current conflict core?
// (we could still use it as lemma, but it probably doesn't help much)
// or use a fallback lemma which just contains v/=val for each decision variable v up to i
// (goal is to have strong enough explanation to avoid this function as much as possible)
NOT_IMPLEMENTED_YET();
/*
do {
@ -623,16 +633,16 @@ namespace polysat {
}
void solver::learn_lemma(pvar v, clause_ref lemma) {
LOG("Learning: " << show_deref(lemma));
if (!lemma)
return;
LOG("Learning: " << show_deref(lemma));
SASSERT(lemma->size() > 0);
SASSERT(m_conflict_level <= m_justification[v].level());
SASSERT(m_conflict_level <= m_justification[v].level()); // ???
clause* cl = lemma.get();
add_lemma(std::move(lemma));
if (cl->size() == 1) {
sat::literal lit = (*cl)[0];
signed_constraint c = m_constraints.lookup(lit);
sat::literal lit = (*cl)[0];
signed_constraint c = m_constraints.lookup(lit);
c->set_unit_clause(cl);
push_cjust(v, c);
activate_constraint_base(c);
@ -641,7 +651,7 @@ namespace polysat {
sat::literal lit = decide_bool(*cl);
SASSERT(lit != sat::null_literal);
signed_constraint c = m_constraints.lookup(lit);
push_cjust(v, c);
push_cjust(v, c); // TODO: Ok, this works for the first guess. but what if we update the guess later?? the next guess should then be part of cjust[v] instead.
}
}
@ -663,7 +673,7 @@ namespace polysat {
};
sat::literal choice = sat::null_literal;
unsigned num_choices = 0; // TODO: should probably cache this?
unsigned num_choices = 0; // TODO: should probably cache this? (or rather the suitability of each literal... it won't change until we backtrack beyond the current point)
for (sat::literal lit : lemma) {
if (is_suitable(lit)) {
@ -689,58 +699,37 @@ namespace polysat {
/**
* Revert a decision that caused a conflict.
* Variable v was assigned by a decision at position i in the search stack.
*
* TODO: we could resolve constraints in cjust[v] against each other to
* obtain stronger propagation. Example:
* (x + 1)*P = 0 and (x + 1)*Q = 0, where gcd(P,Q) = 1, then we have x + 1 = 0.
* We refer to this process as narrowing.
* In general form it can rely on factoring.
* Root finding can further prune viable.
*/
void solver::revert_decision(pvar v) {
rational val = m_value[v];
LOG_H3("Reverting decision: pvar " << v << " := " << val);
NOT_IMPLEMENTED_YET();
/*
SASSERT(m_justification[v].is_decision());
backjump(m_justification[v].level()-1);
m_viable.add_non_viable(v, val);
auto confl = std::move(m_conflict);
clause_ref lemma = m_conflict.build_lemma();
m_conflict.reset();
for (constraint* c : confl.units()) {
// Add the conflict as justification for the exclusion of 'val'
push_cjust(v, c);
// NOTE: in general, narrow may change the conflict.
// But since we just backjumped, narrowing should not result in an additional conflict.
// TODO: this call to "narrow" may still lead to a conflict,
// because we do not detect all conflicts immediately.
// Consider:
// - Assert constraint zx > yx, watching y and z.
// - Guess x = 0.
// - We have a conflict but we don't know. It will be discovered when y and z are assigned,
// and then may lead to an assertion failure through this call to narrow.
// TODO: what to do with "unassigned" constraints at this point? (we probably should have resolved those away, even in the 'backtrack' case.)
// NOTE: they are constraints from clauses that were added to cjust… how to deal with that? should we add the whole clause to cjust?
SASSERT(!c->is_undef());
// if (!c->is_undef()) // TODO: this check to be removed once this is fixed properly.
c->narrow(*this);
if (is_conflict()) {
LOG_H1("Conflict during revert_decision/narrow!");
return;
}
}
// m_conflict.reset();
// TODO: we need to decide_bool on the clause (learn_lemma takes care of this).
// if the lemma was asserting, then this will propagate the last literal. otherwise we do the enumerative guessing as normal.
// we need to exclude the current value of v. narrowing of the guessed constraint *should* take care of it but we cannot count on that.
// the narrow/decide we are doing now will be done implicitly by the solver loop.
learn_lemma(v, std::move(reason));
// TODO: what do we add as 'cjust' for this restriction? the guessed
// constraint from the lemma should be the right choice. but, how to
// carry this over when the guess is reverted? need to remember the
// variable 'v' somewhere on the lemma.
// the restriction v /= val can live before the guess... (probably should ensure that the guess stays close to the current position in the stack to prevent confusion...)
m_viable.add_non_viable(v, val);
learn_lemma(v, std::move(lemma));
// TODO: check if still necessary... won't the next solver iteration do this anyway? (well, it might choose a different variable... so this "unrolls" the next loop iteration to get a stable variable order)
/*
if (is_conflict()) {
LOG_H1("Conflict during revert_decision/learn_lemma!");
return;
}
narrow(v);
if (m_justification[v].is_unassigned()) {
m_free_vars.del_var_eh(v);
@ -754,9 +743,17 @@ namespace polysat {
LOG_H3("Reverting boolean decision: " << lit);
SASSERT(m_bvars.is_decision(var));
// TODO:
// Current situation: we have a decision for boolean literal L on top of the stack, and a conflict core.
//
// In a CDCL solver, this means ~L is in the lemma (actually, as the asserting literal). We drop the decision and replace it by the propagation (~L)^lemma.
//
// - we know L must be false
// - if L isn't in the core, we can still add it (weakening the lemma) to obtain "core => ~L"
// - then we can add the propagation (~L)^lemma and continue with the next guess
NOT_IMPLEMENTED_YET();
/*
if (reason) {
LOG("Reason: " << show_deref(reason));
bool contains_var = std::any_of(reason->begin(), reason->end(), [var](sat::literal reason_lit) { return reason_lit.var() == var; });
@ -888,7 +885,7 @@ namespace polysat {
add_watch(c);
c.narrow(*this);
#if ENABLE_LINEAR_SOLVER
m_linear_solver.activate_constraint(c.is_positive(), c.get()); // TODO: linear solver should probably take a signed_constraint
m_linear_solver.activate_constraint(c);
#endif
}
@ -896,6 +893,7 @@ namespace polysat {
void solver::deactivate_constraint(signed_constraint c) {
LOG("Deactivating constraint: " << c);
erase_watch(c);
c->set_unit_clause(nullptr);
}
void solver::backjump(unsigned new_level) {

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

@ -55,6 +55,7 @@ namespace polysat {
friend class clause_builder;
friend class conflict_core;
friend class conflict_explainer;
friend class inference_engine;
friend class forbidden_intervals;
friend class linear_solver;
friend class viable;

24
src/math/polysat/variable_elimination.cpp
View file

@ -12,8 +12,32 @@ Author:
--*/
#include "math/polysat/variable_elimination.h"
#include "math/polysat/solver.h"
#include <algorithm>
namespace polysat {
bool ve_reduction::perform(solver& s, pvar v, conflict_core& core) {
// without any further hints, we just do core reduction with the stronger premise "C contains a c' that evaluates to false",
// and kick out all other constraints.
auto pred = [&s, v](signed_constraint c) -> bool {
return !c->contains_var(v) && c.is_currently_false(s);
};
auto it = std::find_if(core.begin(), core.end(), pred);
if (it != core.end()) {
signed_constraint c = *it;
core.reset();
core.set(c);
// core.insert(c);
// core.set_needs_model(true);
return true;
}
return false;
}
bool ve_forbidden_intervals::perform(solver& s, pvar v, conflict_core& core) {
NOT_IMPLEMENTED_YET();
return false;
}
}

30
src/math/polysat/variable_elimination.h
View file

@ -16,37 +16,21 @@ Author:
namespace polysat {
class solver;
class variable_elimination_engine {
public:
virtual ~variable_elimination_engine() {}
virtual bool perform(pvar v, conflict_core& core) = 0;
virtual bool perform(solver& s, pvar v, conflict_core& core) = 0;
};
// discovers when a variable has already been removed... (special case of ve_reduction?)
class ve_trivial final : public variable_elimination_engine {
class ve_reduction : public variable_elimination_engine {
public:
bool perform(pvar v, conflict_core& core) override { NOT_IMPLEMENTED_YET(); return false; }
bool perform(solver& s, pvar v, conflict_core& core) override;
};
// ve by core reduction: try core reduction on all constraints that contain the variable to be eliminated.
// if we cannot eliminate all such constraints, then should we keep all of them instead of eliminating only some? since they might still be useful for saturation.
class ve_reduction final : public variable_elimination_engine {
class ve_forbidden_intervals : public variable_elimination_engine {
public:
bool perform(pvar v, conflict_core& core) override { NOT_IMPLEMENTED_YET(); return false; }
};
class ve_forbidden_intervals final : public variable_elimination_engine {
public:
bool perform(pvar v, conflict_core& core) override { NOT_IMPLEMENTED_YET(); return false; }
};
class variable_elimination final {
scoped_ptr_vector<variable_elimination_engine> ve_engines;
public:
variable_elimination() {}
/// Try to eliminate the variable v from the given core
bool perform(pvar v, conflict_core& core) { NOT_IMPLEMENTED_YET(); return false; }
bool perform(solver& s, pvar v, conflict_core& core) override;
};
}