mirror of
https://github.com/Z3Prover/z3
synced 2025-04-24 17:45:32 +00:00
updates
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner
parent
c205b59a21
commit
31c68b6e23
6 changed files with 170 additions and 97 deletions
|
|
@ -21,6 +21,7 @@
|
|||
#include "sat_solver.h"
|
||||
#include "card_extension.h"
|
||||
#include "sat_params.hpp"
|
||||
#include "timer.h"
|
||||
|
||||
namespace sat {
|
||||
|
||||
|
|
@ -65,7 +66,7 @@ namespace sat {
|
|||
void local_search::init_cur_solution() {
|
||||
//cur_solution.resize(num_vars() + 1, false);
|
||||
for (unsigned v = 0; v < num_vars(); ++v) {
|
||||
cur_solution[v] = (rand() % 2 == 1);
|
||||
cur_solution[v] = (m_rand() % 2 == 1);
|
||||
}
|
||||
}
|
||||
|
||||
|
|
@ -138,7 +139,7 @@ namespace sat {
|
|||
init_cur_solution();
|
||||
|
||||
// init varibale information
|
||||
// variable 0 is the virtual variable
|
||||
// the last variable is the virtual variable
|
||||
|
||||
m_vars.back().m_score = INT_MIN;
|
||||
m_vars.back().m_conf_change = false;
|
||||
|
|
@ -169,8 +170,6 @@ namespace sat {
|
|||
if (objective_value > best_objective_value) {
|
||||
best_solution = cur_solution;
|
||||
best_objective_value = objective_value;
|
||||
stop = clock();
|
||||
best_time = (double)(stop - start) / CLOCKS_PER_SEC;
|
||||
}
|
||||
}
|
||||
|
||||
|
|
@ -197,7 +196,8 @@ namespace sat {
|
|||
}
|
||||
}
|
||||
|
||||
local_search::local_search(solver& s) {
|
||||
local_search::local_search(solver& s) :
|
||||
m_par(0) {
|
||||
|
||||
// copy units
|
||||
unsigned trail_sz = s.init_trail_size();
|
||||
|
|
@ -264,7 +264,7 @@ namespace sat {
|
|||
add_cardinality(lits.size(), lits.c_ptr(), n);
|
||||
}
|
||||
//
|
||||
// optionally handle xor constraints.
|
||||
// xor constraints should be disabled.
|
||||
//
|
||||
SASSERT(ext->m_xors.empty());
|
||||
}
|
||||
|
|
@ -273,24 +273,31 @@ namespace sat {
|
|||
local_search::~local_search() {
|
||||
}
|
||||
|
||||
void local_search::add_soft(int v, int weight) {
|
||||
// TBD
|
||||
ob_term t;
|
||||
t.var_id = v;
|
||||
t.coefficient = weight;
|
||||
ob_constraint.push_back(t);
|
||||
void local_search::add_soft(bool_var v, int weight) {
|
||||
ob_constraint.push_back(ob_term(v, weight));
|
||||
}
|
||||
|
||||
lbool local_search::check(parallel& p) {
|
||||
flet<parallel*> _p(m_par, &p);
|
||||
return check();
|
||||
}
|
||||
|
||||
lbool local_search::check() {
|
||||
return check(0, 0);
|
||||
}
|
||||
|
||||
lbool local_search::operator()() {
|
||||
lbool local_search::check(unsigned sz, literal const* assumptions) {
|
||||
//sat_params params;
|
||||
//std::cout << "my parameter value: " << params.cliff() << "\n";
|
||||
unsigned num_constraints = m_constraints.size();
|
||||
for (unsigned i = 0; i < sz; ++i) {
|
||||
add_clause(1, assumptions + i);
|
||||
}
|
||||
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
|
||||
start = clock();
|
||||
timer timer;
|
||||
timer.start();
|
||||
// ################## start ######################
|
||||
//std::cout << "Start initialize and local search, restart in every " << max_steps << " steps\n";
|
||||
unsigned tries, step;
|
||||
|
|
@ -309,25 +316,20 @@ namespace sat {
|
|||
flip(flipvar);
|
||||
m_vars[flipvar].m_time_stamp = 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';
|
||||
}
|
||||
if (elapsed_time > cutoff_time)
|
||||
reach_cutoff_time = true;
|
||||
if (reach_known_best_value || reach_cutoff_time)
|
||||
IF_VERBOSE(1, if (tries % 10 == 0) verbose_stream() << tries << ": " << timer.get_seconds() << '\n';);
|
||||
|
||||
if (!m_limit.inc())
|
||||
break;
|
||||
}
|
||||
if (reach_known_best_value) {
|
||||
std::cout << elapsed_time << "\n";
|
||||
}
|
||||
else {
|
||||
std::cout << -1 << "\n";
|
||||
}
|
||||
IF_VERBOSE(1, verbose_stream() << timer.get_seconds() << " " << (reach_known_best_value ? "reached":"not reached") << "\n";);
|
||||
|
||||
// remove unit clauses from assumptions.
|
||||
m_constraints.shrink(num_constraints);
|
||||
//print_solution();
|
||||
std::cout << tries * max_steps + step << '\n';
|
||||
IF_VERBOSE(1, verbose_stream() << tries * max_steps + step << '\n';);
|
||||
if (m_unsat_stack.empty() && ob_constraint.empty()) { // or all variables in ob_constraint are true
|
||||
return l_true;
|
||||
}
|
||||
// TBD: adjust return status
|
||||
return l_undef;
|
||||
}
|
||||
|
|
@ -354,7 +356,7 @@ namespace sat {
|
|||
case -2: // from -1 to -2
|
||||
for (unsigned j = 0; j < c.size(); ++j) {
|
||||
v = c[j].var();
|
||||
// flipping the slack increasing var will no long sat this constraint
|
||||
// flipping the slack increasing var will no longer satisfy this constraint
|
||||
if (is_true(c[j])) {
|
||||
//score[v] -= constraint_weight[c];
|
||||
dec_score(v);
|
||||
|
|
@ -378,7 +380,7 @@ namespace sat {
|
|||
v = c[j].var();
|
||||
// flip the slack decreasing var will falsify this constraint
|
||||
if (is_false(c[j])) {
|
||||
//score[v] -= constraint_weight[c];
|
||||
// score[v] -= constraint_weight[c];
|
||||
dec_score(v);
|
||||
dec_slack_score(v);
|
||||
}
|
||||
|
|
@ -459,14 +461,13 @@ namespace sat {
|
|||
vi.m_in_goodvar_stack = true;
|
||||
}
|
||||
}
|
||||
|
||||
}
|
||||
|
||||
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.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);
|
||||
//std::cout << v_imp << "\n";
|
||||
// std::cout << v_imp << "\n";
|
||||
// break tie 1: max imp
|
||||
// break tie 2: conf_change
|
||||
// break tie 3: time_stamp
|
||||
|
|
@ -521,7 +522,7 @@ namespace sat {
|
|||
}
|
||||
|
||||
// Diversification Mode
|
||||
constraint const& c = m_constraints[m_unsat_stack[rand() % m_unsat_stack.size()]]; // a random unsat constraint
|
||||
constraint const& c = m_constraints[m_unsat_stack[m_rand() % m_unsat_stack.size()]]; // a random unsat constraint
|
||||
// Within c, from all slack increasing var, choose the oldest one
|
||||
unsigned c_size = c.size();
|
||||
for (unsigned i = 0; i < c_size; ++i) {
|
||||
|
|
@ -534,13 +535,10 @@ namespace sat {
|
|||
|
||||
void local_search::set_parameters() {
|
||||
|
||||
srand(m_config.seed());
|
||||
cutoff_time = m_config.cutoff_time();
|
||||
m_rand.set_seed(m_config.seed());
|
||||
s_id = m_config.strategy_id();
|
||||
best_known_value = m_config.best_known_value();
|
||||
|
||||
|
||||
|
||||
if (s_id == 0)
|
||||
max_steps = 2 * num_vars();
|
||||
else {
|
||||
|
|
|
|||
|
|
@ -21,30 +21,29 @@
|
|||
|
||||
#include "vector.h"
|
||||
#include "sat_types.h"
|
||||
#include "rlimit.h"
|
||||
|
||||
namespace sat {
|
||||
|
||||
class parallel;
|
||||
|
||||
class local_search_config {
|
||||
unsigned m_seed;
|
||||
unsigned m_cutoff_time;
|
||||
unsigned m_strategy_id;
|
||||
int m_best_known_value;
|
||||
public:
|
||||
local_search_config()
|
||||
{
|
||||
m_seed = 0;
|
||||
m_cutoff_time = 1;
|
||||
m_strategy_id = 0;
|
||||
m_best_known_value = INT_MAX;
|
||||
}
|
||||
|
||||
unsigned seed() const { return m_seed; }
|
||||
unsigned cutoff_time() const { return m_cutoff_time; }
|
||||
unsigned strategy_id() const { return m_strategy_id; }
|
||||
unsigned best_known_value() const { return m_best_known_value; }
|
||||
|
||||
void set_seed(unsigned s) { m_seed = s; }
|
||||
void set_cutoff_time(unsigned t) { m_cutoff_time = t; }
|
||||
void set_strategy_id(unsigned i) { m_strategy_id = i; }
|
||||
void set_best_known_value(unsigned v) { m_best_known_value = v; }
|
||||
};
|
||||
|
|
@ -58,21 +57,8 @@ namespace sat {
|
|||
struct ob_term {
|
||||
bool_var var_id; // variable id, begin with 1
|
||||
int coefficient; // non-zero integer
|
||||
ob_term(bool_var v, int c): var_id(v), coefficient(c) {}
|
||||
};
|
||||
|
||||
// data structure for a term in constraint
|
||||
struct term {
|
||||
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
|
||||
};
|
||||
|
||||
|
||||
// objective function: maximize
|
||||
svector<ob_term> ob_constraint; // the objective function *constraint*, sorted in decending order
|
||||
|
||||
// information about the variable
|
||||
int_vector coefficient_in_ob_constraint; // initialized to be 0
|
||||
|
||||
struct var_info {
|
||||
bool m_conf_change; // whether its configure changes since its last flip
|
||||
|
|
@ -92,6 +78,24 @@ namespace sat {
|
|||
{}
|
||||
};
|
||||
|
||||
struct constraint {
|
||||
unsigned m_k;
|
||||
int m_slack;
|
||||
literal_vector m_literals;
|
||||
constraint(unsigned k) : m_k(k), m_slack(0) {}
|
||||
unsigned size() const { return m_literals.size(); }
|
||||
literal const& operator[](unsigned idx) const { return m_literals[idx]; }
|
||||
};
|
||||
|
||||
local_search_config m_config;
|
||||
|
||||
// objective function: maximize
|
||||
svector<ob_term> ob_constraint; // the objective function *constraint*, sorted in decending order
|
||||
|
||||
// information about the variable
|
||||
int_vector coefficient_in_ob_constraint; // var! initialized to be 0
|
||||
|
||||
|
||||
vector<var_info> m_vars;
|
||||
|
||||
inline int score(bool_var v) const { return m_vars[v].m_score; }
|
||||
|
|
@ -107,23 +111,14 @@ namespace sat {
|
|||
inline int time_stamp(bool_var v) const { return m_vars[v].m_time_stamp; }
|
||||
inline int cscc(bool_var v) const { return m_vars[v].m_cscc; }
|
||||
inline void inc_cscc(bool_var v) { m_vars[v].m_cscc++; }
|
||||
|
||||
unsigned num_vars() const { return m_vars.size() - 1; } // var index from 1 to num_vars
|
||||
|
||||
/* TBD: other scores */
|
||||
|
||||
struct constraint {
|
||||
unsigned m_k;
|
||||
int m_slack;
|
||||
literal_vector m_literals;
|
||||
constraint(unsigned k) : m_k(k), m_slack(0) {}
|
||||
unsigned size() const { return m_literals.size(); }
|
||||
literal const& operator[](unsigned idx) const { return m_literals[idx]; }
|
||||
};
|
||||
|
||||
vector<constraint> m_constraints;
|
||||
|
||||
inline bool is_pos(literal t) const { return !t.sign(); }
|
||||
inline bool is_true(bool_var v) const { return cur_solution[v]; }
|
||||
inline bool is_true(literal l) const { return cur_solution[l.var()] != l.sign(); }
|
||||
inline bool is_false(literal l) const { return cur_solution[l.var()] == l.sign(); }
|
||||
|
||||
|
|
@ -141,22 +136,21 @@ namespace sat {
|
|||
int_vector goodvar_stack;
|
||||
|
||||
// information about solution
|
||||
bool_vector cur_solution; // the current solution
|
||||
bool_vector cur_solution; // !var: the current solution
|
||||
int objective_value; // the objective function value corresponds to the current solution
|
||||
bool_vector best_solution; // the best solution so far
|
||||
bool_vector best_solution; // !var: the best solution so far
|
||||
int best_objective_value = -1; // 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
|
||||
unsigned max_steps = 2000000000; // < 2147483647
|
||||
clock_t start, stop;
|
||||
double best_time;
|
||||
|
||||
// for tuning
|
||||
int s_id = 0; // strategy id
|
||||
|
||||
reslimit m_limit;
|
||||
random_gen m_rand;
|
||||
parallel* m_par;
|
||||
|
||||
void init();
|
||||
void reinit();
|
||||
|
|
@ -220,24 +214,31 @@ namespace sat {
|
|||
m_unsat_stack.pop_back();
|
||||
}
|
||||
|
||||
|
||||
public:
|
||||
local_search(solver& s);
|
||||
|
||||
reslimit& rlimit() { return m_limit; }
|
||||
|
||||
~local_search();
|
||||
|
||||
void add_soft(int l, int weight);
|
||||
void add_soft(bool_var v, int weight);
|
||||
|
||||
void add_cardinality(unsigned sz, literal const* c, unsigned k);
|
||||
|
||||
lbool operator()();
|
||||
lbool check();
|
||||
|
||||
lbool check(unsigned sz, literal const* assumptions) { return l_undef; } // TBD
|
||||
lbool check(unsigned sz, literal const* assumptions);
|
||||
|
||||
void cancel() {} // TBD
|
||||
lbool check(parallel& p);
|
||||
|
||||
local_search_config& config() { return m_config; }
|
||||
|
||||
local_search_config m_config;
|
||||
unsigned num_vars() const { return m_vars.size() - 1; } // var index from 1 to num_vars
|
||||
|
||||
void set_phase(bool_var v, bool f) {}
|
||||
|
||||
bool get_phase(bool_var v) const { return is_true(v); }
|
||||
};
|
||||
}
|
||||
|
||||
|
|
|
|||
|
|
@ -106,6 +106,7 @@ namespace sat {
|
|||
for (unsigned i = 0; i < num_extra_solvers; ++i) {
|
||||
m_limits.push_back(reslimit());
|
||||
}
|
||||
|
||||
for (unsigned i = 0; i < num_extra_solvers; ++i) {
|
||||
s.m_params.set_uint("random_seed", s.m_rand());
|
||||
if (i == 1 + num_threads/2) {
|
||||
|
|
@ -204,5 +205,59 @@ namespace sat {
|
|||
return (c.size() <= 40 && c.glue() <= 8) || c.glue() <= 2;
|
||||
}
|
||||
|
||||
void parallel::set_phase(solver& s) {
|
||||
#pragma omp critical (par_solver)
|
||||
{
|
||||
m_phase.reserve(s.num_vars(), 0);
|
||||
for (unsigned i = 0; i < s.num_vars(); ++i) {
|
||||
if (s.value(i) != l_undef) {
|
||||
m_phase[i] += (s.value(i) == l_true) ? 1 : -1;
|
||||
continue;
|
||||
}
|
||||
switch (s.m_phase[i]) {
|
||||
case POS_PHASE:
|
||||
m_phase[i]++;
|
||||
break;
|
||||
case NEG_PHASE:
|
||||
m_phase[i]--;
|
||||
break;
|
||||
default:
|
||||
break;
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
void parallel::get_phase(solver& s) {
|
||||
#pragma omp critical (par_solver)
|
||||
{
|
||||
m_phase.reserve(s.num_vars(), 0);
|
||||
for (unsigned i = 0; i < s.num_vars(); ++i) {
|
||||
if (m_phase[i] < 0) {
|
||||
s.m_phase[i] = NEG_PHASE;
|
||||
}
|
||||
else if (m_phase[i] > 0) {
|
||||
s.m_phase[i] = POS_PHASE;
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
void parallel::get_phase(local_search& s) {
|
||||
#pragma omp critical (par_solver)
|
||||
{
|
||||
m_phase.reserve(s.num_vars(), 0);
|
||||
for (unsigned i = 0; i < s.num_vars(); ++i) {
|
||||
if (m_phase[i] < 0) {
|
||||
s.set_phase(i, false);
|
||||
}
|
||||
else if (m_phase[i] > 0) {
|
||||
s.set_phase(i, true);
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
|
||||
};
|
||||
|
||||
|
|
|
|||
|
|
@ -26,6 +26,8 @@ Revision History:
|
|||
|
||||
namespace sat {
|
||||
|
||||
class local_search;
|
||||
|
||||
class parallel {
|
||||
|
||||
// shared pool of learned clauses.
|
||||
|
|
@ -56,6 +58,7 @@ namespace sat {
|
|||
index_set m_unit_set;
|
||||
literal_vector m_lits;
|
||||
vector_pool m_pool;
|
||||
int_vector m_phase;
|
||||
|
||||
scoped_limits m_scoped_rlimit;
|
||||
vector<reslimit> m_limits;
|
||||
|
|
@ -86,6 +89,15 @@ namespace sat {
|
|||
|
||||
// receive clauses from shared clause pool
|
||||
void get_clauses(solver& s);
|
||||
|
||||
// exchange phase of variables.
|
||||
void set_phase(solver& s);
|
||||
|
||||
void get_phase(solver& s);
|
||||
|
||||
void set_phase(local_search& s);
|
||||
|
||||
void get_phase(local_search& s);
|
||||
};
|
||||
|
||||
};
|
||||
|
|
|
|||
|
|
@ -864,7 +864,7 @@ namespace sat {
|
|||
|
||||
lbool solver::check_par(unsigned num_lits, literal const* lits) {
|
||||
int num_threads = static_cast<int>(m_config.m_num_threads);
|
||||
int num_extra_solvers = num_threads - 1 + (m_local_search ? 1 : 0);
|
||||
int num_extra_solvers = num_threads - 1 - (m_local_search ? 1 : 0);
|
||||
sat::parallel par(*this);
|
||||
par.reserve(num_threads, 1 << 12);
|
||||
par.init_solvers(*this, num_extra_solvers);
|
||||
|
|
@ -878,7 +878,7 @@ namespace sat {
|
|||
for (int i = 0; i < num_threads; ++i) {
|
||||
try {
|
||||
lbool r = l_undef;
|
||||
if (m_local_search && i + 1 == num_extra_solvers) {
|
||||
if (m_local_search && i == num_extra_solvers) {
|
||||
r = m_local_search->check(num_lits, lits);
|
||||
}
|
||||
else if (i < num_extra_solvers) {
|
||||
|
|
@ -898,7 +898,7 @@ namespace sat {
|
|||
}
|
||||
if (first) {
|
||||
if (m_local_search) {
|
||||
m_local_search->cancel();
|
||||
m_local_search->rlimit().cancel();
|
||||
}
|
||||
for (int j = 0; j < num_extra_solvers; ++j) {
|
||||
if (i != j) {
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue