mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 18:31:49 +00:00
wip - local search - use dispatch model from bool local search instead of separate phases.
This commit is contained in:
Nikolaj Bjorner
parent
ac068888e7
commit
bd10ddf6ae
|
|
@ -61,7 +61,8 @@ namespace sat {
|
|||
|
||||
void ddfw::check_with_plugin() {
|
||||
m_plugin->init_search();
|
||||
while (m_limit.inc() && m_min_sz > 0) {
|
||||
m_steps_since_progress = 0;
|
||||
while (m_min_sz > 0 && m_steps_since_progress++ <= 1500000) {
|
||||
if (should_reinit_weights()) do_reinit_weights();
|
||||
else if (do_flip<true>());
|
||||
else if (do_literal_flip<true>());
|
||||
|
|
@ -106,7 +107,7 @@ namespace sat {
|
|||
if (v == null_bool_var)
|
||||
return false;
|
||||
if (reward(v) > 0 || (reward(v) == 0 && m_rand(100) <= m_config.m_use_reward_zero_pct)) {
|
||||
if (uses_plugin)
|
||||
if (uses_plugin && is_external(v))
|
||||
m_plugin->flip(v);
|
||||
else
|
||||
flip(v);
|
||||
|
|
@ -159,6 +160,24 @@ namespace sat {
|
|||
*/
|
||||
template<bool uses_plugin>
|
||||
bool_var ddfw::pick_literal_var() {
|
||||
#if false
|
||||
unsigned sz = m_clauses.size();
|
||||
unsigned start = rand();
|
||||
for (unsigned i = 0; i < 100; ++i) {
|
||||
unsigned cl = (i + start) % sz;
|
||||
if (m_unsat.contains(cl))
|
||||
continue;
|
||||
for (auto lit : *m_clauses[cl].m_clause) {
|
||||
if (is_true(lit))
|
||||
continue;
|
||||
double r = uses_plugin ? plugin_reward(lit.var()) : reward(lit.var());
|
||||
if (r < 0)
|
||||
continue;
|
||||
//verbose_stream() << "false " << r << " " << lit << "\n";
|
||||
return lit.var();
|
||||
}
|
||||
}
|
||||
#endif
|
||||
return null_bool_var;
|
||||
}
|
||||
|
||||
|
|
@ -453,6 +472,7 @@ namespace sat {
|
|||
if (m_unsat.empty())
|
||||
save_model();
|
||||
else if (m_unsat.size() < m_min_sz) {
|
||||
m_steps_since_progress = 0;
|
||||
if (m_unsat.size() < 50 || m_min_sz * 10 > m_unsat.size() * 11)
|
||||
save_model();
|
||||
}
|
||||
|
|
|
|||
|
|
@ -126,7 +126,7 @@ namespace sat {
|
|||
unsigned m_restart_count = 0, m_reinit_count = 0, m_parsync_count = 0;
|
||||
uint64_t m_restart_next = 0, m_reinit_next = 0, m_parsync_next = 0;
|
||||
uint64_t m_flips = 0, m_last_flips = 0, m_shifts = 0;
|
||||
unsigned m_min_sz = 0;
|
||||
unsigned m_min_sz = 0, m_steps_since_progress = 0;
|
||||
hashtable<unsigned, unsigned_hash, default_eq<unsigned>> m_models;
|
||||
stopwatch m_stopwatch;
|
||||
|
||||
|
|
|
|||
|
|
@ -1302,9 +1302,6 @@ namespace sat {
|
|||
return l_undef;
|
||||
}
|
||||
|
||||
// uncomment this to test bounded local search:
|
||||
// bounded_local_search();
|
||||
|
||||
log_stats();
|
||||
if (m_config.m_max_conflicts > 0 && m_config.m_burst_search > 0) {
|
||||
m_restart_threshold = m_config.m_burst_search;
|
||||
|
|
|
|||
|
|
@ -26,34 +26,9 @@ namespace arith {
|
|||
void sls::reset() {
|
||||
m_literals.reset();
|
||||
m_vars.reset();
|
||||
m_clauses.reset();
|
||||
m_terms.reset();
|
||||
}
|
||||
|
||||
lbool sls::operator()(bool_vector& phase) {
|
||||
|
||||
unsigned num_steps = 0;
|
||||
for (unsigned v = 0; v < s.s().num_vars(); ++v)
|
||||
init_bool_var_assignment(v);
|
||||
verbose_stream() << "max arith steps " << m_max_arith_steps << "\n";
|
||||
m_max_arith_steps = std::max(1000u, m_max_arith_steps);
|
||||
while (m.inc() && m_best_min_unsat > 0 && num_steps < m_max_arith_steps) {
|
||||
if (!flip())
|
||||
break;
|
||||
++m_stats.m_num_flips;
|
||||
++num_steps;
|
||||
unsigned num_unsat = unsat().size();
|
||||
if (num_unsat < m_best_min_unsat) {
|
||||
m_best_min_unsat = num_unsat;
|
||||
num_steps = 0;
|
||||
save_best_values();
|
||||
}
|
||||
}
|
||||
store_best_values();
|
||||
log();
|
||||
return unsat().empty() ? l_true : l_undef;
|
||||
}
|
||||
|
||||
void sls::log() {
|
||||
IF_VERBOSE(2, verbose_stream() << "(sls :flips " << m_stats.m_num_flips << " :unsat " << unsat().size() << ")\n");
|
||||
}
|
||||
|
|
@ -105,7 +80,6 @@ namespace arith {
|
|||
reset();
|
||||
m_literals.reserve(s.s().num_vars() * 2);
|
||||
add_vars();
|
||||
m_clauses.resize(d->num_clauses());
|
||||
for (unsigned i = 0; i < d->num_clauses(); ++i)
|
||||
for (sat::literal lit : *d->get_clause_info(i).m_clause)
|
||||
init_literal(lit);
|
||||
|
|
@ -116,22 +90,6 @@ namespace arith {
|
|||
d->set(this);
|
||||
}
|
||||
|
||||
void sls::set_bounds_begin() {
|
||||
m_max_arith_steps = 0;
|
||||
}
|
||||
|
||||
void sls::set_bounds(enode* n) {
|
||||
++m_max_arith_steps;
|
||||
}
|
||||
|
||||
void sls::set_bounds_end(unsigned num_literals) {
|
||||
m_max_arith_steps = (m_config.L * m_max_arith_steps); // / num_literals;
|
||||
}
|
||||
|
||||
bool sls::flip() {
|
||||
log();
|
||||
return flip_unsat() || flip_clauses() || flip_dscore();
|
||||
}
|
||||
|
||||
// distance to true
|
||||
int64_t sls::dtt(int64_t args, ineq const& ineq) const {
|
||||
|
|
@ -207,31 +165,6 @@ namespace arith {
|
|||
return false;
|
||||
}
|
||||
|
||||
bool sls::flip_unsat() {
|
||||
unsigned start = s.random();
|
||||
unsigned sz = unsat().size();
|
||||
for (unsigned i = sz; i-- > 0; )
|
||||
if (flip_clause(unsat().elem_at((i + start) % sz)))
|
||||
return true;
|
||||
return false;
|
||||
}
|
||||
|
||||
bool sls::flip_clause(unsigned cl) {
|
||||
auto const& clause = get_clause(cl);
|
||||
for (literal lit : clause) {
|
||||
if (is_true(lit))
|
||||
continue;
|
||||
auto const* ineq = atom(lit);
|
||||
if (!ineq)
|
||||
continue;
|
||||
SASSERT(!ineq->is_true());
|
||||
if (flip(*ineq))
|
||||
return true;
|
||||
|
||||
}
|
||||
return false;
|
||||
}
|
||||
|
||||
// flip on the first positive score
|
||||
// it could be changed to flip on maximal positive score
|
||||
// or flip on maximal non-negative score
|
||||
|
|
@ -255,77 +188,17 @@ namespace arith {
|
|||
return false;
|
||||
}
|
||||
|
||||
bool sls::flip_clauses() {
|
||||
unsigned start = s.random();
|
||||
unsigned sz = m_bool_search->num_clauses();
|
||||
for (unsigned i = sz; i-- > 0; )
|
||||
if (flip_clause((i + start) % sz))
|
||||
return true;
|
||||
return false;
|
||||
}
|
||||
|
||||
bool sls::flip_dscore() {
|
||||
paws();
|
||||
unsigned start = s.random();
|
||||
unsigned sz = unsat().size();
|
||||
for (unsigned i = sz; i-- > 0; )
|
||||
if (flip_dscore(unsat().elem_at((i + start) % sz)))
|
||||
return true;
|
||||
return false;
|
||||
}
|
||||
|
||||
bool sls::flip_dscore(unsigned cl) {
|
||||
auto const& clause = get_clause(cl);
|
||||
int64_t new_value, min_value, min_score(-1);
|
||||
var_t min_var = UINT_MAX;
|
||||
for (auto lit : clause) {
|
||||
auto const* ineq = atom(lit);
|
||||
if (!ineq || ineq->is_true())
|
||||
continue;
|
||||
for (auto const& [coeff, v] : ineq->m_args) {
|
||||
if (cm(*ineq, v, new_value)) {
|
||||
int64_t score = dscore(v, new_value);
|
||||
if (UINT_MAX == min_var || score < min_score) {
|
||||
min_var = v;
|
||||
min_value = new_value;
|
||||
min_score = score;
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
if (min_var != UINT_MAX) {
|
||||
update(min_var, min_value);
|
||||
return true;
|
||||
}
|
||||
return false;
|
||||
}
|
||||
|
||||
/**
|
||||
* redistribute weights of clauses.
|
||||
* TODO - re-use ddfw weights instead.
|
||||
*/
|
||||
void sls::paws() {
|
||||
for (unsigned cl = num_clauses(); cl-- > 0; ) {
|
||||
auto& clause = get_clause_info(cl);
|
||||
bool above = 10000 * m_config.sp <= (s.random() % 10000);
|
||||
if (!above && clause.is_true() && get_weight(cl) > 1)
|
||||
get_weight(cl) -= 1;
|
||||
if (above && !clause.is_true())
|
||||
get_weight(cl) += 1;
|
||||
}
|
||||
}
|
||||
|
||||
//
|
||||
// dscore(op) = sum_c (dts(c,alpha) - dts(c,alpha_after)) * weight(c)
|
||||
// TODO - use cached dts instead of computed dts
|
||||
// cached dts has to be updated when the score of literals are updated.
|
||||
//
|
||||
int64_t sls::dscore(var_t v, int64_t new_value) const {
|
||||
double sls::dscore(var_t v, int64_t new_value) const {
|
||||
auto const& vi = m_vars[v];
|
||||
int64_t score(0);
|
||||
double score = 0;
|
||||
for (auto const& [coeff, lit] : vi.m_literals)
|
||||
for (auto cl : m_bool_search->get_use_list(lit))
|
||||
score += (compute_dts(cl) - dts(cl, v, new_value)) * int64_t(get_weight(cl));
|
||||
score += (compute_dts(cl) - dts(cl, v, new_value)) * m_bool_search->get_weight(cl);
|
||||
return score;
|
||||
}
|
||||
|
||||
|
|
@ -437,46 +310,6 @@ namespace arith {
|
|||
m_vars[v].m_literals.push_back({ c, lit });
|
||||
}
|
||||
|
||||
void sls::add_bounds(sat::literal_vector& bounds) {
|
||||
unsigned bvars = s.s().num_vars();
|
||||
auto add_ineq = [&](sat::literal lit, ineq& i) {
|
||||
m_literals.set(lit.index(), &i);
|
||||
bounds.push_back(lit);
|
||||
};
|
||||
for (unsigned v = 0; v < s.get_num_vars(); ++v) {
|
||||
rational lo, hi;
|
||||
bool is_strict_lo = false, is_strict_hi = false;
|
||||
lp::constraint_index ci;
|
||||
if (!s.is_registered_var(v))
|
||||
continue;
|
||||
lp::column_index vi = s.lp().to_column_index(v);
|
||||
if (vi.is_null())
|
||||
continue;
|
||||
bool has_lo = s.lp().has_lower_bound(vi.index(), ci, lo, is_strict_lo);
|
||||
bool has_hi = s.lp().has_upper_bound(vi.index(), ci, hi, is_strict_hi);
|
||||
|
||||
if (has_lo && has_hi && lo == hi) {
|
||||
auto& ineq = new_ineq(sls::ineq_kind::EQ, to_numeral(lo));
|
||||
sat::literal lit(bvars++);
|
||||
add_arg(lit, ineq, 1, v);
|
||||
add_ineq(lit, ineq);
|
||||
continue;
|
||||
}
|
||||
if (has_lo) {
|
||||
auto& ineq = new_ineq(is_strict_lo ? sls::ineq_kind::LT : sls::ineq_kind::LE, to_numeral(-lo));
|
||||
sat::literal lit(bvars++);
|
||||
add_arg(lit, ineq, -1, v);
|
||||
add_ineq(lit, ineq);
|
||||
}
|
||||
if (has_hi) {
|
||||
auto& ineq = new_ineq(is_strict_hi ? sls::ineq_kind::LT : sls::ineq_kind::LE, to_numeral(hi));
|
||||
sat::literal lit(bvars++);
|
||||
add_arg(lit, ineq, 1, v);
|
||||
add_ineq(lit, ineq);
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
int64_t sls::to_numeral(rational const& r) {
|
||||
if (r.is_int64())
|
||||
return r.get_int64();
|
||||
|
|
@ -635,4 +468,3 @@ namespace arith {
|
|||
init_bool_var_assignment(v);
|
||||
}
|
||||
}
|
||||
|
||||
|
|
|
|||
|
|
@ -100,11 +100,6 @@ namespace arith {
|
|||
svector<std::pair<int64_t, sat::literal>> m_literals;
|
||||
};
|
||||
|
||||
struct clause {
|
||||
unsigned m_weight = 1;
|
||||
int64_t m_dts = 1;
|
||||
};
|
||||
|
||||
solver& s;
|
||||
ast_manager& m;
|
||||
sat::ddfw* m_bool_search = nullptr;
|
||||
|
|
@ -114,7 +109,6 @@ namespace arith {
|
|||
config m_config;
|
||||
scoped_ptr_vector<ineq> m_literals;
|
||||
vector<var_info> m_vars;
|
||||
vector<clause> m_clauses;
|
||||
svector<std::pair<lp::tv, euf::theory_var>> m_terms;
|
||||
bool m_dscore_mode = false;
|
||||
|
||||
|
|
@ -129,15 +123,9 @@ namespace arith {
|
|||
|
||||
void reset();
|
||||
ineq* atom(sat::literal lit) const { return m_literals[lit.index()]; }
|
||||
unsigned& get_weight(unsigned idx) { return m_clauses[idx].m_weight; }
|
||||
unsigned get_weight(unsigned idx) const { return m_clauses[idx].m_weight; }
|
||||
bool flip();
|
||||
|
||||
void log();
|
||||
bool flip_unsat();
|
||||
bool flip_clauses();
|
||||
bool flip_dscore();
|
||||
bool flip_dscore(unsigned cl);
|
||||
bool flip_clause(unsigned cl);
|
||||
|
||||
bool flip(ineq const& ineq);
|
||||
int64_t dtt(ineq const& ineq) const { return dtt(ineq.m_args_value, ineq); }
|
||||
int64_t dtt(int64_t args, ineq const& ineq) const;
|
||||
|
|
@ -149,14 +137,12 @@ namespace arith {
|
|||
void update(var_t v, int64_t new_value);
|
||||
double dscore_reward(sat::bool_var v);
|
||||
double dtt_reward(sat::bool_var v);
|
||||
void paws();
|
||||
int64_t dscore(var_t v, int64_t new_value) const;
|
||||
double dscore(var_t v, int64_t new_value) const;
|
||||
void save_best_values();
|
||||
void store_best_values();
|
||||
void add_vars();
|
||||
sls::ineq& new_ineq(ineq_kind op, int64_t const& bound);
|
||||
void add_arg(sat::literal lit, ineq& ineq, int64_t const& c, var_t v);
|
||||
void add_bounds(sat::literal_vector& bounds);
|
||||
void add_args(sat::literal lit, ineq& ineq, lp::tv t, euf::theory_var v, int64_t sign);
|
||||
void init_literal(sat::literal lit);
|
||||
void init_bool_var_assignment(sat::bool_var v);
|
||||
|
|
@ -168,12 +154,7 @@ namespace arith {
|
|||
public:
|
||||
sls(solver& s);
|
||||
~sls() override {}
|
||||
lbool operator ()(bool_vector& phase);
|
||||
void set_bounds_begin();
|
||||
void set_bounds_end(unsigned num_literals);
|
||||
void set_bounds(euf::enode* n);
|
||||
void set(sat::ddfw* d);
|
||||
|
||||
void init_search() override;
|
||||
void finish_search() override;
|
||||
void flip(sat::bool_var v) override;
|
||||
|
|
|
|||
|
|
@ -512,10 +512,6 @@ namespace arith {
|
|||
bool enable_ackerman_axioms(euf::enode* n) const override { return !a.is_add(n->get_expr()); }
|
||||
bool has_unhandled() const override { return m_not_handled != nullptr; }
|
||||
|
||||
void set_bounds_begin() override { m_local_search.set_bounds_begin(); }
|
||||
void set_bounds_end(unsigned num_literals) override { m_local_search.set_bounds_end(num_literals); }
|
||||
void set_bounds(enode* n) override { m_local_search.set_bounds(n); }
|
||||
lbool local_search(bool_vector& phase) override { return m_local_search(phase); }
|
||||
void set_bool_search(sat::ddfw* ddfw) override { m_local_search.set(ddfw); }
|
||||
|
||||
// bounds and equality propagation callbacks
|
||||
|
|
|
|||
|
|
@ -32,9 +32,7 @@ namespace euf {
|
|||
for (auto* th : m_solvers)
|
||||
th->set_bool_search(&bool_search);
|
||||
|
||||
bool_search.rlimit().push(m_max_bool_steps);
|
||||
lbool r = bool_search.check(0, nullptr, nullptr);
|
||||
bool_search.rlimit().pop();
|
||||
lbool r = bool_search.check(0, nullptr, nullptr);
|
||||
|
||||
auto const& mdl = bool_search.get_model();
|
||||
for (unsigned i = 0; i < mdl.size(); ++i)
|
||||
|
|
@ -42,40 +40,4 @@ namespace euf {
|
|||
|
||||
return bool_search.unsat_set().empty() ? l_true : l_undef;
|
||||
}
|
||||
|
||||
bool solver::is_propositional(sat::literal lit) {
|
||||
expr* e = m_bool_var2expr.get(lit.var(), nullptr);
|
||||
return !e || is_uninterp_const(e) || !m_egraph.find(e);
|
||||
}
|
||||
|
||||
void solver::setup_bounds(sat::ddfw& bool_search, bool_vector const& phase) {
|
||||
unsigned num_literals = 0;
|
||||
unsigned num_bool = 0;
|
||||
for (auto* th : m_solvers)
|
||||
th->set_bounds_begin();
|
||||
|
||||
auto count_literal = [&](sat::literal l) {
|
||||
if (is_propositional(l)) {
|
||||
++num_bool;
|
||||
return;
|
||||
}
|
||||
euf::enode* n = m_egraph.find(m_bool_var2expr.get(l.var(), nullptr));
|
||||
for (auto* s : m_solvers)
|
||||
s->set_bounds(n);
|
||||
};
|
||||
|
||||
for (auto cl : bool_search.unsat_set()) {
|
||||
auto& c = *bool_search.get_clause_info(cl).m_clause;
|
||||
num_literals += c.size();
|
||||
for (auto l : c)
|
||||
count_literal(l);
|
||||
}
|
||||
|
||||
m_max_bool_steps = (m_ls_config.L * num_bool); // / num_literals;
|
||||
m_max_bool_steps = std::max(10000u, m_max_bool_steps);
|
||||
verbose_stream() << "num literals " << num_literals << " num bool " << num_bool << " max bool steps " << m_max_bool_steps << "\n";
|
||||
|
||||
for (auto* th : m_solvers)
|
||||
th->set_bounds_end(num_literals);
|
||||
}
|
||||
}
|
||||
|
|
|
|||
|
|
@ -260,12 +260,7 @@ namespace euf {
|
|||
constraint& mk_constraint(constraint*& c, constraint::kind_t k);
|
||||
constraint& conflict_constraint() { return mk_constraint(m_conflict, constraint::kind_t::conflict); }
|
||||
constraint& eq_constraint() { return mk_constraint(m_eq, constraint::kind_t::eq); }
|
||||
constraint& lit_constraint(enode* n);
|
||||
|
||||
// local search
|
||||
unsigned m_max_bool_steps = 10;
|
||||
bool is_propositional(sat::literal lit);
|
||||
void setup_bounds(sat::ddfw& bool_search, bool_vector const& mdl);
|
||||
constraint& lit_constraint(enode* n);
|
||||
|
||||
// user propagator
|
||||
void check_for_user_propagator() {
|
||||
|
|
|
|||
Loading…
Reference in a new issue