From cf2512ce90ddaf482f317258b9e227d8b04f1a43 Mon Sep 17 00:00:00 2001 From: Miguel Neves Date: Tue, 17 Oct 2017 16:03:58 -0700 Subject: [PATCH 1/3] Added literal promotion --- src/sat/sat_lookahead.cpp | 26 +++++++++++++++++++++++--- src/sat/sat_lookahead.h | 2 ++ 2 files changed, 25 insertions(+), 3 deletions(-) diff --git a/src/sat/sat_lookahead.cpp b/src/sat/sat_lookahead.cpp index edb881aa4..bdc856fb3 100644 --- a/src/sat/sat_lookahead.cpp +++ b/src/sat/sat_lookahead.cpp @@ -1144,6 +1144,18 @@ namespace sat { SASSERT(m_trail_lim.empty() || m_trail.size() >= m_trail_lim.back()); } + void lookahead::promote(unsigned base) { + if (m_trail.empty()) return; + unsigned last_lvl = get_level(m_trail.back()); + base -= last_lvl; + for (unsigned i = m_trail.size(); i > 0; ) { + literal lit = m_trail[--i]; + if (is_fixed_at(lit, c_fixed_truth)) break; + SASSERT(is_fixed_at(lit, last_lvl)); + m_stamp[lit.var()] += base; + } + } + // // The current version is modeled after CDCL SAT solving data-structures. // It borrows from the watch list data-structure. The cost tradeoffs are somewhat @@ -1680,6 +1692,8 @@ namespace sat { num_units += do_double(lit, dl_lvl); if (dl_lvl > level) { base = dl_lvl; + promote(base + m_lookahead[i].m_offset); + SASSERT(get_level(m_trail.back()) == base + m_lookahead[i].m_offset); } unsat = inconsistent(); pop_lookahead1(lit, num_units); @@ -1867,11 +1881,14 @@ namespace sat { SASSERT(dl_no_overflow(base)); base += m_lookahead.size(); unsigned dl_truth = base + m_lookahead.size() * m_config.m_dl_max_iterations; + promote(dl_truth); scoped_level _sl(*this, dl_truth); + SASSERT(get_level(m_trail.back()) == dl_truth); + SASSERT(is_fixed(l)); IF_VERBOSE(2, verbose_stream() << "double: " << l << " depth: " << m_trail_lim.size() << "\n";); - lookahead_backtrack(); - assign(l); - propagate(); + //lookahead_backtrack(); + //assign(l); + //propagate(); //SASSERT(!inconsistent()); unsigned old_sz = m_trail.size(); bool change = true; @@ -1914,6 +1931,8 @@ namespace sat { base += 2 * m_lookahead.size(); SASSERT(dl_truth >= base); } + lookahead_backtrack(); + SASSERT(get_level(m_trail.back()) == dl_truth); SASSERT(m_level == dl_truth); base = dl_truth; return m_trail.size() - old_sz; @@ -1932,6 +1951,7 @@ namespace sat { if (is_undef(l)) { TRACE("sat", tout << "assign: " << l << " @ " << m_level << " " << m_trail_lim.size() << " " << m_search_mode << "\n";); set_true(l); + SASSERT(m_trail.empty() || get_level(m_trail.back()) >= get_level(l)); m_trail.push_back(l); if (m_search_mode == lookahead_mode::searching) { m_stats.m_propagations++; diff --git a/src/sat/sat_lookahead.h b/src/sat/sat_lookahead.h index d30485254..8420ae1f5 100644 --- a/src/sat/sat_lookahead.h +++ b/src/sat/sat_lookahead.h @@ -246,6 +246,7 @@ namespace sat { inline bool is_true(literal l) const { return is_true_at(l, m_level); } inline void set_true(literal l) { m_stamp[l.var()] = m_level + l.sign(); } inline void set_undef(literal l) { m_stamp[l.var()] = 0; } + inline unsigned get_level(literal l) { return m_stamp[l.var()] & UINT_MAX - 1; } void set_level(literal d, literal s) { m_stamp[d.var()] = (m_stamp[s.var()] & ~0x1) + d.sign(); } lbool value(literal l) const { return is_undef(l) ? l_undef : is_true(l) ? l_true : l_false; } @@ -479,6 +480,7 @@ namespace sat { unsigned push_lookahead1(literal lit, unsigned level); void pop_lookahead1(literal lit, unsigned num_units); void lookahead_backtrack(); + void promote(unsigned base); double mix_diff(double l, double r) const; clause const& get_clause(watch_list::iterator it) const; bool is_nary_propagation(clause const& c, literal l) const; From ba6b024ac4d1d54574b5e92450dea4f29598a004 Mon Sep 17 00:00:00 2001 From: Miguel Neves Date: Thu, 19 Oct 2017 19:52:56 -0700 Subject: [PATCH 2/3] Reverted to March_CU like lookahead --- src/sat/sat_lookahead.cpp | 45 ++++++++++++++++++++++----------------- src/sat/sat_lookahead.h | 5 ++--- 2 files changed, 27 insertions(+), 23 deletions(-) diff --git a/src/sat/sat_lookahead.cpp b/src/sat/sat_lookahead.cpp index bdc856fb3..7e9e2d230 100644 --- a/src/sat/sat_lookahead.cpp +++ b/src/sat/sat_lookahead.cpp @@ -340,6 +340,13 @@ namespace sat { } bool lookahead::is_unsat() const { + for (unsigned idx = 0; idx < m_binary.size(); ++idx) { + literal l = to_literal(idx); + for (literal lit : m_binary[idx]) { + if (is_true(l) && is_false(lit)) + return true; + } + } // check if there is a clause whose literals are false. // every clause is terminated by a null-literal. for (nary* n : m_nary_clauses) { @@ -432,8 +439,21 @@ namespace sat { bool lookahead::missed_conflict() const { if (inconsistent()) return false; + for (literal l1 : m_trail) { + for (literal l2 : m_binary[l1.index()]) { + if (is_false(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_false(b.m_v))) + return true; + } + } for (nary * n : m_nary_clauses) { - if (n->size() == 0) return true; + if (n->size() == 0) + return true; } return false; } @@ -1144,18 +1164,6 @@ namespace sat { SASSERT(m_trail_lim.empty() || m_trail.size() >= m_trail_lim.back()); } - void lookahead::promote(unsigned base) { - if (m_trail.empty()) return; - unsigned last_lvl = get_level(m_trail.back()); - base -= last_lvl; - for (unsigned i = m_trail.size(); i > 0; ) { - literal lit = m_trail[--i]; - if (is_fixed_at(lit, c_fixed_truth)) break; - SASSERT(is_fixed_at(lit, last_lvl)); - m_stamp[lit.var()] += base; - } - } - // // The current version is modeled after CDCL SAT solving data-structures. // It borrows from the watch list data-structure. The cost tradeoffs are somewhat @@ -1496,7 +1504,7 @@ namespace sat { 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()]) { + if (get_level(l) > get_level(n->get_head())) { n->set_head(l); } } @@ -1692,7 +1700,6 @@ namespace sat { num_units += do_double(lit, dl_lvl); if (dl_lvl > level) { base = dl_lvl; - promote(base + m_lookahead[i].m_offset); SASSERT(get_level(m_trail.back()) == base + m_lookahead[i].m_offset); } unsat = inconsistent(); @@ -1881,15 +1888,13 @@ namespace sat { SASSERT(dl_no_overflow(base)); base += m_lookahead.size(); unsigned dl_truth = base + m_lookahead.size() * m_config.m_dl_max_iterations; - promote(dl_truth); scoped_level _sl(*this, dl_truth); SASSERT(get_level(m_trail.back()) == dl_truth); SASSERT(is_fixed(l)); IF_VERBOSE(2, verbose_stream() << "double: " << l << " depth: " << m_trail_lim.size() << "\n";); - //lookahead_backtrack(); - //assign(l); - //propagate(); - //SASSERT(!inconsistent()); + lookahead_backtrack(); + assign(l); + propagate(); unsigned old_sz = m_trail.size(); bool change = true; literal last_changed = null_literal; diff --git a/src/sat/sat_lookahead.h b/src/sat/sat_lookahead.h index 8420ae1f5..e84213cfe 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.85; + m_delta_rho = (double)0.7; m_dl_max_iterations = 2; m_tc1_limit = 10000000; m_reward_type = ternary_reward; @@ -246,7 +246,7 @@ namespace sat { inline bool is_true(literal l) const { return is_true_at(l, m_level); } inline void set_true(literal l) { m_stamp[l.var()] = m_level + l.sign(); } inline void set_undef(literal l) { m_stamp[l.var()] = 0; } - inline unsigned get_level(literal l) { return m_stamp[l.var()] & UINT_MAX - 1; } + inline unsigned get_level(literal l) const { return m_stamp[l.var()] & UINT_MAX - 1; } void set_level(literal d, literal s) { m_stamp[d.var()] = (m_stamp[s.var()] & ~0x1) + d.sign(); } lbool value(literal l) const { return is_undef(l) ? l_undef : is_true(l) ? l_true : l_false; } @@ -480,7 +480,6 @@ namespace sat { unsigned push_lookahead1(literal lit, unsigned level); void pop_lookahead1(literal lit, unsigned num_units); void lookahead_backtrack(); - void promote(unsigned base); double mix_diff(double l, double r) const; clause const& get_clause(watch_list::iterator it) const; bool is_nary_propagation(clause const& c, literal l) const; From d58f42c821181ffe8e6798c1de4fe9ce87219b30 Mon Sep 17 00:00:00 2001 From: Miguel Neves Date: Thu, 19 Oct 2017 20:02:05 -0700 Subject: [PATCH 3/3] Merge --- src/sat/sat_lookahead.h | 1 - 1 file changed, 1 deletion(-) diff --git a/src/sat/sat_lookahead.h b/src/sat/sat_lookahead.h index f98a117c8..e84213cfe 100644 --- a/src/sat/sat_lookahead.h +++ b/src/sat/sat_lookahead.h @@ -248,7 +248,6 @@ namespace sat { inline void set_undef(literal l) { m_stamp[l.var()] = 0; } inline unsigned get_level(literal l) const { return m_stamp[l.var()] & UINT_MAX - 1; } void set_level(literal d, literal s) { m_stamp[d.var()] = (m_stamp[s.var()] & ~0x1) + d.sign(); } - unsigned get_level(literal d) const { return m_stamp[d.var()]; } lbool value(literal l) const { return is_undef(l) ? l_undef : is_true(l) ? l_true : l_false; } // set the level within a scope of the search.