mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-20 12:53:38 +00:00
Code Activity

porting more code

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2017-02-21 21:33:18 -08:00
parent eec1d9ef84
commit eec10c6e32
1 changed files with 168 additions and 158 deletions
Download patch file Download diff file Expand all files Collapse all files

326
src/sat/sat_local_search.cpp
View file

@ -1,21 +1,21 @@
/*++ /*++
Copyright (c) 2017 Microsoft Corporation Copyright (c) 2017 Microsoft Corporation
Module Name: Module Name:
sat_local_search.cpp sat_local_search.cpp
Abstract: Abstract:
Local search module for cardinality clauses. Local search module for cardinality clauses.
Author: Author:
Sixue Liu 2017-2-21 Sixue Liu 2017-2-21
Notes: Notes:
--*/ --*/
#include "sat_local_search.h" #include "sat_local_search.h"
@ -29,7 +29,7 @@ namespace sat {
} }
void local_search::init_orig() { void local_search::init_orig() {
int v, c; int v, c;
for (c = 1; c <= num_constraints; ++c) { for (c = 1; c <= num_constraints; ++c) {
constraint_slack[c] = constraint_k[c]; constraint_slack[c] = constraint_k[c];
@ -108,7 +108,7 @@ namespace sat {
} }
void local_search::init_greedy() { void local_search::init_greedy() {
int v, c; int v, c;
for (c = 1; c <= num_constraints; ++c) { for (c = 1; c <= num_constraints; ++c) {
constraint_slack[c] = constraint_k[c]; constraint_slack[c] = constraint_k[c];
} }
@ -223,100 +223,110 @@ namespace sat {
void local_search::flip(int flipvar) void local_search::flip(int flipvar)
{ {
// already changed truth value!!!! // already changed truth value!!!!
cur_solution[flipvar] = !cur_solution[flipvar]; cur_solution[flipvar] = !cur_solution[flipvar];
int v, c; int v, c;
int org_flipvar_score = score[flipvar]; int org_flipvar_score = score[flipvar];
int org_flipvar_sscore = sscore[flipvar]; int org_flipvar_sscore = sscore[flipvar];
// update related clauses and neighbor vars // update related clauses and neighbor vars
for (unsigned i = 0; i < var_term[flipvar].size(); ++i) { svector<term> const& constraints = var_term[flipvar];
c = var_term[flipvar][i].constraint_id; unsigned num_constraints = constraints.size();
if (cur_solution[flipvar] == var_term[flipvar][i].sense) { for (unsigned i = 0; i < num_constraints; ++i) {
//++true_terms_count[c]; c = constraints[i].constraint_id;
--constraint_slack[c]; if (cur_solution[flipvar] == constraints[i].sense) {
if (constraint_slack[c] == -2) { // from -1 to -2 //++true_terms_count[c];
for (unsigned j = 0; j < constraint_term[c].size(); ++j) { --constraint_slack[c];
v = constraint_term[c][j].var_id; switch (constraint_slack[c]) {
// flipping the slack increasing var will no long sat this constraint case -2: // from -1 to -2
if (cur_solution[v] == constraint_term[c][j].sense) for (unsigned j = 0; j < constraint_term[c].size(); ++j) {
//score[v] -= constraint_weight[c]; v = constraint_term[c][j].var_id;
--score[v]; // flipping the slack increasing var will no long sat this constraint
} if (cur_solution[v] == constraint_term[c][j].sense)
}
else if (constraint_slack[c] == -1) { // from 0 to -1: sat -> unsat
for (unsigned j = 0; j < constraint_term[c].size(); ++j) {
v = constraint_term[c][j].var_id;
++cscc[v];
//score[v] += constraint_weight[c];
++score[v];
// slack increasing var
if (cur_solution[v] == constraint_term[c][j].sense)
++sscore[v];
}
unsat(c);
}
else if (constraint_slack[c] == 0) { // from 1 to 0
for (unsigned j = 0; j < constraint_term[c].size(); ++j) {
v = constraint_term[c][j].var_id;
// flip the slack decreasing var will falsify this constraint
if (cur_solution[v] != constraint_term[c][j].sense) {
//score[v] -= constraint_weight[c];
--score[v];
--sscore[v];
}
}
}
}
else { // if (cur_solution[flipvar] != var_term[i].sense)
//--true_terms_count[c];
++constraint_slack[c];
if (constraint_slack[c] == 1) { // from 0 to 1
for (unsigned j = 0; j < constraint_term[c].size(); ++j) {
v = constraint_term[c][j].var_id;
// flip the slack decreasing var will no long falsify this constraint
if (cur_solution[v] != constraint_term[c][j].sense) {
//score[v] += constraint_weight[c];
++score[v];
++sscore[v];
}
}
}
else if (constraint_slack[c] == 0) { // from -1 to 0: unsat -> sat
for (unsigned j = 0; j < constraint_term[c].size(); ++j) {
v = constraint_term[c][j].var_id;
++cscc[v];
//score[v] -= constraint_weight[c]; //score[v] -= constraint_weight[c];
--score[v]; --score[v];
// slack increasing var no longer sat this var
if (cur_solution[v] == constraint_term[c][j].sense)
--sscore[v];
}
sat(c);
} }
else if (constraint_slack[c] == -1) { // from -2 to -1 break;
for (unsigned j = 0; j < constraint_term[c].size(); ++j) { case -1: // from 0 to -1: sat -> unsat
v = constraint_term[c][j].var_id; for (unsigned j = 0; j < constraint_term[c].size(); ++j) {
// flip the slack increasing var will satisfy this constraint v = constraint_term[c][j].var_id;
if (cur_solution[v] == constraint_term[c][j].sense) ++cscc[v];
//score[v] += constraint_weight[c]; //score[v] += constraint_weight[c];
++score[v]; ++score[v];
// slack increasing var
if (cur_solution[v] == constraint_term[c][j].sense)
++sscore[v];
}
unsat(c);
break;
case 0: // from 1 to 0
for (unsigned j = 0; j < constraint_term[c].size(); ++j) {
v = constraint_term[c][j].var_id;
// flip the slack decreasing var will falsify this constraint
if (cur_solution[v] != constraint_term[c][j].sense) {
//score[v] -= constraint_weight[c];
--score[v];
--sscore[v];
} }
} }
} break;
} default:
break;
}
}
else { // if (cur_solution[flipvar] != var_term[i].sense)
//--true_terms_count[c];
++constraint_slack[c];
switch (constraint_slack[c]) {
case 1: // from 0 to 1
for (unsigned j = 0; j < constraint_term[c].size(); ++j) {
v = constraint_term[c][j].var_id;
// flip the slack decreasing var will no long falsify this constraint
if (cur_solution[v] != constraint_term[c][j].sense) {
//score[v] += constraint_weight[c];
++score[v];
++sscore[v];
}
}
break;
case 0: // from -1 to 0: unsat -> sat
for (unsigned j = 0; j < constraint_term[c].size(); ++j) {
v = constraint_term[c][j].var_id;
++cscc[v];
//score[v] -= constraint_weight[c];
--score[v];
// slack increasing var no longer sat this var
if (cur_solution[v] == constraint_term[c][j].sense)
--sscore[v];
}
sat(c);
break;
case -1: // from -2 to -1
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];
++score[v];
}
break;
default:
break;
}
}
}
score[flipvar] = -org_flipvar_score; score[flipvar] = -org_flipvar_score;
sscore[flipvar] = -org_flipvar_sscore; sscore[flipvar] = -org_flipvar_sscore;
conf_change[flipvar] = false; conf_change[flipvar] = false;
cscc[flipvar] = 0; cscc[flipvar] = 0;
/* update CCD */ /* update CCD */
// remove the vars no longer okvar in okvar stack // remove the vars no longer okvar in okvar stack
// remove the vars no longer goodvar in goodvar stack // remove the vars no longer goodvar in goodvar stack
for (unsigned i = goodvar_stack.size(); i > 0;) { for (unsigned i = goodvar_stack.size(); i > 0;) {
--i; --i;
v = goodvar_stack[i]; v = goodvar_stack[i];
if (score[v] <= 0) { if (score[v] <= 0) {
@ -324,69 +334,69 @@ namespace sat {
goodvar_stack.pop_back(); goodvar_stack.pop_back();
already_in_goodvar_stack[v] = false; already_in_goodvar_stack[v] = false;
} }
} }
// 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
for (unsigned i = 0; i < var_neighbor[flipvar].size(); ++i) { for (unsigned i = 0; i < var_neighbor[flipvar].size(); ++i) {
v = var_neighbor[flipvar][i]; v = var_neighbor[flipvar][i];
conf_change[v] = true; conf_change[v] = 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);
already_in_goodvar_stack[v] = true; already_in_goodvar_stack[v] = true;
} }
} }
} }
bool local_search::tie_breaker_sat(int v, int best_var) bool local_search::tie_breaker_sat(int v, int best_var)
{ {
// most improvement on objective value // most improvement on objective value
int v_imp = cur_solution[v] ? -coefficient_in_ob_constraint[v] : coefficient_in_ob_constraint[v]; int v_imp = cur_solution[v] ? -coefficient_in_ob_constraint[v] : coefficient_in_ob_constraint[v];
int b_imp = cur_solution[best_var] ? -coefficient_in_ob_constraint[best_var] : coefficient_in_ob_constraint[best_var]; int b_imp = cur_solution[best_var] ? -coefficient_in_ob_constraint[best_var] : coefficient_in_ob_constraint[best_var];
// break tie 1: max imp // break tie 1: max imp
if (v_imp > b_imp) if (v_imp > b_imp)
return true; return true;
else if (v_imp == b_imp) { else if (v_imp == b_imp) {
// break tie 2: conf_change // break tie 2: conf_change
if (conf_change[v] && !conf_change[best_var]) if (conf_change[v] && !conf_change[best_var])
return true; return true;
else if (conf_change[v] == conf_change[best_var]) { else if (conf_change[v] == conf_change[best_var]) {
// break tie 3: time_stamp // break tie 3: time_stamp
if (time_stamp[v] < time_stamp[best_var]) if (time_stamp[v] < time_stamp[best_var])
return true; return true;
} }
} }
return false; return false;
} }
bool local_search::tie_breaker_ccd(int v, int best_var) bool local_search::tie_breaker_ccd(int v, int best_var)
{ {
// break tie 1: max score // break tie 1: max score
if (score[v] > score[best_var]) if (score[v] > score[best_var])
return true; return true;
else if (score[v] == score[best_var]) { else if (score[v] == score[best_var]) {
// break tie 2: max sscore // break tie 2: max sscore
if (sscore[v] > sscore[best_var]) if (sscore[v] > sscore[best_var])
return true; return true;
else if (sscore[v] == sscore[best_var]) { else if (sscore[v] == sscore[best_var]) {
// break tie 3: cscc // break tie 3: cscc
if (cscc[v] > cscc[best_var]) if (cscc[v] > cscc[best_var])
return true; return true;
else if (cscc[v] == cscc[best_var]) { else if (cscc[v] == cscc[best_var]) {
// break tie 4: oldest one // break tie 4: oldest one
if (time_stamp[v] < time_stamp[best_var]) if (time_stamp[v] < time_stamp[best_var])
return true; return true;
} }
} }
} }
return false; return false;
} }
int local_search::pick_var() int local_search::pick_var()
{ {
int c, v; int c, v;
int best_var = 0; int best_var = 0;
// SAT Mode // SAT Mode
if (m_unsat_stack.empty()) { if (m_unsat_stack.empty()) {
//++as; //++as;
for (int i = 1; i <= ob_num_terms; ++i) { for (int i = 1; i <= ob_num_terms; ++i) {
v = ob_constraint[i].var_id; v = ob_constraint[i].var_id;
@ -394,11 +404,11 @@ namespace sat {
best_var = v; best_var = v;
} }
return best_var; return best_var;
} }
// Unsat Mode: CCD > RD // Unsat Mode: CCD > RD
// CCD mode // CCD mode
if (!goodvar_stack.empty()) { if (!goodvar_stack.empty()) {
//++ccd; //++ccd;
best_var = goodvar_stack[0]; best_var = goodvar_stack[0];
for (unsigned i = 1; i < goodvar_stack.size(); ++i) { for (unsigned i = 1; i < goodvar_stack.size(); ++i) {
@ -407,35 +417,35 @@ namespace sat {
best_var = v; best_var = v;
} }
return best_var; return best_var;
} }
// Diversification Mode // Diversification Mode
c = m_unsat_stack[rand() % m_unsat_stack.size()]; // a random unsat constraint c = m_unsat_stack[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
for (unsigned i = 0; i < constraint_term[c].size(); ++i) { for (unsigned i = 0; i < constraint_term[c].size(); ++i) {
v = constraint_term[c][i].var_id; v = constraint_term[c][i].var_id;
if (cur_solution[v] == constraint_term[c][i].sense && time_stamp[v] < time_stamp[best_var]) if (cur_solution[v] == constraint_term[c][i].sense && time_stamp[v] < time_stamp[best_var])
best_var = v; best_var = v;
} }
//++rd; //++rd;
return best_var; return best_var;
} }
void local_search::set_parameters() { void local_search::set_parameters() {
if (s_id == 0) if (s_id == 0)
max_steps = num_vars; max_steps = num_vars;
else if (s_id == 1) else if (s_id == 1)
max_steps = (int) (1.5 * num_vars); max_steps = (int) (1.5 * num_vars);
else if (s_id == 1) else if (s_id == 1)
max_steps = 2 * num_vars; max_steps = 2 * num_vars;
else if (s_id == 2) else if (s_id == 2)
max_steps = (int) (2.5 * num_vars); max_steps = (int) (2.5 * num_vars);
else if (s_id == 3) else if (s_id == 3)
max_steps = 3 * num_vars; max_steps = 3 * num_vars;
else { else {
std::cout << "Invalid strategy id!" << std::endl; std::cout << "Invalid strategy id!" << std::endl;
exit(-1); exit(-1);
} }
} }