mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 13:28:47 +00:00
Code Activity

Sixue's updates

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2017-03-01 10:22:07 -08:00
parent fb4f6d654a
commit 5c11d7f2b3
1 changed files with 36 additions and 17 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

53
src/sat/sat_local_search.cpp
View file

@ -65,8 +65,9 @@ namespace sat {
void local_search::init_cur_solution() { void local_search::init_cur_solution() {
//cur_solution.resize(num_vars() + 1, false); //cur_solution.resize(num_vars() + 1, false);
for (unsigned v = 0; v < num_vars(); ++v) { for (unsigned v = 1; v < num_vars(); ++v) {
cur_solution[v] = (m_rand() % 2 == 1); cur_solution[v] = (m_rand() % 2 == 1);
//std::cout << cur_solution[v] << '\n';
} }
} }
@ -92,7 +93,6 @@ namespace sat {
bool is_true = cur_solution[v]; bool is_true = cur_solution[v];
int_vector& truep = m_vars[v].m_watch[is_true]; int_vector& truep = m_vars[v].m_watch[is_true];
int_vector& falsep = m_vars[v].m_watch[!is_true]; int_vector& falsep = m_vars[v].m_watch[!is_true];
for (unsigned i = 0; i < falsep.size(); ++i) { for (unsigned i = 0; i < falsep.size(); ++i) {
constraint& c = m_constraints[falsep[i]]; constraint& c = m_constraints[falsep[i]];
// will --slack // will --slack
@ -298,10 +298,13 @@ namespace sat {
bool_var flipvar; bool_var flipvar;
timer timer; timer timer;
timer.start(); timer.start();
bool reach_cutoff_time = false;
double elapsed_time;
// ################## start ###################### // ################## start ######################
//std::cout << "Start initialize and local search, restart in every " << max_steps << " steps\n"; //std::cout << "Start initialize and local search, restart in every " << max_steps << " steps\n";
//std::cout << num_vars() << '\n';
unsigned tries, step = 0; unsigned tries, step = 0;
for (tries = 0; m_limit.inc(); ++tries) { for (tries = 1; ; ++tries) {
reinit(); reinit();
for (step = 1; step <= max_steps; ++step) { for (step = 1; step <= max_steps; ++step) {
// feasible // feasible
@ -314,21 +317,36 @@ namespace sat {
} }
flipvar = pick_var(); flipvar = pick_var();
flip(flipvar); flip(flipvar);
m_vars[flipvar].m_time_stamp = step; //std::cout << flipvar << '\t' << m_unsat_stack.size() << '\n';
} //std::cout << goodvar_stack.size() << '\n';
IF_VERBOSE(1, if (tries % 10 == 0) verbose_stream() << tries << ": " << timer.get_seconds() << '\n';);
m_vars[flipvar].m_time_stamp = step;
//if (!m_limit.inc()) break;pick_flip();
}
//IF_VERBOSE(1, if (tries % 10 == 0) verbose_stream() << tries << ": " << timer.get_seconds() << '\n';);
// the following is for tesing
if (tries % 10 == 0) {
elapsed_time = timer.get_seconds();
//std::cout << tries << '\t' << elapsed_time << '\n';
if (elapsed_time > 300) {
reach_cutoff_time = true;
break;
}
}
// tell the SAT solvers about the phase of variables. // tell the SAT solvers about the phase of variables.
if (m_par && tries % 10 == 0) { //if (m_par && tries % 10 == 0) {
m_par->set_phase(*this); //m_par->set_phase(*this);
if (reach_known_best_value || reach_cutoff_time) {
break;
} }
} }
IF_VERBOSE(1, verbose_stream() << timer.get_seconds() << " " << (reach_known_best_value ? "reached":"not reached") << "\n";); std::cout << elapsed_time << '\t' << reach_known_best_value << '\t' << reach_cutoff_time << '\t' << best_objective_value << '\n';
//IF_VERBOSE(1, verbose_stream() << timer.get_seconds() << " " << (reach_known_best_value ? "reached":"not reached") << "\n";);
// remove unit clauses from assumptions. // remove unit clauses from assumptions.
m_constraints.shrink(num_constraints); m_constraints.shrink(num_constraints);
//print_solution(); //print_solution();
IF_VERBOSE(1, verbose_stream() << tries * max_steps + step << '\n';); IF_VERBOSE(1, verbose_stream() << (tries - 1) * max_steps + step << '\n';);
if (m_unsat_stack.empty() && ob_constraint.empty()) { // or all variables in ob_constraint are true if (m_unsat_stack.empty() && ob_constraint.empty()) { // or all variables in ob_constraint are true
return l_true; return l_true;
} }
@ -434,7 +452,6 @@ namespace sat {
break; break;
} }
} }
m_vars[flipvar].m_score = -org_flipvar_score; m_vars[flipvar].m_score = -org_flipvar_score;
m_vars[flipvar].m_slack_score = -org_flipvar_slack_score; m_vars[flipvar].m_slack_score = -org_flipvar_slack_score;
m_vars[flipvar].m_conf_change = false; m_vars[flipvar].m_conf_change = false;
@ -457,10 +474,10 @@ namespace sat {
unsigned sz = vi.m_neighbors.size(); unsigned sz = vi.m_neighbors.size();
for (unsigned i = 0; i < sz; ++i) { for (unsigned i = 0; i < sz; ++i) {
v = vi.m_neighbors[i]; v = vi.m_neighbors[i];
vi.m_conf_change = true; m_vars[v].m_conf_change = true;
if (score(v) > 0 && !already_in_goodvar_stack(v)) { if (score(v) > 0 && !already_in_goodvar_stack(v)) {
goodvar_stack.push_back(v); goodvar_stack.push_back(v);
vi.m_in_goodvar_stack = true; m_vars[v].m_in_goodvar_stack = true;
} }
} }
} }
@ -501,7 +518,7 @@ namespace sat {
bool_var best_var = m_vars.size()-1; // sentinel variable bool_var best_var = m_vars.size()-1; // sentinel variable
// SAT Mode // SAT Mode
if (m_unsat_stack.empty()) { if (m_unsat_stack.empty()) {
//++as; //std::cout << "as\t";
for (unsigned i = 0; i < ob_constraint.size(); ++i) { for (unsigned i = 0; i < ob_constraint.size(); ++i) {
bool_var v = ob_constraint[i].var_id; bool_var v = ob_constraint[i].var_id;
if (tie_breaker_sat(v, best_var)) if (tie_breaker_sat(v, best_var))
@ -527,6 +544,7 @@ namespace sat {
constraint const& c = m_constraints[m_unsat_stack[m_rand() % m_unsat_stack.size()]]; // a random unsat constraint constraint const& c = m_constraints[m_unsat_stack[m_rand() % m_unsat_stack.size()]]; // a random unsat constraint
// Within c, from all slack increasing var, choose the oldest one // Within c, from all slack increasing var, choose the oldest one
unsigned c_size = c.size(); unsigned c_size = c.size();
//std::cout << "rd\t";
for (unsigned i = 0; i < c_size; ++i) { for (unsigned i = 0; i < c_size; ++i) {
bool_var v = c[i].var(); bool_var v = c[i].var();
if (is_true(c[i]) && time_stamp(v) < time_stamp(best_var)) if (is_true(c[i]) && time_stamp(v) < time_stamp(best_var))
@ -538,11 +556,12 @@ namespace sat {
void local_search::set_parameters() { void local_search::set_parameters() {
m_rand.set_seed(m_config.seed()); m_rand.set_seed(m_config.seed());
//srand(m_config.seed());
s_id = m_config.strategy_id(); s_id = m_config.strategy_id();
best_known_value = m_config.best_known_value(); best_known_value = m_config.best_known_value();
if (s_id == 0) if (s_id == 0)
max_steps = 2 * num_vars(); max_steps = 2 * (num_vars() - 1);
else { else {
std::cout << "Invalid strategy id!" << std::endl; std::cout << "Invalid strategy id!" << std::endl;
exit(-1); exit(-1);
@ -557,8 +576,8 @@ namespace sat {
} }
void local_search::print_info() { void local_search::print_info() {
for (unsigned v = 0; v < num_vars(); ++v) { for (unsigned v = 1; v < num_vars(); ++v) {
std::cout << m_vars[v].m_neighbors.size() << '\t' << cur_solution[v] << '\t' << conf_change(v) << '\t' << score(v) << '\t' << slack_score(v) << '\n'; std::cout << v << "\t" << m_vars[v].m_neighbors.size() << '\t' << cur_solution[v] << '\t' << conf_change(v) << '\t' << score(v) << '\t' << slack_score(v) << '\n';
} }
} }
} }