mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-24 21:26:59 +00:00
Code Activity

hackvector!

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2017-02-24 18:13:02 -08:00
parent e407b81f70
commit 61920503bd
2 changed files with 42 additions and 15 deletions
Download patch file Download diff file Expand all files Collapse all files

37
src/sat/sat_local_search.cpp
View file

@ -179,10 +179,12 @@ namespace sat {
} }
void local_search::add_cardinality(unsigned sz, literal const* c, unsigned k) { void local_search::add_cardinality(unsigned sz, literal const* c, unsigned k) {
unsigned id = constraint_term.size(); unsigned id = m_num_constraints;
constraint_term.push_back(svector<term>()); ++m_num_constraints;
// constraint_term.push_back(svector<term>());
for (unsigned i = 0; i < sz; ++i) { 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; term t;
t.constraint_id = id; t.constraint_id = id;
t.var_id = c[i].var(); t.var_id = c[i].var();
@ -195,6 +197,9 @@ namespace sat {
local_search::local_search(solver& s) { local_search::local_search(solver& s) {
m_num_vars = 0;
m_num_constraints = 0;
// copy units // copy units
unsigned trail_sz = s.init_trail_size(); unsigned trail_sz = s.init_trail_size();
for (unsigned i = 0; i < trail_sz; ++i) { for (unsigned i = 0; i < trail_sz; ++i) {
@ -329,6 +334,8 @@ namespace sat {
void local_search::flip(bool_var flipvar) void local_search::flip(bool_var flipvar)
{ {
static unsigned_vector hack_vector;
hack_vector.reset();
// already changed truth value!!!! // already changed truth value!!!!
cur_solution[flipvar] = !cur_solution[flipvar]; cur_solution[flipvar] = !cur_solution[flipvar];
@ -360,6 +367,7 @@ namespace sat {
++cscc[v]; ++cscc[v];
//score[v] += constraint_weight[c]; //score[v] += constraint_weight[c];
++m_var_info[v].m_score; ++m_var_info[v].m_score;
hack_vector.push_back(v);
// slack increasing var // slack increasing var
if (cur_solution[v] == constraint_term[c][j].sense) if (cur_solution[v] == constraint_term[c][j].sense)
++sscore[v]; ++sscore[v];
@ -392,6 +400,7 @@ namespace sat {
if (cur_solution[v] != constraint_term[c][j].sense) { if (cur_solution[v] != constraint_term[c][j].sense) {
//score[v] += constraint_weight[c]; //score[v] += constraint_weight[c];
++m_var_info[v].m_score; ++m_var_info[v].m_score;
hack_vector.push_back(v);
++sscore[v]; ++sscore[v];
} }
} }
@ -412,9 +421,11 @@ namespace sat {
for (unsigned j = 0; j < constraint_term[c].size(); ++j) { for (unsigned j = 0; j < constraint_term[c].size(); ++j) {
v = constraint_term[c][j].var_id; v = constraint_term[c][j].var_id;
// flip the slack increasing var will satisfy this constraint // flip the slack increasing var will satisfy this constraint
if (cur_solution[v] == constraint_term[c][j].sense) if (cur_solution[v] == constraint_term[c][j].sense) {
//score[v] += constraint_weight[c]; //score[v] += constraint_weight[c];
++m_var_info[v].m_score; ++m_var_info[v].m_score;
hack_vector.push_back(v);
}
} }
break; break;
default: default:
@ -442,6 +453,7 @@ namespace sat {
} }
// update all flipvar's neighbor's conf_change to true, add goodvar/okvar // update all flipvar's neighbor's conf_change to true, add goodvar/okvar
#if 0
unsigned sz = var_neighbor[flipvar].size(); unsigned sz = var_neighbor[flipvar].size();
for (unsigned i = 0; i < sz; ++i) { for (unsigned i = 0; i < sz; ++i) {
v = var_neighbor[flipvar][i]; v = var_neighbor[flipvar][i];
@ -451,7 +463,18 @@ namespace sat {
m_var_info[v].m_in_goodvar_stack = true; 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) { bool local_search::tie_breaker_sat(bool_var v, bool_var best_var) {

20
src/sat/sat_local_search.h
View file

@ -28,14 +28,14 @@ namespace sat {
unsigned m_seed; unsigned m_seed;
unsigned m_cutoff_time; unsigned m_cutoff_time;
unsigned m_strategy_id; unsigned m_strategy_id;
unsigned m_best_known_value; int m_best_known_value;
public: public:
local_search_config() local_search_config()
{ {
m_seed = 0; m_seed = 0;
m_cutoff_time = 1; m_cutoff_time = 1;
m_strategy_id = 0; m_strategy_id = 0;
m_best_known_value = UINT_MAX; m_best_known_value = INT_MAX;
} }
unsigned seed() const { return m_seed; } unsigned seed() const { return m_seed; }
@ -49,6 +49,9 @@ namespace sat {
void set_best_known_value(unsigned v) { m_best_known_value = v; } void set_best_known_value(unsigned v) { m_best_known_value = v; }
}; };
#define MAX_VARS 5000
#define MAX_CONSTRAINTS 100
class local_search { class local_search {
typedef svector<bool> bool_vector; typedef svector<bool> bool_vector;
@ -73,12 +76,13 @@ namespace sat {
// terms arrays // terms arrays
vector<svector<term> > var_term; // var_term[i][j] means the j'th term of var i svector<term> var_term[MAX_VARS]; // var_term[i][j] means the j'th term of var i
vector<svector<term> > constraint_term; // constraint_term[i][j] means the j'th term of constraint i svector<term> 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 // parameters of the instance
unsigned num_vars() const { return var_term.size() - 1; } // var index from 1 to num_vars unsigned num_vars() const { return m_num_vars - 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_constraints() const { return m_num_constraints; } // constraint index from 1 to num_constraint
// information about the variable // information about the variable
@ -111,7 +115,7 @@ namespace sat {
// information about the constraints // information about the constraints
int_vector constraint_k; // the right side k of a constraint 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 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; //bool_vector has_true_ob_terms;
// unsat constraint stack // unsat constraint stack
@ -126,7 +130,7 @@ namespace sat {
bool_vector cur_solution; // the current solution bool_vector cur_solution; // the current solution
int objective_value; // the objective function value corresponds to the current solution int objective_value; // the objective function value corresponds to the current solution
bool_vector best_solution; // the best solution so far 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 // for non-known instance, set as maximal
int best_known_value = INT_MAX; // best known value for this instance int best_known_value = INT_MAX; // best known value for this instance