diff --git a/contrib/cmake/src/test/CMakeLists.txt b/contrib/cmake/src/test/CMakeLists.txt index 7ea5f4589..0f756ce2c 100644 --- a/contrib/cmake/src/test/CMakeLists.txt +++ b/contrib/cmake/src/test/CMakeLists.txt @@ -92,6 +92,7 @@ add_executable(test-z3 rational.cpp rcf.cpp region.cpp + sat_local_search.cpp sat_lookahead.cpp sat_user_scope.cpp simple_parser.cpp diff --git a/src/api/api_opt.cpp b/src/api/api_opt.cpp index 6fbc86ab6..32f0d1003 100644 --- a/src/api/api_opt.cpp +++ b/src/api/api_opt.cpp @@ -129,7 +129,6 @@ extern "C" { cancel_eh eh(mk_c(c)->m().limit()); unsigned timeout = to_optimize_ptr(o)->get_params().get_uint("timeout", mk_c(c)->get_timeout()); unsigned rlimit = mk_c(c)->get_rlimit(); - std::cout << "Timeout: " << timeout << "\n"; api::context::set_interruptable si(*(mk_c(c)), eh); { scoped_timer timer(timeout, &eh); diff --git a/src/sat/card_extension.cpp b/src/sat/card_extension.cpp index fd8986cae..4b46b6da1 100644 --- a/src/sat/card_extension.cpp +++ b/src/sat/card_extension.cpp @@ -741,9 +741,16 @@ namespace sat { unsigned index = 2*m_cards.size(); card* c = new (memory::allocate(card::get_obj_size(lits.size()))) card(index, literal(v, false), lits, k); m_cards.push_back(c); - init_watch(v); - m_var_infos[v].m_card = c; - m_var_trail.push_back(v); + if (v == null_bool_var) { + // it is an axiom. + init_watch(*c, true); + m_card_axioms.push_back(c); + } + else { + init_watch(v); + m_var_infos[v].m_card = c; + m_var_trail.push_back(v); + } } void card_extension::add_xor(bool_var v, literal_vector const& lits) { diff --git a/src/sat/card_extension.h b/src/sat/card_extension.h index 4e0c10cd2..1c4aac29b 100644 --- a/src/sat/card_extension.h +++ b/src/sat/card_extension.h @@ -21,10 +21,14 @@ Revision History: #include"sat_extension.h" #include"sat_solver.h" +#include"scoped_ptr_vector.h" namespace sat { class card_extension : public extension { + + friend class local_search; + struct stats { unsigned m_num_propagations; unsigned m_num_conflicts; @@ -118,6 +122,8 @@ namespace sat { ptr_vector m_cards; ptr_vector m_xors; + scoped_ptr_vector m_card_axioms; + // watch literals svector m_var_infos; unsigned_vector m_var_trail; diff --git a/src/sat/sat_local_search.cpp b/src/sat/sat_local_search.cpp index 95f021537..87f0c379f 100644 --- a/src/sat/sat_local_search.cpp +++ b/src/sat/sat_local_search.cpp @@ -19,6 +19,7 @@ #include "sat_local_search.h" #include "sat_solver.h" +#include "card_extension.h" namespace sat { @@ -153,29 +154,32 @@ namespace sat { } + void local_search::add_clause(unsigned sz, literal const* c) { + add_cardinality(sz, c, sz - 1); + } + + void local_search::add_cardinality(unsigned sz, literal const* c, unsigned k) { + 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(k); + } + 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); + add_clause(1, s.m_trail.c_ptr() + i); } - // TBD copy binary: - s.m_watches.size(); + // copy binary clauses { unsigned sz = s.m_watches.size(); for (unsigned l_idx = 0; l_idx < sz; ++l_idx) { @@ -189,45 +193,62 @@ namespace sat { 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); + literal ls[2] = { l, l2 }; + add_clause(2, ls); } } } - + // copy clauses 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); + clause& c = *(*it); + add_clause(c.size(), c.begin()); + } + + // copy cardinality clauses + card_extension* ext = dynamic_cast(s.get_extension()); + if (ext) { + literal_vector lits; + unsigned sz = ext->m_cards.size(); + for (unsigned i = 0; i < sz; ++i) { + card_extension::card& c = *ext->m_cards[i]; + unsigned n = c.size(); + unsigned k = c.k(); + + // c.lit() <=> c.lits() >= k + // + // (c.lits() < k) or c.lit() + // = (c.lits() + (n - k - 1)*~c.lit()) <= n + // + // ~c.lit() or (c.lits() >= k) + // = ~c.lit() or (~c.lits() <= n - k) + // = k*c.lit() + ~c.lits() <= n + // + + lits.reset(); + for (unsigned j = 0; j < n; ++j) lits.push_back(c[j]); + for (unsigned j = 0; j < n - k - 1; ++j) lits.push_back(~c.lit()); + add_cardinality(lits.size(), lits.c_ptr(), n); + + lits.reset(); + for (unsigned j = 0; j < n; ++j) lits.push_back(~c[j]); + for (unsigned j = 0; j < k; ++j) lits.push_back(c.lit()); + add_cardinality(lits.size(), lits.c_ptr(), n); + } + // + // optionally handle xor constraints. + // + SASSERT(ext->m_xors.empty()); } - // 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() { - } void local_search::add_soft(literal l, double weight) { @@ -235,6 +256,46 @@ namespace sat { } lbool local_search::operator()() { + 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(); + for (int step = 1; step <= max_steps; ++step) { + // feasible + if (m_unsat_stack.empty()) { + calculate_and_update_ob(); + if (best_objective_value >= best_known_value) { + reach_known_best_value = true; + break; + } + } + flipvar = pick_var(); + flip(flipvar); + time_stamp[flipvar] = step; + } + // take a look at watch + stop = clock(); + elapsed_time = (double)(stop - start) / CLOCKS_PER_SEC; + if (elapsed_time > cutoff_time) + reach_cutoff_time = true; + if (reach_known_best_value || reach_cutoff_time) + break; + } + if (reach_known_best_value) { + std::cout << elapsed_time << "\n"; + } + else + std::cout << -1 << "\n"; + //print_solution(); + + // TBD: adjust return status return l_undef; } diff --git a/src/sat/sat_local_search.h b/src/sat/sat_local_search.h index 565180976..12f3c3756 100644 --- a/src/sat/sat_local_search.h +++ b/src/sat/sat_local_search.h @@ -122,6 +122,10 @@ namespace sat { void unsat(int constraint_id) { m_unsat_stack.push_back(constraint_id); } + 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) { int last_unsat_constraint = m_unsat_stack.back(); diff --git a/src/test/main.cpp b/src/test/main.cpp index 18b83e90e..6e7b60152 100644 --- a/src/test/main.cpp +++ b/src/test/main.cpp @@ -230,6 +230,7 @@ int main(int argc, char ** argv) { TST(get_consequences); TST(pb2bv); TST_ARGV(sat_lookahead); + TST_ARGV(sat_local_search); //TST_ARGV(hs); } diff --git a/src/test/sat_local_search.cpp b/src/test/sat_local_search.cpp new file mode 100644 index 000000000..1d92b37c7 --- /dev/null +++ b/src/test/sat_local_search.cpp @@ -0,0 +1,136 @@ +#include "sat_local_search.h" +#include "sat_solver.h" + +static int build_instance(char *filename, sat::solver& s, sat::local_search& ls) +{ + 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; + infile.getline(line, 16383); + int num_vars, num_constraints; + sscanf_s(line, "%d %d", &num_vars, &num_constraints); + //cout << "number of variables: " << num_vars << endl; + //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]; + } + + sat::literal_vector lits; + // ob variable + temp_count = 0; + infile >> cur_term; + while (cur_term != 0) { + temp[temp_count++] = cur_term; + infile >> cur_term; + } + if (temp_count != ob_num_terms) { + cout << "Objective function format error." << endl; + exit(-1); + } + 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; + } + // read the constraints, one at a time + card_extension* ext = 0; + int k; + for (c = 1; c <= num_constraints; ++c) { + lits.reset(); + infile >> cur_term; + while (cur_term != 0) { + lits.push_back(sat::literal(abs(cur_term), cur_term > 0)); + infile >> cur_term; + } + infile >> k; + ext->add_at_least(null_bool_var, lits, 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; +} + +void tst_sat_local_search(char ** argv, int argc, int& i) { + if (argc != i + 2) { + std::cout << "require dimacs file name\n"; + return; + } + // sat::solver s; + // populate the sat solver with clauses and cardinality consrtaints from the input + // call the lookahead solver. + // TBD +}