From d8bb10d37f5adb2cca62bffda949a4422d907465 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 21 Feb 2017 22:43:23 -0800 Subject: [PATCH] porting more code Signed-off-by: Nikolaj Bjorner --- src/sat/sat_local_search.cpp | 346 ++++++++++++++++++----------------- src/sat/sat_local_search.h | 43 +++-- src/sat/sat_solver.h | 1 + 3 files changed, 201 insertions(+), 189 deletions(-) diff --git a/src/sat/sat_local_search.cpp b/src/sat/sat_local_search.cpp index 22722de98..95f021537 100644 --- a/src/sat/sat_local_search.cpp +++ b/src/sat/sat_local_search.cpp @@ -18,6 +18,7 @@ --*/ #include "sat_local_search.h" +#include "sat_solver.h" namespace sat { @@ -28,12 +29,68 @@ namespace sat { init_greedy(); } - void local_search::init_orig() { - int v, c; - - for (c = 1; c <= num_constraints; ++c) { - constraint_slack[c] = constraint_k[c]; + void local_search::init_cur_solution() { + for (unsigned v = 1; v <= num_vars; ++v) { + cur_solution[v] = (rand() % 2 == 1); } + } + + // figure out slack, and init unsat stack + void local_search::init_slack() { + for (unsigned c = 1; c <= num_constraints; ++c) { + for (unsigned i = 0; i < constraint_term[c].size(); ++i) { + unsigned 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 + void local_search::init_scores() { + for (unsigned v = 1; v <= num_vars; ++v) { + for (unsigned i = 0; i < var_term[v].size(); ++i) { + int 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 + void local_search::init_goodvars() { + goodvar_stack.reset(); + already_in_goodvar_stack.resize(num_vars+1, false); + for (unsigned 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); + } + } + } + + void local_search::init_orig() { + constraint_slack = constraint_k; // init unsat stack m_unsat_stack.reset(); @@ -49,69 +106,14 @@ namespace sat { 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::init_cur_solution() { - for (int v = 1; v <= num_vars; ++v) { - cur_solution[v] = (rand() % 2 == 1); - } + init_slack(); + init_scores(); + init_goodvars(); } void local_search::init_greedy() { - int v, c; - for (c = 1; c <= num_constraints; ++c) { - constraint_slack[c] = constraint_k[c]; - } + constraint_slack = constraint_k; // init unsat stack m_unsat_stack.reset(); @@ -121,74 +123,21 @@ namespace sat { // 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; + + 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; + for (unsigned v = 1; v <= num_vars; ++v) { // 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; + if (coefficient_in_ob_constraint[v] != 0) + cur_solution[v] = (coefficient_in_ob_constraint[v] > 0); } + + init_slack(); + init_scores(); + init_goodvars(); } @@ -206,6 +155,75 @@ namespace sat { local_search::local_search(solver& s) { + // TBD: use solver::copy as a guideline for importing state from a solver. + + // TBD initialize variables + s.num_vars(); + + // copy units + unsigned trail_sz = s.init_trail_size(); + for (unsigned i = 0; i < trail_sz; ++i) { + unsigned id = constraint_term.size(); + term t; + t.constraint_id = id; + t.var_id = s.m_trail[i].var(); + t.sense = s.m_trail[i].sign(); + var_term[t.var_id].push_back(t); + constraint_term.push_back(svector()); + constraint_term[id].push_back(t); + constraint_k.push_back(0); + } + + // TBD copy binary: + s.m_watches.size(); + { + unsigned sz = s.m_watches.size(); + for (unsigned l_idx = 0; l_idx < sz; ++l_idx) { + literal l = ~to_literal(l_idx); + watch_list const & wlist = s.m_watches[l_idx]; + watch_list::const_iterator it = wlist.begin(); + watch_list::const_iterator end = wlist.end(); + for (; it != end; ++it) { + if (!it->is_binary_non_learned_clause()) + continue; + literal l2 = it->get_literal(); + if (l.index() > l2.index()) + continue; + + unsigned id = constraint_term.size(); + constraint_term.push_back(svector()); + + // TBD: add clause l, l2; + + constraint_k.push_back(1); + } + } + } + + + clause_vector::const_iterator it = s.m_clauses.begin(); + clause_vector::const_iterator end = s.m_clauses.end(); + for (; it != end; ++it) { + clause const& c = *(*it); + unsigned sz = c.size(); + unsigned id = constraint_term.size(); + constraint_term.push_back(svector()); + for (unsigned i = 0; i < sz; ++i) { + term t; + t.constraint_id = id; + t.var_id = c[i].var(); + t.sense = c[i].sign(); + var_term[t.var_id].push_back(t); + constraint_term[id].push_back(t); + } + constraint_k.push_back(sz-1); + } + + // TBD initialize cardinalities from m_ext, retrieve cardinality constraints. + // optionally handle xor constraints. + + num_vars = s.num_vars(); + num_constraints = constraint_term.size(); } local_search::~local_search() { @@ -221,12 +239,12 @@ namespace sat { } - void local_search::flip(int flipvar) + void local_search::flip(bool_var flipvar) { // already changed truth value!!!! cur_solution[flipvar] = !cur_solution[flipvar]; - int v, c; + unsigned v, c; int org_flipvar_score = score[flipvar]; int org_flipvar_sscore = sscore[flipvar]; @@ -346,59 +364,45 @@ namespace sat { } } - bool local_search::tie_breaker_sat(int v, int best_var) - { + bool local_search::tie_breaker_sat(bool_var v, bool_var 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; + // break tie 2: conf_change + // break tie 3: time_stamp + + return + (v_imp > b_imp) || + ((v_imp == b_imp) && + ((conf_change[v] && !conf_change[best_var]) || + ((conf_change[v] == conf_change[best_var]) && + (time_stamp[v] < time_stamp[best_var])))); } - bool local_search::tie_breaker_ccd(int v, int best_var) - { + bool local_search::tie_breaker_ccd(bool_var v, bool_var 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 2: max sscore + // 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]) && + (cscc[v] > cscc[best_var]) || + ((cscc[v] == cscc[best_var]) && + (time_stamp[v] < time_stamp[best_var])))); } - int local_search::pick_var() - { + bool_var local_search::pick_var() { int c, v; - int best_var = 0; + bool_var best_var = null_bool_var; // SAT Mode if (m_unsat_stack.empty()) { //++as; - for (int i = 1; i <= ob_num_terms; ++i) { + for (unsigned i = 0; i < ob_constraint.size(); ++i) { v = ob_constraint[i].var_id; if (tie_breaker_sat(v, best_var)) best_var = v; diff --git a/src/sat/sat_local_search.h b/src/sat/sat_local_search.h index 8de3aadaa..565180976 100644 --- a/src/sat/sat_local_search.h +++ b/src/sat/sat_local_search.h @@ -43,14 +43,11 @@ namespace sat { }; // 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; + unsigned num_vars; // var index from 1 to num_vars + unsigned num_constraints; // constraint index from 1 to num_constraint // 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 + svector ob_constraint; // the objective function *constraint*, sorted in decending order // terms arrays @@ -58,14 +55,14 @@ namespace sat { 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; // initialized 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 @@ -81,6 +78,7 @@ 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 int objective_value; // the objective function value corresponds to the current solution @@ -97,13 +95,22 @@ namespace sat { int s_id = 0; // strategy id void init(); + 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 init_slack(); + void init_scores(); + void init_goodvars(); + + bool_var pick_var(); + + void flip(bool_var v); + + bool tie_breaker_sat(bool_var v1, bool_var v2); + + bool tie_breaker_ccd(bool_var v1, bool_var v2); void set_parameters(); @@ -115,13 +122,13 @@ namespace sat { void unsat(int constraint_id) { m_unsat_stack.push_back(constraint_id); } + // swap the deleted one with the last one and pop 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; + m_unsat_stack.pop_back(); } public: diff --git a/src/sat/sat_solver.h b/src/sat/sat_solver.h index 9393a8e10..bc24f2fde 100644 --- a/src/sat/sat_solver.h +++ b/src/sat/sat_solver.h @@ -155,6 +155,7 @@ namespace sat { friend class card_extension; friend class parallel; friend class lookahead; + friend class local_search; friend struct mk_stat; public: solver(params_ref const & p, reslimit& l);