mirror of
https://github.com/Z3Prover/z3
synced 2025-04-16 13:58:45 +00:00
9fc4015c46
Removing ternary clause optimization from sat_solver simplifies special case handling of ternary clauses throughout the sat solver and dependent solvers (pb_solver). Benchmarking on QF_BV suggests the ternary clause optimization does not have any effect. While removing ternary clause optimization two bugs in unit propagation were also uncovered: it missed propagations when the only a single undef literal remained in the non-watched literals and it did not update blocked literals in cases where it could in the watch list. These performance bugs were for general clauses, ternary clause propagation did not miss propagations (and don't use blocked literals), but fixing these issues for general clauses appear to have made ternary clause optimization irrelevant based on what was measured.
234 lines
8.1 KiB
C++
234 lines
8.1 KiB
C++
/*++
|
|
Copyright (c) 2011 Microsoft Corporation
|
|
|
|
Module Name:
|
|
|
|
sat_cleaner.h
|
|
|
|
Abstract:
|
|
|
|
Eliminate satisfied clauses, and literals assigned to false.
|
|
|
|
Author:
|
|
|
|
Leonardo de Moura (leonardo) 2011-05-24.
|
|
|
|
Revision History:
|
|
|
|
--*/
|
|
#include "sat/sat_cleaner.h"
|
|
#include "sat/sat_solver.h"
|
|
#include "util/trace.h"
|
|
#include "util/stopwatch.h"
|
|
|
|
namespace sat {
|
|
|
|
cleaner::cleaner(solver & _s):
|
|
s(_s),
|
|
m_last_num_units(0),
|
|
m_cleanup_counter(0) {
|
|
reset_statistics();
|
|
}
|
|
|
|
/**
|
|
- Delete watch lists of assigned literals.
|
|
- Delete satisfied binary watched binary clauses
|
|
- Delete watched clauses (they will be reinserted after they are cleaned).
|
|
*/
|
|
void cleaner::cleanup_watches() {
|
|
vector<watch_list>::iterator it = s.m_watches.begin();
|
|
vector<watch_list>::iterator end = s.m_watches.end();
|
|
unsigned l_idx = 0;
|
|
for (; it != end; ++it, ++l_idx) {
|
|
if (s.value(to_literal(l_idx)) != l_undef) {
|
|
it->finalize();
|
|
SASSERT(it->empty());
|
|
continue;
|
|
}
|
|
TRACE("cleanup_bug", tout << "processing wlist of " << to_literal(l_idx) << "\n";);
|
|
watch_list & wlist = *it;
|
|
watch_list::iterator it2 = wlist.begin();
|
|
watch_list::iterator it_prev = it2;
|
|
watch_list::iterator end2 = wlist.end();
|
|
for (; it2 != end2; ++it2) {
|
|
switch (it2->get_kind()) {
|
|
case watched::BINARY:
|
|
TRACE("cleanup_bug",
|
|
tout << ~to_literal(l_idx) << " " << it2->get_literal() << "\n";
|
|
tout << s.value(~to_literal(l_idx)) << " " << s.value(it2->get_literal()) << "\n";
|
|
tout << s.was_eliminated(it2->get_literal()) << " " << s.inconsistent() << "\n";);
|
|
SASSERT(s.value(it2->get_literal()) == l_true || s.value(it2->get_literal()) == l_undef);
|
|
if (s.value(it2->get_literal()) == l_undef) {
|
|
*it_prev = *it2;
|
|
++it_prev;
|
|
}
|
|
TRACE("cleanup_bug", tout << "keeping: " << ~to_literal(l_idx) << " " << it2->get_literal() << "\n";);
|
|
break;
|
|
case watched::CLAUSE:
|
|
// skip
|
|
break;
|
|
case watched::EXT_CONSTRAINT:
|
|
*it_prev = *it2;
|
|
++it_prev;
|
|
break;
|
|
default:
|
|
UNREACHABLE();
|
|
break;
|
|
}
|
|
}
|
|
wlist.set_end(it_prev);
|
|
}
|
|
}
|
|
|
|
void cleaner::cleanup_clauses(clause_vector & cs) {
|
|
clause_vector::iterator it = cs.begin();
|
|
clause_vector::iterator it2 = it;
|
|
clause_vector::iterator end = cs.end();
|
|
for (; it != end; ++it) {
|
|
clause & c = *(*it);
|
|
TRACE("sat_cleaner_bug", tout << "cleaning: " << c << "\n";
|
|
for (unsigned i = 0; i < c.size(); i++) tout << c[i] << ": " << s.value(c[i]) << "\n";);
|
|
CTRACE("sat_cleaner_frozen", c.frozen(), tout << c << "\n";);
|
|
unsigned sz = c.size();
|
|
unsigned i = 0, j = 0;
|
|
m_cleanup_counter += sz;
|
|
for (; i < sz; i++) {
|
|
switch (s.value(c[i])) {
|
|
case l_true:
|
|
goto end_loop;
|
|
case l_false:
|
|
m_elim_literals++;
|
|
break;
|
|
case l_undef:
|
|
if (i != j) {
|
|
std::swap(c[j], c[i]);
|
|
}
|
|
j++;
|
|
break;
|
|
}
|
|
}
|
|
end_loop:
|
|
CTRACE("sat_cleaner_frozen", c.frozen(),
|
|
tout << "sat: " << (i < sz) << ", new_size: " << j << "\n";
|
|
tout << mk_lits_pp(j, c.begin()) << "\n";);
|
|
if (i < sz) {
|
|
m_elim_clauses++;
|
|
s.del_clause(c);
|
|
}
|
|
else {
|
|
unsigned new_sz = j;
|
|
CTRACE("sat_cleaner_bug", new_sz < 2, tout << "new_sz: " << new_sz << "\n";
|
|
if (c.size() > 0) tout << "unit: " << c[0] << "\n";
|
|
s.display_watches(tout););
|
|
switch (new_sz) {
|
|
case 0:
|
|
s.set_conflict();
|
|
s.del_clause(c);
|
|
break;
|
|
case 1:
|
|
s.assign_unit(c[0]);
|
|
s.del_clause(c);
|
|
break;
|
|
case 2:
|
|
SASSERT(s.value(c[0]) == l_undef && s.value(c[1]) == l_undef);
|
|
TRACE("cleanup_bug", tout << "clause became binary: " << c[0] << " " << c[1] << "\n";);
|
|
s.mk_bin_clause(c[0], c[1], c.is_learned());
|
|
s.del_clause(c);
|
|
break;
|
|
default:
|
|
s.shrink(c, sz, new_sz);
|
|
*it2 = *it;
|
|
it2++;
|
|
if (!c.frozen()) {
|
|
s.attach_clause(c);
|
|
}
|
|
break;
|
|
}
|
|
}
|
|
}
|
|
cs.set_end(it2);
|
|
}
|
|
|
|
struct cleaner::report {
|
|
cleaner & m_cleaner;
|
|
stopwatch m_watch;
|
|
unsigned m_elim_clauses;
|
|
unsigned m_elim_literals;
|
|
report(cleaner & c):
|
|
m_cleaner(c),
|
|
m_elim_clauses(c.m_elim_clauses),
|
|
m_elim_literals(c.m_elim_literals) {
|
|
m_watch.start();
|
|
}
|
|
~report() {
|
|
m_watch.stop();
|
|
IF_VERBOSE(2,
|
|
verbose_stream() << " (sat-cleaner";
|
|
verbose_stream() << " :elim-literals " << (m_cleaner.m_elim_literals - m_elim_literals);
|
|
verbose_stream() << " :elim-clauses " << (m_cleaner.m_elim_clauses - m_elim_clauses);
|
|
verbose_stream() << " :cost " << m_cleaner.m_cleanup_counter << m_watch << ")\n";);
|
|
}
|
|
};
|
|
|
|
bool cleaner::is_clean() const {
|
|
for (clause* cp : s.m_clauses) {
|
|
for (literal lit : *cp) {
|
|
if (s.value(lit) != l_undef && s.lvl(lit) == 0) return false;
|
|
}
|
|
}
|
|
for (clause* cp : s.m_learned) {
|
|
for (literal lit : *cp) {
|
|
if (s.value(lit) != l_undef && s.lvl(lit) == 0) return false;
|
|
}
|
|
}
|
|
unsigned idx = 0;
|
|
for (auto& wlist : s.m_watches) {
|
|
literal lit = to_literal(idx);
|
|
if (s.value(lit) != l_undef && s.lvl(lit) == 0 && !wlist.empty()) return false;
|
|
++idx;
|
|
}
|
|
return true;
|
|
}
|
|
|
|
/**
|
|
\brief Return true if cleaner executed.
|
|
*/
|
|
bool cleaner::operator()(bool force) {
|
|
CASSERT("cleaner_bug", s.check_invariant());
|
|
unsigned trail_sz = s.m_trail.size();
|
|
|
|
s.propagate(false); // make sure that everything was propagated.
|
|
TRACE("sat_cleaner_bug", s.display(tout); s.display_watches(tout););
|
|
if (s.m_inconsistent)
|
|
return false;
|
|
if (m_last_num_units == trail_sz)
|
|
return false; // there are no new assigned literals since last time... nothing to be done
|
|
if (!force && m_cleanup_counter > 0)
|
|
return false; // prevent simplifier from being executed over and over again.
|
|
report rpt(*this);
|
|
m_last_num_units = trail_sz;
|
|
m_cleanup_counter = 0;
|
|
do {
|
|
trail_sz = s.m_trail.size();
|
|
cleanup_watches();
|
|
cleanup_clauses(s.m_clauses);
|
|
cleanup_clauses(s.m_learned);
|
|
s.propagate(false);
|
|
}
|
|
while (trail_sz < s.m_trail.size() && !s.inconsistent());
|
|
CASSERT("cleaner_bug", s.check_invariant());
|
|
return true;
|
|
}
|
|
|
|
void cleaner::reset_statistics() {
|
|
m_elim_clauses = 0;
|
|
m_elim_literals = 0;
|
|
}
|
|
|
|
void cleaner::collect_statistics(statistics & st) const {
|
|
st.update("sat elim clauses", m_elim_clauses);
|
|
st.update("sat elim literals", m_elim_literals);
|
|
}
|
|
|
|
};
|