diff --git a/src/opt/opt_context.cpp b/src/opt/opt_context.cpp index 1396ae9c4..33aaa0b27 100644 --- a/src/opt/opt_context.cpp +++ b/src/opt/opt_context.cpp @@ -1436,6 +1436,9 @@ namespace opt { if (m_solver) { m_solver->updt_params(m_params); } + if (m_sat_solver) { + m_sat_solver->updt_params(m_params); + } m_optsmt.updt_params(m_params); for (auto & kv : m_maxsmts) { kv.m_value->updt_params(m_params); diff --git a/src/opt/opt_lns.cpp b/src/opt/opt_lns.cpp index 1fc6913e4..d5038dc29 100644 --- a/src/opt/opt_lns.cpp +++ b/src/opt/opt_lns.cpp @@ -14,11 +14,9 @@ Author: Nikolaj Bjorner (nbjorner) 2018-3-13 -Notes: - - --*/ +#include "ast/ast_pp.h" #include "opt/opt_lns.h" #include "opt/opt_context.h" @@ -36,12 +34,12 @@ namespace opt { void lns::display(std::ostream & out) const { for (auto const& q : m_queue) { - out << q.m_index << ": " << q.m_assignment << "\n"; + expr_ref tmp(mk_and(q.m_assignment)); + out << q.m_index << ": " << tmp << "\n"; } } lbool lns::operator()() { - if (m_queue.empty()) { expr_ref_vector lits(m), atoms(m); m_ctx.get_lns_literals(lits); @@ -60,8 +58,7 @@ namespace opt { } params_ref p; - p.set_uint("sat.inprocess.max", 3); - p.set_uint("smt.max_conflicts", 10000); + p.set_uint("inprocess.max", 3ul); m_solver->updt_params(p); while (m_qhead < m_queue.size()) { @@ -71,13 +68,20 @@ namespace opt { } unsigned& index = m_queue[m_qhead].m_index; expr* lit = nullptr; - for (; index < m_atoms.size() && (lit = m_atoms[index].get(), (atoms.contains(lit) || m_units.contains(lit))); ++index) ; + for (; index < m_atoms.size(); ++index) { + lit = m_atoms[index].get(); + if (!atoms.contains(lit) && !m_failed.contains(lit)) break; + } if (index == m_atoms.size()) { m_qhead++; continue; } IF_VERBOSE(2, verbose_stream() << "(opt.lns :queue " << m_qhead << " :index " << index << ")\n"); + + p.set_uint("local_search_threads", 0); + p.set_uint("unit_walk_threads", 0); + m_solver->updt_params(p); // recalibrate state to an initial satisfying assignment lbool is_sat = m_solver->check_sat(m_queue[m_qhead].m_assignment); @@ -86,22 +90,27 @@ namespace opt { return l_undef; } - expr* lit = m_atoms[index].get(); expr_ref_vector lits(m); lits.push_back(lit); ++index; - // Update configuration for local search: - // p.set_uint("sat.local_search_threads", 2); - // p.set_uint("sat.unit_walk_threads", 1); - + // freeze phase in both SAT solver and local search to current assignment + p.set_uint("inprocess.max", 3); + p.set_bool("phase.sticky", true); + p.set_uint("local_search_threads", 1); + p.set_uint("max_conflicts", 100000); + p.set_uint("unit_walk_threads", 1); + m_solver->updt_params(p); + is_sat = m_solver->check_sat(lits); - IF_VERBOSE(2, verbose_stream() << "(opt.lns :lookahead-status " << is_sat << " " << lit << ")\n"); + IF_VERBOSE(2, verbose_stream() << "(opt.lns :lookahead-status " << is_sat << " " << mk_pp(lit, m) << ")\n"); if (is_sat == l_true && add_assignment()) { return l_true; } if (is_sat == l_false) { - m_units.insert(lit); + m_failed.insert(lit); + expr_ref nlit(m.mk_not(lit), m); + m_solver->assert_expr(nlit); } if (!m.limit().inc()) { return l_undef; diff --git a/src/opt/opt_lns.h b/src/opt/opt_lns.h index 29c2adc90..827df3081 100644 --- a/src/opt/opt_lns.h +++ b/src/opt/opt_lns.h @@ -46,7 +46,7 @@ namespace opt { expr_ref_vector m_models_trail; expr_ref_vector m_atoms; obj_hashtable m_models; - obj_hashtable m_fixed; + obj_hashtable m_failed; bool add_assignment(); public: diff --git a/src/sat/sat_config.cpp b/src/sat/sat_config.cpp index c37312ae7..2439be36f 100644 --- a/src/sat/sat_config.cpp +++ b/src/sat/sat_config.cpp @@ -55,6 +55,7 @@ namespace sat { m_phase_caching_on = p.phase_caching_on(); m_phase_caching_off = p.phase_caching_off(); + m_phase_sticky = p.phase_sticky(); m_restart_initial = p.restart_initial(); m_restart_factor = p.restart_factor(); diff --git a/src/sat/sat_config.h b/src/sat/sat_config.h index b42761f4b..c70d52a90 100644 --- a/src/sat/sat_config.h +++ b/src/sat/sat_config.h @@ -83,6 +83,7 @@ namespace sat { phase_selection m_phase; unsigned m_phase_caching_on; unsigned m_phase_caching_off; + bool m_phase_sticky; restart_strategy m_restart; unsigned m_restart_initial; double m_restart_factor; // for geometric case diff --git a/src/sat/sat_local_search.cpp b/src/sat/sat_local_search.cpp index 1b5f09e4d..5c2425578 100644 --- a/src/sat/sat_local_search.cpp +++ b/src/sat/sat_local_search.cpp @@ -34,8 +34,13 @@ namespace sat { // add sentinel variable. m_vars.push_back(var_info()); - for (unsigned v = 0; v < num_vars(); ++v) { - m_vars[v].m_value = (0 == (m_rand() % 2)); + if (m_config.phase_sticky()) { + for (var_info& vi : m_vars) + vi.m_value = vi.m_bias < 100; + } + else { + for (var_info& vi : m_vars) + vi.m_value = (0 == (m_rand() % 2)); } m_best_solution.resize(num_vars() + 1, false); @@ -70,13 +75,14 @@ namespace sat { } void local_search::init_cur_solution() { - for (unsigned v = 0; v < num_vars(); ++v) { + IF_VERBOSE(1, verbose_stream() << "(sat.local_search init-cur-solution)\n"); + for (var_info& vi : m_vars) { // use bias with a small probability - if (m_rand() % 10 < 5) { - m_vars[v].m_value = ((unsigned)(m_rand() % 100) < m_vars[v].m_bias); + if (m_rand() % 10 < 5 || m_config.phase_sticky()) { + vi.m_value = ((unsigned)(m_rand() % 100) < vi.m_bias); } else { - m_vars[v].m_value = (m_rand() % 2) == 0; + vi.m_value = (m_rand() % 2) == 0; } } } @@ -189,8 +195,15 @@ namespace sat { init_slack(); init_scores(); init_goodvars(); + set_best_unsat(); + } + void local_search::set_best_unsat() { m_best_unsat = m_unsat_stack.size(); + if (m_best_unsat == 1) { + constraint const& c = m_constraints[m_unsat_stack[0]]; + IF_VERBOSE(2, display(verbose_stream() << "single unsat:", c)); + } } void local_search::calculate_and_update_ob() { @@ -275,7 +288,9 @@ namespace sat { m_constraints.back().push(t); } if (sz == 1 && k == 0) { - m_vars[c[0].var()].m_bias = c[0].sign() ? 0 : 100; + literal lit = c[0]; + m_vars[lit.var()].m_bias = lit.sign() ? 100 : 0; + m_vars[lit.var()].m_value = lit.sign(); } } @@ -289,8 +304,10 @@ namespace sat { m_vars[t.var()].m_watch[is_pos(t)].push_back(pbcoeff(id, coeffs[i])); m_constraints.back().push(t); } - if (sz == 1 && k == 0) { - m_vars[c[0].var()].m_bias = c[0].sign() ? 0 : 100; + if (sz == 1 && k == 0) { + literal lit = c[0]; + m_vars[lit.var()].m_bias = lit.sign() ? 100 : 0; + m_vars[lit.var()].m_value = lit.sign(); } } @@ -304,6 +321,14 @@ namespace sat { m_constraints.reset(); m_vars.reserve(s.num_vars()); + if (m_config.phase_sticky()) { + unsigned v = 0; + for (var_info& vi : m_vars) { + if (vi.m_bias != 0 && vi.m_bias != 100) + vi.m_bias = s.m_phase[v] == POS_PHASE ? 100 : 0; + ++v; + } + } // copy units unsigned trail_sz = s.init_trail_size(); @@ -462,7 +487,7 @@ namespace sat { for (step = 0; step < m_max_steps && !m_unsat_stack.empty(); ++step) { pick_flip_walksat(); if (m_unsat_stack.size() < m_best_unsat) { - m_best_unsat = m_unsat_stack.size(); + set_best_unsat(); m_last_best_unsat_rate = m_best_unsat_rate; m_best_unsat_rate = (double)m_unsat_stack.size() / num_constraints(); } @@ -497,7 +522,7 @@ namespace sat { } } if (m_unsat_stack.size() < m_best_unsat) { - m_best_unsat = m_unsat_stack.size(); + set_best_unsat(); } flipvar = pick_var_gsat(); flip_gsat(flipvar); @@ -876,10 +901,7 @@ namespace sat { } void local_search::set_parameters() { - SASSERT(s_id == 0); - m_rand.set_seed(m_config.seed()); - //srand(m_config.seed()); - s_id = m_config.strategy_id(); + m_rand.set_seed(m_config.random_seed()); m_best_known_value = m_config.best_known_value(); switch (m_config.mode()) { diff --git a/src/sat/sat_local_search.h b/src/sat/sat_local_search.h index 475bd5f25..0f9bc95d7 100644 --- a/src/sat/sat_local_search.h +++ b/src/sat/sat_local_search.h @@ -29,27 +29,31 @@ namespace sat { class parallel; class local_search_config { - unsigned m_seed; - unsigned m_strategy_id; - int m_best_known_value; + unsigned m_random_seed; + int m_best_known_value; local_search_mode m_mode; + bool m_phase_sticky; public: local_search_config() { - m_seed = 0; - m_strategy_id = 0; + m_random_seed = 0; m_best_known_value = INT_MAX; m_mode = local_search_mode::wsat; + m_phase_sticky = false; } - unsigned seed() const { return m_seed; } - unsigned strategy_id() const { return m_strategy_id; } + unsigned random_seed() const { return m_random_seed; } unsigned best_known_value() const { return m_best_known_value; } local_search_mode mode() const { return m_mode; } - - void set_seed(unsigned s) { m_seed = s; } - void set_strategy_id(unsigned i) { m_strategy_id = i; } + bool phase_sticky() const { return m_phase_sticky; } + + void set_random_seed(unsigned s) { m_random_seed = s; } void set_best_known_value(unsigned v) { m_best_known_value = v; } - void set_mode(local_search_mode m) { m_mode = m; } + + void set_config(config const& cfg) { + m_mode = cfg.m_local_search_mode; + m_random_seed = cfg.m_random_seed; + m_phase_sticky = cfg.m_phase_sticky; + } }; @@ -75,6 +79,7 @@ namespace sat { bool m_value; // current solution unsigned m_bias; // bias for current solution in percentage. // if bias is 0, then value is always false, if 100, then always true + // lbool m_unit; // if l_true, then unit atom, if l_false, then unit negative literal bool m_conf_change; // whether its configure changes since its last flip bool m_in_goodvar_stack; int m_score; @@ -135,6 +140,7 @@ namespace sat { inline bool cur_solution(bool_var v) const { return m_vars[v].m_value; } + inline void set_best_unsat(); /* TBD: other scores */ @@ -179,9 +185,6 @@ namespace sat { double m_noise = 9800; // normalized by 10000 double m_noise_delta = 0.05; - // for tuning - int s_id = 0; // strategy id - reslimit m_limit; random_gen m_rand; parallel* m_par; diff --git a/src/sat/sat_params.pyg b/src/sat/sat_params.pyg index 7f6d1f718..850a33cef 100644 --- a/src/sat/sat_params.pyg +++ b/src/sat/sat_params.pyg @@ -5,6 +5,7 @@ def_module_params('sat', ('phase', SYMBOL, 'caching', 'phase selection strategy: always_false, always_true, caching, random'), ('phase.caching.on', UINT, 400, 'phase caching on period (in number of conflicts)'), ('phase.caching.off', UINT, 100, 'phase caching off period (in number of conflicts)'), + ('phase.sticky', BOOL, False, 'use sticky phase caching for local search'), ('restart', SYMBOL, 'luby', 'restart strategy: luby or geometric'), ('restart.initial', UINT, 100, 'initial restart (number of conflicts)'), ('restart.max', UINT, UINT_MAX, 'maximal number of restarts.'), diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp index 192951cba..3dff97875 100644 --- a/src/sat/sat_solver.cpp +++ b/src/sat/sat_solver.cpp @@ -1030,8 +1030,7 @@ namespace sat { lbool solver::do_local_search(unsigned num_lits, literal const* lits) { scoped_limits scoped_rl(rlimit()); local_search srch; - srch.config().set_seed(m_config.m_random_seed); - srch.config().set_mode(m_config.m_local_search_mode); + srch.config().set_config(m_config); srch.import(*this, false); scoped_rl.push_child(&srch.rlimit()); lbool r = srch.check(num_lits, lits, 0); @@ -1055,8 +1054,8 @@ namespace sat { int num_threads = num_extra_solvers + 1 + num_local_search + num_unit_walk; for (int i = 0; i < num_local_search; ++i) { local_search* l = alloc(local_search); - l->config().set_seed(m_config.m_random_seed + i); - l->config().set_mode(m_config.m_local_search_mode); + l->config().set_config(m_config); + l->config().set_random_seed(m_config.m_random_seed + i); l->import(*this, false); ls.push_back(l); } @@ -1277,10 +1276,12 @@ namespace sat { phase = l_false; break; case PS_CACHING: - if (m_phase_cache_on && m_phase[next] != PHASE_NOT_AVAILABLE) + if ((m_phase_cache_on || m_config.m_phase_sticky) && m_phase[next] != PHASE_NOT_AVAILABLE) { phase = m_phase[next] == POS_PHASE ? l_true : l_false; - else + } + else { phase = l_false; + } break; case PS_RANDOM: phase = to_lbool((m_rand() % 2) == 0); @@ -1486,7 +1487,7 @@ namespace sat { void solver::init_search() { m_model_is_current = false; m_phase_counter = 0; - m_phase_cache_on = false; + m_phase_cache_on = m_config.m_phase_sticky; m_conflicts_since_restart = 0; m_restart_threshold = m_config.m_restart_initial; m_luby_idx = 1; @@ -1625,8 +1626,10 @@ namespace sat { unsigned num = num_vars(); m_model.resize(num, l_undef); for (bool_var v = 0; v < num; v++) { - if (!was_eliminated(v)) + if (!was_eliminated(v)) { m_model[v] = value(v); + m_phase[v] = (value(v) == l_true) ? POS_PHASE : NEG_PHASE; + } } TRACE("sat_mc_bug", m_mc.display(tout);); diff --git a/src/sat/sat_unit_walk.cpp b/src/sat/sat_unit_walk.cpp index 7d556c740..4a3cda47c 100644 --- a/src/sat/sat_unit_walk.cpp +++ b/src/sat/sat_unit_walk.cpp @@ -43,9 +43,9 @@ namespace sat { m_runs = 0; m_periods = 0; m_max_runs = UINT_MAX; - m_max_periods = 100; // 5000; // UINT_MAX; // TBD configure + m_max_periods = 5000; // UINT_MAX; // TBD configure m_max_conflicts = 100; - m_sticky_phase = true; + m_sticky_phase = s.get_config().m_phase_sticky; m_flips = 0; } @@ -124,7 +124,15 @@ namespace sat { m_max_trail = 0; if (m_sticky_phase) { for (bool_var v : m_freevars) { - m_phase[v] = m_rand(100 * static_cast(m_phase_tf[v].t + m_phase_tf[v].f)) <= 100 * m_phase_tf[v].t; + if (s.m_phase[v] == POS_PHASE) { + m_phase[v] = true; + } + else if (s.m_phase[v] == NEG_PHASE) { + m_phase[v] = false; + } + else { + m_phase[v] = m_rand(100 * static_cast(m_phase_tf[v].t + m_phase_tf[v].f)) <= 100 * m_phase_tf[v].t; + } } } else { diff --git a/src/util/params.cpp b/src/util/params.cpp index 081b75aee..75dd91129 100644 --- a/src/util/params.cpp +++ b/src/util/params.cpp @@ -323,7 +323,6 @@ class params { typedef std::pair entry; svector m_entries; unsigned m_ref_count; - void del_value(entry & e); void del_values();