mirror of
https://github.com/Z3Prover/z3
synced 2025-04-15 13:28:47 +00:00
porting more code
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner
parent
747ff19aba
commit
eec1d9ef84
|
|
@ -22,28 +22,175 @@ Notes:
|
|||
namespace sat {
|
||||
|
||||
void local_search::init() {
|
||||
|
||||
constraint_slack.resize(num_constraints + 1);
|
||||
cur_solution.resize(num_vars + 1);
|
||||
// etc. initialize other vectors.
|
||||
init_greedy();
|
||||
}
|
||||
|
||||
bool_var local_search::pick_var() {
|
||||
void local_search::init_orig() {
|
||||
int v, c;
|
||||
|
||||
return null_bool_var;
|
||||
for (c = 1; c <= num_constraints; ++c) {
|
||||
constraint_slack[c] = constraint_k[c];
|
||||
}
|
||||
|
||||
// init unsat stack
|
||||
m_unsat_stack.reset();
|
||||
|
||||
// init solution: random now
|
||||
init_cur_solution();
|
||||
|
||||
// init varibale information
|
||||
// variable 0 is the virtual variable
|
||||
|
||||
score.resize(num_vars+1, 0); score[0] = INT_MIN;
|
||||
sscore.resize(num_vars+1, 0); sscore[0] = INT_MIN;
|
||||
time_stamp.resize(num_vars+1, 0); time_stamp[0] = max_steps;
|
||||
conf_change.resize(num_vars+1, true); conf_change[0] = false;
|
||||
cscc.resize(num_vars+1, 1); cscc[0] = 0;
|
||||
|
||||
// figure out slack, and init unsat stack
|
||||
for (c = 1; c <= num_constraints; ++c) {
|
||||
for (unsigned i = 0; i < constraint_term[c].size(); ++i) {
|
||||
v = constraint_term[c][i].var_id;
|
||||
if (cur_solution[v] == constraint_term[c][i].sense)
|
||||
--constraint_slack[c];
|
||||
}
|
||||
// constraint_slack[c] = constraint_k[c] - true_terms_count[c];
|
||||
// violate the at-most-k constraint
|
||||
if (constraint_slack[c] < 0)
|
||||
unsat(c);
|
||||
}
|
||||
|
||||
// figure out variables scores, pscores and sscores
|
||||
for (v = 1; v <= num_vars; ++v) {
|
||||
for (unsigned i = 0; i < var_term[v].size(); ++i) {
|
||||
c = var_term[v][i].constraint_id;
|
||||
if (cur_solution[v] != var_term[v][i].sense) {
|
||||
// will ++true_terms_count[c]
|
||||
// will --slack
|
||||
if (constraint_slack[c] <= 0) {
|
||||
--sscore[v];
|
||||
if (constraint_slack[c] == 0)
|
||||
--score[v];
|
||||
}
|
||||
}
|
||||
else { // if (cur_solution[v] == var_term[v][i].sense)
|
||||
// will --true_terms_count[c]
|
||||
// will ++slack
|
||||
if (constraint_slack[c] <= -1) {
|
||||
++sscore[v];
|
||||
if (constraint_slack[c] == -1)
|
||||
++score[v];
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
// TBD: maybe use util\uint_set or tracked_uint_set instead?
|
||||
|
||||
// init goodvars and okvars stack
|
||||
for (v = 1; v <= num_vars; ++v) {
|
||||
if (score[v] > 0) { // && conf_change[v] == true
|
||||
already_in_goodvar_stack[v] = true;
|
||||
goodvar_stack.push_back(v);
|
||||
}
|
||||
else
|
||||
already_in_goodvar_stack[v] = false;
|
||||
}
|
||||
}
|
||||
|
||||
void local_search::flip(bool_var v) {
|
||||
|
||||
|
||||
void local_search::init_cur_solution() {
|
||||
for (int v = 1; v <= num_vars; ++v) {
|
||||
cur_solution[v] = (rand() % 2 == 1);
|
||||
}
|
||||
}
|
||||
|
||||
bool local_search::tie_breaker_sat(int, int) {
|
||||
|
||||
return false;
|
||||
}
|
||||
|
||||
bool local_search::tie_breaker_ccd(int, int) {
|
||||
|
||||
return false;
|
||||
void local_search::init_greedy() {
|
||||
int v, c;
|
||||
for (c = 1; c <= num_constraints; ++c) {
|
||||
constraint_slack[c] = constraint_k[c];
|
||||
}
|
||||
|
||||
// init unsat stack
|
||||
m_unsat_stack.reset();
|
||||
|
||||
// init solution: greedy
|
||||
init_cur_solution();
|
||||
|
||||
// init varibale information
|
||||
// variable 0 is the virtual variable
|
||||
score[0] = INT_MIN;
|
||||
sscore[0] = INT_MIN;
|
||||
time_stamp[0] = max_steps;
|
||||
conf_change[0] = false;
|
||||
cscc[0] = 0;
|
||||
for (v = 1; v <= num_vars; ++v) {
|
||||
score[v] = 0;
|
||||
sscore[v] = 0;
|
||||
time_stamp[v] = 0;
|
||||
conf_change[v] = true;
|
||||
cscc[v] = 1;
|
||||
// greedy here!!
|
||||
if (coefficient_in_ob_constraint[v] > 0) {
|
||||
cur_solution[v] = true;
|
||||
}
|
||||
else if (coefficient_in_ob_constraint[v] < 0) {
|
||||
cur_solution[v] = false;
|
||||
}
|
||||
}
|
||||
|
||||
// figure out slack, and init unsat stack
|
||||
for (c = 1; c <= num_constraints; ++c) {
|
||||
for (unsigned i = 0; i < constraint_term[c].size(); ++i) {
|
||||
v = constraint_term[c][i].var_id;
|
||||
if (cur_solution[v] == constraint_term[c][i].sense)
|
||||
//++true_terms_count[c];
|
||||
--constraint_slack[c];
|
||||
}
|
||||
//constraint_slack[c] = constraint_k[c] - true_terms_count[c];
|
||||
// violate the at-most-k constraint
|
||||
if (constraint_slack[c] < 0)
|
||||
unsat(c);
|
||||
}
|
||||
|
||||
// figure out variables scores, pscores and sscores
|
||||
for (v = 1; v <= num_vars; ++v) {
|
||||
for (unsigned i = 0; i < var_term[v].size(); ++i) {
|
||||
c = var_term[v][i].constraint_id;
|
||||
if (cur_solution[v] != var_term[v][i].sense) {
|
||||
// will ++true_terms_count[c]
|
||||
// will --slack
|
||||
if (constraint_slack[c] <= 0) {
|
||||
--sscore[v];
|
||||
if (constraint_slack[c] == 0)
|
||||
--score[v];
|
||||
}
|
||||
}
|
||||
else { // if (cur_solution[v] == var_term[v][i].sense)
|
||||
// will --true_terms_count[c]
|
||||
// will ++slack
|
||||
if (constraint_slack[c] <= -1) {
|
||||
++sscore[v];
|
||||
if (constraint_slack[c] == -1)
|
||||
++score[v];
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
// init goodvars and okvars stack
|
||||
for (v = 1; v <= num_vars; ++v) {
|
||||
if (score[v] > 0) { // && conf_change[v] == true
|
||||
already_in_goodvar_stack[v] = true;
|
||||
goodvar_stack.push_back(v);
|
||||
}
|
||||
else
|
||||
already_in_goodvar_stack[v] = false;
|
||||
}
|
||||
}
|
||||
|
||||
|
||||
void local_search::calculate_and_update_ob() {
|
||||
|
||||
|
|
@ -72,6 +219,225 @@ namespace sat {
|
|||
lbool local_search::operator()() {
|
||||
return l_undef;
|
||||
}
|
||||
|
||||
|
||||
void local_search::flip(int flipvar)
|
||||
{
|
||||
// already changed truth value!!!!
|
||||
cur_solution[flipvar] = !cur_solution[flipvar];
|
||||
|
||||
int v, c;
|
||||
int org_flipvar_score = score[flipvar];
|
||||
int org_flipvar_sscore = sscore[flipvar];
|
||||
|
||||
// update related clauses and neighbor vars
|
||||
for (unsigned i = 0; i < var_term[flipvar].size(); ++i) {
|
||||
c = var_term[flipvar][i].constraint_id;
|
||||
if (cur_solution[flipvar] == var_term[flipvar][i].sense) {
|
||||
//++true_terms_count[c];
|
||||
--constraint_slack[c];
|
||||
if (constraint_slack[c] == -2) { // from -1 to -2
|
||||
for (unsigned j = 0; j < constraint_term[c].size(); ++j) {
|
||||
v = constraint_term[c][j].var_id;
|
||||
// flipping the slack increasing var will no long sat this constraint
|
||||
if (cur_solution[v] == constraint_term[c][j].sense)
|
||||
//score[v] -= constraint_weight[c];
|
||||
--score[v];
|
||||
}
|
||||
}
|
||||
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];
|
||||
// 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
|
||||
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];
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
score[flipvar] = -org_flipvar_score;
|
||||
sscore[flipvar] = -org_flipvar_sscore;
|
||||
|
||||
conf_change[flipvar] = false;
|
||||
cscc[flipvar] = 0;
|
||||
|
||||
/* update CCD */
|
||||
// remove the vars no longer okvar in okvar stack
|
||||
// remove the vars no longer goodvar in goodvar stack
|
||||
for (unsigned i = goodvar_stack.size(); i > 0;) {
|
||||
--i;
|
||||
v = goodvar_stack[i];
|
||||
if (score[v] <= 0) {
|
||||
goodvar_stack[i] = goodvar_stack.back();
|
||||
goodvar_stack.pop_back();
|
||||
already_in_goodvar_stack[v] = false;
|
||||
}
|
||||
}
|
||||
// update all flipvar's neighbor's conf_change to true, add goodvar/okvar
|
||||
for (unsigned i = 0; i < var_neighbor[flipvar].size(); ++i) {
|
||||
v = var_neighbor[flipvar][i];
|
||||
conf_change[v] = true;
|
||||
if (score[v] > 0 && !already_in_goodvar_stack[v]) {
|
||||
goodvar_stack.push_back(v);
|
||||
already_in_goodvar_stack[v] = true;
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
bool local_search::tie_breaker_sat(int v, int best_var)
|
||||
{
|
||||
// most improvement on objective value
|
||||
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];
|
||||
// break tie 1: max imp
|
||||
if (v_imp > b_imp)
|
||||
return true;
|
||||
else if (v_imp == b_imp) {
|
||||
// break tie 2: conf_change
|
||||
if (conf_change[v] && !conf_change[best_var])
|
||||
return true;
|
||||
else if (conf_change[v] == conf_change[best_var]) {
|
||||
// break tie 3: time_stamp
|
||||
if (time_stamp[v] < time_stamp[best_var])
|
||||
return true;
|
||||
}
|
||||
}
|
||||
return false;
|
||||
}
|
||||
|
||||
bool local_search::tie_breaker_ccd(int v, int best_var)
|
||||
{
|
||||
// break tie 1: max score
|
||||
if (score[v] > score[best_var])
|
||||
return true;
|
||||
else if (score[v] == score[best_var]) {
|
||||
// break tie 2: max sscore
|
||||
if (sscore[v] > sscore[best_var])
|
||||
return true;
|
||||
else if (sscore[v] == sscore[best_var]) {
|
||||
// break tie 3: cscc
|
||||
if (cscc[v] > cscc[best_var])
|
||||
return true;
|
||||
else if (cscc[v] == cscc[best_var]) {
|
||||
// break tie 4: oldest one
|
||||
if (time_stamp[v] < time_stamp[best_var])
|
||||
return true;
|
||||
}
|
||||
}
|
||||
}
|
||||
return false;
|
||||
}
|
||||
|
||||
int local_search::pick_var()
|
||||
{
|
||||
int c, v;
|
||||
int best_var = 0;
|
||||
|
||||
// SAT Mode
|
||||
if (m_unsat_stack.empty()) {
|
||||
//++as;
|
||||
for (int i = 1; i <= ob_num_terms; ++i) {
|
||||
v = ob_constraint[i].var_id;
|
||||
if (tie_breaker_sat(v, best_var))
|
||||
best_var = v;
|
||||
}
|
||||
return best_var;
|
||||
}
|
||||
|
||||
// Unsat Mode: CCD > RD
|
||||
// CCD mode
|
||||
if (!goodvar_stack.empty()) {
|
||||
//++ccd;
|
||||
best_var = goodvar_stack[0];
|
||||
for (unsigned i = 1; i < goodvar_stack.size(); ++i) {
|
||||
v = goodvar_stack[i];
|
||||
if (tie_breaker_ccd(v, best_var))
|
||||
best_var = v;
|
||||
}
|
||||
return best_var;
|
||||
}
|
||||
|
||||
// Diversification Mode
|
||||
c = m_unsat_stack[rand() % m_unsat_stack.size()]; // a random unsat constraint
|
||||
// Within c, from all slack increasing var, choose the oldest one
|
||||
for (unsigned i = 0; i < constraint_term[c].size(); ++i) {
|
||||
v = constraint_term[c][i].var_id;
|
||||
if (cur_solution[v] == constraint_term[c][i].sense && time_stamp[v] < time_stamp[best_var])
|
||||
best_var = v;
|
||||
}
|
||||
//++rd;
|
||||
return best_var;
|
||||
}
|
||||
|
||||
void local_search::set_parameters() {
|
||||
if (s_id == 0)
|
||||
max_steps = num_vars;
|
||||
else if (s_id == 1)
|
||||
max_steps = (int) (1.5 * num_vars);
|
||||
else if (s_id == 1)
|
||||
max_steps = 2 * num_vars;
|
||||
else if (s_id == 2)
|
||||
max_steps = (int) (2.5 * num_vars);
|
||||
else if (s_id == 3)
|
||||
max_steps = 3 * num_vars;
|
||||
else {
|
||||
std::cout << "Invalid strategy id!" << std::endl;
|
||||
exit(-1);
|
||||
}
|
||||
}
|
||||
|
||||
|
||||
|
||||
}
|
||||
|
|
|
|||
|
|
@ -30,78 +30,82 @@ namespace sat {
|
|||
|
||||
// data structure for a term in objective function
|
||||
struct ob_term {
|
||||
int var_id; // variable id, begin with 1
|
||||
int coefficient; // non-zero integer
|
||||
int var_id; // variable id, begin with 1
|
||||
int coefficient; // non-zero integer
|
||||
};
|
||||
|
||||
// data structure for a term in constraint
|
||||
struct term {
|
||||
int constraint_id; // constraint it belongs to
|
||||
int var_id; // variable id, begin with 1
|
||||
bool sense; // 1 for positive, 0 for negative
|
||||
//int coefficient; // all constraints are cardinality: coefficient=1
|
||||
int constraint_id; // constraint it belongs to
|
||||
int var_id; // variable id, begin with 1
|
||||
bool sense; // 1 for positive, 0 for negative
|
||||
//int coefficient; // all constraints are cardinality: coefficient=1
|
||||
};
|
||||
|
||||
// parameters of the instance
|
||||
int num_vars; // var index from 1 to num_vars
|
||||
int num_constraints; // constraint index from 1 to num_constraint
|
||||
int max_constraint_len;
|
||||
int min_constraint_len;
|
||||
int num_vars; // var index from 1 to num_vars
|
||||
int num_constraints; // constraint index from 1 to num_constraint
|
||||
int max_constraint_len;
|
||||
int min_constraint_len;
|
||||
|
||||
// objective function: maximize
|
||||
int ob_num_terms; // how many terms are in the objective function
|
||||
ob_term* ob_constraint; // the objective function *constraint*, sorting as decending order
|
||||
int ob_num_terms; // how many terms are in the objective function
|
||||
ob_term* ob_constraint; // the objective function *constraint*, sorting as decending order
|
||||
|
||||
|
||||
// terms arrays
|
||||
vector<svector<term> > var_term; //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
|
||||
vector<svector<term> > var_term; // 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
|
||||
|
||||
// information about the variable
|
||||
int_vector coefficient_in_ob_constraint; // initilized to be 0
|
||||
int_vector coefficient_in_ob_constraint; // initilized to be 0
|
||||
int_vector score;
|
||||
int_vector sscore; // slack score
|
||||
int_vector sscore; // slack score
|
||||
|
||||
int_vector time_stamp; // the flip time stamp
|
||||
bool_vector conf_change; // whether its configure changes since its last flip
|
||||
int_vector cscc; // how many times its constraint state configure changes since its last flip
|
||||
vector<int_vector> var_neighbor; // all of its neighborhoods variable
|
||||
int_vector time_stamp; // the flip time stamp
|
||||
bool_vector conf_change; // whether its configure changes since its last flip
|
||||
int_vector cscc; // how many times its constraint state configure changes since its last flip
|
||||
vector<int_vector> var_neighbor; // all of its neighborhoods variable
|
||||
/* TBD: other scores */
|
||||
|
||||
// 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 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
|
||||
int_vector unsat_stack; // store all the unsat constraits
|
||||
int_vector index_in_unsat_stack; // which position is a contraint in the unsat_stack
|
||||
int_vector m_unsat_stack; // store all the unsat constraits
|
||||
int_vector m_index_in_unsat_stack; // which position is a contraint in the unsat_stack
|
||||
|
||||
// configuration changed decreasing variables (score>0 and conf_change==true)
|
||||
int_vector goodvar_stack;
|
||||
bool_vector already_in_goodvar_stack;
|
||||
// information about solution
|
||||
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
|
||||
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
|
||||
// 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
|
||||
|
||||
// cutoff
|
||||
int cutoff_time = 1; // seconds
|
||||
int max_steps = 2000000000; // < 2147483647
|
||||
int cutoff_time = 1; // seconds
|
||||
int max_steps = 2000000000; // < 2147483647
|
||||
|
||||
// for tuning
|
||||
int s_id = 0; // strategy id
|
||||
int s_id = 0; // strategy id
|
||||
|
||||
void init();
|
||||
bool_var pick_var();
|
||||
void flip(bool_var v);
|
||||
void init_orig();
|
||||
void init_greedy();
|
||||
void init_cur_solution();
|
||||
int pick_var();
|
||||
void flip(int v);
|
||||
bool tie_breaker_sat(int, int);
|
||||
bool tie_breaker_ccd(int, int);
|
||||
|
||||
void set_parameters();
|
||||
|
||||
void calculate_and_update_ob();
|
||||
|
||||
|
|
@ -109,6 +113,17 @@ namespace sat {
|
|||
|
||||
void display(std::ostream& out);
|
||||
|
||||
void unsat(int constraint_id) { m_unsat_stack.push_back(constraint_id); }
|
||||
|
||||
void sat(int c) {
|
||||
int last_unsat_constraint = m_unsat_stack.back();
|
||||
m_unsat_stack.pop_back();
|
||||
int index = m_index_in_unsat_stack[c];
|
||||
// swap the deleted one with the last one and pop
|
||||
m_unsat_stack[index] = last_unsat_constraint;
|
||||
m_index_in_unsat_stack[last_unsat_constraint] = index;
|
||||
}
|
||||
|
||||
public:
|
||||
local_search(solver& s);
|
||||
|
||||
|
|
|
|||
Loading…
Reference in a new issue