mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-13 20:38:43 +00:00
Code Activity

fixing local search

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2017-04-17 13:04:57 -07:00
parent 41e1b9f3fe
commit 352f8b6cb9
5 changed files with 32 additions and 23 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

30
src/sat/sat_local_search.cpp
View file

@ -70,9 +70,10 @@ namespace sat {
void local_search::init_cur_solution() {
for (unsigned v = 0; v < num_vars(); ++v) {
// use bias half the time.
if (m_rand() % 100 < 10) {
m_vars[v].m_value = ((unsigned)(m_rand() % 100) < m_vars[v].m_bias);
// use bias with a small probability
if (m_rand() % 100 < 3) {
//m_vars[v].m_value = ((unsigned)(m_rand() % 100) < m_vars[v].m_bias);
m_vars[v].m_value = (50 < m_vars[v].m_bias);
}
}
}
@ -140,14 +141,17 @@ namespace sat {
// the following methods does NOT converge for pseudo-boolean
// can try other way to define "worse" and "better"
// the current best noise is below 1000
if (best_unsat_rate >= last_best_unsat_rate) {
#if 0
if (m_best_unsat_rate > m_last_best_unsat_rate) {
// worse
m_noise -= m_noise * 2 * m_noise_delta;
m_best_unsat_rate *= 1000.0;
}
else {
// better
m_noise += (10000 - m_noise) * m_noise_delta;
}
#endif
for (unsigned i = 0; i < m_constraints.size(); ++i) {
constraint& c = m_constraints[i];
c.m_slack = c.m_k;
@ -178,6 +182,8 @@ namespace sat {
init_slack();
init_scores();
init_goodvars();
m_best_unsat = m_unsat_stack.size();
}
void local_search::calculate_and_update_ob() {
@ -382,13 +388,13 @@ namespace sat {
IF_VERBOSE(1, verbose_stream() << "(sat-local-search" \
<< " :flips " << flips \
<< " :noise " << m_noise \
<< " :unsat " << /*m_unsat_stack.size()*/ best_unsat \
<< " :unsat " << /*m_unsat_stack.size()*/ m_best_unsat \
<< " :time " << (timer.get_seconds() < 0.001 ? 0.0 : timer.get_seconds()) << ")\n";); \
}
void local_search::walksat() {
best_unsat_rate = 1;
last_best_unsat_rate = 1;
m_best_unsat_rate = 1;
m_last_best_unsat_rate = 1;
reinit();
@ -398,10 +404,10 @@ namespace sat {
PROGRESS(tries, total_flips);
for (tries = 1; !m_unsat_stack.empty() && m_limit.inc(); ++tries) {
if (m_unsat_stack.size() < best_unsat) {
best_unsat = m_unsat_stack.size();
last_best_unsat_rate = best_unsat_rate;
best_unsat_rate = (double)m_unsat_stack.size() / num_constraints();
if (m_unsat_stack.size() < m_best_unsat) {
m_best_unsat = m_unsat_stack.size();
m_last_best_unsat_rate = m_best_unsat_rate;
m_best_unsat_rate = (double)m_unsat_stack.size() / num_constraints();
}
for (step = 0; step < m_max_steps && !m_unsat_stack.empty(); ++step) {
pick_flip_walksat();
@ -506,7 +512,7 @@ namespace sat {
SASSERT(c.m_k < constraint_value(c));
// TBD: dynamic noise strategy
//if (m_rand() % 100 < 98) {
if (m_rand() % 10000 >= m_noise) {
if (m_rand() % 10000 <= m_noise) {
// take this branch with 98% probability.
// find the first one, to fast break the rest
unsigned best_bsb = 0;

8
src/sat/sat_local_search.h
View file

@ -164,9 +164,9 @@ namespace sat {
// information about solution
unsigned best_unsat;
double best_unsat_rate;
double last_best_unsat_rate;
unsigned m_best_unsat;
double m_best_unsat_rate;
double m_last_best_unsat_rate;
int m_objective_value; // the objective function value corresponds to the current solution
bool_vector m_best_solution; // !var: the best solution so far
int m_best_objective_value = -1; // the objective value corresponds to the best solution so far
@ -176,7 +176,7 @@ namespace sat {
unsigned m_max_steps = (1 << 30);
// dynamic noise
double m_noise = 400; // normalized by 10000
double m_noise = 9800; // normalized by 10000
double m_noise_delta = 0.05;
// for tuning

12
src/sat/sat_parallel.cpp
View file

@ -115,12 +115,16 @@ namespace sat {
m_solvers[i] = alloc(sat::solver, s.m_params, m_limits[i]);
m_solvers[i]->copy(s);
m_solvers[i]->set_par(this, i);
m_scoped_rlimit.push_child(&m_solvers[i]->rlimit());
push_child(m_solvers[i]->rlimit());
}
s.set_par(this, num_extra_solvers);
s.m_params.set_sym("phase", saved_phase);
}
void parallel::push_child(reslimit& rl) {
m_scoped_rlimit.push_child(&rl);
}
void parallel::exchange(solver& s, literal_vector const& in, unsigned& limit, literal_vector& out) {
if (s.m_par_syncing_clauses) return;
@ -268,12 +272,6 @@ namespace sat {
{
if (m_solver_copy && s.num_non_binary_clauses() > m_solver_copy->m_clauses.size()) {
s.import(*m_solver_copy.get(), true);
m_num_clauses = s.num_non_binary_clauses();
SASSERT(s.num_non_binary_clauses() == m_solver_copy->m_clauses.size());
m_solver_copy = 0;
}
if (m_num_clauses < s.num_non_binary_clauses()) {
m_num_clauses = s.num_non_binary_clauses();
}
for (unsigned i = 0; i < m_phase.size(); ++i) {
s.set_phase(i, m_phase[i]);

2
src/sat/sat_parallel.h
View file

@ -78,6 +78,8 @@ namespace sat {
void init_solvers(solver& s, unsigned num_extra_solvers);
void push_child(reslimit& rl);
// reserve space
void reserve(unsigned num_owners, unsigned sz) { m_pool.reserve(num_owners, sz); }

3
src/sat/sat_solver.cpp
View file

@ -875,6 +875,9 @@ namespace sat {
sat::parallel par(*this);
par.reserve(num_threads, 1 << 12);
par.init_solvers(*this, num_extra_solvers);
for (unsigned i = 0; i < ls.size(); ++i) {
par.push_child(ls[i]->rlimit());
}
int finished_id = -1;
std::string ex_msg;
par_exception_kind ex_kind;