From 806690571e06f12f21239dd8d68d1786ec9cec4e Mon Sep 17 00:00:00 2001 From: Miguel Neves Date: Tue, 17 Oct 2017 13:15:34 -0700 Subject: [PATCH] Lookahead clause size optimization. Fixed some missing propagations --- src/sat/sat_lookahead.cpp | 164 ++++++++++++++++++++++++++------------ src/sat/sat_lookahead.h | 6 +- 2 files changed, 117 insertions(+), 53 deletions(-) diff --git a/src/sat/sat_lookahead.cpp b/src/sat/sat_lookahead.cpp index f5d0910ab..edb881aa4 100644 --- a/src/sat/sat_lookahead.cpp +++ b/src/sat/sat_lookahead.cpp @@ -155,7 +155,7 @@ namespace sat { if (is_stamped(~w)) { // u \/ v, ~v \/ w, u \/ ~w => u is unit TRACE("sat", tout << "tc1: " << u << "\n";); - assign(u); + propagated(u); return false; } if (m_num_tc1 < m_config.m_tc1_limit) { @@ -181,14 +181,14 @@ namespace sat { set_bstamps(~u); if (is_stamped(~v)) { 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)) { // u \/ v is not in index set_bstamps(~v); if (is_stamped(~u)) { - TRACE("sat", tout << "try_add_binary: " << v << "\n";); - assign(v); // v \/ ~u, u \/ v => v is a unit literal + TRACE("sat", tout << "try_add_binary: " << v << "\n";); + propagated(v); // v \/ ~u, u \/ v => v is a unit literal } else if (add_tc1(v, u)) { update_prefix(u); @@ -407,6 +407,37 @@ namespace sat { 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) { switch (m_config.m_reward_type) { case ternary_reward: { @@ -1098,11 +1129,19 @@ namespace sat { } 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(); } 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) { if (is_fixed(l1)) { if (is_false(l1)) { - if (is_undef(l2)) { - propagated(l2); - } - else if (is_false(l2)) { + if (is_false(l2)) { TRACE("sat", tout << l1 << " " << l2 << " " << "\n";); set_conflict(); + return l_false; } - return l_false; + else if (is_undef(l2)) { + propagated(l2); + } + return l_true; } else { return l_true; @@ -1298,10 +1338,11 @@ namespace sat { unsigned sz = m_nary_count[(~l).index()]; literal lit; 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; 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 // find the two unassigned literals, if any if (len == 2) { @@ -1357,53 +1398,35 @@ namespace sat { void lookahead::propagate_clauses_lookahead(literal l) { // clauses where l is negative unsigned sz = m_nary_count[(~l).index()]; - literal lit; SASSERT(m_search_mode == lookahead_mode::lookahead1 || m_search_mode == lookahead_mode::lookahead2); for (nary* n : m_nary[(~l).index()]) { if (sz-- == 0) break; - - if (is_true(n->get_head())) { - continue; - } - literal l1 = null_literal; - literal l2 = null_literal; - bool skip_clause = false; - unsigned nonfixed = 0; - for (literal lit : *n) { - if (!is_fixed(lit)) { - ++nonfixed; - if (l1 == null_literal) { - l1 = lit; - } - else if (l2 == null_literal) { - l2 = lit; + unsigned nonfixed = n->dec_size(); + if (is_true(n->get_head())) continue; + if (inconsistent()) continue; + if (nonfixed <= 1) { + bool found_conflict = true; + for (literal lit : *n) { + if (!is_fixed(lit)) { + propagated(lit); + found_conflict = false; + break; } - else if (m_search_mode == lookahead_mode::lookahead2) { - skip_clause = true; + else if (is_true(lit)) { + n->set_head(lit); + found_conflict = false; break; } } - else if (is_true(lit)) { - n->set_head(lit); - skip_clause = true; - break; + if (found_conflict) { + set_conflict(); + continue; } } - if (skip_clause) { - // skip, the clause - } - else if (l1 == null_literal) { - set_conflict(); - return; - } - else if (l2 == null_literal) { - propagated(l1); - } - else { + else if (m_search_mode == lookahead_mode::lookahead1) { SASSERT(nonfixed >= 2); - SASSERT(m_search_mode == lookahead_mode::lookahead1); switch (m_config.m_reward_type) { case heule_schur_reward: { double to_add = 0; @@ -1418,9 +1441,35 @@ namespace sat { case heule_unit_reward: m_lookahead_reward += pow(0.5, nonfixed); break; + case march_cu_reward: + m_lookahead_reward += 3.3 * pow(0.5, nonfixed - 2); + break; case ternary_reward: 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 { 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) { @@ -1567,9 +1624,9 @@ namespace sat { void lookahead::propagate_binary(literal l) { literal_vector const& lits = m_binary[l.index()]; TRACE("sat", tout << l << " => " << lits << "\n";); - for (literal l : lits) { + for (literal lit : lits) { if (inconsistent()) break; - assign(l); + assign(lit); } } @@ -1584,6 +1641,8 @@ namespace sat { propagate_clauses(m_trail[m_qhead++]); } 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");); } @@ -1600,6 +1659,7 @@ namespace sat { checkpoint(); literal lit = m_lookahead[i].m_lit; if (lit == last_changed) { + SASSERT(!change); break; } if (scope_lvl() == 1) { @@ -1812,6 +1872,7 @@ namespace sat { lookahead_backtrack(); assign(l); propagate(); + //SASSERT(!inconsistent()); unsigned old_sz = m_trail.size(); bool change = true; literal last_changed = null_literal; @@ -1847,6 +1908,7 @@ namespace sat { propagate(); change = true; last_changed = lit; + m_wstack.push_back(~lit); } } base += 2 * m_lookahead.size(); diff --git a/src/sat/sat_lookahead.h b/src/sat/sat_lookahead.h index c9ce7d946..d30485254 100644 --- a/src/sat/sat_lookahead.h +++ b/src/sat/sat_lookahead.h @@ -90,7 +90,7 @@ namespace sat { m_min_cutoff = 30; m_preselect = false; m_level_cand = 600; - m_delta_rho = (double)0.25; + m_delta_rho = (double)0.85; m_dl_max_iterations = 2; m_tc1_limit = 10000000; m_reward_type = ternary_reward; @@ -340,6 +340,8 @@ namespace sat { std::ostream& display_candidates(std::ostream& out) const; bool is_unsat() const; bool is_sat() const; + bool missed_propagation() const; + bool missed_conflict() const; void init_pre_selection(unsigned level); void ensure_H(unsigned level); void h_scores(svector& h, svector& hp); @@ -503,7 +505,7 @@ namespace sat { unsigned do_double(literal l, unsigned& base); unsigned double_look(literal l, unsigned& base); 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(); }