Skip to content

Commit

Permalink
wip - local search - use dispatch model from bool local search instea…
Browse files Browse the repository at this point in the history 
…d of separate phases.
  • Loading branch information
@NikolajBjorner
NikolajBjorner committed Feb 16, 2023
1 parent ac06888 commit bd10ddf
Show file tree
Hide file tree
Showing 8 changed files with 31 additions and 248 deletions.
24 changes: 22 additions & 2 deletions src/sat/sat_ddfw.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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>());
Expand Down Expand Up @@ -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);
Expand Down Expand Up @@ -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;
}

Expand Down Expand Up @@ -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();
}
Expand Down
2 changes: 1 addition & 1 deletion src/sat/sat_ddfw.h
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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;

Expand Down
3 changes: 0 additions & 3 deletions src/sat/sat_solver.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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;
Expand Down
174 changes: 3 additions & 171 deletions src/sat/smt/arith_sls.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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");
}
Expand Down Expand Up @@ -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);
Expand All @@ -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 {
Expand Down Expand Up @@ -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
Expand All @@ -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;
}

Expand Down Expand Up @@ -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();
Expand Down Expand Up @@ -635,4 +468,3 @@ namespace arith {
init_bool_var_assignment(v);
}
}

25 changes: 3 additions & 22 deletions src/sat/smt/arith_sls.h
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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;
Expand All @@ -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;

Expand All @@ -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;
Expand All @@ -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);
Expand All @@ -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;
Expand Down
4 changes: 0 additions & 4 deletions src/sat/smt/arith_solver.h
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
Loading

0 comments on commit bd10ddf

Please sign in to comment.