From 5c11d7f2b30eaf18c05ce2ab098c4745dab200fb Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 1 Mar 2017 10:22:07 -0800 Subject: [PATCH] Sixue's updates Signed-off-by: Nikolaj Bjorner --- src/sat/sat_local_search.cpp | 53 ++++++++++++++++++++++++------------ 1 file changed, 36 insertions(+), 17 deletions(-) diff --git a/src/sat/sat_local_search.cpp b/src/sat/sat_local_search.cpp index 6c210c6c4..b58a1646c 100644 --- a/src/sat/sat_local_search.cpp +++ b/src/sat/sat_local_search.cpp @@ -65,8 +65,9 @@ namespace sat { void local_search::init_cur_solution() { //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); + //std::cout << cur_solution[v] << '\n'; } } @@ -92,7 +93,6 @@ namespace sat { bool is_true = cur_solution[v]; int_vector& truep = 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) { constraint& c = m_constraints[falsep[i]]; // will --slack @@ -298,10 +298,13 @@ namespace sat { bool_var flipvar; timer timer; timer.start(); + bool reach_cutoff_time = false; + double elapsed_time; // ################## start ###################### //std::cout << "Start initialize and local search, restart in every " << max_steps << " steps\n"; + //std::cout << num_vars() << '\n'; unsigned tries, step = 0; - for (tries = 0; m_limit.inc(); ++tries) { + for (tries = 1; ; ++tries) { reinit(); for (step = 1; step <= max_steps; ++step) { // feasible @@ -314,21 +317,36 @@ namespace sat { } flipvar = pick_var(); flip(flipvar); - m_vars[flipvar].m_time_stamp = step; - } - IF_VERBOSE(1, if (tries % 10 == 0) verbose_stream() << tries << ": " << timer.get_seconds() << '\n';); + //std::cout << flipvar << '\t' << m_unsat_stack.size() << '\n'; + //std::cout << goodvar_stack.size() << '\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. - if (m_par && tries % 10 == 0) { - m_par->set_phase(*this); + //if (m_par && tries % 10 == 0) { + //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. m_constraints.shrink(num_constraints); //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 return l_true; } @@ -434,7 +452,6 @@ namespace sat { break; } } - m_vars[flipvar].m_score = -org_flipvar_score; m_vars[flipvar].m_slack_score = -org_flipvar_slack_score; m_vars[flipvar].m_conf_change = false; @@ -457,10 +474,10 @@ namespace sat { unsigned sz = vi.m_neighbors.size(); for (unsigned i = 0; i < sz; ++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)) { 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 // SAT Mode if (m_unsat_stack.empty()) { - //++as; + //std::cout << "as\t"; for (unsigned i = 0; i < ob_constraint.size(); ++i) { bool_var v = ob_constraint[i].var_id; 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 // Within c, from all slack increasing var, choose the oldest one unsigned c_size = c.size(); + //std::cout << "rd\t"; for (unsigned i = 0; i < c_size; ++i) { bool_var v = c[i].var(); if (is_true(c[i]) && time_stamp(v) < time_stamp(best_var)) @@ -538,11 +556,12 @@ namespace sat { void local_search::set_parameters() { m_rand.set_seed(m_config.seed()); + //srand(m_config.seed()); s_id = m_config.strategy_id(); best_known_value = m_config.best_known_value(); if (s_id == 0) - max_steps = 2 * num_vars(); + max_steps = 2 * (num_vars() - 1); else { std::cout << "Invalid strategy id!" << std::endl; exit(-1); @@ -557,8 +576,8 @@ namespace sat { } void local_search::print_info() { - for (unsigned v = 0; 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'; + for (unsigned v = 1; v < num_vars(); ++v) { + 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'; } } }