mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-13 20:38:43 +00:00
Code Activity

updates to local search integration

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2017-03-02 11:23:06 -08:00
parent 40df1949f5
commit c6f943e4d6
4 changed files with 39 additions and 21 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

41
src/sat/sat_local_search.cpp
View file

@ -31,7 +31,6 @@ namespace sat {
m_vars.push_back(var_info());
best_solution.resize(num_vars() + 1, false);
cur_solution.resize(num_vars() + 1, false);
m_index_in_unsat_stack.resize(num_constraints(), 0);
coefficient_in_ob_constraint.resize(num_vars() + 1, 0);
@ -65,7 +64,7 @@ namespace sat {
void local_search::init_cur_solution() {
for (unsigned v = 0; v < num_vars(); ++v) {
cur_solution[v] = (m_rand() % 2 == 1);
m_vars[v].m_value = ((unsigned)(m_rand() % 100) < m_vars[v].m_bias);
}
}
@ -88,7 +87,7 @@ namespace sat {
// figure out variables scores and slack_scores
void local_search::init_scores() {
for (unsigned v = 0; v < num_vars(); ++v) {
bool is_true = cur_solution[v];
bool is_true = cur_solution(v);
int_vector& truep = m_vars[v].m_watch[is_true];
int_vector& falsep = m_vars[v].m_watch[!is_true];
for (unsigned i = 0; i < falsep.size(); ++i) {
@ -162,11 +161,14 @@ namespace sat {
objective_value = 0;
for (i = 0; i < ob_constraint.size(); ++i) {
v = ob_constraint[i].var_id;
if (cur_solution[v])
if (cur_solution(v))
objective_value += ob_constraint[i].coefficient;
}
if (objective_value > best_objective_value) {
best_solution = cur_solution;
best_solution.reset();
for (unsigned v = 0; v < num_vars(); ++v) {
best_solution.push_back(cur_solution(v));
}
best_objective_value = objective_value;
}
}
@ -174,7 +176,7 @@ namespace sat {
bool local_search::all_objectives_are_met() const {
for (unsigned i = 0; i < ob_constraint.size(); ++i) {
bool_var v = ob_constraint[i].var_id;
if (!cur_solution[v]) return false;
if (!cur_solution(v)) return false;
}
return true;
}
@ -216,6 +218,9 @@ namespace sat {
m_vars[t.var()].m_watch[is_pos(t)].push_back(id);
m_constraints.back().m_literals.push_back(t);
}
if (sz == 1 && k == 0) {
m_vars[c[0].var()].m_bias = c[0].sign() ? 0 : 100;
}
}
local_search::local_search(solver& s) :
@ -354,7 +359,7 @@ namespace sat {
// tell the SAT solvers about the phase of variables.
if (m_par && tries % 10 == 0) {
m_par->set_phase(*this);
m_par->get_phase(*this);
}
}
@ -373,6 +378,7 @@ namespace sat {
result = l_undef;
}
IF_VERBOSE(1, verbose_stream() << "(sat-local-search " << result << ")\n";);
IF_VERBOSE(2, display(verbose_stream()););
return result;
}
@ -394,13 +400,13 @@ namespace sat {
void local_search::flip(bool_var flipvar)
{
// already changed truth value!!!!
cur_solution[flipvar] = !cur_solution[flipvar];
m_vars[flipvar].m_value = !cur_solution(flipvar);
unsigned v;
int org_flipvar_score = score(flipvar);
int org_flipvar_slack_score = slack_score(flipvar);
bool flip_is_true = cur_solution[flipvar];
bool flip_is_true = cur_solution(flipvar);
int_vector& truep = m_vars[flipvar].m_watch[flip_is_true];
int_vector& falsep = m_vars[flipvar].m_watch[!flip_is_true];
@ -521,8 +527,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.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);
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";
// break tie 1: max imp
// break tie 2: conf_change
@ -615,14 +621,14 @@ namespace sat {
void local_search::print_info(std::ostream& out) {
for (unsigned v = 0; v < num_vars(); ++v) {
out << "v" << v << "\t" << m_vars[v].m_neighbors.size() << '\t' << cur_solution[v] << '\t' << conf_change(v) << '\t' << score(v) << '\t' << slack_score(v) << '\n';
out << "v" << v << "\t" << m_vars[v].m_neighbors.size() << '\t' << cur_solution(v) << '\t' << conf_change(v) << '\t' << score(v) << '\t' << slack_score(v) << '\n';
}
}
void local_search::extract_model() {
m_model.reset();
for (unsigned v = 0; v < num_vars(); ++v) {
m_model.push_back(cur_solution[v] ? l_true : l_false);
m_model.push_back(cur_solution(v) ? l_true : l_false);
}
}
@ -631,6 +637,9 @@ namespace sat {
constraint const& c = m_constraints[i];
display(out, c);
}
for (bool_var v = 0; v < num_vars(); ++v) {
display(out, v, m_vars[v]);
}
}
void local_search::display(std::ostream& out, constraint const& c) const {
@ -638,7 +647,7 @@ namespace sat {
}
void local_search::display(std::ostream& out, unsigned v, var_info const& vi) const {
out << "v" << v << "\n";
out << "v" << v << " := " << (vi.m_value?"true":"false") << " bias: " << vi.m_bias << "\n";
}
bool local_search::check_goodvar() {
@ -662,7 +671,9 @@ namespace sat {
}
void local_search::set_phase(bool_var v, bool f) {
std::cout << v << " " << f << "\n";
unsigned& bias = m_vars[v].m_bias;
if (f && bias < 100) bias++;
if (!f && bias > 0) bias--;
}
}

14
src/sat/sat_local_search.h
View file

@ -61,6 +61,9 @@ namespace sat {
};
struct var_info {
bool m_value; // current solution
unsigned m_bias; // bias for current solution in percentage.
// if bias is 0, then value is always false, if 100, then always true
bool m_conf_change; // whether its configure changes since its last flip
bool m_in_goodvar_stack;
int m_score;
@ -70,6 +73,8 @@ namespace sat {
bool_var_vector m_neighbors; // neighborhood variables
int_vector m_watch[2];
var_info():
m_value(true),
m_bias(50),
m_conf_change(true),
m_in_goodvar_stack(false),
m_score(0),
@ -111,6 +116,8 @@ 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++; }
inline bool cur_solution(bool_var v) const { return m_vars[v].m_value; }
/* TBD: other scores */
@ -118,9 +125,9 @@ namespace sat {
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(); }
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(); }
unsigned num_constraints() const { return m_constraints.size(); } // constraint index from 1 to num_constraint
@ -136,7 +143,6 @@ namespace sat {
int_vector goodvar_stack;
// information about 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; // !var: the best solution so far
int best_objective_value = -1; // the objective value corresponds to the best solution so far

4
src/sat/sat_parallel.cpp
View file

@ -258,7 +258,7 @@ namespace sat {
}
}
void parallel::set_phase(local_search& s) {
void parallel::get_phase(local_search& s) {
#pragma omp critical (par_solver)
{
for (unsigned i = 0; i < m_phase.size(); ++i) {
@ -273,7 +273,7 @@ namespace sat {
}
}
void parallel::get_phase(local_search& s) {
void parallel::set_phase(local_search& s) {
#pragma omp critical (par_solver)
{
m_phase.reserve(s.num_vars(), 0);

1
src/sat/sat_solver.cpp
View file

@ -963,6 +963,7 @@ namespace sat {
\brief import lemmas/units from parallel sat solvers.
*/
void solver::exchange_par() {
if (m_par && at_search_lvl()) m_par->set_phase(*this);
if (m_par && at_base_lvl()) m_par->get_clauses(*this);
if (m_par && at_base_lvl()) {
// SASSERT(scope_lvl() == search_lvl());