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

updates

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2017-02-27 21:13:52 -08:00
parent 475101e932
commit c205b59a21
2 changed files with 41 additions and 48 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

62
src/sat/sat_local_search.cpp
View file

@ -26,31 +26,32 @@ namespace sat {
void local_search::init() {
// add sentinel variable.
m_vars.push_back(var_info());
best_solution.resize(num_vars() + 1, false);
cur_solution.resize(num_vars() + 1, false);
m_index_in_unsat_stack.resize(num_constraints(), 0);
coefficient_in_ob_constraint.resize(num_vars() + 1, 0);
var_neighbor.reset();
// for dummy var 0
var_neighbor.push_back(bool_var_vector());
for (bool_var v = 1; v <= num_vars(); ++v) {
bool_vector is_neighbor(num_vars() + 1, false);
var_neighbor.push_back(bool_var_vector());
uint_set is_neighbor;
for (bool_var v = 0; v < num_vars(); ++v) {
is_neighbor.reset();
bool pol = true;
var_info& vi = m_vars[v];
for (unsigned k = 0; k < 2; pol = !pol, k++) {
for (unsigned i = 0; i < m_vars[v].m_watch[pol].size(); ++i) {
constraint const& c = m_constraints[m_vars[v].m_watch[pol][i]];
for (unsigned j = 0; j < c.size(); ++j) {
bool_var w = c[j].var();
if (w == v || is_neighbor[w]) continue;
is_neighbor[w] = true;
var_neighbor.back().push_back(w);
if (w == v || is_neighbor.contains(w)) continue;
is_neighbor.insert(w);
vi.m_neighbors.push_back(w);
}
}
}
}
for (unsigned i = 0; i < ob_constraint.size(); ++i)
coefficient_in_ob_constraint[ob_constraint[i].var_id] = ob_constraint[i].coefficient;
@ -63,7 +64,7 @@ namespace sat {
void local_search::init_cur_solution() {
//cur_solution.resize(num_vars() + 1, false);
for (unsigned v = 1; v <= num_vars(); ++v) {
for (unsigned v = 0; v < num_vars(); ++v) {
cur_solution[v] = (rand() % 2 == 1);
}
}
@ -86,7 +87,7 @@ namespace sat {
// figure out variables scores and slack_scores
void local_search::init_scores() {
for (unsigned v = 1; v <= num_vars(); ++v) {
for (unsigned v = 0; v < num_vars(); ++v) {
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];
@ -116,7 +117,7 @@ namespace sat {
// init goodvars
void local_search::init_goodvars() {
goodvar_stack.reset();
for (unsigned v = 1; v <= num_vars(); ++v) {
for (unsigned v = 0; v < num_vars(); ++v) {
if (score(v) > 0) { // && conf_change[v] == true
m_vars[v].m_in_goodvar_stack = true;
goodvar_stack.push_back(v);
@ -139,12 +140,12 @@ namespace sat {
// init varibale information
// variable 0 is the virtual variable
m_vars[0].m_score = INT_MIN;
m_vars[0].m_conf_change = false;
m_vars[0].m_slack_score = INT_MIN;
m_vars[0].m_cscc = 0;
m_vars[0].m_time_stamp = max_steps + 1;
for (unsigned i = 1; i < m_vars.size(); ++i) {
m_vars.back().m_score = INT_MIN;
m_vars.back().m_conf_change = false;
m_vars.back().m_slack_score = INT_MIN;
m_vars.back().m_cscc = 0;
m_vars.back().m_time_stamp = max_steps + 1;
for (unsigned i = 0; i < num_vars(); ++i) {
m_vars[i].m_time_stamp = 0;
m_vars[i].m_cscc = 1;
m_vars[i].m_conf_change = true;
@ -448,13 +449,14 @@ namespace sat {
}
// update all flipvar's neighbor's conf_change to true, add goodvar/okvar
unsigned sz = var_neighbor[flipvar].size();
var_info& vi = m_vars[flipvar];
unsigned sz = vi.m_neighbors.size();
for (unsigned i = 0; i < sz; ++i) {
v = var_neighbor[flipvar][i];
m_vars[v].m_conf_change = true;
v = vi.m_neighbors[i];
vi.m_conf_change = true;
if (score(v) > 0 && !already_in_goodvar_stack(v)) {
goodvar_stack.push_back(v);
m_vars[v].m_in_goodvar_stack = true;
vi.m_in_goodvar_stack = true;
}
}
@ -493,14 +495,12 @@ namespace sat {
}
bool_var local_search::pick_var() {
int v;
bool_var best_var = 0;
bool_var best_var = m_vars.size()-1; // sentinel variable
// SAT Mode
if (m_unsat_stack.empty()) {
//++as;
for (unsigned i = 0; i < ob_constraint.size(); ++i) {
v = ob_constraint[i].var_id;
bool_var v = ob_constraint[i].var_id;
if (tie_breaker_sat(v, best_var))
best_var = v;
}
@ -513,7 +513,7 @@ namespace sat {
//++ccd;
best_var = goodvar_stack[0];
for (unsigned i = 1; i < goodvar_stack.size(); ++i) {
v = goodvar_stack[i];
bool_var v = goodvar_stack[i];
if (tie_breaker_ccd(v, best_var))
best_var = v;
}
@ -525,7 +525,7 @@ namespace sat {
// Within c, from all slack increasing var, choose the oldest one
unsigned c_size = c.size();
for (unsigned i = 0; i < c_size; ++i) {
v = c[i].var();
bool_var v = c[i].var();
if (is_true(c[i]) && time_stamp(v) < time_stamp(best_var))
best_var = v;
}
@ -557,8 +557,8 @@ namespace sat {
}
void local_search::print_info() {
for (unsigned v = 1; v <= num_vars(); ++v) {
std::cout << var_neighbor[v].size() << '\t' << cur_solution[v] << '\t' << conf_change(v) << '\t' << score(v) << '\t' << slack_score(v) << '\n';
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';
}
}
}

27
src/sat/sat_local_search.h
View file

@ -81,35 +81,35 @@ namespace sat {
int m_slack_score;
int m_time_stamp; // the flip time stamp
int m_cscc; // how many times its constraint state configure changes since its last flip
bool_var_vector m_neighbors; // neighborhood variables
int_vector m_watch[2];
var_info():
m_conf_change(true),
m_in_goodvar_stack(false),
m_score(0),
m_slack_score(0)
m_slack_score(0),
m_cscc(0)
{}
};
svector<var_info> m_vars;
inline int score(unsigned v) const { return m_vars[v].m_score; }
vector<var_info> m_vars;
inline int score(bool_var v) const { return m_vars[v].m_score; }
inline void inc_score(bool_var v) { m_vars[v].m_score++; }
inline void dec_score(bool_var v) { m_vars[v].m_score--; }
inline int slack_score(unsigned v) const { return m_vars[v].m_slack_score; }
inline int slack_score(bool_var v) const { return m_vars[v].m_slack_score; }
inline void inc_slack_score(bool_var v) { m_vars[v].m_slack_score++; }
inline void dec_slack_score(bool_var v) { m_vars[v].m_slack_score--; }
inline bool already_in_goodvar_stack(unsigned v) const { return m_vars[v].m_in_goodvar_stack; }
inline bool conf_change(unsigned v) const { return m_vars[v].m_conf_change; }
inline bool already_in_goodvar_stack(bool_var v) const { return m_vars[v].m_in_goodvar_stack; }
inline bool conf_change(bool_var v) const { return m_vars[v].m_conf_change; }
inline int time_stamp(bool_var v) const { return m_vars[v].m_time_stamp; }
inline int cscc(bool_var v) const { return m_vars[v].m_cscc; }
inline void inc_cscc(bool_var v) { m_vars[v].m_cscc++; }
unsigned num_vars() const { return m_vars.size() - 1; } // var index from 1 to num_vars
vector<bool_var_vector> var_neighbor; // all of its neighborhoods variable
/* TBD: other scores */
struct constraint {
@ -123,19 +123,12 @@ namespace sat {
vector<constraint> m_constraints;
// terms arrays
// vector<svector<term> > constraint_term; // constraint_term[i][j] means the j'th term of constraint i
inline bool is_pos(literal t) const { return !t.sign(); }
inline bool is_true(literal l) const { return cur_solution[l.var()] != l.sign(); }
inline bool is_false(literal l) const { return cur_solution[l.var()] == l.sign(); }
// parameters of the instance
unsigned num_constraints() const { return m_constraints.size(); } // constraint index from 1 to num_constraint
// 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
// bool_vector has_true_ob_terms;