Skip to content

Commit

Permalink
fixes and tests for arith-sls
Browse files Browse the repository at this point in the history
  • Loading branch information
@NikolajBjorner
NikolajBjorner committed Mar 1, 2023
1 parent e87fa1c commit 25d45a3
Show file tree
Hide file tree
Showing 7 changed files with 182 additions and 136 deletions.
28 changes: 18 additions & 10 deletions src/sat/sat_ddfw.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -62,13 +62,16 @@ namespace sat {
void ddfw::check_with_plugin() {
m_plugin->init_search();
m_steps_since_progress = 0;
while (m_min_sz > 0 && m_steps_since_progress++ <= 150000) {
unsigned steps = 0;
while (m_min_sz > 0 && m_steps_since_progress++ <= 1500000) {
if (should_reinit_weights()) do_reinit_weights();
else if (steps % 5000 == 0) shift_weights(), m_plugin->on_rescale();
else if (should_restart()) do_restart(), m_plugin->on_restart();
else if (do_flip<true>());
else if (do_literal_flip<true>());
else if (should_restart()) do_restart(), m_plugin->on_restart();
else if (should_parallel_sync()) do_parallel_sync();
else shift_weights(), m_plugin->on_rescale();
++steps;
}
m_plugin->finish_search();
}
Expand Down Expand Up @@ -135,7 +138,7 @@ namespace sat {
if (sum_pos > 0) {
double lim_pos = ((double) m_rand() / (1.0 + m_rand.max_value())) * sum_pos;
for (bool_var v : m_unsat_vars) {
r = uses_plugin ? plugin_reward(v) : reward(v);
r = uses_plugin && is_external(v) ? m_vars[v].m_last_reward : reward(v);
if (r > 0) {
lim_pos -= score(r);
if (lim_pos <= 0)
Expand Down Expand Up @@ -472,9 +475,7 @@ namespace sat {


void ddfw::save_best_values() {
if (m_unsat.empty())
save_model();
else if (m_unsat.size() < m_min_sz) {
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 All @@ -489,13 +490,20 @@ namespace sat {
}
}
}

unsigned h = value_hash();
unsigned occs = 0;
bool contains = m_models.find(h, occs);
if (!m_models.contains(h)) {
for (unsigned v = 0; v < num_vars(); ++v)
for (unsigned v = 0; v < num_vars(); ++v)
bias(v) += value(v) ? 1 : -1;
m_models.insert(h);
if (m_models.size() > m_config.m_max_num_models)
m_models.erase(*m_models.begin());
if (m_models.size() > m_config.m_max_num_models)
m_models.erase(m_models.begin()->m_key);
}
m_models.insert(h, occs + 1);
if (occs > 100) {
m_restart_next = m_flips;
m_models.erase(h);
}
m_min_sz = m_unsat.size();
}
Expand Down
5 changes: 3 additions & 2 deletions src/sat/sat_ddfw.h
View file
Original file line number Diff line number Diff line change
Expand Up @@ -98,6 +98,7 @@ namespace sat {
var_info() {}
bool m_value = false;
double m_reward = 0;
double m_last_reward = 0;
unsigned m_make_count = 0;
int m_bias = 0;
bool m_external = false;
Expand Down Expand Up @@ -127,7 +128,7 @@ namespace sat {
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, m_steps_since_progress = 0;
hashtable<unsigned, unsigned_hash, default_eq<unsigned>> m_models;
u_map<unsigned> m_models;
stopwatch m_stopwatch;

parallel* m_par;
Expand All @@ -153,7 +154,7 @@ namespace sat {

inline double reward(bool_var v) const { return m_vars[v].m_reward; }

inline double plugin_reward(bool_var v) const { return is_external(v) ? m_plugin->reward(v) : reward(v); }
inline double plugin_reward(bool_var v) { return is_external(v) ? (m_vars[v].m_last_reward = m_plugin->reward(v)) : reward(v); }

void set_external(bool_var v) { m_vars[v].m_external = true; }

Expand Down
48 changes: 15 additions & 33 deletions src/sat/sat_solver.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -40,26 +40,6 @@ Revision History:

namespace sat {

/**
* Special cases of kissat style general backoff calculation.
* The version here calculates
* limit := value*log(C)^2*n*log(n)
* (effort calculation in kissat is based on ticks not clauses)
*
* respectively
* limit := conflicts + value*log(C)^2*n*log(n)
*/
void backoff::delta_effort(solver& s) {
count++;
unsigned d = value * count * log2(count + 1);
unsigned cl = log2(s.num_clauses() + 2);
limit = cl * cl * d;
}

void backoff::delta_conflicts(solver& s) {
delta_effort(s);
limit += s.m_conflicts_since_init;
}

solver::solver(params_ref const & p, reslimit& l):
solver_core(l),
Expand Down Expand Up @@ -1302,10 +1282,9 @@ namespace sat {
return l_undef;
}

if (false && m_config.m_phase == PS_LOCAL_SEARCH && m_ext) {
IF_VERBOSE(0, verbose_stream() << "WARNING: local search with theories is in testing mode\n");
if (m_config.m_phase == PS_LOCAL_SEARCH && m_ext) {
bounded_local_search();
exit(0);
// exit(0);
}

log_stats();
Expand Down Expand Up @@ -1367,7 +1346,7 @@ namespace sat {

void solver::bounded_local_search() {
if (m_ext) {
verbose_stream() << "bounded local search\n";
IF_VERBOSE(0, verbose_stream() << "WARNING: local search with theories is in testing mode\n");
do_restart(true);
lbool r = m_ext->local_search(m_best_phase);
verbose_stream() << r << "\n";
Expand All @@ -1388,8 +1367,8 @@ namespace sat {
m_local_search->set_seed(m_rand());
scoped_rl.push_child(&(m_local_search->rlimit()));

m_backoffs.m_local_search.delta_effort(*this);
m_local_search->rlimit().push(m_backoffs.m_local_search.limit);
m_local_search_lim.inc(num_clauses());
m_local_search->rlimit().push(m_local_search_lim.limit);

m_local_search->reinit(*this, m_best_phase);
lbool r = m_local_search->check(_lits.size(), _lits.data(), nullptr);
Expand Down Expand Up @@ -1977,11 +1956,13 @@ namespace sat {
m_search_sat_conflicts = m_config.m_search_sat_conflicts;
m_search_next_toggle = m_search_unsat_conflicts;
m_best_phase_size = 0;

m_reorder.lo = m_config.m_reorder_base;
m_rephase.base = m_config.m_rephase_base;
m_rephase_lim = 0;
m_rephase_inc = 0;
m_reorder_lim = m_config.m_reorder_base;
m_backoffs.m_local_search.value = 500;
m_reorder_inc = 0;
m_local_search_lim.base = 500;

m_conflicts_since_restart = 0;
m_force_conflict_analysis = false;
m_restart_threshold = m_config.m_restart_initial;
Expand Down Expand Up @@ -2981,6 +2962,7 @@ namespace sat {

bool solver::should_rephase() {
return m_conflicts_since_init > m_rephase_lim;
// return m_rephase.should_apply(m_conflicts_since_init);
}

void solver::do_rephase() {
Expand All @@ -2994,7 +2976,7 @@ namespace sat {
case PS_FROZEN:
break;
case PS_BASIC_CACHING:
switch (m_rephase_lim % 4) {
switch (m_rephase.count % 4) {
case 0:
for (auto& p : m_phase) p = (m_rand() % 2) == 0;
break;
Expand Down Expand Up @@ -3031,10 +3013,11 @@ namespace sat {
}
m_rephase_inc += m_config.m_rephase_base;
m_rephase_lim += m_rephase_inc;
m_rephase.inc(m_conflicts_since_init, num_clauses());
}

bool solver::should_reorder() {
return m_conflicts_since_init > m_reorder_lim;
return m_reorder.should_apply(m_conflicts_since_init);
}

void solver::do_reorder() {
Expand Down Expand Up @@ -3078,8 +3061,7 @@ namespace sat {
update_activity(v, m_rand(10)/10.0);
}
#endif
m_reorder_inc += m_config.m_reorder_base;
m_reorder_lim += m_reorder_inc;
m_reorder.inc(m_conflicts_since_init, num_clauses());
}

void solver::updt_phase_counters() {
Expand Down
19 changes: 3 additions & 16 deletions src/sat/sat_solver.h
View file
Original file line number Diff line number Diff line change
Expand Up @@ -87,23 +87,10 @@ namespace sat {
struct no_drat_params : public params_ref {
no_drat_params() { set_bool("drat.disable", true); }
};

struct backoff {
unsigned value = 1;
unsigned lo = 0;
unsigned hi = 0;
unsigned limit = 0;
unsigned count = 0;
void delta_effort(solver& s);
void delta_conflicts(solver& s);
};

class solver : public solver_core {
public:
struct abort_solver {};
struct backoffs {
backoff m_local_search;
};
protected:
enum search_state { s_sat, s_unsat };

Expand Down Expand Up @@ -172,11 +159,11 @@ namespace sat {
unsigned m_search_next_toggle;
unsigned m_phase_counter;
unsigned m_best_phase_size;
backoffs m_backoffs;
backoff m_local_search_lim;
unsigned m_rephase_lim;
unsigned m_rephase_inc;
unsigned m_reorder_lim;
unsigned m_reorder_inc;
backoff m_rephase;
backoff m_reorder;
var_queue m_case_split_queue;
unsigned m_qhead;
unsigned m_scope_lvl;
Expand Down
34 changes: 34 additions & 0 deletions src/sat/sat_types.h
View file
Original file line number Diff line number Diff line change
Expand Up @@ -136,6 +136,40 @@ namespace sat {
std::ostream& operator<<(std::ostream& out, sat::status const& st);
std::ostream& operator<<(std::ostream& out, sat::status_pp const& p);

/**
* Special cases of kissat style general backoff calculation.
* The version here calculates
* limit := value*log(C)^2*n*log(n)
* (effort calculation in kissat is based on ticks not clauses)
*
* respectively
* limit := conflicts + value*log(C)^2*n*log(n)
*/
struct backoff {
unsigned base = 1;
unsigned lo = 0;
unsigned hi = UINT_MAX;
unsigned limit = 0;
unsigned count = 0;

bool should_apply(unsigned n) const {
return limit <= n && lo <= n && n <= hi;
}

void inc(unsigned num_clauses) {
count++;
unsigned d = base * count * log2(count + 1);
unsigned cl = log2(num_clauses + 2);
limit = cl * cl * d;
}

void inc(unsigned num_conflicts, unsigned num_clauses) {
inc(num_clauses);
limit += num_conflicts;
}

};

};


Expand Down
Loading

0 comments on commit 25d45a3

Please sign in to comment.