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

fix autarky detection

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2017-03-31 13:16:04 -07:00
parent 6571aad440
commit c0188a7ec0
3 changed files with 87 additions and 26 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

31
src/sat/sat_local_search.cpp
View file

@ -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;

7
src/sat/sat_local_search.h
View file

@ -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

75
src/sat/sat_lookahead.h
View file

@ -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 {