From eec10c6e32ec0c468d6adaf25f571ec767dfcb8d Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 21 Feb 2017 21:33:18 -0800 Subject: [PATCH] porting more code Signed-off-by: Nikolaj Bjorner --- src/sat/sat_local_search.cpp | 326 ++++++++++++++++++----------------- 1 file changed, 168 insertions(+), 158 deletions(-) diff --git a/src/sat/sat_local_search.cpp b/src/sat/sat_local_search.cpp index ed13b5a1a..22722de98 100644 --- a/src/sat/sat_local_search.cpp +++ b/src/sat/sat_local_search.cpp @@ -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" @@ -29,7 +29,7 @@ namespace sat { } void local_search::init_orig() { - int v, c; + int v, c; for (c = 1; c <= num_constraints; ++c) { constraint_slack[c] = constraint_k[c]; @@ -108,7 +108,7 @@ namespace sat { } void local_search::init_greedy() { - int v, c; + int v, c; for (c = 1; c <= num_constraints; ++c) { constraint_slack[c] = constraint_k[c]; } @@ -223,100 +223,110 @@ namespace sat { void local_search::flip(int flipvar) { - // already changed truth value!!!! - cur_solution[flipvar] = !cur_solution[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]; + 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]; + // update related clauses and neighbor vars + svector const& constraints = var_term[flipvar]; + unsigned num_constraints = constraints.size(); + for (unsigned i = 0; i < num_constraints; ++i) { + c = constraints[i].constraint_id; + if (cur_solution[flipvar] == constraints[i].sense) { + //++true_terms_count[c]; + --constraint_slack[c]; + switch (constraint_slack[c]) { + case -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]; - // 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]; + break; + case -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); + 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; - sscore[flipvar] = -org_flipvar_sscore; + score[flipvar] = -org_flipvar_score; + sscore[flipvar] = -org_flipvar_sscore; - conf_change[flipvar] = false; - cscc[flipvar] = 0; + 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;) { + /* 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) { @@ -324,69 +334,69 @@ namespace sat { 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) { + } + // 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; + // 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; + // 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; + int c, v; + int best_var = 0; - // SAT Mode - if (m_unsat_stack.empty()) { + // SAT Mode + if (m_unsat_stack.empty()) { //++as; for (int i = 1; i <= ob_num_terms; ++i) { v = ob_constraint[i].var_id; @@ -394,11 +404,11 @@ namespace sat { best_var = v; } return best_var; - } + } - // Unsat Mode: CCD > RD - // CCD mode - if (!goodvar_stack.empty()) { + // 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) { @@ -407,35 +417,35 @@ namespace sat { 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) { + // 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; + } + //++rd; + return best_var; } void local_search::set_parameters() { - if (s_id == 0) + if (s_id == 0) max_steps = num_vars; - else if (s_id == 1) + else if (s_id == 1) max_steps = (int) (1.5 * num_vars); - else if (s_id == 1) + else if (s_id == 1) max_steps = 2 * num_vars; - else if (s_id == 2) + else if (s_id == 2) max_steps = (int) (2.5 * num_vars); - else if (s_id == 3) + else if (s_id == 3) max_steps = 3 * num_vars; - else { + else { std::cout << "Invalid strategy id!" << std::endl; exit(-1); - } + } }