diff --git a/src/sat/sat_local_search.cpp b/src/sat/sat_local_search.cpp
index 92173ff4b..c9a947712 100644
--- a/src/sat/sat_local_search.cpp
+++ b/src/sat/sat_local_search.cpp
@@ -137,6 +137,17 @@ namespace sat {
}
void local_search::reinit() {
+ // the following methods does NOT converge for pseudo-boolean
+ // can try other way to define "worse" and "better"
+ // the current best noise is below 1000
+ if (best_unsat_rate >= last_best_unsat_rate) {
+ // worse
+ noise = noise - noise * 2 * noise_delta;
+ }
+ else {
+ // better
+ noise = noise + (10000 - noise) * noise_delta;
+ }
for (unsigned i = 0; i < m_constraints.size(); ++i) {
constraint& c = m_constraints[i];
c.m_slack = c.m_k;
@@ -370,11 +381,16 @@ namespace sat {
if (tries % 10 == 0 || m_unsat_stack.empty()) { \
IF_VERBOSE(1, verbose_stream() << "(sat-local-search" \
<< " :flips " << flips \
- << " :unsat " << m_unsat_stack.size() \
+ << " :noise " << noise \
+ << " :unsat " << /*m_unsat_stack.size()*/ best_unsat \
<< " :time " << (timer.get_seconds() < 0.001 ? 0.0 : timer.get_seconds()) << ")\n";); \
}
void local_search::walksat() {
+ best_unsat_rate = 1;
+ last_best_unsat_rate = 1;
+
+
reinit();
timer timer;
timer.start();
@@ -382,12 +398,17 @@ namespace sat {
PROGRESS(tries, total_flips);
for (tries = 1; !m_unsat_stack.empty() && m_limit.inc(); ++tries) {
+ if (m_unsat_stack.size() < best_unsat) {
+ best_unsat = m_unsat_stack.size();
+ last_best_unsat_rate = best_unsat_rate;
+ best_unsat_rate = (double)m_unsat_stack.size() / num_constraints();
+ }
for (step = 0; step < m_max_steps && !m_unsat_stack.empty(); ++step) {
pick_flip_walksat();
}
total_flips += step;
PROGRESS(tries, total_flips);
- if (m_par && tries % 30 == 0) {
+ if (m_par && tries % 20 == 0) {
m_par->get_phase(*this);
reinit();
}
@@ -483,7 +504,9 @@ namespace sat {
unsigned num_unsat = m_unsat_stack.size();
constraint const& c = m_constraints[m_unsat_stack[m_rand() % m_unsat_stack.size()]];
SASSERT(c.m_k < constraint_value(c));
- if (m_rand() % 100 < 98) {
+ // TBD: dynamic noise strategy
+ //if (m_rand() % 100 < 98) {
+ if (m_rand() % 10000 >= noise) {
// take this branch with 98% probability.
// find the first one, to fast break the rest
unsigned best_bsb = 0;
@@ -533,7 +556,7 @@ namespace sat {
best_var = v;
n = 1;
}
- else {// if (bb == best_bb)
+ else {// if (bsb == best_bb)
++n;
if (m_rand() % n == 0) {
best_var = v;
diff --git a/src/sat/sat_local_search.h b/src/sat/sat_local_search.h
index 108df4e6d..7fb5396fe 100644
--- a/src/sat/sat_local_search.h
+++ b/src/sat/sat_local_search.h
@@ -164,6 +164,9 @@ namespace sat {
// information about solution
+ unsigned best_unsat;
+ double best_unsat_rate;
+ double 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
@@ -172,6 +175,10 @@ namespace sat {
unsigned m_max_steps = (1 << 30);
+ // dynamic noise
+ unsigned noise = 400; // normalized by 10000
+ double noise_delta = 0.05;
+
// for tuning
int s_id = 0; // strategy id
diff --git a/src/sat/sat_lookahead.h b/src/sat/sat_lookahead.h
index ac985c23c..fa9fea724 100644
--- a/src/sat/sat_lookahead.h
+++ b/src/sat/sat_lookahead.h
@@ -220,7 +220,7 @@ namespace sat {
// ----------------------------------------
void add_binary(literal l1, literal l2) {
- TRACE("sat", tout << "binary: " << l1 << " " << l2 << "\n";);
+ TRACE("sat", tout << "binary: " << l1 << " " << l2 << "\n";);
SASSERT(l1 != l2);
// don't add tautologies and don't add already added binaries
if (~l1 == l2) return;
@@ -375,7 +375,7 @@ namespace sat {
progress = false;
float mean = sum / (float)(m_candidates.size() + 0.0001);
sum = 0;
- for (unsigned i = 0; i < m_candidates.size(); ++i) {
+ for (unsigned i = 0; i < m_candidates.size() && m_candidates.size() >= max_num_cand * 2; ++i) {
if (m_candidates[i].m_rating >= mean) {
sum += m_candidates[i].m_rating;
}
@@ -1133,11 +1133,14 @@ namespace sat {
m_search_mode = lookahead_mode::searching;
// convert windfalls to binary clauses.
if (!unsat) {
+ literal nlit = ~lit;
for (unsigned i = 0; i < m_wstack.size(); ++i) {
++m_stats.m_windfall_binaries;
+ literal l2 = m_wstack[i];
//update_prefix(~lit);
//update_prefix(m_wstack[i]);
- add_binary(~lit, m_wstack[i]);
+ TRACE("sat", tout << "windfall: " << nlit << " " << l2 << "\n";);
+ add_binary(nlit, l2);
}
}
m_wstack.reset();
@@ -1280,6 +1283,9 @@ namespace sat {
else {
TRACE("sat", tout << "propagating " << l << ": " << c << "\n";);
SASSERT(is_undef(c[0]));
+ DEBUG_CODE(for (unsigned i = 2; i < c.size(); ++i) {
+ SASSERT(is_false(c[i]));
+ });
*it2 = *it;
it2++;
propagated(c[0]);
@@ -1354,7 +1360,7 @@ namespace sat {
TRACE("sat", tout << "lookahead: " << lit << " @ " << m_lookahead[i].m_offset << "\n";);
reset_wnb(lit);
push_lookahead1(lit, level);
- do_double(lit, base);
+ //do_double(lit, base);
bool unsat = inconsistent();
pop_lookahead1(lit);
if (unsat) {
@@ -1433,30 +1439,55 @@ namespace sat {
set_wnb(l, p == null_literal ? 0 : get_wnb(p));
}
- void update_wnb(literal l, unsigned level) {
- if (m_weighted_new_binaries == 0) {
- {
- scoped_level _sl(*this, level);
- clause_vector::const_iterator it = m_full_watches[l.index()].begin(), end = m_full_watches[l.index()].end();
- for (; it != end; ++it) {
- clause& c = *(*it);
- unsigned sz = c.size();
- bool found = false;
-
- for (unsigned i = 0; !found && i < sz; ++i) {
- found = is_true(c[i]);
- }
- IF_VERBOSE(2, verbose_stream() << "skip autarky\n";);
- if (!found) return;
+ bool check_autarky(literal l, unsigned level) {
+ // no propagations are allowed to reduce clauses.
+ clause_vector::const_iterator it = m_full_watches[l.index()].begin();
+ clause_vector::const_iterator end = m_full_watches[l.index()].end();
+ for (; it != end; ++it) {
+ clause& c = *(*it);
+ unsigned sz = c.size();
+ bool found = false;
+ for (unsigned i = 0; !found && i < sz; ++i) {
+ found = is_true(c[i]);
+ if (found) {
+ TRACE("sat", tout << c[i] << " is true in " << c << "\n";);
}
}
- if (get_wnb(l) == 0) {
+ IF_VERBOSE(2, verbose_stream() << "skip autarky " << l << "\n";);
+ if (!found) return false;
+ }
+ //
+ // bail out if there is a pending binary propagation.
+ // In general, we would have to check, recursively that
+ // a binary propagation does not create reduced clauses.
+ //
+ literal_vector const& lits = m_binary[l.index()];
+ TRACE("sat", tout << l << ": " << lits << "\n";);
+ for (unsigned i = 0; i < lits.size(); ++i) {
+ literal l2 = lits[i];
+ if (is_true(l2)) continue;
+ SASSERT(!is_false(l2));
+ return false;
+ }
+
+ return true;
+ }
+
+ void update_wnb(literal l, unsigned level) {
+ if (m_weighted_new_binaries == 0) {
+ if (!check_autarky(l, level)) {
+ // skip
+ }
+ else if (get_wnb(l) == 0) {
++m_stats.m_autarky_propagations;
IF_VERBOSE(1, verbose_stream() << "(sat.lookahead autarky " << l << ")\n";);
- TRACE("sat", tout << "autarky: " << l << " @ " << m_stamp[l.var()] << "\n";);
+
+ TRACE("sat", tout << "autarky: " << l << " @ " << m_stamp[l.var()]
+ << " "
+ << (!m_binary[l.index()].empty() || !m_full_watches[l.index()].empty()) << "\n";);
reset_wnb();
assign(l);
- propagate();
+ propagate();
init_wnb();
}
else {