mirror of
https://github.com/Z3Prover/z3
synced 2025-04-28 19:35:50 +00:00
pb propagation
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner
parent
2033e649b5
commit
2d0ab6a615
2 changed files with 100 additions and 78 deletions
|
|
@ -46,6 +46,8 @@ namespace sat {
|
|||
m_lit(lit),
|
||||
m_k(k),
|
||||
m_size(wlits.size()),
|
||||
m_slack(0),
|
||||
m_num_watch(0),
|
||||
m_max_sum(0) {
|
||||
for (unsigned i = 0; i < wlits.size(); ++i) {
|
||||
m_wlits[i] = wlits[i];
|
||||
|
|
@ -237,7 +239,6 @@ namespace sat {
|
|||
p.negate();
|
||||
}
|
||||
|
||||
TRACE("sat", display(tout << "init watch: ", p, true););
|
||||
SASSERT(p.lit() == null_literal || value(p.lit()) == l_true);
|
||||
unsigned sz = p.size(), bound = p.k();
|
||||
|
||||
|
|
@ -280,6 +281,7 @@ namespace sat {
|
|||
p.set_slack(slack);
|
||||
p.set_num_watch(num_watch);
|
||||
}
|
||||
TRACE("sat", display(tout << "init watch: ", p, true););
|
||||
}
|
||||
|
||||
/*
|
||||
|
|
@ -296,7 +298,7 @@ namespace sat {
|
|||
Lw = Lw u {l_s}
|
||||
Lu = Lu \ {l_s}
|
||||
}
|
||||
if (Sw < bound) conflict
|
||||
if (Sw < k) conflict
|
||||
while (Sw < k + a_max) {
|
||||
assign (l_max)
|
||||
a_max = max { ai | li in Lw, li = undef }
|
||||
|
|
@ -308,7 +310,19 @@ namespace sat {
|
|||
|
||||
|
||||
*/
|
||||
void card_extension::add_index(pb& p, unsigned index, literal lit) {
|
||||
if (value(lit) == l_undef) {
|
||||
m_pb_undef.push_back(index);
|
||||
if (p[index].first > m_a_max) {
|
||||
m_a_max = p[index].first;
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
lbool card_extension::add_assign(pb& p, literal alit) {
|
||||
|
||||
TRACE("sat", display(tout << "assign: " << alit << "\n", p, true););
|
||||
SASSERT(!s().inconsistent());
|
||||
unsigned sz = p.size();
|
||||
unsigned bound = p.k();
|
||||
unsigned num_watch = p.num_watch();
|
||||
|
|
@ -316,63 +330,43 @@ namespace sat {
|
|||
SASSERT(value(alit) == l_false);
|
||||
SASSERT(p.lit() == null_literal || value(p.lit()) == l_true);
|
||||
SASSERT(num_watch <= sz);
|
||||
SASSERT(num_watch > 0);
|
||||
unsigned index = 0;
|
||||
unsigned a_max = 0;
|
||||
unsigned max_index = 0;
|
||||
m_a_max = 0;
|
||||
m_pb_undef.reset();
|
||||
for (; index < num_watch; ++index) {
|
||||
literal lit = p[index].second;
|
||||
if (lit == alit) {
|
||||
break;
|
||||
}
|
||||
if (value(lit) == l_undef) {
|
||||
m_pb_undef.push_back(index);
|
||||
if (p[index].first > a_max) {
|
||||
a_max = p[index].first;
|
||||
max_index = index;
|
||||
}
|
||||
}
|
||||
add_index(p, index, lit);
|
||||
}
|
||||
|
||||
for (unsigned j = index + 1; a_max == 0 && j < num_watch; ++j) {
|
||||
literal lit = p[j].second;
|
||||
if (value(lit) == l_undef) {
|
||||
m_pb_undef.push_back(j);
|
||||
a_max = p[j].first;
|
||||
max_index = j;
|
||||
}
|
||||
}
|
||||
for (unsigned j = num_watch; a_max == 0 && j < sz; ++j) {
|
||||
literal lit = p[j].second;
|
||||
if (value(lit) == l_undef) {
|
||||
p.swap(j, num_watch);
|
||||
m_pb_undef.push_back(num_watch);
|
||||
a_max = p[num_watch].first;
|
||||
max_index = num_watch;
|
||||
}
|
||||
SASSERT(index < num_watch);
|
||||
|
||||
unsigned index1 = index + 1;
|
||||
for (; m_a_max == 0 && index1 < num_watch; ++index1) {
|
||||
add_index(p, index1, p[index1].second);
|
||||
}
|
||||
|
||||
unsigned val = p[index].first;
|
||||
SASSERT(num_watch > 0);
|
||||
SASSERT(index < num_watch);
|
||||
SASSERT(value(p[index].second) == l_false);
|
||||
SASSERT(val <= slack);
|
||||
slack -= val;
|
||||
// find literals to swap with:
|
||||
for (unsigned j = num_watch; j < sz && slack < bound + a_max; ++j) {
|
||||
if (value(p[j].second) != l_false) {
|
||||
for (unsigned j = num_watch; j < sz && slack < bound + m_a_max; ++j) {
|
||||
literal lit = p[j].second;
|
||||
if (value(lit) != l_false) {
|
||||
slack += p[j].first;
|
||||
watch_literal(p, p[j]);
|
||||
p.swap(num_watch, j);
|
||||
if (value(p[num_watch].second) == l_undef && a_max < p[num_watch].first) {
|
||||
m_pb_undef.push_back(num_watch);
|
||||
a_max = p[num_watch].first;
|
||||
max_index = num_watch;
|
||||
}
|
||||
add_index(p, num_watch, lit);
|
||||
++num_watch;
|
||||
}
|
||||
}
|
||||
|
||||
SASSERT(!s().inconsistent());
|
||||
DEBUG_CODE(for (auto idx : m_pb_undef) { SASSERT(value(p[idx].second) == l_undef); });
|
||||
|
||||
if (slack < bound) {
|
||||
// maintain watching the literal
|
||||
slack += val;
|
||||
|
|
@ -385,34 +379,30 @@ namespace sat {
|
|||
}
|
||||
|
||||
// swap out the watched literal.
|
||||
p.set_slack(slack);
|
||||
--num_watch;
|
||||
SASSERT(num_watch > 0);
|
||||
p.set_slack(slack);
|
||||
p.set_num_watch(num_watch);
|
||||
p.swap(num_watch, index);
|
||||
if (num_watch == max_index) {
|
||||
max_index = index;
|
||||
}
|
||||
|
||||
SASSERT(max_index < sz);
|
||||
while (slack < bound + a_max && !s().inconsistent()) {
|
||||
// variable at max-index must be assigned to true.
|
||||
assign(p, p[max_index].second);
|
||||
|
||||
a_max = 0;
|
||||
// find the next a_max among m_pb_undef
|
||||
while (!m_pb_undef.empty() && l_undef != value(p[m_pb_undef.back()].second)) {
|
||||
if (slack < bound + m_a_max) {
|
||||
while (!s().inconsistent() && !m_pb_undef.empty()) {
|
||||
index1 = m_pb_undef.back();
|
||||
literal lit = p[index1].second;
|
||||
if (slack >= bound + p[index1].first) {
|
||||
break;
|
||||
}
|
||||
m_pb_undef.pop_back();
|
||||
if (value(lit) == l_undef) {
|
||||
assign(p, lit);
|
||||
}
|
||||
}
|
||||
if (m_pb_undef.empty()) {
|
||||
break;
|
||||
}
|
||||
max_index = m_pb_undef.back();
|
||||
a_max = p[max_index].first;
|
||||
m_pb_undef.pop_back();
|
||||
}
|
||||
|
||||
return s().inconsistent() ? l_false : l_true;
|
||||
|
||||
TRACE("sat", display(tout << "assign: " << alit << "\n", p, true););
|
||||
|
||||
return l_undef;
|
||||
}
|
||||
|
||||
void card_extension::watch_literal(pb& p, wliteral l) {
|
||||
|
|
@ -467,6 +457,7 @@ namespace sat {
|
|||
set_conflict(p, lit);
|
||||
break;
|
||||
default:
|
||||
SASSERT(validate_unit_propagation(p, lit));
|
||||
m_stats.m_num_pb_propagations++;
|
||||
m_num_propagations_since_pop++;
|
||||
if (s().m_config.m_drat) {
|
||||
|
|
@ -483,7 +474,7 @@ namespace sat {
|
|||
}
|
||||
|
||||
void card_extension::display(std::ostream& out, pb const& p, bool values) const {
|
||||
out << p.lit() << "[" << p.size() << "]";
|
||||
out << p.lit() << "[ watch: " << p.num_watch() << ", slack: " << p.slack() << "]";
|
||||
if (p.lit() != null_literal && values) {
|
||||
out << "@(" << value(p.lit());
|
||||
if (value(p.lit()) != l_undef) {
|
||||
|
|
@ -514,7 +505,7 @@ namespace sat {
|
|||
}
|
||||
|
||||
void card_extension::asserted_pb(literal l, ptr_vector<pb>* pbs, pb* p0) {
|
||||
TRACE("sat", tout << l << " " << !is_tag_empty(pbs) << " " << (p0 != 0) << "\n";);
|
||||
TRACE("sat", tout << "literal: " << l << " has pb: " << !is_tag_empty(pbs) << " p0 != 0: " << (p0 != 0) << "\n";);
|
||||
if (!is_tag_empty(pbs)) {
|
||||
ptr_vector<pb>::iterator begin = pbs->begin();
|
||||
ptr_vector<pb>::iterator it = begin, it2 = it, end = pbs->end();
|
||||
|
|
@ -524,20 +515,28 @@ namespace sat {
|
|||
continue;
|
||||
}
|
||||
switch (add_assign(p, ~l)) {
|
||||
case l_false: // conflict
|
||||
for (; it != end; ++it, ++it2) {
|
||||
*it2 = *it;
|
||||
}
|
||||
SASSERT(s().inconsistent());
|
||||
pbs->set_end(it2);
|
||||
return;
|
||||
case l_true: // unit propagation, keep watching the literal
|
||||
if (it2 != it) {
|
||||
*it2 = *it;
|
||||
}
|
||||
++it2;
|
||||
break;
|
||||
case l_false: // conflict.
|
||||
SASSERT(s().inconsistent());
|
||||
for (; it != end; ++it, ++it2) {
|
||||
*it2 = *it;
|
||||
}
|
||||
pbs->set_end(it2);
|
||||
return;
|
||||
case l_undef: // watch literal was swapped
|
||||
if (s().inconsistent()) {
|
||||
++it;
|
||||
for (; it != end; ++it, ++it2) {
|
||||
*it2 = *it;
|
||||
}
|
||||
pbs->set_end(it2);
|
||||
return;
|
||||
}
|
||||
break;
|
||||
}
|
||||
}
|
||||
|
|
@ -844,6 +843,7 @@ namespace sat {
|
|||
literal consequent = s().m_not_l;
|
||||
justification js = s().m_conflict;
|
||||
TRACE("sat", tout << consequent << " " << js << "\n";);
|
||||
TRACE("sat", s().display(tout););
|
||||
m_conflict_lvl = s().get_max_lvl(consequent, js);
|
||||
if (consequent != null_literal) {
|
||||
consequent.neg();
|
||||
|
|
@ -942,7 +942,7 @@ namespace sat {
|
|||
m_bound += offset;
|
||||
inc_coeff(consequent, offset);
|
||||
get_pb_antecedents(consequent, p, m_lemma);
|
||||
TRACE("sat", tout << m_lemma << "\n";);
|
||||
TRACE("sat", display(tout, p, true); tout << m_lemma << "\n";);
|
||||
for (unsigned i = 0; i < m_lemma.size(); ++i) {
|
||||
process_antecedent(~m_lemma[i], offset);
|
||||
}
|
||||
|
|
@ -989,6 +989,7 @@ namespace sat {
|
|||
SASSERT(lvl(v) == m_conflict_lvl);
|
||||
s().reset_mark(v);
|
||||
--idx;
|
||||
TRACE("sat", tout << "Unmark: v" << v << "\n";);
|
||||
--m_num_marks;
|
||||
js = s().m_justification[v];
|
||||
offset = get_abs_coeff(v);
|
||||
|
|
@ -1153,6 +1154,7 @@ namespace sat {
|
|||
|
||||
if (level > 0 && !s().is_marked(v) && level == m_conflict_lvl) {
|
||||
s().mark(v);
|
||||
TRACE("sat", tout << "Mark: v" << v << "\n";);
|
||||
++m_num_marks;
|
||||
}
|
||||
inc_coeff(l, offset);
|
||||
|
|
@ -1347,20 +1349,12 @@ namespace sat {
|
|||
void card_extension::get_pb_antecedents(literal l, pb const& p, literal_vector& r) {
|
||||
if (p.lit() != null_literal) r.push_back(p.lit());
|
||||
SASSERT(p.lit() == null_literal || value(p.lit()) == l_true);
|
||||
unsigned k = p.k();
|
||||
unsigned max_sum = p.max_sum();
|
||||
for (unsigned i = p.size(); i > 0 && max_sum >= k; ) {
|
||||
--i;
|
||||
TRACE("sat", display(tout, p, true););
|
||||
for (unsigned i = p.num_watch(); i < p.size(); ++i) {
|
||||
literal lit = p[i].second;
|
||||
if (lit == l) {
|
||||
max_sum -= p[i].first;
|
||||
}
|
||||
else if (value(lit) == l_false) {
|
||||
r.push_back(~p[i].second);
|
||||
max_sum -= p[i].first;
|
||||
}
|
||||
SASSERT(l_false == value(lit));
|
||||
r.push_back(~lit);
|
||||
}
|
||||
SASSERT(max_sum < k);
|
||||
}
|
||||
|
||||
void card_extension::get_card_antecedents(literal l, card const& c, literal_vector& r) {
|
||||
|
|
@ -1776,6 +1770,31 @@ namespace sat {
|
|||
}
|
||||
return true;
|
||||
}
|
||||
bool card_extension::validate_unit_propagation(pb const& p, literal alit) {
|
||||
if (p.lit() != null_literal && value(p.lit()) != l_true) return false;
|
||||
|
||||
unsigned k = p.k();
|
||||
unsigned sum = 0;
|
||||
unsigned a_min = 0;
|
||||
TRACE("sat", display(tout << "validate: " << alit << "\n", p, true););
|
||||
for (unsigned i = 0; i < p.size(); ++i) {
|
||||
literal lit = p[i].second;
|
||||
lbool val = value(lit);
|
||||
if (val == l_false) {
|
||||
// no-op
|
||||
}
|
||||
else if (lit == alit) {
|
||||
a_min = p[i].first;
|
||||
sum += p[i].first;
|
||||
}
|
||||
else {
|
||||
sum += p[i].first;
|
||||
}
|
||||
}
|
||||
return sum < k + a_min;
|
||||
return true;
|
||||
}
|
||||
|
||||
bool card_extension::validate_lemma() {
|
||||
int val = -m_bound;
|
||||
normalize_active_coeffs();
|
||||
|
|
|
|||
|
|
@ -232,10 +232,12 @@ namespace sat {
|
|||
|
||||
|
||||
// pb functionality
|
||||
unsigned m_a_max;
|
||||
void copy_pb(card_extension& result);
|
||||
void asserted_pb(literal l, ptr_vector<pb>* pbs, pb* p);
|
||||
void init_watch(pb& p, bool is_true);
|
||||
lbool add_assign(pb& p, literal alit);
|
||||
void add_index(pb& p, unsigned index, literal lit);
|
||||
void watch_literal(pb& p, wliteral lit);
|
||||
void clear_watch(pb& p);
|
||||
void set_conflict(pb& p, literal lit);
|
||||
|
|
@ -280,6 +282,7 @@ namespace sat {
|
|||
bool validate_assign(literal_vector const& lits, literal lit);
|
||||
bool validate_lemma();
|
||||
bool validate_unit_propagation(card const& c);
|
||||
bool validate_unit_propagation(pb const& p, literal lit);
|
||||
bool validate_conflict(literal_vector const& lits, ineq& p);
|
||||
|
||||
ineq m_A, m_B, m_C;
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue