From ba0ec79375b9aee57cc93aa932807a9b06643a09 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 27 Feb 2017 19:03:32 -0800 Subject: [PATCH] adapt to vectors Signed-off-by: Nikolaj Bjorner --- src/sat/sat_local_search.cpp | 323 +++++++++++++++++------------------ src/sat/sat_local_search.h | 48 +++--- 2 files changed, 176 insertions(+), 195 deletions(-) diff --git a/src/sat/sat_local_search.cpp b/src/sat/sat_local_search.cpp index cd611176a..e73b84760 100644 --- a/src/sat/sat_local_search.cpp +++ b/src/sat/sat_local_search.cpp @@ -37,11 +37,10 @@ namespace sat { var_neighbor.push_back(bool_var_vector()); for (bool_var v = 1; v <= num_vars(); ++v) { - //std::cout << pos_var_term[v].size() << '\t' << neg_var_term[v].size() << '\n'; bool_vector is_neighbor(num_vars() + 1, false); var_neighbor.push_back(bool_var_vector()); - for (unsigned i = 0; i < pos_var_term[v].size(); ++i) { - unsigned c = pos_var_term[v][i]; + for (unsigned i = 0; i < m_vars[v].m_watch[true].size(); ++i) { + unsigned c = m_vars[v].m_watch[true][i]; for (unsigned j = 0; j < constraint_term[c].size(); ++j) { bool_var w = constraint_term[c][j].var_id; if (w == v || is_neighbor[w]) continue; @@ -49,15 +48,15 @@ namespace sat { var_neighbor.back().push_back(w); } } - for (unsigned i = 0; i < neg_var_term[v].size(); ++i) { - unsigned c = neg_var_term[v][i]; - for (unsigned j = 0; j < constraint_term[c].size(); ++j) { - bool_var w = constraint_term[c][j].var_id; - if (w == v || is_neighbor[w]) continue; - is_neighbor[w] = true; - var_neighbor.back().push_back(w); - } - } + for (unsigned i = 0; i < m_vars[v].m_watch[false].size(); ++i) { + unsigned c = m_vars[v].m_watch[false][i]; + for (unsigned j = 0; j < constraint_term[c].size(); ++j) { + bool_var w = constraint_term[c][j].var_id; + if (w == v || is_neighbor[w]) continue; + is_neighbor[w] = true; + var_neighbor.back().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; @@ -91,35 +90,30 @@ namespace sat { } } - // figure out variables scores and sscores + // figure out variables scores and slack_scores void local_search::init_scores() { for (unsigned v = 1; v <= num_vars(); ++v) { - int_vector truep, falsep; - if (cur_solution[v]) { - truep = pos_var_term[v]; - falsep = neg_var_term[v]; - } - else { - truep = neg_var_term[v]; - falsep = pos_var_term[v]; - } - for (unsigned i = 0; i < falsep.size(); ++i) { - int c = falsep[i]; - // will --slack - if (constraint_slack[c] <= 0) { - --sscore[v]; - if (constraint_slack[c] == 0) - --m_var_info[v].m_score; - } - } - for (unsigned i = 0; i < truep.size(); ++i) { - int c = truep[i]; + 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]; + + for (unsigned i = 0; i < falsep.size(); ++i) { + int c = falsep[i]; + // will --slack + if (constraint_slack[c] <= 0) { + dec_slack_score(v); + if (constraint_slack[c] == 0) + dec_score(v); + } + } + for (unsigned i = 0; i < truep.size(); ++i) { + int c = truep[i]; // will --true_terms_count[c] // will ++slack if (constraint_slack[c] <= -1) { - ++sscore[v]; + inc_slack_score(v); if (constraint_slack[c] == -1) - ++m_var_info[v].m_score; + inc_score(v); } } } @@ -130,7 +124,7 @@ namespace sat { goodvar_stack.reset(); for (unsigned v = 1; v <= num_vars(); ++v) { if (score(v) > 0) { // && conf_change[v] == true - m_var_info[v].m_in_goodvar_stack = true; + m_vars[v].m_in_goodvar_stack = true; goodvar_stack.push_back(v); } } @@ -148,23 +142,24 @@ namespace sat { // init varibale information // variable 0 is the virtual variable - m_var_info.reset(); - sscore.reset(); - time_stamp.reset(); - cscc.reset(); - - m_var_info.resize(num_vars() + 1, var_info()); - m_var_info[0].m_score = INT_MIN; - m_var_info[0].m_conf_change = false; - sscore.resize(num_vars() + 1, 0); sscore[0] = INT_MIN; - time_stamp.resize(num_vars() + 1, 0); time_stamp[0] = max_steps + 1; - cscc.resize(num_vars() + 1, 1); cscc[0] = 0; - - + time_stamp.reserve(m_vars.size()); + cscc.reserve(m_vars.size()); + m_vars[0].m_score = INT_MIN; + m_vars[0].m_conf_change = false; + m_vars[0].m_slack_score = INT_MIN; + cscc[0] = 0; + time_stamp[0] = max_steps + 1; + for (unsigned i = 1; i < m_vars.size(); ++i) { + time_stamp[i] = 0; + cscc[i] = 1; + m_vars[i].m_conf_change = true; + m_vars[i].m_in_goodvar_stack = false; + m_vars[i].m_score = 0; + m_vars[i].m_slack_score = 0; + } init_slack(); init_scores(); init_goodvars(); - } void local_search::calculate_and_update_ob() { @@ -196,20 +191,14 @@ namespace sat { } void local_search::add_cardinality(unsigned sz, literal const* c, unsigned k) { - unsigned id = m_num_constraints; - ++m_num_constraints; - // constraint_term.push_back(svector()); + unsigned id = num_constraints(); + constraint_term.push_back(svector()); for (unsigned i = 0; i < sz; ++i) { - m_num_vars = std::max(c[i].var() + 1, m_num_vars); - // var_term.reserve(c[i].var() + 1); + m_vars.reserve(c[i].var() + 1); term t; t.var_id = c[i].var(); t.sense = c[i].sign(); - if (t.sense) - pos_var_term[t.var_id].push_back(id); - else - neg_var_term[t.var_id].push_back(id); - //var_term[t.var_id].push_back(t); + m_vars[t.var_id].m_watch[t.sense].push_back(id); constraint_term[id].push_back(t); } constraint_k.push_back(k); @@ -217,9 +206,6 @@ namespace sat { local_search::local_search(solver& s) { - m_num_vars = 0; - m_num_constraints = 0; - // copy units unsigned trail_sz = s.init_trail_size(); for (unsigned i = 0; i < trail_sz; ++i) { @@ -325,17 +311,17 @@ namespace sat { reach_known_best_value = true; break; } - } + } flipvar = pick_var(); flip(flipvar); time_stamp[flipvar] = step; } if (tries % 10 == 0) { - // take a look at watch - stop = clock(); - elapsed_time = (double)(stop - start) / CLOCKS_PER_SEC; - std::cout << tries << ": " << elapsed_time << '\n'; - } + // take a look at watch + stop = clock(); + elapsed_time = (double)(stop - start) / CLOCKS_PER_SEC; + std::cout << tries << ": " << elapsed_time << '\n'; + } if (elapsed_time > cutoff_time) reach_cutoff_time = true; if (reach_known_best_value || reach_cutoff_time) @@ -360,107 +346,102 @@ namespace sat { unsigned v, c; int org_flipvar_score = score(flipvar); - int org_flipvar_sscore = sscore[flipvar]; + int org_flipvar_slack_score = slack_score(flipvar); - int_vector truep, falsep; - if (cur_solution[flipvar]) { - truep = pos_var_term[flipvar]; - falsep = neg_var_term[flipvar]; - } - else { - truep = neg_var_term[flipvar]; - falsep = pos_var_term[flipvar]; - } + bool is_true = cur_solution[flipvar]; + int_vector& truep = m_vars[flipvar].m_watch[is_true]; + int_vector& falsep = m_vars[flipvar].m_watch[!is_true]; // update related clauses and neighbor vars - for (unsigned i = 0; i < truep.size(); ++i) { - c = truep[i]; - //++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]; - --m_var_info[v].m_score; - } - 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]; - ++m_var_info[v].m_score; - // 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]; - --m_var_info[v].m_score; - --sscore[v]; - } - } - break; - default: - break; - } - } - for (unsigned i = 0; i < falsep.size(); ++i) { - c = falsep[i]; - //--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]; - ++m_var_info[v].m_score; - ++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]; - --m_var_info[v].m_score; - // 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]; - ++m_var_info[v].m_score; - } - } - break; - default: - break; - } + for (unsigned i = 0; i < truep.size(); ++i) { + c = truep[i]; + //++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]; + dec_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]; + inc_score(v); + // slack increasing var + if (cur_solution[v] == constraint_term[c][j].sense) + inc_slack_score(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]; + dec_score(v); + dec_slack_score(v); + } + } + break; + default: + break; + } + } + for (unsigned i = 0; i < falsep.size(); ++i) { + c = falsep[i]; + //--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]; + inc_score(v); + inc_slack_score(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]; + dec_score(v); + // slack increasing var no longer sat this var + if (cur_solution[v] == constraint_term[c][j].sense) + dec_slack_score(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]; + inc_score(v); + } + } + break; + default: + break; + } } - m_var_info[flipvar].m_score = -org_flipvar_score; - sscore[flipvar] = -org_flipvar_sscore; + m_vars[flipvar].m_score = -org_flipvar_score; + m_vars[flipvar].m_slack_score = -org_flipvar_slack_score; - m_var_info[flipvar].m_conf_change = false; + m_vars[flipvar].m_conf_change = false; cscc[flipvar] = 0; /* update CCD */ @@ -471,7 +452,7 @@ namespace sat { if (score(v) <= 0) { goodvar_stack[i] = goodvar_stack.back(); goodvar_stack.pop_back(); - m_var_info[v].m_in_goodvar_stack = false; + m_vars[v].m_in_goodvar_stack = false; } } // update all flipvar's neighbor's conf_change to true, add goodvar/okvar @@ -479,10 +460,10 @@ namespace sat { unsigned sz = var_neighbor[flipvar].size(); for (unsigned i = 0; i < sz; ++i) { v = var_neighbor[flipvar][i]; - m_var_info[v].m_conf_change = true; + m_vars[v].m_conf_change = true; if (score(v) > 0 && !already_in_goodvar_stack(v)) { goodvar_stack.push_back(v); - m_var_info[v].m_in_goodvar_stack = true; + m_vars[v].m_in_goodvar_stack = true; } } @@ -507,14 +488,14 @@ namespace sat { bool local_search::tie_breaker_ccd(bool_var v, bool_var best_var) { // break tie 1: max score - // break tie 2: max sscore + // break tie 2: max slack_score // break tie 3: cscc // break tie 4: oldest one return ((score(v) > score(best_var)) || ((score(v) == score(best_var)) && - ((sscore[v] > sscore[best_var]) || - ((sscore[v] == sscore[best_var]) && + ((slack_score(v) > slack_score(best_var)) || + ((slack_score(v) == slack_score(best_var)) && ((cscc[v] > cscc[best_var]) || ((cscc[v] == cscc[best_var]) && (time_stamp[v] < time_stamp[best_var]))))))); @@ -586,7 +567,7 @@ 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' << sscore[v] << '\n'; + std::cout << var_neighbor[v].size() << '\t' << cur_solution[v] << '\t' << conf_change(v) << '\t' << score(v) << '\t' << slack_score(v) << '\n'; } } } diff --git a/src/sat/sat_local_search.h b/src/sat/sat_local_search.h index d1708a105..226e1e984 100644 --- a/src/sat/sat_local_search.h +++ b/src/sat/sat_local_search.h @@ -49,8 +49,6 @@ namespace sat { void set_best_known_value(unsigned v) { m_best_known_value = v; } }; -#define MAX_VARS 5000 -#define MAX_CONSTRAINTS 100 class local_search { @@ -58,14 +56,13 @@ namespace sat { // data structure for a term in objective function struct ob_term { - int var_id; // variable id, begin with 1 + bool_var 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_var var_id; // variable id, begin with 1 bool sense; // 1 for positive, 0 for negative //int coefficient; // all constraints are cardinality: coefficient=1 }; @@ -76,42 +73,46 @@ namespace sat { // terms arrays - //svector var_term[MAX_VARS]; // var_term[i][j] means the j'th term of var i - int_vector pos_var_term[MAX_VARS]; - int_vector neg_var_term[MAX_VARS]; - svector constraint_term[MAX_CONSTRAINTS]; // constraint_term[i][j] means the j'th term of constraint i - unsigned m_num_vars, m_num_constraints; + vector > constraint_term; // constraint_term[i][j] means the j'th term of constraint i // parameters of the instance - unsigned num_vars() const { return m_num_vars - 1; } // var index from 1 to num_vars - unsigned num_constraints() const { return m_num_constraints; } // constraint index from 1 to num_constraint + unsigned num_vars() const { return m_vars.size() - 1; } // var index from 1 to num_vars + unsigned num_constraints() const { return constraint_term.size(); } // constraint index from 1 to num_constraint // information about the variable int_vector coefficient_in_ob_constraint; // initialized to be 0 - // int_vector score; - int_vector sscore; // slack score + // int_vector sscore; // slack score struct var_info { bool m_conf_change; // whether its configure changes since its last flip bool m_in_goodvar_stack; int m_score; + int m_slack_score; + int_vector m_watch[2]; var_info(): m_conf_change(true), m_in_goodvar_stack(false), - m_score(0) + m_score(0), + m_slack_score(0) {} }; - svector m_var_info; + svector m_vars; - inline int score(unsigned v) const { return m_var_info[v].m_score; } - inline bool already_in_goodvar_stack(unsigned v) const { return m_var_info[v].m_in_goodvar_stack; } - inline bool conf_change(unsigned v) const { return m_var_info[v].m_conf_change; } + inline int score(unsigned 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--; } - int_vector time_stamp; // the flip time stamp - // bool_vector conf_change; - int_vector cscc; // how many times its constraint state configure changes since its last flip - vector var_neighbor; // all of its neighborhoods variable + inline int slack_score(unsigned 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; } + + int_vector time_stamp; // the flip time stamp + 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 @@ -126,7 +127,6 @@ namespace sat { // 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