From eec1d9ef849f79f37c2a45114b811302c84662e6 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 21 Feb 2017 21:19:13 -0800 Subject: [PATCH] porting more code Signed-off-by: Nikolaj Bjorner --- src/sat/sat_local_search.cpp | 394 +++++++++++++++++++++++++++++++++-- src/sat/sat_local_search.h | 81 ++++--- 2 files changed, 428 insertions(+), 47 deletions(-) diff --git a/src/sat/sat_local_search.cpp b/src/sat/sat_local_search.cpp index 5b8f44783..ed13b5a1a 100644 --- a/src/sat/sat_local_search.cpp +++ b/src/sat/sat_local_search.cpp @@ -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); + } + } + } diff --git a/src/sat/sat_local_search.h b/src/sat/sat_local_search.h index 169596888..8de3aadaa 100644 --- a/src/sat/sat_local_search.h +++ b/src/sat/sat_local_search.h @@ -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 > 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 + 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 // 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 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 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);