From f7e14b32839bf76e470bcc775d36bc8fc121c134 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 14 Nov 2017 18:19:21 -0800 Subject: [PATCH] add global autarky option, update translation of solvers to retain vsids, remove stale code Signed-off-by: Nikolaj Bjorner --- src/api/c++/z3++.h | 1 + src/sat/sat_config.cpp | 1 + src/sat/sat_config.h | 1 + src/sat/sat_lookahead.cpp | 77 ++++++++++++++++++++++++++------------- src/sat/sat_lookahead.h | 12 ++---- src/sat/sat_params.pyg | 1 + src/sat/sat_solver.cpp | 41 +++++++++------------ src/sat/sat_solver.h | 3 -- 8 files changed, 76 insertions(+), 61 deletions(-) diff --git a/src/api/c++/z3++.h b/src/api/c++/z3++.h index 558151b61..06c12741c 100644 --- a/src/api/c++/z3++.h +++ b/src/api/c++/z3++.h @@ -2117,6 +2117,7 @@ namespace z3 { return expr(ctx(), Z3_mk_and(ctx(), n, args.ptr())); } } + std::string dimacs() const { return std::string(Z3_goal_to_dimacs_string(ctx(), m_goal)); } friend std::ostream & operator<<(std::ostream & out, goal const & g); }; inline std::ostream & operator<<(std::ostream & out, goal const & g) { out << Z3_goal_to_string(g.ctx(), g); return out; } diff --git a/src/sat/sat_config.cpp b/src/sat/sat_config.cpp index 4dce25b99..e062841b7 100644 --- a/src/sat/sat_config.cpp +++ b/src/sat/sat_config.cpp @@ -112,6 +112,7 @@ namespace sat { m_lookahead_cube_fraction = p.lookahead_cube_fraction(); m_lookahead_cube_cutoff = p.lookahead_cube_cutoff(); + m_lookahead_global_autarky = p.lookahead_global_autarky(); // These parameters are not exposed m_simplify_mult1 = _p.get_uint("simplify_mult1", 300); diff --git a/src/sat/sat_config.h b/src/sat/sat_config.h index 6de1261ad..4fc1f4e7e 100644 --- a/src/sat/sat_config.h +++ b/src/sat/sat_config.h @@ -87,6 +87,7 @@ namespace sat { unsigned m_lookahead_cube_cutoff; double m_lookahead_cube_fraction; reward_t m_lookahead_reward; + bool m_lookahead_global_autarky; bool m_incremental; unsigned m_simplify_mult1; diff --git a/src/sat/sat_lookahead.cpp b/src/sat/sat_lookahead.cpp index 27d174653..d79aeffde 100644 --- a/src/sat/sat_lookahead.cpp +++ b/src/sat/sat_lookahead.cpp @@ -233,6 +233,7 @@ namespace sat { if (is_sat()) { return false; } + std::cout << "include newbies\n"; } SASSERT(!m_candidates.empty()); // cut number of candidates down to max_num_cand. @@ -314,12 +315,19 @@ namespace sat { double lookahead::init_candidates(unsigned level, bool newbies) { m_candidates.reset(); double sum = 0; + unsigned skip_candidates = 0; + bool autarky = get_config().m_lookahead_global_autarky; for (bool_var x : m_freevars) { SASSERT(is_undef(x)); if (!m_select_lookahead_vars.empty()) { if (m_select_lookahead_vars.contains(x)) { - m_candidates.push_back(candidate(x, m_rating[x])); - sum += m_rating[x]; + if (!autarky || newbies || in_reduced_clause(x)) { + m_candidates.push_back(candidate(x, m_rating[x])); + sum += m_rating[x]; + } + else { + skip_candidates++; + } } } else if (newbies || active_prefix(x)) { @@ -328,6 +336,9 @@ namespace sat { } } TRACE("sat", display_candidates(tout << "sum: " << sum << "\n");); + if (skip_candidates > 0) { + IF_VERBOSE(0, verbose_stream() << "candidates: " << m_candidates.size() << " skip: " << skip_candidates << "\n";); + } return sum; } @@ -1294,8 +1305,7 @@ namespace sat { unsigned idx = l.index(); unsigned sz = m_ternary_count[idx]--; auto& tv = m_ternary[idx]; - for (unsigned i = sz; i > 0; ) { - --i; + for (unsigned i = sz; i-- > 0; ) { binary const& b = tv[i]; if (b.m_u == u && b.m_v == v) { std::swap(tv[i], tv[sz-1]); @@ -1769,10 +1779,6 @@ namespace sat { 0 : get_lookahead_reward(p)); } - bool lookahead::check_autarky(literal l, unsigned level) { - return false; - } - void lookahead::update_lookahead_reward(literal l, unsigned level) { if (m_lookahead_reward != 0) { inc_lookahead_reward(l, m_lookahead_reward); @@ -1859,6 +1865,43 @@ namespace sat { return m_trail.size() - old_sz; } + /** + \brief check if literal occurs in a non-tautological reduced clause. + */ + bool lookahead::in_reduced_clause(bool_var v) { + return + in_reduced_clause(literal(v, false)) || + in_reduced_clause(literal(v, true)); + } + + bool lookahead::in_reduced_clause(literal lit) { + if (lit == null_literal) return true; + if (m_trail_lim.empty()) return true; + unsigned sz = m_nary_count[lit.index()]; + for (nary* n : m_nary[lit.index()]) { + if (sz-- == 0) break; + if (!n->is_reduced()) continue; + bool has_true = false; + for (literal l : *n) { + if (is_true(l)) { + has_true = true; + break; + } + } + if (!has_true) return true; + } + + auto const& tv = m_ternary[lit.index()]; + sz = tv.size(); + unsigned i = m_ternary_count[lit.index()]; + for (; i < sz; ++i) { + binary const& b = tv[i]; + if (!is_true(b.m_u) && !is_true(b.m_v)) + return true; + } + return false; + } + void lookahead::validate_assign(literal l) { if (m_s.m_config.m_drat && m_search_mode == lookahead_mode::searching) { m_assumptions.push_back(l); @@ -1959,20 +2002,6 @@ namespace sat { return true; } - lbool lookahead::cube() { - literal_vector lits; - bool_var_vector vars; - for (bool_var v : m_freevars) vars.push_back(v); - while (true) { - lbool result = cube(vars, lits, UINT_MAX); - if (lits.empty() || result != l_undef) { - return l_undef; - } - display_cube(std::cout, lits); - } - return l_undef; - } - lbool lookahead::cube(bool_var_vector const& vars, literal_vector& lits, unsigned backtrack_level) { scoped_ext _scoped_ext(*this); lits.reset(); @@ -2330,13 +2359,9 @@ namespace sat { // TBD: keep count of ternary and >3-ary clauses. st.update("lh add binary", m_stats.m_add_binary); st.update("lh del binary", m_stats.m_del_binary); - st.update("lh add ternary", m_stats.m_add_ternary); - st.update("lh del ternary", m_stats.m_del_ternary); st.update("lh propagations", m_stats.m_propagations); st.update("lh decisions", m_stats.m_decisions); st.update("lh windfalls", m_stats.m_windfall_binaries); - st.update("lh autarky propagations", m_stats.m_autarky_propagations); - st.update("lh autarky equivalences", m_stats.m_autarky_equivalences); st.update("lh double lookahead propagations", m_stats.m_double_lookahead_propagations); st.update("lh double lookahead rounds", m_stats.m_double_lookahead_rounds); } diff --git a/src/sat/sat_lookahead.h b/src/sat/sat_lookahead.h index 6cf75937f..9f110b1a0 100644 --- a/src/sat/sat_lookahead.h +++ b/src/sat/sat_lookahead.h @@ -115,12 +115,8 @@ namespace sat { unsigned m_propagations; unsigned m_add_binary; unsigned m_del_binary; - unsigned m_add_ternary; - unsigned m_del_ternary; unsigned m_decisions; unsigned m_windfall_binaries; - unsigned m_autarky_propagations; - unsigned m_autarky_equivalences; unsigned m_double_lookahead_propagations; unsigned m_double_lookahead_rounds; stats() { reset(); } @@ -151,9 +147,10 @@ namespace sat { } unsigned size() const { return m_size; } unsigned dec_size() { SASSERT(m_size > 0); return --m_size; } - void inc_size() { SASSERT(m_size < num_lits()); ++m_size; } + void inc_size() { SASSERT(is_reduced()); ++m_size; } literal get_head() const { return m_head; } void set_head(literal l) { m_head = l; } + bool is_reduced() const { return m_size < num_lits(); } literal operator[](unsigned i) { SASSERT(i < num_lits()); return m_literals[i]; } literal const* begin() const { return m_literals; } @@ -497,7 +494,6 @@ namespace sat { double get_lookahead_reward(literal l) const { return m_lits[l.index()].m_lookahead_reward; } void reset_lookahead_reward(literal l); - bool check_autarky(literal l, unsigned level); void update_lookahead_reward(literal l, unsigned level); bool dl_enabled(literal l) const { return m_lits[l.index()].m_double_lookahead != m_istamp_id; } void dl_disable(literal l) { m_lits[l.index()].m_double_lookahead = m_istamp_id; } @@ -510,6 +506,8 @@ namespace sat { unsigned scope_lvl() const { return m_trail_lim.size(); } + bool in_reduced_clause(literal l); + bool in_reduced_clause(bool_var v); void validate_assign(literal l); void assign(literal l); void propagated(literal l); @@ -565,8 +563,6 @@ namespace sat { Otherwise, cut-fraction gives an adaptive threshold for creating cuts. */ - lbool cube(); - lbool cube(bool_var_vector const& vars, literal_vector& lits, unsigned backtrack_level); literal select_lookahead(literal_vector const& assumptions, bool_var_vector const& vars); diff --git a/src/sat/sat_params.pyg b/src/sat/sat_params.pyg index 7b33ee8e7..bae1d0c11 100644 --- a/src/sat/sat_params.pyg +++ b/src/sat/sat_params.pyg @@ -41,6 +41,7 @@ def_module_params('sat', ('lookahead_search', BOOL, False, 'use lookahead solver'), ('lookahead.preselect', BOOL, False, 'use pre-selection of subset of variables for branching'), ('lookahead_simplify', BOOL, False, 'use lookahead solver during simplification'), + ('lookahead.global_autarky', BOOL, False, 'prefer to branch on variables that occur in clauses that are reduced'), ('lookahead.reward', SYMBOL, 'march_cu', 'select lookahead heuristic: ternary, heule_schur (Heule Schur), heuleu (Heule Unit), unit, or march_cu'), ('dimacs.inprocess.display', BOOL, False, 'display SAT instance in DIMACS format if unsolved after inprocess.max inprocessing passes'))) diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp index b0b5d8495..42b10d5c8 100644 --- a/src/sat/sat_solver.cpp +++ b/src/sat/sat_solver.cpp @@ -98,7 +98,12 @@ namespace sat { } m_phase[v] = src.m_phase[v]; m_prev_phase[v] = src.m_prev_phase[v]; - // m_activity[v] = src.m_activity[v], but then update case_split_queue ? + +#if 1 + // inherit activity: + m_activity[v] = src.m_activity[v]; + m_case_split_queue.activity_changed_eh(v, false); +#endif } } @@ -115,7 +120,7 @@ namespace sat { assign(src.m_trail[i], justification()); } - // copy binary clauses that are unblocked. + // copy binary clauses { unsigned sz = src.m_watches.size(); for (unsigned l_idx = 0; l_idx < sz; ++l_idx) { @@ -123,13 +128,21 @@ namespace sat { if (src.was_eliminated(l.var())) continue; watch_list const & wlist = src.m_watches[l_idx]; for (auto & wi : wlist) { - if (!wi.is_binary_unblocked_clause()) + if (!wi.is_binary_clause()) continue; literal l2 = wi.get_literal(); if (l.index() > l2.index() || src.was_eliminated(l2.var())) continue; - mk_clause_core(l, l2); + + watched w1(l2, wi.is_learned()); + watched w2(l, wi.is_learned()); + if (wi.is_blocked()) { + w1.set_blocked(); + w2.set_blocked(); + } + m_watches[(~l).index()].push_back(w1); + m_watches[(~l2).index()].push_back(w2); } } } @@ -868,12 +881,6 @@ namespace sat { if (m_config.m_lookahead_search && num_lits == 0) { return lookahead_search(); } -#if 0 - // deprecated - if (m_config.m_lookahead_cube && num_lits == 0) { - return lookahead_cube(); - } -#endif if (m_config.m_local_search) { return do_local_search(num_lits, lits); @@ -976,20 +983,6 @@ namespace sat { return r; } - lbool solver::lookahead_cube() { - lookahead lh(*this); - lbool r = l_undef; - try { - r = lh.cube(); - } - catch (z3_exception&) { - lh.collect_statistics(m_aux_stats); - throw; - } - lh.collect_statistics(m_aux_stats); - return r; - } - lbool solver::lookahead_search() { lookahead lh(*this); lbool r = l_undef; diff --git a/src/sat/sat_solver.h b/src/sat/sat_solver.h index cb8c2b763..45f91e7a8 100644 --- a/src/sat/sat_solver.h +++ b/src/sat/sat_solver.h @@ -180,7 +180,6 @@ namespace sat { friend class lookahead; friend class local_search; friend struct mk_stat; - friend class ccc; friend class elim_vars; friend class scoped_detach; public: @@ -395,9 +394,7 @@ namespace sat { void exchange_par(); lbool check_par(unsigned num_lits, literal const* lits); lbool lookahead_search(); - lbool lookahead_cube(); lbool do_local_search(unsigned num_lits, literal const* lits); - lbool do_ccc(); // ----------------------- //