From 61920503bd088a94a7802660013c2e907f9b5ab5 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 24 Feb 2017 18:13:02 -0800 Subject: [PATCH] hackvector! Signed-off-by: Nikolaj Bjorner --- src/sat/sat_local_search.cpp | 37 +++++++++++++++++++++++++++++------- src/sat/sat_local_search.h | 20 +++++++++++-------- 2 files changed, 42 insertions(+), 15 deletions(-) diff --git a/src/sat/sat_local_search.cpp b/src/sat/sat_local_search.cpp index 6d99ef47d..b9ae4afdc 100644 --- a/src/sat/sat_local_search.cpp +++ b/src/sat/sat_local_search.cpp @@ -179,10 +179,12 @@ namespace sat { } void local_search::add_cardinality(unsigned sz, literal const* c, unsigned k) { - unsigned id = constraint_term.size(); - constraint_term.push_back(svector()); + unsigned id = m_num_constraints; + ++m_num_constraints; + // constraint_term.push_back(svector()); for (unsigned i = 0; i < sz; ++i) { - var_term.reserve(c[i].var() + 1); + m_num_vars = std::max(c[i].var() + 1, m_num_vars); + // var_term.reserve(c[i].var() + 1); term t; t.constraint_id = id; t.var_id = c[i].var(); @@ -195,6 +197,9 @@ namespace sat { local_search::local_search(solver& s) { + m_num_vars = 0; + m_num_constraints = 0; + // copy units unsigned trail_sz = s.init_trail_size(); for (unsigned i = 0; i < trail_sz; ++i) { @@ -329,6 +334,8 @@ namespace sat { void local_search::flip(bool_var flipvar) { + static unsigned_vector hack_vector; + hack_vector.reset(); // already changed truth value!!!! cur_solution[flipvar] = !cur_solution[flipvar]; @@ -360,6 +367,7 @@ namespace sat { ++cscc[v]; //score[v] += constraint_weight[c]; ++m_var_info[v].m_score; + hack_vector.push_back(v); // slack increasing var if (cur_solution[v] == constraint_term[c][j].sense) ++sscore[v]; @@ -392,6 +400,7 @@ namespace sat { if (cur_solution[v] != constraint_term[c][j].sense) { //score[v] += constraint_weight[c]; ++m_var_info[v].m_score; + hack_vector.push_back(v); ++sscore[v]; } } @@ -412,9 +421,11 @@ namespace sat { for (unsigned j = 0; j < constraint_term[c].size(); ++j) { v = constraint_term[c][j].var_id; // flip the slack increasing var will satisfy this constraint - if (cur_solution[v] == constraint_term[c][j].sense) - //score[v] += constraint_weight[c]; - ++m_var_info[v].m_score; + if (cur_solution[v] == constraint_term[c][j].sense) { + //score[v] += constraint_weight[c]; + ++m_var_info[v].m_score; + hack_vector.push_back(v); + } } break; default: @@ -442,6 +453,7 @@ namespace sat { } // update all flipvar's neighbor's conf_change to true, add goodvar/okvar +#if 0 unsigned sz = var_neighbor[flipvar].size(); for (unsigned i = 0; i < sz; ++i) { v = var_neighbor[flipvar][i]; @@ -451,7 +463,18 @@ namespace sat { m_var_info[v].m_in_goodvar_stack = true; } } - +#else + unsigned sz = hack_vector.size(); + for (unsigned i = 0; i < sz; ++i) + { + v = hack_vector[i]; + m_var_info[v].m_conf_change = true; + if (score(v) > 0 && !already_in_goodvar_stack(v)) { + goodvar_stack.push_back(v); + m_var_info[v].m_in_goodvar_stack = true; + } + } +#endif } bool local_search::tie_breaker_sat(bool_var v, bool_var best_var) { diff --git a/src/sat/sat_local_search.h b/src/sat/sat_local_search.h index 97e1974f2..2836ac4e3 100644 --- a/src/sat/sat_local_search.h +++ b/src/sat/sat_local_search.h @@ -28,14 +28,14 @@ namespace sat { unsigned m_seed; unsigned m_cutoff_time; unsigned m_strategy_id; - unsigned m_best_known_value; + int m_best_known_value; public: local_search_config() { m_seed = 0; m_cutoff_time = 1; m_strategy_id = 0; - m_best_known_value = UINT_MAX; + m_best_known_value = INT_MAX; } unsigned seed() const { return m_seed; } @@ -49,6 +49,9 @@ namespace sat { void set_best_known_value(unsigned v) { m_best_known_value = v; } }; +#define MAX_VARS 5000 +#define MAX_CONSTRAINTS 100 + class local_search { typedef svector bool_vector; @@ -73,12 +76,13 @@ namespace sat { // terms arrays - vector > var_term; // var_term[i][j] means the j'th term of var i - vector > constraint_term; // constraint_term[i][j] means the j'th term of constraint i + svector var_term[MAX_VARS]; // var_term[i][j] means the j'th term of var i + svector constraint_term[MAX_CONSTRAINTS]; // constraint_term[i][j] means the j'th term of constraint i + unsigned m_num_vars, m_num_constraints; // parameters of the instance - unsigned num_vars() const { return var_term.size() - 1; } // var index from 1 to num_vars - unsigned num_constraints() const { return constraint_term.size(); } // constraint index from 1 to num_constraint + unsigned num_vars() const { return m_num_vars - 1; } // var index from 1 to num_vars + unsigned num_constraints() const { return m_num_constraints; } // constraint index from 1 to num_constraint // information about the variable @@ -111,7 +115,7 @@ namespace sat { // information about the constraints int_vector constraint_k; // the right side k of a constraint int_vector constraint_slack; // =constraint_k[i]-true_terms[i], if >=0 then sat - //int_vector nb_slack; // constraint_k - ob_var(same in ob) - none_ob_true_terms_count. if < 0: some ob var might be flipped to false, result in an ob decreasing + //int_vector nb_slack; // constraint_k - ob_var(same in ob) - none_ob_true_terms_count. if < 0: some ob var might be flipped to false, result in an ob decreasing //bool_vector has_true_ob_terms; // unsat constraint stack @@ -126,7 +130,7 @@ namespace sat { bool_vector cur_solution; // the current solution int objective_value; // the objective function value corresponds to the current solution bool_vector best_solution; // the best solution so far - int best_objective_value = 0; // the objective value corresponds to the best solution so far + int best_objective_value = -1; // the objective value corresponds to the best solution so far // for non-known instance, set as maximal int best_known_value = INT_MAX; // best known value for this instance