From 4d911691181e5ccb236d14db879d6412e256a9d6 Mon Sep 17 00:00:00 2001 From: Miguel Neves Date: Fri, 6 Oct 2017 16:10:05 -0700 Subject: [PATCH 1/2] Cuber fixes. Added March_CU heuristics --- src/api/python/z3/z3.py | 2 +- src/sat/sat_config.cpp | 3 + src/sat/sat_config.h | 3 +- src/sat/sat_lookahead.cpp | 160 ++++++++++++++++++++++++++------------ src/sat/sat_lookahead.h | 17 +++- src/sat/sat_params.pyg | 4 +- 6 files changed, 130 insertions(+), 59 deletions(-) diff --git a/src/api/python/z3/z3.py b/src/api/python/z3/z3.py index 94221b3db..4379e3fe1 100644 --- a/src/api/python/z3/z3.py +++ b/src/api/python/z3/z3.py @@ -120,7 +120,7 @@ def _get_args(args): try: if len(args) == 1 and (isinstance(args[0], tuple) or isinstance(args[0], list)): return args[0] - elif len(args) == 1 and isinstance(args[0], set): + elif len(args) == 1 and (isinstance(args[0], set) or isinstance(args[0], AstVector)): return [arg for arg in args[0]] else: return args diff --git a/src/sat/sat_config.cpp b/src/sat/sat_config.cpp index 49a146489..c77774283 100644 --- a/src/sat/sat_config.cpp +++ b/src/sat/sat_config.cpp @@ -100,6 +100,9 @@ namespace sat { else if (p.lookahead_reward() == symbol("unit")) { m_lookahead_reward = unit_literal_reward; } + else if (p.lookahead_reward() == symbol("march_cu")) { + m_lookahead_reward = march_cu_reward; + } else { throw sat_param_exception("invalid reward type supplied: accepted heuristics are 'ternary', 'heuleu', 'unit' or 'heule_schur'"); } diff --git a/src/sat/sat_config.h b/src/sat/sat_config.h index a7c8590fb..214a93f5d 100644 --- a/src/sat/sat_config.h +++ b/src/sat/sat_config.h @@ -61,7 +61,8 @@ namespace sat { ternary_reward, unit_literal_reward, heule_schur_reward, - heule_unit_reward + heule_unit_reward, + march_cu_reward }; struct config { diff --git a/src/sat/sat_lookahead.cpp b/src/sat/sat_lookahead.cpp index 596b9abe7..59149ec0f 100644 --- a/src/sat/sat_lookahead.cpp +++ b/src/sat/sat_lookahead.cpp @@ -217,7 +217,7 @@ namespace sat { bool lookahead::select(unsigned level) { init_pre_selection(level); unsigned level_cand = std::max(m_config.m_level_cand, m_freevars.size() / 50); - unsigned max_num_cand = level == 0 ? m_freevars.size() : level_cand / level; + unsigned max_num_cand = (level > 0 && m_config.m_preselect) ? level_cand / level : m_freevars.size(); max_num_cand = std::max(m_config.m_min_cutoff, max_num_cand); double sum = 0; @@ -251,30 +251,40 @@ namespace sat { } TRACE("sat", display_candidates(tout);); SASSERT(!m_candidates.empty()); - if (m_candidates.size() > max_num_cand) { - unsigned j = m_candidates.size()/2; - while (j > 0) { - --j; - sift_up(j); - } - while (true) { - m_candidates[0] = m_candidates.back(); - m_candidates.pop_back(); - if (m_candidates.size() == max_num_cand) break; - sift_up(0); - } + heap_sort(); + while (m_candidates.size() > max_num_cand) { + m_candidates.pop_back(); } SASSERT(!m_candidates.empty() && m_candidates.size() <= max_num_cand); TRACE("sat", display_candidates(tout);); return true; } - void lookahead::sift_up(unsigned j) { + void lookahead::heap_sort() { + if (m_candidates.size() > 1) { + heapify(); + for (unsigned i = m_candidates.size() - 1; i > 0; --i) { + candidate c = m_candidates[i]; + m_candidates[i] = m_candidates[0]; + m_candidates[0] = c; + sift_down(0, i); + } + } + } + + void lookahead::heapify() { + unsigned i = 1 + (m_candidates.size() - 2) / 2; + while(i > 0) { + sift_down(--i, m_candidates.size()); + } + } + + void lookahead::sift_down(unsigned j, unsigned sz) { unsigned i = j; candidate c = m_candidates[j]; - for (unsigned k = 2*j + 1; k < m_candidates.size(); i = k, k = 2*k + 1) { - // pick largest parent - if (k + 1 < m_candidates.size() && m_candidates[k].m_rating < m_candidates[k+1].m_rating) { + for (unsigned k = 2 * j + 1; k < sz; i = k, k = 2 * k + 1) { + // pick smallest child + if (k + 1 < sz && m_candidates[k].m_rating > m_candidates[k + 1].m_rating) { ++k; } if (c.m_rating <= m_candidates[k].m_rating) break; @@ -432,6 +442,9 @@ namespace sat { case heule_unit_reward: heule_unit_scores(); break; + case march_cu_reward: + march_cu_scores(); + break; case unit_literal_reward: heule_schur_scores(); break; @@ -478,7 +491,7 @@ namespace sat { for (bool_var x : m_freevars) { literal l(x, false); m_rating[l.var()] = heule_unit_score(l) * heule_unit_score(~l); - } + } } double lookahead::heule_unit_score(literal l) { @@ -493,7 +506,23 @@ namespace sat { sum += pow(0.5, m_nary_literals[cls_idx]); } return sum; - } + } + + void lookahead::march_cu_scores() { + for (bool_var x : m_freevars) { + literal l(x, false); + double pos = march_cu_score(l), neg = march_cu_score(~l); + m_rating[l.var()] = 1024 * pos * neg + pos + neg + 1; + } + } + + double lookahead::march_cu_score(literal l) { + double sum = 1.0 + literal_big_occs(~l); + for (literal lit : m_binary[l.index()]) { + if (is_undef(lit)) sum += literal_big_occs(lit); + } + return sum; + } void lookahead::ensure_H(unsigned level) { while (m_H.size() <= level) { @@ -884,7 +913,7 @@ namespace sat { } void lookahead::init() { - m_delta_trigger = m_num_vars/10; + m_delta_trigger = 0.0; m_config.m_dl_success = 0.8; m_inconsistent = false; m_qhead = 0; @@ -1068,6 +1097,7 @@ namespace sat { m_lookahead_reward += num_units; break; case heule_unit_reward: + case march_cu_reward: case heule_schur_reward: break; default: @@ -1391,6 +1421,9 @@ 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()]; @@ -1486,6 +1519,9 @@ namespace sat { case heule_unit_reward: m_lookahead_reward += 0.25; break; + case march_cu_reward: + m_lookahead_reward += 3.3; + break; case unit_literal_reward: break; } @@ -1516,6 +1552,9 @@ namespace sat { case heule_unit_reward: m_lookahead_reward += pow(0.5, sz); break; + case march_cu_reward: + m_lookahead_reward += 3.3 * pow(0.5, sz - 2); + break; case ternary_reward: m_lookahead_reward = (double)0.001; break; @@ -1525,10 +1564,18 @@ namespace sat { } // Sum_{ clause C that contains ~l } 1 + // FIXME: counts occurences of ~l; misleading double lookahead::literal_occs(literal l) { double result = m_binary[l.index()].size(); - unsigned_vector const& nclauses = m_nary[(~l).index()]; - result += m_nary_count[(~l).index()]; + //unsigned_vector const& nclauses = m_nary[(~l).index()]; + result += literal_big_occs(l); + return result; + } + + // Sum_{ clause C that contains ~l such that |C| > 2} 1 + // FIXME: counts occurences of ~l; misleading + double lookahead::literal_big_occs(literal l) { + double result = m_nary_count[(~l).index()]; result += m_ternary_count[(~l).index()]; return result; } @@ -1542,22 +1589,19 @@ namespace sat { } } - void lookahead::propagate() { while (!inconsistent() && m_qhead < m_trail.size()) { unsigned i = m_qhead; - unsigned sz = m_trail.size(); - for (; i < sz && !inconsistent(); ++i) { + for (; i < m_trail.size() && !inconsistent(); ++i) { literal l = m_trail[i]; TRACE("sat", tout << "propagate " << l << " @ " << m_level << "\n";); propagate_binary(l); } - while (m_qhead < sz && !inconsistent()) { + while (m_qhead < m_trail.size() && !inconsistent()) { propagate_clauses(m_trail[m_qhead++]); } - SASSERT(m_qhead == sz || (inconsistent() && m_qhead < sz)); + SASSERT(m_qhead == m_trail.size() || (inconsistent() && m_qhead < m_trail.size())); } - TRACE("sat_verbose", display(tout << scope_lvl() << " " << (inconsistent()?"unsat":"sat") << "\n");); } @@ -1566,12 +1610,15 @@ namespace sat { TRACE("sat", display_lookahead(tout); ); unsigned base = 2; bool change = true; - bool first = true; + literal last_changed = null_literal; while (change && !inconsistent()) { change = false; for (unsigned i = 0; !inconsistent() && i < m_lookahead.size(); ++i) { checkpoint(); literal lit = m_lookahead[i].m_lit; + if (lit == last_changed) { + break; + } if (is_fixed_at(lit, c_fixed_truth)) continue; unsigned level = base + m_lookahead[i].m_offset; if (m_stamp[lit.var()] >= level) { @@ -1584,7 +1631,7 @@ namespace sat { unsigned old_trail_sz = m_trail.size(); reset_lookahead_reward(lit); push_lookahead1(lit, level); - if (!first) do_double(lit, base); + do_double(lit, base); bool unsat = inconsistent(); unsigned num_units = m_trail.size() - old_trail_sz; pop_lookahead1(lit, num_units); @@ -1595,6 +1642,7 @@ namespace sat { propagate(); init_lookahead_reward(); change = true; + last_changed = lit; } else { update_lookahead_reward(lit, level); @@ -1604,13 +1652,9 @@ namespace sat { if (c_fixed_truth - 2 * m_lookahead.size() < base) { break; } - if (first && !change) { - first = false; - change = true; - } reset_lookahead_reward(); init_lookahead_reward(); - // base += 2 * m_lookahead.size(); + base += 2 * m_lookahead.size(); } reset_lookahead_reward(); TRACE("sat", display_lookahead(tout); ); @@ -1664,6 +1708,7 @@ namespace sat { case ternary_reward: return l + r + (1 << 10) * l * r; case heule_schur_reward: return l * r; case heule_unit_reward: return l * r; + case march_cu_reward: return 1024 * (1024 * l * r + l + r); case unit_literal_reward: return l * r; default: UNREACHABLE(); return l * r; } @@ -1753,14 +1798,16 @@ namespace sat { } } - void lookahead::do_double(literal l, unsigned& base) { - if (!inconsistent() && scope_lvl() > 1 && dl_enabled(l)) { + void lookahead::do_double(literal l, unsigned& base) { + if (!inconsistent() && dl_enabled(l)) { if (get_lookahead_reward(l) > m_delta_trigger) { if (dl_no_overflow(base)) { ++m_stats.m_double_lookahead_rounds; double_look(l, base); - m_delta_trigger = get_lookahead_reward(l); - dl_disable(l); + if (!inconsistent()) { + m_delta_trigger = get_lookahead_reward(l); + dl_disable(l); + } } } else { @@ -1772,21 +1819,30 @@ namespace sat { void lookahead::double_look(literal l, unsigned& base) { SASSERT(!inconsistent()); SASSERT(dl_no_overflow(base)); - unsigned dl_truth = base + 2 * m_lookahead.size() * (m_config.m_dl_max_iterations + 1); + base += m_lookahead.size(); + unsigned dl_truth = base + m_lookahead.size() * m_config.m_dl_max_iterations; scoped_level _sl(*this, dl_truth); IF_VERBOSE(2, verbose_stream() << "double: " << l << " depth: " << m_trail_lim.size() << "\n";); init_lookahead_reward(); assign(l); propagate(); bool change = true; + literal last_changed = null_literal; unsigned num_iterations = 0; while (change && num_iterations < m_config.m_dl_max_iterations && !inconsistent()) { change = false; num_iterations++; - base += 2*m_lookahead.size(); for (unsigned i = 0; !inconsistent() && i < m_lookahead.size(); ++i) { literal lit = m_lookahead[i].m_lit; - if (is_fixed_at(lit, dl_truth)) continue; + if (lit == last_changed) { + SASSERT(change == false); + break; + } + if (is_fixed_at(lit, dl_truth)) continue; + if (base + m_lookahead.size() + m_lookahead[i].m_offset >= dl_truth) { + change = false; + break; + } if (push_lookahead2(lit, base + m_lookahead[i].m_offset)) { TRACE("sat", tout << "unit: " << ~lit << "\n";); ++m_stats.m_double_lookahead_propagations; @@ -1795,10 +1851,12 @@ namespace sat { assign(~lit); propagate(); change = true; + last_changed = lit; init_lookahead_reward(); } } - SASSERT(dl_truth - 2 * m_lookahead.size() > base); + base += 2 * m_lookahead.size(); + SASSERT(dl_truth >= base); } reset_lookahead_reward(); SASSERT(m_level == dl_truth); @@ -1838,14 +1896,13 @@ namespace sat { void lookahead::propagated(literal l) { assign(l); - switch (m_search_mode) { - case lookahead_mode::searching: - break; - case lookahead_mode::lookahead1: + for (unsigned i = m_trail.size() - 1; i < m_trail.size() && !inconsistent(); ++i) { + literal l = m_trail[i]; + TRACE("sat", tout << "propagate " << l << " @ " << m_level << "\n";); + propagate_binary(l); + } + if (m_search_mode == lookahead_mode::lookahead1) { m_wstack.push_back(l); - break; - case lookahead_mode::lookahead2: - break; } } @@ -1953,10 +2010,11 @@ namespace sat { backtrack(m_cube_state.m_cube, m_cube_state.m_is_decision); return l_undef; } + int prev_nfreevars = m_freevars.size(); literal lit = choose(); if (inconsistent()) { TRACE("sat", tout << "inconsistent: " << m_cube_state.m_cube << "\n";); - m_cube_state.m_freevars_threshold = m_freevars.size(); + m_cube_state.m_freevars_threshold = prev_nfreevars; if (!backtrack(m_cube_state.m_cube, m_cube_state.m_is_decision)) return l_false; continue; } diff --git a/src/sat/sat_lookahead.h b/src/sat/sat_lookahead.h index 9a50dceed..4011996bb 100644 --- a/src/sat/sat_lookahead.h +++ b/src/sat/sat_lookahead.h @@ -73,6 +73,7 @@ namespace sat { double m_max_score; unsigned m_max_hlevel; unsigned m_min_cutoff; + bool m_preselect; unsigned m_level_cand; double m_delta_rho; unsigned m_dl_max_iterations; @@ -86,9 +87,10 @@ namespace sat { m_alpha = 3.5; m_max_score = 20.0; m_min_cutoff = 30; + m_preselect = false; m_level_cand = 600; - m_delta_rho = (double)0.9995; - m_dl_max_iterations = 32; + m_delta_rho = (double)0.99995; + m_dl_max_iterations = 2; m_tc1_limit = 10000000; m_reward_type = ternary_reward; m_cube_cutoff = 0; @@ -289,7 +291,10 @@ namespace sat { double get_rating(bool_var v) const { return m_rating[v]; } double get_rating(literal l) const { return get_rating(l.var()); } bool select(unsigned level); - void sift_up(unsigned j); + //void sift_up(unsigned j); + void heap_sort(); + void heapify(); + void sift_down(unsigned j, unsigned sz); double init_candidates(unsigned level, bool newbies); std::ostream& display_candidates(std::ostream& out) const; bool is_unsat() const; @@ -301,6 +306,8 @@ namespace sat { double heule_schur_score(literal l); void heule_unit_scores(); double heule_unit_score(literal l); + void march_cu_scores(); + double march_cu_score(literal l); double l_score(literal l, svector const& h, double factor, double sqfactor, double afactor); // ------------------------------------ @@ -460,6 +467,7 @@ namespace sat { void do_double(literal l, unsigned& base); void 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";); printf("CONFLICT\n"); m_inconsistent = true; } bool inconsistent() { return m_inconsistent; } unsigned scope_lvl() const { return m_trail_lim.size(); } @@ -544,7 +552,8 @@ namespace sat { void collect_statistics(statistics& st) const; - double literal_occs(literal l); + double literal_occs(literal l); + double literal_big_occs(literal l); }; } diff --git a/src/sat/sat_params.pyg b/src/sat/sat_params.pyg index 01708b775..296c75180 100644 --- a/src/sat/sat_params.pyg +++ b/src/sat/sat_params.pyg @@ -31,7 +31,7 @@ def_module_params('sat', ('drat.check', BOOL, False, 'build up internal proof and check'), ('cardinality.solver', BOOL, False, 'use cardinality solver'), ('pb.solver', SYMBOL, 'circuit', 'method for handling Pseudo-Boolean constraints: circuit (arithmetical circuit), sorting (sorting circuit), totalizer (use totalizer encoding), solver (use SMT solver)'), - ('xor.solver', BOOL, False, 'use xor solver'), + ('xor.solver', BOOL, False, 'use xor solver'), ('atmost1_encoding', SYMBOL, 'grouped', 'encoding used for at-most-1 constraints grouped, bimander, ordered'), ('local_search_threads', UINT, 0, 'number of local search threads to find satisfiable solution'), ('local_search', BOOL, False, 'use local search instead of CDCL'), @@ -40,7 +40,7 @@ def_module_params('sat', ('lookahead.cube.cutoff', UINT, 0, 'cut-off depth to create cubes. Only enabled when non-zero. Used when lookahead_cube is true.'), ('lookahead_search', BOOL, False, 'use lookahead solver'), ('lookahead_simplify', BOOL, False, 'use lookahead solver during simplification'), - ('lookahead.reward', SYMBOL, 'heuleu', 'select lookahead heuristic: ternary, heule_schur (Heule Schur), heuleu (Heule Unit), or unit'), + ('lookahead.reward', SYMBOL, 'march_cu', 'select lookahead heuristic: ternary, heule_schur (Heule Schur), heuleu (Heule Unit), unit, or march_cu'), ('dimacs.display', BOOL, False, 'display SAT instance in DIMACS format and return unknown instead of solving'), ('dimacs.inprocess.display', BOOL, False, 'display SAT instance in DIMACS format if unsolved after inprocess.max inprocessing passes'))) From 01897831fb58de35c0202a1fbdfb71f0fa5f64b4 Mon Sep 17 00:00:00 2001 From: Miguel Neves Date: Tue, 10 Oct 2017 15:59:53 -0700 Subject: [PATCH 2/2] Dynamic delta trigger decrease --- src/sat/sat_lookahead.cpp | 5 ++++- src/sat/sat_lookahead.h | 5 +++-- 2 files changed, 7 insertions(+), 3 deletions(-) diff --git a/src/sat/sat_lookahead.cpp b/src/sat/sat_lookahead.cpp index 59149ec0f..63b013ca0 100644 --- a/src/sat/sat_lookahead.cpp +++ b/src/sat/sat_lookahead.cpp @@ -914,6 +914,7 @@ namespace sat { void lookahead::init() { m_delta_trigger = 0.0; + m_delta_decrease = 0.0; m_config.m_dl_success = 0.8; m_inconsistent = false; m_qhead = 0; @@ -1608,6 +1609,7 @@ namespace sat { void lookahead::compute_lookahead_reward() { init_lookahead_reward(); TRACE("sat", display_lookahead(tout); ); + m_delta_decrease = pow(m_config.m_delta_rho, 1.0 / (double)m_lookahead.size()); unsigned base = 2; bool change = true; literal last_changed = null_literal; @@ -1811,7 +1813,8 @@ namespace sat { } } else { - m_delta_trigger *= m_config.m_delta_rho; + SASSERT(m_delta_decrease > 0.0); + m_delta_trigger *= m_delta_decrease; } } } diff --git a/src/sat/sat_lookahead.h b/src/sat/sat_lookahead.h index 4011996bb..76f5437b5 100644 --- a/src/sat/sat_lookahead.h +++ b/src/sat/sat_lookahead.h @@ -89,7 +89,7 @@ namespace sat { m_min_cutoff = 30; m_preselect = false; m_level_cand = 600; - m_delta_rho = (double)0.99995; + m_delta_rho = (double)0.25; m_dl_max_iterations = 2; m_tc1_limit = 10000000; m_reward_type = ternary_reward; @@ -146,7 +146,8 @@ namespace sat { }; config m_config; - double m_delta_trigger; + double m_delta_trigger; + double m_delta_decrease; drat m_drat; literal_vector m_assumptions;