mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 13:28:47 +00:00
Code Activity

Lookahead clause size optimization. Fixed some missing propagations

Browse source
This commit is contained in:
Miguel Neves 2017-10-17 13:15:34 -07:00
parent 4394ce96ae
commit 806690571e
2 changed files with 117 additions and 53 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

164
src/sat/sat_lookahead.cpp
View file

@ -155,7 +155,7 @@ namespace sat {
if (is_stamped(~w)) { if (is_stamped(~w)) {
// u \/ v, ~v \/ w, u \/ ~w => u is unit // u \/ v, ~v \/ w, u \/ ~w => u is unit
TRACE("sat", tout << "tc1: " << u << "\n";); TRACE("sat", tout << "tc1: " << u << "\n";);
assign(u); propagated(u);
return false; return false;
} }
if (m_num_tc1 < m_config.m_tc1_limit) { if (m_num_tc1 < m_config.m_tc1_limit) {
@ -181,14 +181,14 @@ namespace sat {
set_bstamps(~u); set_bstamps(~u);
if (is_stamped(~v)) { if (is_stamped(~v)) {
TRACE("sat", tout << "try_add_binary: " << u << "\n";); TRACE("sat", tout << "try_add_binary: " << u << "\n";);
assign(u); // u \/ ~v, u \/ v => u is a unit literal propagated(u); // u \/ ~v, u \/ v => u is a unit literal
} }
else if (!is_stamped(v) && add_tc1(u, v)) { else if (!is_stamped(v) && add_tc1(u, v)) {
// u \/ v is not in index // u \/ v is not in index
set_bstamps(~v); set_bstamps(~v);
if (is_stamped(~u)) { if (is_stamped(~u)) {
TRACE("sat", tout << "try_add_binary: " << v << "\n";); TRACE("sat", tout << "try_add_binary: " << v << "\n";);
assign(v); // v \/ ~u, u \/ v => v is a unit literal propagated(v); // v \/ ~u, u \/ v => v is a unit literal
} }
else if (add_tc1(v, u)) { else if (add_tc1(v, u)) {
update_prefix(u); update_prefix(u);
@ -407,6 +407,37 @@ namespace sat {
return true; return true;
} }
bool lookahead::missed_propagation() const {
for (literal l1 : m_trail) {
SASSERT(is_true(l1));
for (literal l2 : m_binary[l1.index()]) {
if (is_undef(l2)) return true;
}
unsigned sz = m_ternary_count[(~l1).index()];
for (binary b : m_ternary[(~l1).index()]) {
if (sz-- == 0) break;
if ((is_false(b.m_u) && is_undef(b.m_v)) || (is_false(b.m_v) && is_undef(b.m_u)))
return true;
}
}
for (nary * n : m_nary_clauses) {
if (n->size() == 1 && !is_true(n->get_head())) {
for (literal lit : *n) {
if (is_undef(lit)) return true;
}
}
}
return false;
}
bool lookahead::missed_conflict() const {
if (inconsistent()) return false;
for (nary * n : m_nary_clauses) {
if (n->size() == 0) return true;
}
return false;
}
void lookahead::init_pre_selection(unsigned level) { void lookahead::init_pre_selection(unsigned level) {
switch (m_config.m_reward_type) { switch (m_config.m_reward_type) {
case ternary_reward: { case ternary_reward: {
@ -1098,11 +1129,19 @@ namespace sat {
} }
void lookahead::lookahead_backtrack() { void lookahead::lookahead_backtrack() {
while (!m_trail.empty() && is_undef(m_trail.back())) { literal lit = null_literal;
while (!m_trail.empty() && is_undef((lit = m_trail.back()))) {
if (m_qhead == m_trail.size()) {
unsigned sz = m_nary_count[(~lit).index()];
for (nary* n : m_nary[(~lit).index()]) {
if (sz-- == 0) break;
n->inc_size();
}
--m_qhead;
}
m_trail.pop_back(); m_trail.pop_back();
} }
SASSERT(m_trail_lim.empty() || m_trail.size() >= m_trail_lim.back()); SASSERT(m_trail_lim.empty() || m_trail.size() >= m_trail_lim.back());
m_qhead = std::min(m_qhead, m_trail.size());
} }
// //
@ -1137,14 +1176,15 @@ namespace sat {
lbool lookahead::propagate_ternary(literal l1, literal l2) { lbool lookahead::propagate_ternary(literal l1, literal l2) {
if (is_fixed(l1)) { if (is_fixed(l1)) {
if (is_false(l1)) { if (is_false(l1)) {
if (is_undef(l2)) { if (is_false(l2)) {
propagated(l2);
}
else if (is_false(l2)) {
TRACE("sat", tout << l1 << " " << l2 << " " << "\n";); TRACE("sat", tout << l1 << " " << l2 << " " << "\n";);
set_conflict(); set_conflict();
return l_false;
} }
return l_false; else if (is_undef(l2)) {
propagated(l2);
}
return l_true;
} }
else { else {
return l_true; return l_true;
@ -1298,10 +1338,11 @@ namespace sat {
unsigned sz = m_nary_count[(~l).index()]; unsigned sz = m_nary_count[(~l).index()];
literal lit; literal lit;
SASSERT(m_search_mode == lookahead_mode::searching); SASSERT(m_search_mode == lookahead_mode::searching);
for (nary * n : m_nary[(~l).index()]) { for (nary* n : m_nary[(~l).index()]) {
if (sz-- == 0) break; if (sz-- == 0) break;
unsigned len = n->dec_size(); unsigned len = n->dec_size();
if (m_inconsistent) continue; if (is_true(n->get_head())) continue;
if (inconsistent()) continue;
if (len <= 1) continue; // already processed if (len <= 1) continue; // already processed
// find the two unassigned literals, if any // find the two unassigned literals, if any
if (len == 2) { if (len == 2) {
@ -1357,53 +1398,35 @@ namespace sat {
void lookahead::propagate_clauses_lookahead(literal l) { void lookahead::propagate_clauses_lookahead(literal l) {
// clauses where l is negative // clauses where l is negative
unsigned sz = m_nary_count[(~l).index()]; unsigned sz = m_nary_count[(~l).index()];
literal lit;
SASSERT(m_search_mode == lookahead_mode::lookahead1 || SASSERT(m_search_mode == lookahead_mode::lookahead1 ||
m_search_mode == lookahead_mode::lookahead2); m_search_mode == lookahead_mode::lookahead2);
for (nary* n : m_nary[(~l).index()]) { for (nary* n : m_nary[(~l).index()]) {
if (sz-- == 0) break; if (sz-- == 0) break;
unsigned nonfixed = n->dec_size();
if (is_true(n->get_head())) { if (is_true(n->get_head())) continue;
continue; if (inconsistent()) continue;
} if (nonfixed <= 1) {
literal l1 = null_literal; bool found_conflict = true;
literal l2 = null_literal; for (literal lit : *n) {
bool skip_clause = false; if (!is_fixed(lit)) {
unsigned nonfixed = 0; propagated(lit);
for (literal lit : *n) { found_conflict = false;
if (!is_fixed(lit)) { break;
++nonfixed;
if (l1 == null_literal) {
l1 = lit;
}
else if (l2 == null_literal) {
l2 = lit;
} }
else if (m_search_mode == lookahead_mode::lookahead2) { else if (is_true(lit)) {
skip_clause = true; n->set_head(lit);
found_conflict = false;
break; break;
} }
} }
else if (is_true(lit)) { if (found_conflict) {
n->set_head(lit); set_conflict();
skip_clause = true; continue;
break;
} }
} }
if (skip_clause) { else if (m_search_mode == lookahead_mode::lookahead1) {
// skip, the clause
}
else if (l1 == null_literal) {
set_conflict();
return;
}
else if (l2 == null_literal) {
propagated(l1);
}
else {
SASSERT(nonfixed >= 2); SASSERT(nonfixed >= 2);
SASSERT(m_search_mode == lookahead_mode::lookahead1);
switch (m_config.m_reward_type) { switch (m_config.m_reward_type) {
case heule_schur_reward: { case heule_schur_reward: {
double to_add = 0; double to_add = 0;
@ -1418,9 +1441,35 @@ namespace sat {
case heule_unit_reward: case heule_unit_reward:
m_lookahead_reward += pow(0.5, nonfixed); m_lookahead_reward += pow(0.5, nonfixed);
break; break;
case march_cu_reward:
m_lookahead_reward += 3.3 * pow(0.5, nonfixed - 2);
break;
case ternary_reward: case ternary_reward:
if (nonfixed == 2) { if (nonfixed == 2) {
m_lookahead_reward += (*m_heur)[l1.index()] * (*m_heur)[l2.index()]; literal l1 = null_literal;
literal l2 = null_literal;
for (literal lit : *n) {
if (!is_fixed(lit)) {
if (l1 == null_literal) {
l1 = lit;
}
else {
SASSERT(l2 != null_literal);
l2 = lit;
break;
}
}
}
if (l1 == null_literal) {
set_conflict();
continue;
}
else if (l2 == null_literal) {
propagated(l1);
}
else {
m_lookahead_reward += (*m_heur)[l1.index()] * (*m_heur)[l2.index()];
}
} }
else { else {
m_lookahead_reward += (double)0.001; m_lookahead_reward += (double)0.001;
@ -1431,6 +1480,14 @@ namespace sat {
} }
} }
} }
// clauses where l is positive:
sz = m_nary_count[l.index()];
for (nary* n : m_nary[l.index()]) {
if (sz-- == 0) break;
if (m_stamp[l.var()] > m_stamp[n->get_head().var()]) {
n->set_head(l);
}
}
} }
void lookahead::remove_clause_at(literal l, nary& n) { void lookahead::remove_clause_at(literal l, nary& n) {
@ -1567,9 +1624,9 @@ namespace sat {
void lookahead::propagate_binary(literal l) { void lookahead::propagate_binary(literal l) {
literal_vector const& lits = m_binary[l.index()]; literal_vector const& lits = m_binary[l.index()];
TRACE("sat", tout << l << " => " << lits << "\n";); TRACE("sat", tout << l << " => " << lits << "\n";);
for (literal l : lits) { for (literal lit : lits) {
if (inconsistent()) break; if (inconsistent()) break;
assign(l); assign(lit);
} }
} }
@ -1584,6 +1641,8 @@ namespace sat {
propagate_clauses(m_trail[m_qhead++]); propagate_clauses(m_trail[m_qhead++]);
} }
SASSERT(m_qhead == m_trail.size() || (inconsistent() && m_qhead < m_trail.size())); SASSERT(m_qhead == m_trail.size() || (inconsistent() && m_qhead < m_trail.size()));
//SASSERT(!missed_conflict());
//SASSERT(inconsistent() || !missed_propagation());
TRACE("sat_verbose", display(tout << scope_lvl() << " " << (inconsistent()?"unsat":"sat") << "\n");); TRACE("sat_verbose", display(tout << scope_lvl() << " " << (inconsistent()?"unsat":"sat") << "\n"););
} }
@ -1600,6 +1659,7 @@ namespace sat {
checkpoint(); checkpoint();
literal lit = m_lookahead[i].m_lit; literal lit = m_lookahead[i].m_lit;
if (lit == last_changed) { if (lit == last_changed) {
SASSERT(!change);
break; break;
} }
if (scope_lvl() == 1) { if (scope_lvl() == 1) {
@ -1812,6 +1872,7 @@ namespace sat {
lookahead_backtrack(); lookahead_backtrack();
assign(l); assign(l);
propagate(); propagate();
//SASSERT(!inconsistent());
unsigned old_sz = m_trail.size(); unsigned old_sz = m_trail.size();
bool change = true; bool change = true;
literal last_changed = null_literal; literal last_changed = null_literal;
@ -1847,6 +1908,7 @@ namespace sat {
propagate(); propagate();
change = true; change = true;
last_changed = lit; last_changed = lit;
m_wstack.push_back(~lit);
} }
} }
base += 2 * m_lookahead.size(); base += 2 * m_lookahead.size();

6
src/sat/sat_lookahead.h
View file

@ -90,7 +90,7 @@ namespace sat {
m_min_cutoff = 30; m_min_cutoff = 30;
m_preselect = false; m_preselect = false;
m_level_cand = 600; m_level_cand = 600;
m_delta_rho = (double)0.25; m_delta_rho = (double)0.85;
m_dl_max_iterations = 2; m_dl_max_iterations = 2;
m_tc1_limit = 10000000; m_tc1_limit = 10000000;
m_reward_type = ternary_reward; m_reward_type = ternary_reward;
@ -340,6 +340,8 @@ namespace sat {
std::ostream& display_candidates(std::ostream& out) const; std::ostream& display_candidates(std::ostream& out) const;
bool is_unsat() const; bool is_unsat() const;
bool is_sat() const; bool is_sat() const;
bool missed_propagation() const;
bool missed_conflict() const;
void init_pre_selection(unsigned level); void init_pre_selection(unsigned level);
void ensure_H(unsigned level); void ensure_H(unsigned level);
void h_scores(svector<double>& h, svector<double>& hp); void h_scores(svector<double>& h, svector<double>& hp);
@ -503,7 +505,7 @@ namespace sat {
unsigned do_double(literal l, unsigned& base); unsigned do_double(literal l, unsigned& base);
unsigned double_look(literal l, unsigned& base); unsigned double_look(literal l, unsigned& base);
void set_conflict() { TRACE("sat", tout << "conflict\n";); m_inconsistent = true; } void set_conflict() { TRACE("sat", tout << "conflict\n";); m_inconsistent = true; }
bool inconsistent() { return m_inconsistent; } bool inconsistent() const { return m_inconsistent; }
unsigned scope_lvl() const { return m_trail_lim.size(); } unsigned scope_lvl() const { return m_trail_lim.size(); }