mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-24 17:45:32 +00:00
Code Activity

Update use of insert_eval and lemma scores to support propagation

Browse source
This commit is contained in:
Jakob Rath 2022-12-07 16:08:24 +01:00
parent fca4f18194
commit 85715eb164
6 changed files with 76 additions and 59 deletions
Download patch file Download diff file Expand all files Collapse all files

9
src/math/polysat/clause_builder.cpp
View file

@ -75,13 +75,14 @@ namespace polysat {
m_literals.push_back(c.blit());
}
void clause_builder::insert_eval(sat::literal lit) {
insert_eval(m_solver->lit2cnstr(lit));
void clause_builder::insert_eval(sat::literal lit, bool status) {
insert_eval(m_solver->lit2cnstr(lit), status);
}
void clause_builder::insert_eval(signed_constraint c) {
void clause_builder::insert_eval(signed_constraint c, bool status) {
if (c.bvalue(*m_solver) == l_undef) {
m_solver->assign_eval(~c.blit());
sat::literal lit = c.blit();
m_solver->assign_eval(status ? lit : ~lit);
}
insert(c);
}

16
src/math/polysat/clause_builder.h
View file

@ -51,11 +51,17 @@ namespace polysat {
void insert(signed_constraint c);
void insert(inequality const& i) { insert(i.as_signed_constraint()); }
/// Inserting constraints into the clause.
/// If they are not yet on the search stack, add them as evaluated to false.
/// \pre Constraint must be false in the current assignment.
void insert_eval(sat::literal lit);
void insert_eval(signed_constraint c);
/// Insert constraints into the clause.
/// If they are not yet on the search stack, add them as evaluated to the given status.
/// \pre Constraint must evaluate to true or false according to the given status in the current assignment.
void insert_eval(sat::literal lit, bool status);
void insert_eval(signed_constraint c, bool status);
/// Insert constraints into the clause.
/// If they are not yet on the search stack, add them as evaluated to \b false.
/// \pre Constraint must be \b false in the current assignment.
void insert_eval(sat::literal lit) { insert_eval(lit, false); }
void insert_eval(signed_constraint c) { insert_eval(c, false); }
void insert_eval(inequality const& i) { insert_eval(i.as_signed_constraint()); }
using const_iterator = decltype(m_literals)::const_iterator;

50
src/math/polysat/saturation.cpp
View file

@ -96,8 +96,7 @@ namespace polysat {
SASSERT(all_of(m_lemma, [this](sat::literal lit) { return is_forced_false(s.lit2cnstr(lit)); }));
// NSB review question: insert_eval: Is this right?
m_lemma.insert_eval(c);
m_lemma.insert(c);
core.add_lemma(m_rule, m_lemma.build());
return true;
}
@ -514,20 +513,20 @@ namespace polysat {
auto prop1 = [&](signed_constraint c) {
m_lemma.reset();
m_lemma.insert(~s.eq(b));
m_lemma.insert(~s.eq(y));
m_lemma.insert(x_eq_0);
m_lemma.insert(a_eq_0);
m_lemma.insert_eval(~s.eq(b));
m_lemma.insert_eval(~s.eq(y));
m_lemma.insert_eval(x_eq_0);
m_lemma.insert_eval(a_eq_0);
return propagate(core, axb_l_y, c);
};
auto prop2 = [&](signed_constraint ante, signed_constraint c) {
m_lemma.reset();
m_lemma.insert(~s.eq(b));
m_lemma.insert(~s.eq(y));
m_lemma.insert(x_eq_0);
m_lemma.insert(a_eq_0);
m_lemma.insert(~ante);
m_lemma.insert_eval(~s.eq(b));
m_lemma.insert_eval(~s.eq(y));
m_lemma.insert_eval(x_eq_0);
m_lemma.insert_eval(a_eq_0);
m_lemma.insert_eval(~ante);
return propagate(core, axb_l_y, c);
};
@ -648,27 +647,34 @@ namespace polysat {
signed_constraint b_is_odd = s.odd(b);
signed_constraint a_is_odd = s.odd(a);
signed_constraint x_is_odd = s.odd(X);
#if 0
LOG_H1("try_parity: " << X << " on: " << lit_pp(s, axb_l_y.as_signed_constraint()));
LOG("y: " << y << " a: " << a << " b: " << b);
LOG("b_is_odd: " << lit_pp(s, b_is_odd));
LOG("a_is_odd: " << lit_pp(s, a_is_odd));
LOG("x_is_odd: " << lit_pp(s, x_is_odd));
#endif
if (!b_is_odd.is_currently_true(s)) {
if (!a_is_odd.is_currently_true(s))
return false;
if (!x_is_odd.is_currently_true(s))
return false;
m_lemma.reset();
m_lemma.insert(~s.eq(y));
m_lemma.insert(~a_is_odd);
m_lemma.insert(~x_is_odd);
m_lemma.insert_eval(~s.eq(y));
m_lemma.insert_eval(~a_is_odd);
m_lemma.insert_eval(~x_is_odd);
if (propagate(core, axb_l_y, b_is_odd))
return true;
return false;
}
m_lemma.reset();
m_lemma.insert(~s.eq(y));
m_lemma.insert(~b_is_odd);
m_lemma.insert_eval(~s.eq(y));
m_lemma.insert_eval(~b_is_odd);
if (propagate(core, axb_l_y, a_is_odd))
return true;
m_lemma.reset();
m_lemma.insert(~s.eq(y));
m_lemma.insert(~b_is_odd);
m_lemma.insert_eval(~s.eq(y));
m_lemma.insert_eval(~b_is_odd);
if (propagate(core, axb_l_y, x_is_odd))
return true;
return false;
@ -693,14 +699,14 @@ namespace polysat {
if (!is_forced_diseq(a, 0, a_eq_0))
return false;
m_lemma.reset();
m_lemma.insert(s.eq(y));
m_lemma.insert(~s.eq(b));
m_lemma.insert(a_eq_0);
m_lemma.insert_eval(s.eq(y));
m_lemma.insert_eval(~s.eq(b));
m_lemma.insert_eval(a_eq_0);
if (propagate(core, axb_l_y, s.even(X)))
return true;
if (!is_forced_diseq(X, 0, x_eq_0))
return false;
m_lemma.insert(x_eq_0);
m_lemma.insert_eval(x_eq_0);
if (propagate(core, axb_l_y, s.even(a)))
return true;
return false;

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

@ -824,17 +824,12 @@ namespace polysat {
backjump_and_learn(max_jump_level);
}
//
// NSB review: this code assumes that these lemmas are false.
// It does not allow saturation to add unit propagation into freshly created literals.
//
std::optional<lemma_score> solver::compute_lemma_score(clause const& lemma) {
unsigned max_level = 0; // highest level in lemma
unsigned lits_at_max_level = 0; // how many literals at the highest level in lemma
unsigned snd_level = 0; // second-highest level in lemma
bool is_propagation = false;
unsigned max_level = 0; // highest level in lemma
unsigned lits_at_max_level = 0; // how many literals at the highest level in lemma
unsigned snd_level = 0; // second-highest level in lemma
bool is_propagation = false; // whether there is an unassigned literal (at most one)
for (sat::literal lit : lemma) {
SASSERT(m_bvars.is_assigned(lit)); // any new constraints should have been assign_eval'd
if (m_bvars.is_true(lit)) // may happen if we only use the clause to justify a new constraint; it is not a real lemma
return std::nullopt;
if (!m_bvars.is_assigned(lit)) {
@ -861,15 +856,19 @@ namespace polysat {
// Do the standard backjumping known from SAT solving (back to second-highest level in the lemma, propagate it there).
// - Semantic split clause: multiple literals on the highest level in the lemma.
// Backtrack to "highest level - 1" and split on the lemma there.
// For now, we follow the same convention for computing the jump levels.
// For now, we follow the same convention for computing the jump levels,
// but we support an additional type of clause:
// - Propagation clause: a single literal is unassigned and should be propagated after backjumping.
// backjump to max_level so we can propagate
unsigned jump_level;
unsigned branching_factor = lits_at_max_level;
if (is_propagation)
jump_level = max_level;
if (lits_at_max_level <= 1)
jump_level = max_level, branching_factor = 1;
else if (lits_at_max_level <= 1)
jump_level = snd_level;
else
jump_level = (max_level == 0) ? 0 : (max_level - 1);
return {{jump_level, lits_at_max_level}};
return {{jump_level, branching_factor}};
}
void solver::backjump_and_learn(unsigned max_jump_level) {
@ -886,6 +885,10 @@ namespace polysat {
auto appraise_lemma = [&](clause* lemma) {
m_simplify_clause.apply(*lemma);
auto score = compute_lemma_score(*lemma);
if (score)
LOG(" score: " << *score);
else
LOG(" score: <none>");
if (score && *score < best_score) {
best_score = *score;
best_lemma = lemma;
@ -905,6 +908,9 @@ namespace polysat {
unsigned const jump_level = std::max(best_score.jump_level(), base_level());
SASSERT(jump_level <= max_jump_level);
LOG("best_score: " << best_score);
LOG("best_lemma: " << *best_lemma);
m_conflict.reset();
backjump(jump_level);
@ -940,10 +946,7 @@ namespace polysat {
SASSERT(!is_conflict());
}
LOG("best_score: " << best_score);
LOG("best_lemma: " << *best_lemma);
if (best_score.literals_at_max_level() > 1) {
if (best_score.branching_factor() > 1) {
// NOTE: at this point it is possible that the best_lemma is non-asserting.
// We need to double-check, because the backjump level may not be exact (see comment on checking is_conflict above).
bool const is_asserting = all_of(*best_lemma, [this](sat::literal lit) { return m_bvars.is_assigned(lit); });
@ -1269,7 +1272,8 @@ namespace polysat {
out << lpad(4, lit) << ": " << rpad(30, c);
if (!c)
return out;
out << " [ " << s.m_bvars.value(lit);
out << " [ b:" << rpad(7, s.m_bvars.value(lit));
out << " p:" << rpad(7, c.eval(s));
if (s.m_bvars.is_assigned(lit)) {
out << ' ';
if (s.m_bvars.is_assumption(lit))

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

@ -52,20 +52,19 @@ namespace polysat {
*
* Comparison criterion:
* - Lowest jump level has priority, because otherwise, some of the accumulated lemmas may still be false after backjumping.
* - To break ties on jump level, choose clause with the fewest literals at its highest decision level;
* to limit case splits.
* - To break ties on jump level, choose clause with the lowest branching factor.
*/
class lemma_score {
unsigned m_jump_level;
unsigned m_literals_at_max_level;
unsigned m_branching_factor; // how many literals will be unassigned after backjumping to jump_level
public:
lemma_score(unsigned jump_level, unsigned at_max_level)
: m_jump_level(jump_level), m_literals_at_max_level(at_max_level)
lemma_score(unsigned jump_level, unsigned bf)
: m_jump_level(jump_level), m_branching_factor(bf)
{ }
unsigned jump_level() const { return m_jump_level; }
unsigned literals_at_max_level() const { return m_literals_at_max_level; }
unsigned branching_factor() const { return m_branching_factor; }
static lemma_score max() {
return {UINT_MAX, UINT_MAX};
@ -73,20 +72,20 @@ namespace polysat {
bool operator==(lemma_score const& other) const {
return m_jump_level == other.m_jump_level
&& m_literals_at_max_level == other.m_literals_at_max_level;
&& m_branching_factor == other.m_branching_factor;
}
bool operator!=(lemma_score const& other) const { return !operator==(other); }
bool operator<(lemma_score const& other) const {
return m_jump_level < other.m_jump_level
|| (m_jump_level == other.m_jump_level && m_literals_at_max_level < other.m_literals_at_max_level);
|| (m_jump_level == other.m_jump_level && m_branching_factor < other.m_branching_factor);
}
bool operator>(lemma_score const& other) const { return other.operator<(*this); }
bool operator<=(lemma_score const& other) const { return operator==(other) || operator<(other); }
bool operator>=(lemma_score const& other) const { return operator==(other) || operator>(other); }
std::ostream& display(std::ostream& out) const {
return out << "jump_level=" << m_jump_level << " at_max_level=" << m_literals_at_max_level;
return out << "jump_level=" << m_jump_level << " branching_factor=" << m_branching_factor;
}
};
@ -413,6 +412,7 @@ namespace polysat {
signed_constraint eq(pdd const& p, unsigned q) { return eq(p - q); }
signed_constraint odd(pdd const& p) { return ~even(p); }
signed_constraint even(pdd const& p) { return parity(p, 1); }
/** parity(p) >= k (<=> p * 2^(K-k) == 0) */
signed_constraint parity(pdd const& p, unsigned k) { return eq(p*rational::power_of_two(p.manager().power_of_2() - k)); }
signed_constraint diseq(pdd const& p, rational const& q) { return diseq(p - q); }
signed_constraint diseq(pdd const& p, unsigned q) { return diseq(p - q); }

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

@ -725,7 +725,7 @@ namespace polysat {
}
while (e != first);
SASSERT(all_of(lemma, [this](sat::literal lit) { return s.m_bvars.value(lit) == l_false; }));
SASSERT(all_of(lemma, [this](sat::literal lit) { return s.m_bvars.value(lit) == l_false || s.lit2cnstr(lit).is_currently_false(s); }));
core.add_lemma("viable", lemma.build());
core.logger().log(inf_fi(*this, v));
return true;