From 747ff19abad1cc118338623267ef749ee44f57e0 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 21 Feb 2017 20:34:39 -0800 Subject: [PATCH] adding skeleton for local search Signed-off-by: Nikolaj Bjorner --- contrib/cmake/src/sat/CMakeLists.txt | 1 + src/sat/sat_local_search.cpp | 77 +++++++++++++++++ src/sat/sat_local_search.h | 125 +++++++++++++++++++++++++++ src/sat/sat_lookahead.h | 35 +++++--- 4 files changed, 226 insertions(+), 12 deletions(-) create mode 100644 src/sat/sat_local_search.cpp create mode 100644 src/sat/sat_local_search.h diff --git a/contrib/cmake/src/sat/CMakeLists.txt b/contrib/cmake/src/sat/CMakeLists.txt index 00c988f5c..5494049d7 100644 --- a/contrib/cmake/src/sat/CMakeLists.txt +++ b/contrib/cmake/src/sat/CMakeLists.txt @@ -12,6 +12,7 @@ z3_add_component(sat sat_elim_eqs.cpp sat_iff3_finder.cpp sat_integrity_checker.cpp + sat_local_search.cpp sat_model_converter.cpp sat_mus.cpp sat_parallel.cpp diff --git a/src/sat/sat_local_search.cpp b/src/sat/sat_local_search.cpp new file mode 100644 index 000000000..5b8f44783 --- /dev/null +++ b/src/sat/sat_local_search.cpp @@ -0,0 +1,77 @@ +/*++ +Copyright (c) 2017 Microsoft Corporation + +Module Name: + + sat_local_search.cpp + +Abstract: + + Local search module for cardinality clauses. + +Author: + + Sixue Liu 2017-2-21 + +Notes: + +--*/ + +#include "sat_local_search.h" + +namespace sat { + + void local_search::init() { + + } + + bool_var local_search::pick_var() { + + return null_bool_var; + } + + void local_search::flip(bool_var v) { + + + } + + bool local_search::tie_breaker_sat(int, int) { + + return false; + } + + bool local_search::tie_breaker_ccd(int, int) { + + return false; + } + + void local_search::calculate_and_update_ob() { + + } + + void local_search::verify_solution() { + + } + + void local_search::display(std::ostream& out) { + + } + + local_search::local_search(solver& s) { + + } + + local_search::~local_search() { + + } + + void local_search::add_soft(literal l, double weight) { + + } + + lbool local_search::operator()() { + return l_undef; + } + + +} diff --git a/src/sat/sat_local_search.h b/src/sat/sat_local_search.h new file mode 100644 index 000000000..169596888 --- /dev/null +++ b/src/sat/sat_local_search.h @@ -0,0 +1,125 @@ +/*++ +Copyright (c) 2017 Microsoft Corporation + +Module Name: + + sat_local_search.h + +Abstract: + + Local search module for cardinality clauses. + +Author: + + Sixue Liu 2017-2-21 + +Notes: + +--*/ +#ifndef _SAT_LOCAL_SEARCH_H_ +#define _SAT_LOCAL_SEARCH_H_ + +#include "vector.h" +#include "sat_types.h" + +namespace sat { + + class local_search { + + typedef svector bool_vector; + + // data structure for a term in objective function + struct ob_term { + int 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 sense; // 1 for positive, 0 for negative + //int coefficient; // all constraints are cardinality: coefficient=1 + }; + + // 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; + + // 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 + + + // 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 + + // information about the variable + int_vector coefficient_in_ob_constraint; // initilized to be 0 + int_vector 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 + /* TBD: other scores */ + + // information about the constraints + int_vector constraint_k; // the right side k of a constraint + int_vector constraint_slack; // =constraint_k[i]-true_terms[i], if >=0 then sat + int_vector nb_slack; // constraint_k - ob_var(same in ob) - none_ob_true_terms_count. if < 0: some ob var might be flipped to false, result in an ob decreasing + bool_vector has_true_ob_terms; + + // unsat constraint stack + int_vector unsat_stack; // store all the unsat constraits + int_vector index_in_unsat_stack; // which position is a contraint in the unsat_stack + + // 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 + bool_vector best_solution; // the best solution so far + int best_objective_value = 0; // the objective value corresponds to the best solution so far + // for non-known instance, set as maximal + int best_known_value = INT_MAX; // best known value for this instance + + // cutoff + int cutoff_time = 1; // seconds + int max_steps = 2000000000; // < 2147483647 + + // for tuning + int s_id = 0; // strategy id + + void init(); + bool_var pick_var(); + void flip(bool_var v); + bool tie_breaker_sat(int, int); + bool tie_breaker_ccd(int, int); + + + void calculate_and_update_ob(); + + void verify_solution(); + + void display(std::ostream& out); + + public: + local_search(solver& s); + + ~local_search(); + + void add_soft(literal l, double weight); + + lbool operator()(); + + + }; +} + +#endif diff --git a/src/sat/sat_lookahead.h b/src/sat/sat_lookahead.h index eb713ab7c..4872a548a 100644 --- a/src/sat/sat_lookahead.h +++ b/src/sat/sat_lookahead.h @@ -281,7 +281,7 @@ namespace sat { } // - // lit1 => lit2. + // lit1 => lit2.n // if lit2 is a node, put lit1 above lit2 // @@ -351,23 +351,34 @@ namespace sat { } } + lbool backtrack(literal_vector& trail) { + if (inconsistent()) { + if (trail.empty()) return l_false; + pop(); + assign(~trail.back()); + trail.pop_back(); + return l_true; + } + return l_undef; + } + lbool search() { literal_vector trail; -#define BACKTRACK \ - if (inconsistent()) { \ - if (trail.empty()) return l_false; \ - pop(); \ - assign(~trail.back()); \ - trail.pop_back(); \ - continue; \ - } \ - while (true) { s.checkpoint(); - BACKTRACK; + switch (backtrack(trail)) { + case l_true: continue; + case l_false: return l_false; + case l_undef: break; + } + literal l = choose(); - BACKTRACK; + switch (backtrack(trail)) { + case l_true: continue; + case l_false: return l_false; + case l_undef: break; + } if (l == null_literal) { return l_true; }