mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 13:28:47 +00:00
Code Activity

revise local search

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2019-02-11 13:14:20 -08:00
parent 22783a4bcb
commit 5fe40a25dc
3 changed files with 159 additions and 486 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

478
src/sat/sat_local_search.cpp
View file

@ -26,7 +26,8 @@ Notes:
namespace sat { namespace sat {
void local_search::init() { void local_search::init() {
flet<bool> _init(m_initializing, true);
m_unsat_stack.reset();
for (unsigned i = 0; i < m_assumptions.size(); ++i) { for (unsigned i = 0; i < m_assumptions.size(); ++i) {
add_clause(1, m_assumptions.c_ptr() + i); add_clause(1, m_assumptions.c_ptr() + i);
} }
@ -37,7 +38,7 @@ namespace sat {
if (m_config.phase_sticky()) { if (m_config.phase_sticky()) {
for (var_info& vi : m_vars) for (var_info& vi : m_vars)
if (!vi.m_unit) if (!vi.m_unit)
vi.m_value = vi.m_bias < 100; vi.m_value = vi.m_bias > 50;
} }
else { else {
for (var_info& vi : m_vars) for (var_info& vi : m_vars)
@ -45,42 +46,14 @@ namespace sat {
vi.m_value = (0 == (m_rand() % 2)); vi.m_value = (0 == (m_rand() % 2));
} }
m_best_solution.resize(num_vars() + 1, false);
m_index_in_unsat_stack.resize(num_constraints(), 0); m_index_in_unsat_stack.resize(num_constraints(), 0);
coefficient_in_ob_constraint.resize(num_vars() + 1, 0);
if (m_config.mode() == local_search_mode::gsat) {
uint_set is_neighbor;
for (bool_var v = 0; v < num_vars(); ++v) {
is_neighbor.reset();
bool pol = true;
var_info& vi = m_vars[v];
for (unsigned k = 0; k < 2; pol = !pol, k++) {
for (auto const& wi : m_vars[v].m_watch[pol]) {
constraint const& c = m_constraints[wi.m_constraint_id];
for (literal lit : c) {
bool_var w = lit.var();
if (w == v || is_neighbor.contains(w)) continue;
is_neighbor.insert(w);
vi.m_neighbors.push_back(w);
}
}
}
}
}
for (auto const& c : ob_constraint) {
coefficient_in_ob_constraint[c.var_id] = c.coefficient;
}
set_parameters(); set_parameters();
} }
void local_search::init_cur_solution() { void local_search::init_cur_solution() {
for (var_info& vi : m_vars) { for (var_info& vi : m_vars) {
// use bias with a small probability
if (!vi.m_unit) { if (!vi.m_unit) {
if (m_rand() % 10 < 5 || m_config.phase_sticky()) { if (m_config.phase_sticky()) {
vi.m_value = ((unsigned)(m_rand() % 100) < vi.m_bias); vi.m_value = ((unsigned)(m_rand() % 100) < vi.m_bias);
} }
else { else {
@ -116,7 +89,6 @@ namespace sat {
coeff_vector& falsep = m_vars[v].m_watch[!is_true]; coeff_vector& falsep = m_vars[v].m_watch[!is_true];
for (auto const& coeff : falsep) { for (auto const& coeff : falsep) {
constraint& c = m_constraints[coeff.m_constraint_id]; constraint& c = m_constraints[coeff.m_constraint_id];
//SASSERT(falsep[i].m_coeff == 1);
// will --slack // will --slack
if (c.m_slack <= 0) { if (c.m_slack <= 0) {
dec_slack_score(v); dec_slack_score(v);
@ -125,7 +97,6 @@ namespace sat {
} }
} }
for (auto const& coeff : truep) { for (auto const& coeff : truep) {
//SASSERT(coeff.m_coeff == 1);
constraint& c = m_constraints[coeff.m_constraint_id]; constraint& c = m_constraints[coeff.m_constraint_id];
// will --true_terms_count[c] // will --true_terms_count[c]
// will ++slack // will ++slack
@ -151,22 +122,19 @@ namespace sat {
void local_search::reinit() { void local_search::reinit() {
IF_VERBOSE(1, verbose_stream() << "(sat-local-search reinit)\n";); //
if (true || !m_is_pb) { // the following methods does NOT converge for pseudo-boolean
// // can try other way to define "worse" and "better"
// the following methods does NOT converge for pseudo-boolean // the current best noise is below 1000
// can try other way to define "worse" and "better" //
// the current best noise is below 1000 if (m_best_unsat_rate > m_last_best_unsat_rate) {
// // worse
if (m_best_unsat_rate > m_last_best_unsat_rate) { m_noise -= m_noise * 2 * m_noise_delta;
// worse m_best_unsat_rate *= 1000.0;
m_noise -= m_noise * 2 * m_noise_delta; }
m_best_unsat_rate *= 1000.0; else {
} // better
else { m_noise += (10000 - m_noise) * m_noise_delta;
// better
m_noise += (10000 - m_noise) * m_noise_delta;
}
} }
for (constraint & c : m_constraints) { for (constraint & c : m_constraints) {
@ -186,11 +154,9 @@ namespace sat {
m_vars.back().m_score = INT_MIN; m_vars.back().m_score = INT_MIN;
m_vars.back().m_conf_change = false; m_vars.back().m_conf_change = false;
m_vars.back().m_slack_score = INT_MIN; m_vars.back().m_slack_score = INT_MIN;
m_vars.back().m_cscc = 0;
m_vars.back().m_time_stamp = m_max_steps + 1; m_vars.back().m_time_stamp = m_max_steps + 1;
for (unsigned i = 0; i < num_vars(); ++i) { for (unsigned i = 0; i < num_vars(); ++i) {
m_vars[i].m_time_stamp = 0; m_vars[i].m_time_stamp = 0;
m_vars[i].m_cscc = 1;
m_vars[i].m_conf_change = true; m_vars[i].m_conf_change = true;
m_vars[i].m_in_goodvar_stack = false; m_vars[i].m_in_goodvar_stack = false;
m_vars[i].m_score = 0; m_vars[i].m_score = 0;
@ -208,6 +174,7 @@ namespace sat {
if (m_is_unsat) { if (m_is_unsat) {
IF_VERBOSE(0, verbose_stream() << "unsat during reinit\n"); IF_VERBOSE(0, verbose_stream() << "unsat during reinit\n");
} }
DEBUG_CODE(verify_slack(););
} }
bool local_search::propagate(literal lit) { bool local_search::propagate(literal lit) {
@ -230,9 +197,9 @@ namespace sat {
return false; return false;
} }
if (unit) { if (unit) {
for (literal lit : m_prop_queue) { for (literal lit2 : m_prop_queue) {
VERIFY(is_true(lit)); VERIFY(is_true(lit2));
add_unit(lit); add_unit(lit2, lit);
} }
} }
return true; return true;
@ -253,32 +220,7 @@ namespace sat {
constraint const& c = m_constraints[m_unsat_stack[0]]; constraint const& c = m_constraints[m_unsat_stack[0]];
IF_VERBOSE(2, display(verbose_stream() << "single unsat:", c)); IF_VERBOSE(2, display(verbose_stream() << "single unsat:", c));
} }
} }
void local_search::calculate_and_update_ob() {
unsigned i, v;
int objective_value = 0;
for (i = 0; i < ob_constraint.size(); ++i) {
v = ob_constraint[i].var_id;
if (cur_solution(v))
objective_value += ob_constraint[i].coefficient;
}
if (objective_value > m_best_objective_value) {
m_best_solution.reset();
for (unsigned v = 0; v < num_vars(); ++v) {
m_best_solution.push_back(cur_solution(v));
}
m_best_objective_value = objective_value;
}
}
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;
}
return true;
}
void local_search::verify_solution() const { void local_search::verify_solution() const {
IF_VERBOSE(0, verbose_stream() << "verifying solution\n"); IF_VERBOSE(0, verbose_stream() << "verifying solution\n");
@ -289,10 +231,24 @@ namespace sat {
void local_search::verify_unsat_stack() const { void local_search::verify_unsat_stack() const {
for (unsigned i : m_unsat_stack) { for (unsigned i : m_unsat_stack) {
constraint const& c = m_constraints[i]; constraint const& c = m_constraints[i];
if (c.m_k >= constraint_value(c)) {
IF_VERBOSE(0, display(verbose_stream() << i << " ", c) << "\n");
IF_VERBOSE(0, verbose_stream() << "units " << m_units << "\n");
}
VERIFY(c.m_k < constraint_value(c)); VERIFY(c.m_k < constraint_value(c));
} }
} }
bool local_search::verify_goodvar() const {
unsigned g = 0;
for (unsigned v = 0; v < num_vars(); ++v) {
if (conf_change(v) && score(v) > 0) {
++g;
}
}
return g == m_goodvar_stack.size();
}
unsigned local_search::constraint_coeff(constraint const& c, literal l) const { unsigned local_search::constraint_coeff(constraint const& c, literal l) const {
for (auto const& pb : m_vars[l.var()].m_watch[is_pos(l)]) { for (auto const& pb : m_vars[l.var()].m_watch[is_pos(l)]) {
if (pb.m_constraint_id == c.m_id) return pb.m_coeff; if (pb.m_constraint_id == c.m_id) return pb.m_coeff;
@ -301,6 +257,24 @@ namespace sat {
return 0; return 0;
} }
void local_search::verify_constraint(constraint const& c) const {
unsigned value = constraint_value(c);
IF_VERBOSE(11, display(verbose_stream() << "verify ", c););
TRACE("sat", display(verbose_stream() << "verify ", c););
if (c.m_k < value) {
IF_VERBOSE(0, display(verbose_stream() << "violated constraint: ", c) << "value: " << value << "\n";);
}
}
void local_search::verify_slack(constraint const& c) const {
VERIFY(constraint_value(c) + c.m_slack == c.m_k);
}
void local_search::verify_slack() const {
for (constraint const& c : m_constraints) {
verify_slack(c);
}
}
unsigned local_search::constraint_value(constraint const& c) const { unsigned local_search::constraint_value(constraint const& c) const {
unsigned value = 0; unsigned value = 0;
@ -311,15 +285,6 @@ namespace sat {
} }
return value; return value;
} }
void local_search::verify_constraint(constraint const& c) const {
unsigned value = constraint_value(c);
IF_VERBOSE(11, display(verbose_stream() << "verify ", c););
TRACE("sat", display(verbose_stream() << "verify ", c););
if (c.m_k < value) {
IF_VERBOSE(0, display(verbose_stream() << "violated constraint: ", c) << "value: " << value << "\n";);
}
}
void local_search::add_clause(unsigned sz, literal const* c) { void local_search::add_clause(unsigned sz, literal const* c) {
add_cardinality(sz, c, sz - 1); add_cardinality(sz, c, sz - 1);
@ -328,7 +293,7 @@ namespace sat {
// ~c <= k // ~c <= k
void local_search::add_cardinality(unsigned sz, literal const* c, unsigned k) { void local_search::add_cardinality(unsigned sz, literal const* c, unsigned k) {
if (sz == 1 && k == 0) { if (sz == 1 && k == 0) {
add_unit(c[0]); add_unit(c[0], null_literal);
return; return;
} }
if (k == 1 && sz == 2) { if (k == 1 && sz == 2) {
@ -353,7 +318,7 @@ namespace sat {
// c * coeffs <= k // c * coeffs <= k
void local_search::add_pb(unsigned sz, literal const* c, unsigned const* coeffs, unsigned k) { void local_search::add_pb(unsigned sz, literal const* c, unsigned const* coeffs, unsigned k) {
if (sz == 1 && k == 0) { if (sz == 1 && k == 0) {
add_unit(~c[0]); add_unit(~c[0], null_literal);
return; return;
} }
unsigned id = m_constraints.size(); unsigned id = m_constraints.size();
@ -366,15 +331,19 @@ namespace sat {
} }
} }
void local_search::add_unit(literal lit) { void local_search::add_unit(literal lit, literal exp) {
bool_var v = lit.var(); bool_var v = lit.var();
if (is_unit(lit)) return; if (is_unit(lit)) return;
VERIFY(!m_units.contains(v)); SASSERT(!m_units.contains(v));
m_vars[v].m_bias = lit.sign() ? 0 : 100; if (m_vars[v].m_value == lit.sign() && !m_initializing) {
flip_walksat(v);
}
m_vars[v].m_value = !lit.sign(); m_vars[v].m_value = !lit.sign();
m_vars[v].m_bias = lit.sign() ? 0 : 100;
m_vars[v].m_unit = true; m_vars[v].m_unit = true;
m_vars[v].m_explain = exp;
m_units.push_back(v); m_units.push_back(v);
verify_unsat_stack(); DEBUG_CODE(verify_unsat_stack(););
} }
local_search::local_search() : local_search::local_search() :
@ -383,19 +352,19 @@ namespace sat {
} }
void local_search::import(solver& s, bool _init) { void local_search::import(solver& s, bool _init) {
flet<bool> linit(m_initializing, true);
m_is_pb = false; m_is_pb = false;
m_vars.reset(); m_vars.reset();
m_constraints.reset(); m_constraints.reset();
m_units.reset(); m_units.reset();
m_unsat_stack.reset(); m_unsat_stack.reset();
m_vars.reserve(s.num_vars()); m_vars.reserve(s.num_vars());
m_config.set_config(s.get_config());
if (m_config.phase_sticky()) { if (m_config.phase_sticky()) {
unsigned v = 0; unsigned v = 0;
for (var_info& vi : m_vars) { for (var_info& vi : m_vars) {
if (!vi.m_unit) vi.m_bias = s.m_phase[v++] == POS_PHASE ? 98 : 2;
vi.m_bias = s.m_phase[v] == POS_PHASE ? 100 : 0;
++v;
} }
} }
@ -524,9 +493,6 @@ namespace sat {
local_search::~local_search() { local_search::~local_search() {
} }
void local_search::add_soft(bool_var v, int weight) {
ob_constraint.push_back(ob_term(v, weight));
}
lbool local_search::check() { lbool local_search::check() {
return check(0, nullptr); return check(0, nullptr);
@ -534,7 +500,7 @@ namespace sat {
#define PROGRESS(tries, flips) \ #define PROGRESS(tries, flips) \
if (tries % 10 == 0 || m_unsat_stack.empty()) { \ if (tries % 10 == 0 || m_unsat_stack.empty()) { \
IF_VERBOSE(1, verbose_stream() << "(sat-local-search" \ IF_VERBOSE(1, verbose_stream() << "(sat.local-search" \
<< " :flips " << flips \ << " :flips " << flips \
<< " :noise " << m_noise \ << " :noise " << m_noise \
<< " :unsat " << /*m_unsat_stack.size()*/ m_best_unsat \ << " :unsat " << /*m_unsat_stack.size()*/ m_best_unsat \
@ -547,10 +513,10 @@ namespace sat {
m_last_best_unsat_rate = 1; m_last_best_unsat_rate = 1;
reinit(); reinit();
DEBUG_CODE(verify_slack(););
timer timer; timer timer;
timer.start(); timer.start();
unsigned step = 0, total_flips = 0, tries = 0; unsigned step = 0, total_flips = 0, tries = 0;
PROGRESS(tries, total_flips);
for (tries = 1; !m_unsat_stack.empty() && m_limit.inc(); ++tries) { for (tries = 1; !m_unsat_stack.empty() && m_limit.inc(); ++tries) {
++m_stats.m_num_restarts; ++m_stats.m_num_restarts;
@ -572,39 +538,7 @@ namespace sat {
reinit(); reinit();
} }
} }
} PROGRESS(0, total_flips);
void local_search::gsat() {
reinit();
bool_var flipvar;
timer timer;
timer.start();
unsigned tries, step = 0, total_flips = 0;
for (tries = 1; m_limit.inc() && !m_unsat_stack.empty(); ++tries) {
reinit();
for (step = 1; step <= m_max_steps; ) {
// feasible
if (m_unsat_stack.empty()) {
calculate_and_update_ob();
if (m_best_objective_value >= m_best_known_value) {
break;
}
}
if (m_unsat_stack.size() < m_best_unsat) {
set_best_unsat();
}
flipvar = pick_var_gsat();
flip_gsat(flipvar);
m_vars[flipvar].m_time_stamp = step++;
}
total_flips += step;
PROGRESS(tries, total_flips);
// tell the SAT solvers about the phase of variables.
if (m_par && tries % 10 == 0) {
m_par->get_phase(*this);
}
}
} }
lbool local_search::check(unsigned sz, literal const* assumptions, parallel* p) { lbool local_search::check(unsigned sz, literal const* assumptions, parallel* p) {
@ -612,28 +546,24 @@ namespace sat {
m_model.reset(); m_model.reset();
m_assumptions.reset(); m_assumptions.reset();
m_assumptions.append(sz, assumptions); m_assumptions.append(sz, assumptions);
unsigned num_units = m_units.size();
init(); init();
walksat();
switch (m_config.mode()) {
case local_search_mode::gsat: // remove unit clauses
gsat(); for (unsigned i = m_units.size(); i-- > num_units; ) {
break; m_vars[m_units[i]].m_unit = false;
case local_search_mode::wsat:
walksat();
break;
} }
m_units.shrink(num_units);
// remove unit clauses from assumptions. m_vars.pop_back(); // remove sentinel variable
m_constraints.shrink(num_constraints() - sz);
TRACE("sat", display(tout);); TRACE("sat", display(tout););
lbool result; lbool result;
if (m_is_unsat) { if (m_is_unsat) {
// result = l_false; result = l_false;
result = l_undef;
} }
else if (m_unsat_stack.empty() && all_objectives_are_met()) { else if (m_unsat_stack.empty()) {
verify_solution(); verify_solution();
extract_model(); extract_model();
result = l_true; result = l_true;
@ -641,7 +571,7 @@ namespace sat {
else { else {
result = l_undef; result = l_undef;
} }
IF_VERBOSE(1, verbose_stream() << "(sat-local-search " << result << ")\n";); IF_VERBOSE(1, verbose_stream() << "(sat.local-search " << result << ")\n";);
IF_VERBOSE(20, display(verbose_stream());); IF_VERBOSE(20, display(verbose_stream()););
return result; return result;
} }
@ -763,7 +693,7 @@ namespace sat {
if (is_true(lit)) { if (is_true(lit)) {
flip_walksat(best_var); flip_walksat(best_var);
} }
add_unit(~lit); add_unit(~lit, null_literal);
if (!propagate(~lit)) { if (!propagate(~lit)) {
IF_VERBOSE(0, verbose_stream() << "unsat\n"); IF_VERBOSE(0, verbose_stream() << "unsat\n");
m_is_unsat = true; m_is_unsat = true;
@ -779,6 +709,7 @@ namespace sat {
} }
void local_search::flip_walksat(bool_var flipvar) { void local_search::flip_walksat(bool_var flipvar) {
++m_stats.m_num_flips; ++m_stats.m_num_flips;
VERIFY(!is_unit(flipvar)); VERIFY(!is_unit(flipvar));
m_vars[flipvar].m_value = !cur_solution(flipvar); m_vars[flipvar].m_value = !cur_solution(flipvar);
@ -794,6 +725,7 @@ namespace sat {
constraint& c = m_constraints[ci]; constraint& c = m_constraints[ci];
int old_slack = c.m_slack; int old_slack = c.m_slack;
c.m_slack -= pbc.m_coeff; c.m_slack -= pbc.m_coeff;
DEBUG_CODE(verify_slack(c););
if (c.m_slack < 0 && old_slack >= 0) { // from non-negative to negative: sat -> unsat if (c.m_slack < 0 && old_slack >= 0) { // from non-negative to negative: sat -> unsat
unsat(ci); unsat(ci);
} }
@ -803,220 +735,21 @@ namespace sat {
constraint& c = m_constraints[ci]; constraint& c = m_constraints[ci];
int old_slack = c.m_slack; int old_slack = c.m_slack;
c.m_slack += pbc.m_coeff; c.m_slack += pbc.m_coeff;
DEBUG_CODE(verify_slack(c););
if (c.m_slack >= 0 && old_slack < 0) { // from negative to non-negative: unsat -> sat if (c.m_slack >= 0 && old_slack < 0) { // from negative to non-negative: unsat -> sat
sat(ci); sat(ci);
} }
} }
// verify_unsat_stack(); DEBUG_CODE(verify_unsat_stack(););
}
void local_search::flip_gsat(bool_var flipvar) {
// already changed truth value!!!!
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);
coeff_vector& truep = m_vars[flipvar].m_watch[flip_is_true];
coeff_vector& falsep = m_vars[flipvar].m_watch[!flip_is_true];
// update related clauses and neighbor vars
for (unsigned i = 0; i < truep.size(); ++i) {
constraint & c = m_constraints[truep[i].m_constraint_id];
//++true_terms_count[c];
--c.m_slack;
switch (c.m_slack) {
case -2: // from -1 to -2
for (literal l : c) {
v = l.var();
// flipping the slack increasing var will no longer satisfy this constraint
if (is_true(l)) {
//score[v] -= constraint_weight[c];
dec_score(v);
}
}
break;
case -1: // from 0 to -1: sat -> unsat
for (literal l : c) {
v = l.var();
inc_cscc(v);
//score[v] += constraint_weight[c];
inc_score(v);
// slack increasing var
if (is_true(l))
inc_slack_score(v);
}
unsat(truep[i].m_constraint_id);
break;
case 0: // from 1 to 0
for (literal l : c) {
v = l.var();
// flip the slack decreasing var will falsify this constraint
if (is_false(l)) {
// score[v] -= constraint_weight[c];
dec_score(v);
dec_slack_score(v);
}
}
break;
default:
break;
}
}
for (pbcoeff const& f : falsep) {
constraint& c = m_constraints[f.m_constraint_id];
//--true_terms_count[c];
++c.m_slack;
switch (c.m_slack) {
case 1: // from 0 to 1
for (literal l : c) {
v = l.var();
// flip the slack decreasing var will no long falsify this constraint
if (is_false(l)) {
//score[v] += constraint_weight[c];
inc_score(v);
inc_slack_score(v);
}
}
break;
case 0: // from -1 to 0: unsat -> sat
for (literal l : c) {
v = l.var();
inc_cscc(v);
//score[v] -= constraint_weight[c];
dec_score(v);
// slack increasing var no longer sat this var
if (is_true(l))
dec_slack_score(v);
}
sat(f.m_constraint_id);
break;
case -1: // from -2 to -1
for (literal l : c) {
v = l.var();
// flip the slack increasing var will satisfy this constraint
if (is_true(l)) {
//score[v] += constraint_weight[c];
inc_score(v);
}
}
break;
default:
break;
}
}
m_vars[flipvar].m_score = -org_flipvar_score;
m_vars[flipvar].m_slack_score = -org_flipvar_slack_score;
m_vars[flipvar].m_conf_change = false;
m_vars[flipvar].m_cscc = 0;
/* update CCD */
// remove the vars no longer goodvar in goodvar stack
for (unsigned i = m_goodvar_stack.size(); i > 0;) {
--i;
v = m_goodvar_stack[i];
if (score(v) <= 0) {
m_goodvar_stack[i] = m_goodvar_stack.back();
m_goodvar_stack.pop_back();
m_vars[v].m_in_goodvar_stack = false;
}
}
// update all flipvar's neighbor's conf_change to true, add goodvar/okvar
var_info& vi = m_vars[flipvar];
for (auto v : vi.m_neighbors) {
m_vars[v].m_conf_change = true;
if (score(v) > 0 && !already_in_goodvar_stack(v)) {
m_goodvar_stack.push_back(v);
m_vars[v].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";
// break tie 1: max imp
// break tie 2: conf_change
// break tie 3: time_stamp
return
(v_imp > b_imp) ||
((v_imp == b_imp) &&
((conf_change(v) && !conf_change(best_var)) ||
((conf_change(v) == conf_change(best_var)) &&
(time_stamp(v) < time_stamp(best_var)))));
}
bool local_search::tie_breaker_ccd(bool_var v, bool_var best_var) {
// break tie 1: max score
// break tie 2: max slack_score
// break tie 3: cscc
// break tie 4: oldest one
return
((score(v) > score(best_var)) ||
((score(v) == score(best_var)) &&
((slack_score(v) > slack_score(best_var)) ||
((slack_score(v) == slack_score(best_var)) &&
((cscc(v) > cscc(best_var)) ||
((cscc(v) == cscc(best_var)) &&
(time_stamp(v) < time_stamp(best_var))))))));
}
bool_var local_search::pick_var_gsat() {
bool_var best_var = m_vars.size()-1; // sentinel variable
// SAT Mode
if (m_unsat_stack.empty()) {
//std::cout << "as\t";
for (auto const& c : ob_constraint) {
bool_var v = c.var_id;
if (tie_breaker_sat(v, best_var))
best_var = v;
}
return best_var;
}
// Unsat Mode: CCD > RD
// CCD mode
if (!m_goodvar_stack.empty()) {
//++ccd;
best_var = m_goodvar_stack[0];
for (bool_var v : m_goodvar_stack) {
if (tie_breaker_ccd(v, best_var))
best_var = v;
}
return best_var;
}
// Diversification Mode
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
for (literal l : c) {
bool_var v = l.var();
if (is_true(l) && time_stamp(v) < time_stamp(best_var))
best_var = v;
}
return best_var;
} }
void local_search::set_parameters() { void local_search::set_parameters() {
m_rand.set_seed(m_config.random_seed()); m_rand.set_seed(m_config.random_seed());
m_best_known_value = m_config.best_known_value(); m_best_known_value = m_config.best_known_value();
switch (m_config.mode()) { m_max_steps = std::min(static_cast<unsigned>(20 * num_vars()), static_cast<unsigned>(1 << 17)); // cut steps off at 100K
case local_search_mode::gsat:
m_max_steps = 2 * num_vars();
break;
case local_search_mode::wsat:
m_max_steps = std::min(static_cast<unsigned>(20 * num_vars()), static_cast<unsigned>(1 << 17)); // cut steps off at 100K
break;
}
TRACE("sat", TRACE("sat",
tout << "seed:\t" << m_config.random_seed() << '\n'; tout << "seed:\t" << m_config.random_seed() << '\n';
tout << "best_known_value:\t" << m_config.best_known_value() << '\n'; tout << "best_known_value:\t" << m_config.best_known_value() << '\n';
@ -1062,7 +795,9 @@ namespace sat {
} }
std::ostream& local_search::display(std::ostream& out, unsigned v, var_info const& vi) const { std::ostream& local_search::display(std::ostream& out, unsigned v, var_info const& vi) const {
return out << "v" << v << " := " << (vi.m_value?"true":"false") << " bias: " << vi.m_bias << "\n"; out << "v" << v << " := " << (vi.m_value?"true":"false") << " bias: " << vi.m_bias;
if (vi.m_unit) out << " u " << vi.m_explain;
return out << "\n";
} }
void local_search::collect_statistics(statistics& st) const { void local_search::collect_statistics(statistics& st) const {
@ -1078,26 +813,6 @@ namespace sat {
} }
bool local_search::check_goodvar() {
unsigned g = 0;
for (unsigned v = 0; v < num_vars(); ++v) {
if (conf_change(v) && score(v) > 0) {
++g;
if (!already_in_goodvar_stack(v))
std::cout << "3\n";
}
}
if (g == m_goodvar_stack.size())
return true;
else {
if (g < m_goodvar_stack.size())
std::cout << "1\n";
else
std::cout << "2\n"; // delete too many
return false;
}
}
void local_search::set_phase(bool_var v, lbool f) { void local_search::set_phase(bool_var v, lbool f) {
unsigned& bias = m_vars[v].m_bias; unsigned& bias = m_vars[v].m_bias;
if (f == l_true && bias < 100) bias++; if (f == l_true && bias < 100) bias++;
@ -1105,4 +820,13 @@ namespace sat {
// f == l_undef ? // f == l_undef ?
} }
void local_search::set_bias(bool_var v, lbool f) {
switch (f) {
case l_true: m_vars[v].m_bias = 99; break;
case l_false: m_vars[v].m_bias = 1; break;
default: break;
}
}
} }

163
src/sat/sat_local_search.h
View file

@ -36,6 +36,16 @@ namespace sat {
local_search_mode m_mode; local_search_mode m_mode;
bool m_phase_sticky; bool m_phase_sticky;
bool m_dbg_flips; bool m_dbg_flips;
friend class local_search;
void set_config(config const& cfg) {
m_mode = cfg.m_local_search_mode;
m_random_seed = cfg.m_random_seed;
m_phase_sticky = cfg.m_phase_sticky;
m_dbg_flips = cfg.m_local_search_dbg_flips;
}
public: public:
local_search_config() { local_search_config() {
m_random_seed = 0; m_random_seed = 0;
@ -54,12 +64,6 @@ namespace sat {
void set_random_seed(unsigned s) { m_random_seed = s; } void set_random_seed(unsigned s) { m_random_seed = s; }
void set_best_known_value(unsigned v) { m_best_known_value = v; } void set_best_known_value(unsigned v) { m_best_known_value = v; }
void set_config(config const& cfg) {
m_mode = cfg.m_local_search_mode;
m_random_seed = cfg.m_random_seed;
m_phase_sticky = cfg.m_phase_sticky;
m_dbg_flips = cfg.m_local_search_dbg_flips;
}
}; };
@ -74,12 +78,6 @@ namespace sat {
typedef svector<bool> bool_vector; typedef svector<bool> bool_vector;
typedef svector<pbcoeff> coeff_vector; typedef svector<pbcoeff> coeff_vector;
// data structure for a term in objective function
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) {}
};
struct stats { struct stats {
unsigned m_num_flips; unsigned m_num_flips;
@ -93,12 +91,12 @@ namespace sat {
unsigned m_bias; // bias for current solution in percentage. unsigned m_bias; // bias for current solution in percentage.
// if bias is 0, then value is always false, if 100, then always true // if bias is 0, then value is always false, if 100, then always true
bool m_unit; // is this a unit literal bool m_unit; // is this a unit literal
literal m_explain; // explanation for unit assignment
bool m_conf_change; // whether its configure changes since its last flip bool m_conf_change; // whether its configure changes since its last flip
bool m_in_goodvar_stack; bool m_in_goodvar_stack;
int m_score; int m_score;
int m_slack_score; int m_slack_score;
int m_time_stamp; // the flip time stamp int m_time_stamp; // the flip time stamp
int m_cscc; // how many times its constraint state configure changes since its last flip
bool_var_vector m_neighbors; // neighborhood variables bool_var_vector m_neighbors; // neighborhood variables
coeff_vector m_watch[2]; coeff_vector m_watch[2];
literal_vector m_bin[2]; literal_vector m_bin[2];
@ -112,7 +110,6 @@ namespace sat {
m_in_goodvar_stack(false), m_in_goodvar_stack(false),
m_score(0), m_score(0),
m_slack_score(0), m_slack_score(0),
m_cscc(0),
m_flips(0), m_flips(0),
m_slow_break(1e-5) m_slow_break(1e-5)
{} {}
@ -132,19 +129,44 @@ namespace sat {
literal const* end() const { return m_literals.end(); } literal const* end() const { return m_literals.end(); }
}; };
stats m_stats;
local_search_config m_config; stats m_stats;
local_search_config m_config;
// objective function: maximize
svector<ob_term> ob_constraint; // the objective function *constraint*, sorted in descending order
// information about the variable
int_vector coefficient_in_ob_constraint; // var! initialized to be 0
vector<var_info> m_vars; // variables
svector<bool_var> m_units; // unit clauses
vector<constraint> m_constraints; // all constraints
literal_vector m_assumptions; // temporary assumptions
literal_vector m_prop_queue; // propagation queue
unsigned m_num_non_binary_clauses;
bool m_is_pb;
bool m_is_unsat;
unsigned_vector m_unsat_stack; // store all the unsat constraints
unsigned_vector m_index_in_unsat_stack; // which position is a constraint in the unsat_stack
// configuration changed decreasing variables (score>0 and conf_change==true)
bool_var_vector m_goodvar_stack;
bool m_initializing;
// information about solution
unsigned m_best_unsat;
double m_best_unsat_rate;
double m_last_best_unsat_rate;
// for non-known instance, set as maximal
int m_best_known_value = INT_MAX; // best known value for this instance
unsigned m_max_steps = (1 << 30);
// dynamic noise
double m_noise = 9800; // normalized by 10000
double m_noise_delta = 0.05;
reslimit m_limit;
random_gen m_rand;
parallel* m_par;
model m_model;
vector<var_info> m_vars;
svector<bool_var> m_units;
inline int score(bool_var v) const { return m_vars[v].m_score; } inline int score(bool_var v) const { return m_vars[v].m_score; }
inline void inc_score(bool_var v) { m_vars[v].m_score++; } inline void inc_score(bool_var v) { m_vars[v].m_score++; }
@ -157,21 +179,10 @@ namespace sat {
inline bool already_in_goodvar_stack(bool_var v) const { return m_vars[v].m_in_goodvar_stack; } inline bool already_in_goodvar_stack(bool_var v) const { return m_vars[v].m_in_goodvar_stack; }
inline bool conf_change(bool_var v) const { return m_vars[v].m_conf_change; } inline bool conf_change(bool_var v) const { return m_vars[v].m_conf_change; }
inline int time_stamp(bool_var v) const { return m_vars[v].m_time_stamp; } 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; }
inline void set_best_unsat(); inline void set_best_unsat();
/* TBD: other scores */ /* TBD: other scores */
vector<constraint> m_constraints;
literal_vector m_assumptions;
literal_vector m_prop_queue;
unsigned m_num_non_binary_clauses;
bool m_is_pb;
inline bool is_pos(literal t) const { return !t.sign(); } 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(bool_var v) const { return cur_solution(v); }
@ -182,101 +193,37 @@ namespace sat {
unsigned num_constraints() const { return m_constraints.size(); } // constraint index from 1 to num_constraint unsigned num_constraints() const { return m_constraints.size(); } // constraint index from 1 to num_constraint
unsigned constraint_slack(unsigned ci) const { return m_constraints[ci].m_slack; } unsigned constraint_slack(unsigned ci) const { return m_constraints[ci].m_slack; }
// unsat constraint stack
bool m_is_unsat;
unsigned_vector m_unsat_stack; // store all the unsat constraints
unsigned_vector m_index_in_unsat_stack; // which position is a constraint in the unsat_stack
// configuration changed decreasing variables (score>0 and conf_change==true)
bool_var_vector m_goodvar_stack;
// information about solution
unsigned m_best_unsat;
double m_best_unsat_rate;
double m_last_best_unsat_rate;
int m_objective_value; // the objective function value corresponds to the current solution
bool_vector m_best_solution; // !var: the best solution so far
int m_best_objective_value = -1; // the objective value corresponds to the best solution so far
// for non-known instance, set as maximal
int m_best_known_value = INT_MAX; // best known value for this instance
unsigned m_max_steps = (1 << 30);
// dynamic noise
double m_noise = 9800; // normalized by 10000
double m_noise_delta = 0.05;
reslimit m_limit;
random_gen m_rand;
parallel* m_par;
model m_model;
void init(); void init();
void reinit(); void reinit();
void reinit_orig(); void reinit_orig();
void init_cur_solution(); void init_cur_solution();
void init_slack(); void init_slack();
void init_scores(); void init_scores();
void init_goodvars(); void init_goodvars();
bool_var pick_var_gsat();
void flip_gsat(bool_var v);
void pick_flip_walksat(); void pick_flip_walksat();
void flip_walksat(bool_var v); void flip_walksat(bool_var v);
bool propagate(literal lit); bool propagate(literal lit);
void add_propagation(literal lit); void add_propagation(literal lit);
void walksat(); void walksat();
void gsat();
void unsat(unsigned c); void unsat(unsigned c);
void sat(unsigned c); void sat(unsigned c);
bool tie_breaker_sat(bool_var v1, bool_var v2);
bool tie_breaker_ccd(bool_var v1, bool_var v2);
void set_parameters(); void set_parameters();
void calculate_and_update_ob();
bool all_objectives_are_met() const;
void verify_solution() const; void verify_solution() const;
void verify_unsat_stack() const; void verify_unsat_stack() const;
void verify_constraint(constraint const& c) const; void verify_constraint(constraint const& c) const;
void verify_slack(constraint const& c) const;
void verify_slack() const;
bool verify_goodvar() const;
unsigned constraint_value(constraint const& c) const; unsigned constraint_value(constraint const& c) const;
unsigned constraint_coeff(constraint const& c, literal l) const; unsigned constraint_coeff(constraint const& c, literal l) const;
void print_info(std::ostream& out); void print_info(std::ostream& out);
void extract_model(); void extract_model();
bool check_goodvar();
void add_clause(unsigned sz, literal const* c); void add_clause(unsigned sz, literal const* c);
void add_unit(literal lit, literal explain);
void add_unit(literal lit);
std::ostream& display(std::ostream& out) const; std::ostream& display(std::ostream& out) const;
std::ostream& display(std::ostream& out, constraint const& c) const; std::ostream& display(std::ostream& out, constraint const& c) const;
std::ostream& display(std::ostream& out, unsigned v, var_info const& vi) const; std::ostream& display(std::ostream& out, unsigned v, var_info const& vi) const;
public: public:
@ -287,8 +234,6 @@ namespace sat {
~local_search(); ~local_search();
void add_soft(bool_var v, int weight);
void add_cardinality(unsigned sz, literal const* c, unsigned k); void add_cardinality(unsigned sz, literal const* c, unsigned k);
void add_pb(unsigned sz, literal const* c, unsigned const* coeffs, unsigned k); void add_pb(unsigned sz, literal const* c, unsigned const* coeffs, unsigned k);
@ -307,8 +252,14 @@ namespace sat {
void set_phase(bool_var v, lbool f); void set_phase(bool_var v, lbool f);
void set_bias(bool_var v, lbool f);
bool get_phase(bool_var v) const { return is_true(v); } bool get_phase(bool_var v) const { return is_true(v); }
inline bool cur_solution(bool_var v) const { return m_vars[v].m_value; }
double break_count(bool_var v) const { return m_vars[v].m_slow_break; }
model& get_model() { return m_model; } model& get_model() { return m_model; }
void collect_statistics(statistics& st) const; void collect_statistics(statistics& st) const;

4
src/sat/sat_solver.cpp
View file

@ -1172,7 +1172,6 @@ namespace sat {
SASSERT(!m_local_search); SASSERT(!m_local_search);
m_local_search = alloc(local_search); m_local_search = alloc(local_search);
local_search& srch = *m_local_search; local_search& srch = *m_local_search;
srch.config().set_config(m_config);
srch.import(*this, false); srch.import(*this, false);
scoped_rl.push_child(&srch.rlimit()); scoped_rl.push_child(&srch.rlimit());
lbool r = srch.check(num_lits, lits, nullptr); lbool r = srch.check(num_lits, lits, nullptr);
@ -1197,9 +1196,8 @@ namespace sat {
int num_threads = num_extra_solvers + 1 + num_local_search + num_unit_walk; int num_threads = num_extra_solvers + 1 + num_local_search + num_unit_walk;
for (int i = 0; i < num_local_search; ++i) { for (int i = 0; i < num_local_search; ++i) {
local_search* l = alloc(local_search); local_search* l = alloc(local_search);
l->config().set_config(m_config);
l->config().set_random_seed(m_config.m_random_seed + i);
l->import(*this, false); l->import(*this, false);
l->config().set_random_seed(m_config.m_random_seed + i);
ls.push_back(l); ls.push_back(l);
} }