From 43ddad0ecdb776e80e693765d5f7c4b538f98129 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 22 Feb 2017 14:57:25 -0800 Subject: [PATCH] initial pass Signed-off-by: Nikolaj Bjorner --- src/sat/card_extension.cpp | 3 +- src/sat/sat_local_search.cpp | 130 +++++++++++++++++++++------------- src/sat/sat_local_search.h | 19 +++-- src/sat/tactic/goal2sat.cpp | 5 +- src/test/sat_local_search.cpp | 130 +++++++++++----------------------- 5 files changed, 139 insertions(+), 148 deletions(-) diff --git a/src/sat/card_extension.cpp b/src/sat/card_extension.cpp index 4b46b6da1..e0bb04c10 100644 --- a/src/sat/card_extension.cpp +++ b/src/sat/card_extension.cpp @@ -739,7 +739,8 @@ namespace sat { void card_extension::add_at_least(bool_var v, literal_vector const& lits, unsigned k) { unsigned index = 2*m_cards.size(); - card* c = new (memory::allocate(card::get_obj_size(lits.size()))) card(index, literal(v, false), lits, k); + literal lit = v == null_bool_var ? null_literal : literal(v, false); + card* c = new (memory::allocate(card::get_obj_size(lits.size()))) card(index, lit, lits, k); m_cards.push_back(c); if (v == null_bool_var) { // it is an axiom. diff --git a/src/sat/sat_local_search.cpp b/src/sat/sat_local_search.cpp index 87f0c379f..84e1355b1 100644 --- a/src/sat/sat_local_search.cpp +++ b/src/sat/sat_local_search.cpp @@ -24,21 +24,40 @@ namespace sat { void local_search::init() { - constraint_slack.resize(num_constraints + 1); - cur_solution.resize(num_vars + 1); - // etc. initialize other vectors. - init_greedy(); + constraint_slack.resize(num_constraints(), 0); + cur_solution.resize(num_vars(), false); + m_index_in_unsat_stack.resize(num_constraints(), 0); + coefficient_in_ob_constraint.resize(num_vars(), 0); + var_neighbor.reset(); + for (bool_var v = 0; v < num_vars(); ++v) { + bool_vector is_neighbor(num_vars(), false); + var_neighbor.push_back(bool_var_vector()); + for (unsigned i = 0; i < var_term[v].size(); ++ i) { + unsigned c = var_term[v][i].constraint_id; + 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); + } + } + } + } + + void local_search::reinit() { + reinit_greedy(); } void local_search::init_cur_solution() { - for (unsigned v = 1; v <= num_vars; ++v) { + cur_solution.resize(num_vars() + 1, false); + for (unsigned v = 0; 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 c = 0; 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) @@ -53,7 +72,7 @@ namespace sat { // figure out variables scores, pscores and sscores void local_search::init_scores() { - for (unsigned v = 1; v <= num_vars; ++v) { + for (unsigned v = 0; 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) { @@ -81,8 +100,8 @@ namespace sat { // 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) { + already_in_goodvar_stack.resize(num_vars(), false); + for (unsigned v = 0; v < num_vars(); ++v) { if (score[v] > 0) { // && conf_change[v] == true already_in_goodvar_stack[v] = true; goodvar_stack.push_back(v); @@ -90,7 +109,7 @@ namespace sat { } } - void local_search::init_orig() { + void local_search::reinit_orig() { constraint_slack = constraint_k; // init unsat stack @@ -102,18 +121,24 @@ namespace sat { // 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; + score.reset(); + sscore.reset(); + time_stamp.reset(); + conf_change.reset(); + cscc.reset(); + + score.resize(num_vars(), 0); score[0] = INT_MIN; + sscore.resize(num_vars(), 0); sscore[0] = INT_MIN; + time_stamp.resize(num_vars(), 0); time_stamp[0] = max_steps; + conf_change.resize(num_vars(), true); conf_change[0] = false; + cscc.resize(num_vars(), 1); cscc[0] = 0; init_slack(); init_scores(); init_goodvars(); } - void local_search::init_greedy() { + void local_search::reinit_greedy() { constraint_slack = constraint_k; // init unsat stack @@ -125,14 +150,20 @@ namespace sat { // 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; - for (unsigned v = 1; v <= num_vars; ++v) { + score.reset(); + sscore.reset(); + time_stamp.reset(); + conf_change.reset(); + cscc.reset(); + + score.resize(num_vars(), 0); score[0] = INT_MIN; + sscore.resize(num_vars(), 0); sscore[0] = INT_MIN; + time_stamp.resize(num_vars(), 0); time_stamp[0] = max_steps; + conf_change.resize(num_vars(), true); conf_change[0] = false; + cscc.resize(num_vars(), 1); cscc[0] = 0; + for (unsigned v = 0; v < num_vars(); ++v) { // greedy here!! - if (coefficient_in_ob_constraint[v] != 0) + if (coefficient_in_ob_constraint.get(v, 0) != 0) cur_solution[v] = (coefficient_in_ob_constraint[v] > 0); } @@ -162,6 +193,7 @@ namespace sat { unsigned id = constraint_term.size(); constraint_term.push_back(svector()); for (unsigned i = 0; i < sz; ++i) { + var_term.resize(c[i].var() + 1); term t; t.constraint_id = id; t.var_id = c[i].var(); @@ -173,6 +205,7 @@ namespace sat { } local_search::local_search(solver& s) { + // copy units unsigned trail_sz = s.init_trail_size(); for (unsigned i = 0; i < trail_sz; ++i) { @@ -242,10 +275,6 @@ namespace sat { // SASSERT(ext->m_xors.empty()); } - - - num_vars = s.num_vars(); - num_constraints = constraint_term.size(); } local_search::~local_search() { @@ -256,17 +285,18 @@ namespace sat { } lbool local_search::operator()() { - bool reach_cutoff_time = false; - bool reach_known_best_value = false; - bool_var flipvar; + init(); + bool reach_cutoff_time = false; + bool reach_known_best_value = false; + bool_var flipvar; double elapsed_time = 0; clock_t start = clock(), stop; // TBD, use stopwatch facility - srand(0); // TBD, use random facility and parameters to set random seed. - set_parameters(); - // ################## start ###################### - //cout << "Start initialize and local search, restart in every " << max_steps << " steps" << endl; - for (unsigned tries = 0; ; ++tries) { - init(); + srand(0); // TBD, use random facility and parameters to set random seed. + set_parameters(); + // ################## start ###################### + //cout << "Start initialize and local search, restart in every " << max_steps << " steps" << endl; + for (unsigned tries = 0; ; ++tries) { + reinit(); for (int step = 1; step <= max_steps; ++step) { // feasible if (m_unsat_stack.empty()) { @@ -287,11 +317,11 @@ namespace sat { reach_cutoff_time = true; if (reach_known_best_value || reach_cutoff_time) break; - } - if (reach_known_best_value) { + } + if (reach_known_best_value) { std::cout << elapsed_time << "\n"; - } - else + } + else std::cout << -1 << "\n"; //print_solution(); @@ -311,8 +341,8 @@ namespace sat { // 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) { + unsigned num_cs = constraints.size(); + for (unsigned i = 0; i < num_cs; ++i) { c = constraints[i].constraint_id; if (cur_solution[flipvar] == constraints[i].sense) { //++true_terms_count[c]; @@ -427,8 +457,8 @@ namespace sat { 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]; + int v_imp = cur_solution[v] ? -coefficient_in_ob_constraint.get(v, 0) : coefficient_in_ob_constraint.get(v, 0); + int b_imp = cur_solution[best_var] ? -coefficient_in_ob_constraint.get(best_var, 0) : coefficient_in_ob_constraint.get(best_var, 0); // break tie 1: max imp // break tie 2: conf_change // break tie 3: time_stamp @@ -458,7 +488,7 @@ namespace sat { bool_var local_search::pick_var() { int c, v; - bool_var best_var = null_bool_var; + bool_var best_var = num_vars()-1; // SAT Mode if (m_unsat_stack.empty()) { @@ -498,15 +528,15 @@ namespace sat { void local_search::set_parameters() { if (s_id == 0) - max_steps = num_vars; + max_steps = num_vars(); else if (s_id == 1) - max_steps = (int) (1.5 * num_vars); + max_steps = (int) (1.5 * num_vars()); else if (s_id == 1) - max_steps = 2 * num_vars; + max_steps = 2 * num_vars(); else if (s_id == 2) - max_steps = (int) (2.5 * num_vars); + max_steps = (int) (2.5 * num_vars()); else if (s_id == 3) - max_steps = 3 * num_vars; + 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 12f3c3756..1d314abf8 100644 --- a/src/sat/sat_local_search.h +++ b/src/sat/sat_local_search.h @@ -42,9 +42,6 @@ namespace sat { //int coefficient; // all constraints are cardinality: coefficient=1 }; - // parameters of the instance - unsigned num_vars; // var index from 1 to num_vars - unsigned num_constraints; // constraint index from 1 to num_constraint // objective function: maximize svector ob_constraint; // the objective function *constraint*, sorted in decending order @@ -53,6 +50,11 @@ namespace sat { // 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 + + // parameters of the instance + unsigned num_vars() const { return var_term.size(); } // 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 @@ -62,7 +64,7 @@ namespace sat { 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 + vector var_neighbor; // all of its neighborhoods variable /* TBD: other scores */ // information about the constraints @@ -94,10 +96,12 @@ namespace sat { // for tuning int s_id = 0; // strategy id + void init(); - void init_orig(); - void init_greedy(); + void reinit(); + void reinit_orig(); + void reinit_greedy(); void init_cur_solution(); void init_slack(); @@ -124,7 +128,6 @@ namespace sat { void add_clause(unsigned sz, literal const* c); - void add_cardinality(unsigned sz, literal const* c, unsigned k); // swap the deleted one with the last one and pop void sat(int c) { @@ -141,6 +144,8 @@ namespace sat { ~local_search(); void add_soft(literal l, double weight); + + void add_cardinality(unsigned sz, literal const* c, unsigned k); lbool operator()(); diff --git a/src/sat/tactic/goal2sat.cpp b/src/sat/tactic/goal2sat.cpp index 30a458ece..8530a9d76 100644 --- a/src/sat/tactic/goal2sat.cpp +++ b/src/sat/tactic/goal2sat.cpp @@ -447,14 +447,15 @@ struct goal2sat::imp { lits[i].neg(); } sat::bool_var v = m_solver.mk_var(true); + sat::literal lit(v, sign); m_ext->add_at_least(v, lits, lits.size() - k.get_unsigned()); if (root) { m_result_stack.reset(); - mk_clause(sat::literal(v, sign)); + mk_clause(lit); } else { m_result_stack.shrink(sz - t->get_num_args()); - m_result_stack.push_back(sat::literal(v, sign)); + m_result_stack.push_back(lit); } } diff --git a/src/test/sat_local_search.cpp b/src/test/sat_local_search.cpp index 1d92b37c7..83c8e7b14 100644 --- a/src/test/sat_local_search.cpp +++ b/src/test/sat_local_search.cpp @@ -1,18 +1,18 @@ #include "sat_local_search.h" #include "sat_solver.h" -static int build_instance(char *filename, sat::solver& s, sat::local_search& ls) +static bool build_instance(char const * filename, sat::solver& s, sat::local_search& local_search) { char line[16383]; int cur_term; // for temperally storage - int temp[16383]; - int temp_count; std::ifstream infile(filename); //if (infile == NULL) //linux - if (!infile) - return 0; + if (!infile) { + std::cout << "File not found " << filename << "\n"; + return false; + } infile.getline(line, 16383); int num_vars, num_constraints; sscanf_s(line, "%d %d", &num_vars, &num_constraints); @@ -20,44 +20,36 @@ static int build_instance(char *filename, sat::solver& s, sat::local_search& ls) //cout << "number of constraints: " << num_constraints << endl; - // write in the objective function - temp_count = 0; - infile >> cur_term; - while (cur_term != 0) { - temp[temp_count++] = cur_term; - infile >> cur_term; - } - int ob_num_terms = temp_count; - -#if 0 - TBD make this compile: - ob_constraint = new ob_term[ob_num_terms + 1]; - // coefficient - ob_constraint[0].coefficient = 0; // virtual var: all variables not in ob are pointed to this var - for (i = 1; i <= ob_num_terms; ++i) { - ob_constraint[i].coefficient = temp[i - 1]; - } - + unsigned_vector coefficients; sat::literal_vector lits; - // ob variable - temp_count = 0; + + // process objective function: + // read coefficents infile >> cur_term; while (cur_term != 0) { - temp[temp_count++] = cur_term; + coefficients.push_back(cur_term); infile >> cur_term; } - if (temp_count != ob_num_terms) { - cout << "Objective function format error." << endl; - exit(-1); + + // read variables + infile >> cur_term; + while (cur_term != 0) { + lits.push_back(sat::literal(abs(cur_term), cur_term < 0)); + infile >> cur_term; } - for (i = 1; i <= ob_num_terms; ++i) { - ob_constraint[i].var_id = temp[i - 1]; - coefficient_in_ob_constraint[ob_constraint[i].var_id] = ob_constraint[i].coefficient; + + if (lits.size() != coefficients.size()) { + std::cout << "Objective function format error. They have different lenghts.\n"; + return false; } + + for (unsigned i = 0; i < lits.size(); ++i) { + local_search.add_soft(lits[i], coefficients[i]); + } + // read the constraints, one at a time - card_extension* ext = 0; int k; - for (c = 1; c <= num_constraints; ++c) { + for (int c = 1; c <= num_constraints; ++c) { lits.reset(); infile >> cur_term; while (cur_term != 0) { @@ -65,63 +57,11 @@ static int build_instance(char *filename, sat::solver& s, sat::local_search& ls) infile >> cur_term; } infile >> k; - ext->add_at_least(null_bool_var, lits, lits.size() - k); + local_search.add_cardinality(lits.size(), lits.c_ptr(), static_cast(lits.size() - k)); } -#endif infile.close(); - - -#if 0 - Move all of this to initialization code for local search solver: - - // create var_term array - for (v = 1; v <= num_vars; ++v) { - var_term[v] = new term[var_term_count[v]]; - var_term_count[v] = 0; // reset to 0, for building up the array - } - // scan all constraints to build up var term arrays - for (c = 1; c <= num_constraints; ++c) { - for (i = 0; i < constraint_term_count[c]; ++i) { - v = constraint_term[c][i].var_id; - var_term[v][var_term_count[v]++] = constraint_term[c][i]; - } - } - - - // build neighborhood relationship - bool *is_neighbor; - is_neighbor = new bool[num_vars + 1]; - for (v = 1; v <= num_vars; ++v) { - // init as not neighbor - for (i = 1; i <= num_vars; ++i) { - is_neighbor[i] = false; - } - temp_count = 0; - // for each constraint v appears - for (i = 0; i < var_term_count[v]; ++i) { - c = var_term[v][i].constraint_id; - for (j = 0; j < constraint_term_count[c]; ++j) { - if (constraint_term[c][j].var_id == v) - continue; - // not neighbor yet - if (!is_neighbor[constraint_term[c][j].var_id]) { - is_neighbor[constraint_term[c][j].var_id] = true; - temp[temp_count++] = constraint_term[c][j].var_id; - } - } - } - // create and build neighbor - var_neighbor_count[v] = temp_count; - var_neighbor[v] = new int[var_neighbor_count[v]]; - for (i = 0; i < var_neighbor_count[v]; ++i) { - var_neighbor[v][i] = temp[i]; - } - } - delete[] is_neighbor; - -#endif - return 1; + return true; } void tst_sat_local_search(char ** argv, int argc, int& i) { @@ -129,6 +69,20 @@ void tst_sat_local_search(char ** argv, int argc, int& i) { std::cout << "require dimacs file name\n"; return; } + reslimit limit; + params_ref params; + sat::solver solver(params, limit); + sat::local_search local_search(solver); + char const* file_name = argv[i + 1]; + ++i; + + if (!build_instance(file_name, solver, local_search)) { + return; + } + + std::cout << "local instance built\n"; + local_search(); + // sat::solver s; // populate the sat solver with clauses and cardinality consrtaints from the input // call the lookahead solver.