mirror of
https://github.com/Z3Prover/z3
synced 2025-04-27 19:05:51 +00:00
fixing local search
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner
parent
bf8ea92b99
commit
59b142f803
11 changed files with 107 additions and 57 deletions
|
|
@ -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);
|
||||
|
|
|
|||
|
|
@ -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;
|
||||
|
|
|
|||
|
|
@ -46,7 +46,7 @@ namespace opt {
|
|||
expr_ref_vector m_models_trail;
|
||||
expr_ref_vector m_atoms;
|
||||
obj_hashtable<expr> m_models;
|
||||
obj_hashtable<expr> m_fixed;
|
||||
obj_hashtable<expr> m_failed;
|
||||
|
||||
bool add_assignment();
|
||||
public:
|
||||
|
|
|
|||
|
|
@ -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();
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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()) {
|
||||
|
|
|
|||
|
|
@ -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;
|
||||
|
|
|
|||
|
|
@ -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.'),
|
||||
|
|
|
|||
|
|
@ -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););
|
||||
|
||||
|
|
|
|||
|
|
@ -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<unsigned>(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<unsigned>(m_phase_tf[v].t + m_phase_tf[v].f)) <= 100 * m_phase_tf[v].t;
|
||||
}
|
||||
}
|
||||
}
|
||||
else {
|
||||
|
|
|
|||
|
|
@ -323,7 +323,6 @@ class params {
|
|||
typedef std::pair<symbol, value> entry;
|
||||
svector<entry> m_entries;
|
||||
unsigned m_ref_count;
|
||||
|
||||
void del_value(entry & e);
|
||||
void del_values();
|
||||
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue