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

Simplify handling of side lemmas in conflict

Browse source
This commit is contained in:
Jakob Rath 2022-10-07 16:19:41 +02:00
parent 8b4a36e3bd
commit 8333664433
6 changed files with 90 additions and 58 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -321,6 +321,21 @@ namespace polysat {
m_vars.insert(v);
}
void conflict::add_lemma(signed_constraint const* cs, unsigned cs_len) {
clause_builder cb(s);
for (unsigned i = 0; i < cs_len; ++i)
cb.push(cs[i]);
clause_ref lemma = cb.build();
SASSERT(lemma);
lemma->set_redundant(true);
m_lemmas.push_back(std::move(lemma));
}
void conflict::add_lemma(std::initializer_list<signed_constraint> cs) {
add_lemma(std::data(cs), cs.size());
}
#if 0
void conflict::bool_propagate(signed_constraint c, signed_constraint const* premises, unsigned premises_len) {
if (c.is_always_false()) {
VERIFY(false); // TODO: this case can probably happen, but needs special attention
@ -347,6 +362,7 @@ namespace polysat {
void conflict::bool_propagate(signed_constraint c, std::initializer_list<signed_constraint> premises) {
bool_propagate(c, std::data(premises), premises.size());
}
#endif
void conflict::remove(signed_constraint c) {
SASSERT(contains(c));
@ -365,14 +381,7 @@ namespace polysat {
m_kind = conflict_kind_t::ok;
}
void conflict::insert(signed_constraint c, clause_ref lemma) {
unsigned const idx = c.blit().to_uint();
SASSERT(!contains(c)); // not required, but this case should be checked
SASSERT(!m_lemmas.contains(idx)); // not required, but this case should be checked
insert(c);
m_lemmas.insert(idx, lemma);
}
#if 0
clause* conflict::side_lemma(sat::literal lit) const {
unsigned const idx = lit.to_uint();
return m_lemmas.get(idx, {}).get();
@ -383,6 +392,7 @@ namespace polysat {
unsigned const idx = lit.to_uint();
m_lemmas.insert(idx, std::move(lemma));
}
#endif
void conflict::resolve_bool(sat::literal lit, clause const& cl) {
// Note: core: x, y, z; corresponds to clause ~x \/ ~y \/ ~z
@ -503,11 +513,19 @@ namespace polysat {
logger().log_lemma(lemma);
logger().end_conflict();
learn_side_lemmas();
return lemma.build();
}
clause_ref_vector conflict::take_side_lemmas() {
#ifndef NDEBUG
on_scope_exit check_empty([this]() {
SASSERT(m_lemmas.empty());
});
#endif
return std::move(m_lemmas);
}
#if 0
void conflict::learn_side_lemmas() {
auto needs_side_lemma = [this](sat::literal lit) -> bool {
return s.m_bvars.value(lit) == l_undef && side_lemma(lit);
@ -529,9 +547,11 @@ namespace polysat {
todo.push_back(lit2);
// Store and bool-propagate the lemma
s.m_constraints.store(lemma, s, false);
SASSERT(s.m_bvars.value(lit) != l_undef);
}
m_lemmas.reset();
}
#endif
bool conflict::minimize_vars(signed_constraint c) {
if (m_vars.empty())

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

@ -109,7 +109,7 @@ namespace polysat {
unsigned_vector m_var_occurrences; // for each variable, the number of constraints in m_literals that contain it
// Additional lemmas that justify new constraints generated during conflict resolution
u_map<clause_ref> m_lemmas;
clause_ref_vector m_lemmas;
conflict_kind_t m_kind = conflict_kind_t::ok;
@ -119,11 +119,10 @@ namespace polysat {
void set_impl(signed_constraint c);
bool minimize_vars(signed_constraint c);
#if 0
void set_side_lemma(signed_constraint c, clause_ref lemma) { SASSERT(c); set_side_lemma(c.blit(), std::move(lemma)); }
void set_side_lemma(sat::literal lit, clause_ref lemma);
/** Store relevant side lemmas */
void learn_side_lemmas();
#endif
public:
conflict(solver& s);
@ -174,8 +173,10 @@ namespace polysat {
bool contains_pvar(pvar v) const { return m_vars.contains(v) || m_bail_vars.contains(v); }
bool pvar_occurs_in_constraints(pvar v) const { return v < m_var_occurrences.size() && m_var_occurrences[v] > 0; }
#if 0
clause* side_lemma(signed_constraint c) const { SASSERT(c); return side_lemma(c.blit()); }
clause* side_lemma(sat::literal lit) const;
#endif
/**
* Insert constraint c into conflict state.
@ -185,17 +186,17 @@ namespace polysat {
*/
void insert(signed_constraint c);
/**
* Insert constraint c that is justified by the given lemma.
*/
void insert(signed_constraint c, clause_ref lemma);
/** 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);
/** Add a side lemma to the conflict; to be learned in addition to the main lemma after conflict resolution finishes. */
void add_lemma(std::initializer_list<signed_constraint> cs);
void add_lemma(signed_constraint const* cs, unsigned cs_len);
#if 0
/**
* Derive new constraint c by bool-propagation from premises c1, ..., cn;
* as if c was unit-propagated by the lemma c1 /\ ... /\ cn ==> c.
@ -203,6 +204,7 @@ namespace polysat {
*/
void bool_propagate(signed_constraint c, signed_constraint const* premises, unsigned premises_len);
void bool_propagate(signed_constraint c, std::initializer_list<signed_constraint> premises);
#endif
/** Remove c from core */
void remove(signed_constraint c);
@ -226,6 +228,11 @@ namespace polysat {
/** Convert the core into a lemma to be learned. */
clause_ref build_lemma();
/** Move the accumulated side lemmas out of the conflict */
clause_ref_vector take_side_lemmas();
clause_ref_vector const& side_lemmas() const { return m_lemmas; }
std::ostream& display(std::ostream& out) const;
};

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

@ -15,24 +15,9 @@ Author:
#include "math/polysat/log.h"
#include "math/polysat/solver.h"
namespace polysat {
// TODO: rename file
/*
struct post_propagate2 : public inference {
const char* name;
signed_constraint conclusion;
signed_constraint premise1;
signed_constraint premise2;
post_propagate2(const char* name, signed_constraint conclusion, signed_constraint premise1, signed_constraint premise2)
: name(name), conclusion(conclusion), premise1(premise1), premise2(premise2) {}
std::ostream& display(std::ostream& out) const override {
return out << "Post-propagate (by " << name << "), "
<< "conclusion " << conclusion.blit() << ": " << conclusion
<< " from " << premise1.blit() << ": " << premise1
<< " and " << premise2.blit() << ": " << premise2;
}
};
*/
namespace polysat {
struct inference_sup : public inference {
const char* name;
@ -76,33 +61,22 @@ namespace polysat {
// c2 ... constraint that is currently false
// Try to replace it with a new false constraint (derived from superposition with a true constraint)
lbool ex_polynomial_superposition::find_replacement(signed_constraint c2, pvar v, conflict& core) {
vector<signed_constraint> premises;
#if 0
for (auto si : s.m_search) {
if (!si.is_boolean())
continue;
if (si.is_resolved())
continue;
auto c1 = s.lit2cnstr(si.lit());
if (!c1->contains_var(v))
continue;
if (!c1.is_eq())
continue;
if (!c1.is_currently_true(s))
continue;
#else
for (auto c1 : s.m_viable.get_constraints(v)) {
if (!c1->contains_var(v)) // side conditions do not contain v; skip them here
continue;
if (!c1.is_eq())
continue;
SASSERT(c1.is_currently_true(s));
#endif
SASSERT(c2.is_currently_false(s));
SASSERT_EQ(c1.bvalue(s), l_true);
SASSERT_EQ(c2.bvalue(s), l_true);
signed_constraint c = resolve1(v, c1, c2);
if (!c)
continue;
SASSERT(c.is_currently_false(s));
// TODO: move this case distinction into conflict::add_lemma?
char const* inf_name = "?";
switch (c.bvalue(s)) {
case l_false:
@ -117,12 +91,12 @@ namespace polysat {
inf_name = "l_undef";
// c evaluates to false,
// c should be unit-propagated to l_true by c1 /\ c2 ==> c
core.bool_propagate(c, {c1, c2});
// TODO: log inference?
core.add_lemma({c, ~c1, ~c2});
core.log_inference(inference_sup("l_undef lemma", v, c2, c1));
SASSERT_EQ(l_true, c.bvalue(s));
SASSERT(c.is_currently_false(s));
break;
case l_true:
// c is just another constraint on the search stack; could be equivalent or better
inf_name = "l_true";
break;
default:

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

@ -60,9 +60,11 @@ namespace polysat {
for (auto const& c : core) {
sat::literal const lit = c.blit();
out_indent() << lit << ": " << c << '\n';
#if 0
clause* lemma = core.side_lemma(lit);
if (lemma)
out_indent() << " justified by: " << lemma << '\n';
#endif
m_used_constraints.insert(lit.index());
for (pvar v : c->vars())
m_used_vars.insert(v);
@ -88,6 +90,11 @@ namespace polysat {
out_indent() << "(backjump)\n";
break;
}
for (clause* lemma : core.side_lemmas()) {
out_indent() << "Side lemma: " << *lemma << "\n";
for (sat::literal lit : *lemma)
out_indent() << " " << lit_pp(s, lit) << "\n";
}
out().flush();
}
@ -103,10 +110,10 @@ namespace polysat {
void file_inference_logger::log_lemma(clause_builder const& cb) {
out() << hline() << "\nLemma:";
for (auto const& lit : cb)
for (sat::literal lit : cb)
out() << " " << lit;
out() << "\n";
for (auto const& lit : cb)
for (sat::literal lit : cb)
out_indent() << lit_pp(s, lit) << "\n";
out().flush();
}

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

@ -801,9 +801,12 @@ namespace polysat {
// LOG("max_level: " << max_level);
// LOG("jump_level: " << jump_level);
backjump_and_learn(jump_level, *lemma);
/*
m_conflict.reset();
backjump(jump_level);
learn_lemma(*lemma);
*/
}
/**
@ -898,9 +901,16 @@ namespace polysat {
return;
}
unsigned jump_level = get_level(v) - 1;
backjump_and_learn(jump_level, *lemma);
/*
clause_ref_vector side_lemmas = m_conflict.take_side_lemmas();
m_conflict.reset();
backjump(get_level(v) - 1);
for (auto cl : side_lemmas)
add_clause(*cl);
learn_lemma(*lemma);
*/
}
void solver::revert_bool_decision(sat::literal const lit) {
@ -917,9 +927,13 @@ namespace polysat {
SASSERT(all_of(lemma, [this](sat::literal lit1) { return m_bvars.is_false(lit1); }));
SASSERT(all_of(lemma, [this, var](sat::literal lit1) { return var == lit1.var() || m_bvars.level(lit1) < m_bvars.level(var); }));
unsigned jump_level = m_bvars.level(var) - 1;
backjump_and_learn(jump_level, lemma);
/*
m_conflict.reset();
backjump(m_bvars.level(var) - 1);
learn_lemma(lemma);
*/
// At this point, the lemma is asserting for ~lit,
// and has been propagated by learn_lemma/add_clause.
SASSERT(all_of(lemma, [this](sat::literal lit1) { return m_bvars.is_assigned(lit1); }));
@ -930,6 +944,15 @@ namespace polysat {
SASSERT(can_bdecide());
}
void solver::backjump_and_learn(unsigned jump_level, clause& lemma) {
clause_ref_vector side_lemmas = m_conflict.take_side_lemmas();
m_conflict.reset();
backjump(jump_level);
for (auto cl : side_lemmas)
add_clause(*cl);
learn_lemma(lemma);
}
bool solver::lemma_invariant(clause const* lemma) {
SASSERT(lemma);
LOG("Lemma: " << *lemma);

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

@ -212,6 +212,7 @@ namespace polysat {
void backjump_lemma();
void revert_decision(pvar v);
void revert_bool_decision(sat::literal lit);
void backjump_and_learn(unsigned jump_level, clause& lemma);
// activity of variables based on standard VSIDS
unsigned m_activity_inc = 128;