mirror of
https://github.com/Z3Prover/z3
synced 2025-04-10 03:07:07 +00:00
90490cb22f
re-introduce shorthands in sat::solver for visited and have them convert literals to unsigned.
601 lines
19 KiB
C++
601 lines
19 KiB
C++
/*++
|
|
Copyright (c) 2011 Microsoft Corporation
|
|
|
|
Module Name:
|
|
|
|
sat_solver.cpp
|
|
|
|
Abstract:
|
|
|
|
SAT solver main class.
|
|
|
|
Author:
|
|
|
|
Leonardo de Moura (leonardo) 2011-05-21.
|
|
|
|
Revision History:
|
|
|
|
--*/
|
|
|
|
|
|
#include "sat/sat_solver.h"
|
|
|
|
namespace sat {
|
|
|
|
// -----------------------
|
|
//
|
|
// GC
|
|
//
|
|
// -----------------------
|
|
|
|
bool solver::should_gc() const {
|
|
return
|
|
m_conflicts_since_gc > m_gc_threshold &&
|
|
(m_config.m_gc_strategy != GC_DYN_PSM || at_base_lvl());
|
|
}
|
|
|
|
void solver::do_gc() {
|
|
if (!should_gc()) return;
|
|
TRACE("sat", tout << m_conflicts_since_gc << " " << m_gc_threshold << "\n";);
|
|
unsigned gc = m_stats.m_gc_clause;
|
|
m_conflicts_since_gc = 0;
|
|
m_gc_threshold += m_config.m_gc_increment;
|
|
IF_VERBOSE(10, verbose_stream() << "(sat.gc)\n";);
|
|
CASSERT("sat_gc_bug", check_invariant());
|
|
switch (m_config.m_gc_strategy) {
|
|
case GC_GLUE:
|
|
gc_glue();
|
|
break;
|
|
case GC_PSM:
|
|
gc_psm();
|
|
break;
|
|
case GC_GLUE_PSM:
|
|
gc_glue_psm();
|
|
break;
|
|
case GC_PSM_GLUE:
|
|
gc_psm_glue();
|
|
break;
|
|
case GC_DYN_PSM:
|
|
if (!m_assumptions.empty()) {
|
|
gc_glue_psm();
|
|
break;
|
|
}
|
|
if (!at_base_lvl())
|
|
return;
|
|
gc_dyn_psm();
|
|
break;
|
|
default:
|
|
UNREACHABLE();
|
|
break;
|
|
}
|
|
if (m_ext) m_ext->gc();
|
|
if (gc > 0 && should_defrag()) {
|
|
defrag_clauses();
|
|
}
|
|
CASSERT("sat_gc_bug", check_invariant());
|
|
}
|
|
|
|
/**
|
|
\brief Lex on (glue, size)
|
|
*/
|
|
struct glue_lt {
|
|
bool operator()(clause const * c1, clause const * c2) const {
|
|
if (c1->glue() < c2->glue()) return true;
|
|
return c1->glue() == c2->glue() && c1->size() < c2->size();
|
|
}
|
|
};
|
|
|
|
/**
|
|
\brief Lex on (psm, size)
|
|
*/
|
|
struct psm_lt {
|
|
bool operator()(clause const * c1, clause const * c2) const {
|
|
if (c1->psm() < c2->psm()) return true;
|
|
return c1->psm() == c2->psm() && c1->size() < c2->size();
|
|
}
|
|
};
|
|
|
|
/**
|
|
\brief Lex on (glue, psm, size)
|
|
*/
|
|
struct glue_psm_lt {
|
|
bool operator()(clause const * c1, clause const * c2) const {
|
|
if (c1->glue() < c2->glue()) return true;
|
|
if (c1->glue() > c2->glue()) return false;
|
|
if (c1->psm() < c2->psm()) return true;
|
|
if (c1->psm() > c2->psm()) return false;
|
|
return c1->size() < c2->size();
|
|
}
|
|
};
|
|
|
|
/**
|
|
\brief Lex on (psm, glue, size)
|
|
*/
|
|
struct psm_glue_lt {
|
|
bool operator()(clause const * c1, clause const * c2) const {
|
|
if (c1->psm() < c2->psm()) return true;
|
|
if (c1->psm() > c2->psm()) return false;
|
|
if (c1->glue() < c2->glue()) return true;
|
|
if (c1->glue() > c2->glue()) return false;
|
|
return c1->size() < c2->size();
|
|
}
|
|
};
|
|
|
|
void solver::gc_glue() {
|
|
std::stable_sort(m_learned.begin(), m_learned.end(), glue_lt());
|
|
gc_half("glue");
|
|
}
|
|
|
|
void solver::gc_psm() {
|
|
save_psm();
|
|
std::stable_sort(m_learned.begin(), m_learned.end(), psm_lt());
|
|
gc_half("psm");
|
|
}
|
|
|
|
void solver::gc_glue_psm() {
|
|
save_psm();
|
|
std::stable_sort(m_learned.begin(), m_learned.end(), glue_psm_lt());
|
|
gc_half("glue-psm");
|
|
}
|
|
|
|
void solver::gc_psm_glue() {
|
|
save_psm();
|
|
std::stable_sort(m_learned.begin(), m_learned.end(), psm_glue_lt());
|
|
gc_half("psm-glue");
|
|
}
|
|
|
|
/**
|
|
\brief Compute the psm of all learned clauses.
|
|
*/
|
|
void solver::save_psm() {
|
|
for (clause* cp : m_learned) {
|
|
cp->set_psm(psm(*cp));
|
|
}
|
|
}
|
|
|
|
/**
|
|
\brief GC (the second) half of the clauses in the database.
|
|
*/
|
|
void solver::gc_half(char const * st_name) {
|
|
TRACE("sat", tout << "gc\n";);
|
|
unsigned sz = m_learned.size();
|
|
unsigned new_sz = sz/2; // std::min(sz/2, m_clauses.size()*2);
|
|
unsigned j = new_sz;
|
|
for (unsigned i = new_sz; i < sz; i++) {
|
|
clause & c = *(m_learned[i]);
|
|
if (can_delete(c)) {
|
|
detach_clause(c);
|
|
del_clause(c);
|
|
}
|
|
else {
|
|
m_learned[j] = &c;
|
|
j++;
|
|
}
|
|
}
|
|
new_sz = j;
|
|
m_stats.m_gc_clause += sz - new_sz;
|
|
m_learned.shrink(new_sz);
|
|
IF_VERBOSE(SAT_VB_LVL, verbose_stream() << "(sat-gc :strategy " << st_name << " :deleted " << (sz - new_sz) << ")\n";);
|
|
}
|
|
|
|
bool solver::can_delete(clause const & c) const {
|
|
if (c.on_reinit_stack())
|
|
return false;
|
|
literal l0 = c[0];
|
|
if (value(l0) != l_true)
|
|
return true;
|
|
justification const & jst = m_justification[l0.var()];
|
|
return !jst.is_clause() || cls_allocator().get_clause(jst.get_clause_offset()) != &c;
|
|
}
|
|
|
|
/**
|
|
\brief Use gc based on dynamic psm. Clauses are initially frozen.
|
|
*/
|
|
void solver::gc_dyn_psm() {
|
|
TRACE("sat", tout << "gc\n";);
|
|
// To do gc at scope_lvl() > 0, I will need to use the reinitialization stack, or live with the fact
|
|
// that I may miss some propagations for reactivated clauses.
|
|
SASSERT(at_base_lvl());
|
|
// compute
|
|
// d_tk
|
|
unsigned h = 0;
|
|
unsigned V_tk = 0;
|
|
for (bool_var v = 0; v < num_vars(); v++) {
|
|
if (m_assigned_since_gc[v]) {
|
|
V_tk++;
|
|
m_assigned_since_gc[v] = false;
|
|
}
|
|
if (m_phase[v] != m_prev_phase[v]) {
|
|
h++;
|
|
m_prev_phase[v] = m_phase[v];
|
|
}
|
|
}
|
|
double d_tk = V_tk == 0 ? static_cast<double>(num_vars() + 1) : static_cast<double>(h)/static_cast<double>(V_tk);
|
|
if (d_tk < m_min_d_tk)
|
|
m_min_d_tk = d_tk;
|
|
TRACE("sat_frozen", tout << "m_min_d_tk: " << m_min_d_tk << "\n";);
|
|
unsigned frozen = 0;
|
|
unsigned deleted = 0;
|
|
unsigned activated = 0;
|
|
clause_vector::iterator it = m_learned.begin();
|
|
clause_vector::iterator it2 = it;
|
|
clause_vector::iterator end = m_learned.end();
|
|
for (; it != end; ++it) {
|
|
clause & c = *(*it);
|
|
if (!c.frozen()) {
|
|
// Active clause
|
|
if (c.glue() > m_config.m_gc_small_lbd) {
|
|
// I never delete clauses with small lbd
|
|
if (c.was_used()) {
|
|
c.reset_inact_rounds();
|
|
}
|
|
else {
|
|
c.inc_inact_rounds();
|
|
if (c.inact_rounds() > m_config.m_gc_k) {
|
|
detach_clause(c);
|
|
del_clause(c);
|
|
m_stats.m_gc_clause++;
|
|
deleted++;
|
|
continue;
|
|
}
|
|
}
|
|
c.unmark_used();
|
|
if (psm(c) > static_cast<unsigned>(c.size() * m_min_d_tk)) {
|
|
// move to frozen;
|
|
TRACE("sat_frozen", tout << "freezing size: " << c.size() << " psm: " << psm(c) << " " << c << "\n";);
|
|
detach_clause(c);
|
|
c.reset_inact_rounds();
|
|
c.freeze();
|
|
m_num_frozen++;
|
|
frozen++;
|
|
}
|
|
}
|
|
}
|
|
else {
|
|
// frozen clause
|
|
clause & c = *(*it);
|
|
if (psm(c) <= static_cast<unsigned>(c.size() * m_min_d_tk)) {
|
|
c.unfreeze();
|
|
m_num_frozen--;
|
|
activated++;
|
|
if (!activate_frozen_clause(c)) {
|
|
// clause was satisfied, reduced to a conflict, unit or binary clause.
|
|
del_clause(c);
|
|
continue;
|
|
}
|
|
}
|
|
else {
|
|
c.inc_inact_rounds();
|
|
if (c.inact_rounds() > m_config.m_gc_k) {
|
|
del_clause(c);
|
|
m_stats.m_gc_clause++;
|
|
deleted++;
|
|
continue;
|
|
}
|
|
}
|
|
}
|
|
*it2 = *it;
|
|
++it2;
|
|
}
|
|
m_learned.set_end(it2);
|
|
IF_VERBOSE(SAT_VB_LVL, verbose_stream() << "(sat-gc :d_tk " << d_tk << " :min-d_tk " << m_min_d_tk <<
|
|
" :frozen " << frozen << " :activated " << activated << " :deleted " << deleted << ")\n";);
|
|
}
|
|
|
|
// return true if should keep the clause, and false if we should delete it.
|
|
bool solver::activate_frozen_clause(clause & c) {
|
|
TRACE("sat_gc", tout << "reactivating:\n" << c << "\n";);
|
|
SASSERT(at_base_lvl());
|
|
// do some cleanup
|
|
unsigned sz = c.size();
|
|
unsigned j = 0;
|
|
for (unsigned i = 0; i < sz; i++) {
|
|
literal l = c[i];
|
|
switch (value(l)) {
|
|
case l_true:
|
|
return false;
|
|
case l_false:
|
|
break;
|
|
case l_undef:
|
|
if (i != j) {
|
|
std::swap(c[i], c[j]);
|
|
}
|
|
j++;
|
|
break;
|
|
}
|
|
}
|
|
TRACE("sat", tout << "after cleanup:\n" << mk_lits_pp(j, c.begin()) << "\n";);
|
|
unsigned new_sz = j;
|
|
switch (new_sz) {
|
|
case 0:
|
|
if (m_config.m_drat) m_drat.add();
|
|
set_conflict();
|
|
return false;
|
|
case 1:
|
|
assign_unit(c[0]);
|
|
return false;
|
|
case 2:
|
|
mk_bin_clause(c[0], c[1], true);
|
|
return false;
|
|
default:
|
|
shrink(c, sz, new_sz);
|
|
attach_clause(c);
|
|
return true;
|
|
}
|
|
}
|
|
|
|
/**
|
|
\brief Compute phase saving measure for the given clause.
|
|
*/
|
|
unsigned solver::psm(clause const & c) const {
|
|
unsigned r = 0;
|
|
for (literal l : c) {
|
|
if (l.sign() ^ m_phase[l.var()]) {
|
|
r++;
|
|
}
|
|
}
|
|
return r;
|
|
}
|
|
|
|
/**
|
|
* Control the size of the reinit-stack.
|
|
* by agressively garbage collecting lemmas that are not asserting.
|
|
*/
|
|
|
|
void solver::gc_reinit_stack(unsigned num_scopes) {
|
|
return;
|
|
SASSERT (!at_base_lvl());
|
|
unsigned new_lvl = scope_lvl() - num_scopes;
|
|
ptr_vector<clause> to_gc;
|
|
unsigned j = m_scopes[new_lvl].m_clauses_to_reinit_lim;
|
|
unsigned sz = m_clauses_to_reinit.size();
|
|
if (sz - j <= 2000)
|
|
return;
|
|
for (unsigned i = j; i < sz; ++i) {
|
|
auto cw = m_clauses_to_reinit[i];
|
|
if (cw.is_binary() || is_asserting(new_lvl, cw))
|
|
m_clauses_to_reinit[j++] = cw;
|
|
else
|
|
to_gc.push_back(cw.get_clause());
|
|
}
|
|
m_clauses_to_reinit.shrink(j);
|
|
if (to_gc.empty())
|
|
return;
|
|
for (clause* c : to_gc) {
|
|
SASSERT(c->on_reinit_stack());
|
|
c->set_removed(true);
|
|
c->set_reinit_stack(false);
|
|
}
|
|
j = 0;
|
|
for (unsigned i = 0; i < m_learned.size(); ++i) {
|
|
clause & c = *(m_learned[i]);
|
|
if (c.was_removed()) {
|
|
detach_clause(c);
|
|
del_clause(c);
|
|
}
|
|
else
|
|
m_learned[j++] = &c;
|
|
}
|
|
SASSERT(m_learned.size() - j == to_gc.size());
|
|
m_learned.shrink(j);
|
|
}
|
|
|
|
bool solver::is_asserting(unsigned new_lvl, clause_wrapper const& cw) const {
|
|
if (!cw.is_learned())
|
|
return true;
|
|
bool seen_true = false;
|
|
for (literal lit : cw) {
|
|
switch (value(lit)) {
|
|
case l_true:
|
|
if (lvl(lit) > new_lvl || seen_true)
|
|
return false;
|
|
seen_true = true;
|
|
continue;
|
|
case l_false:
|
|
continue;
|
|
case l_undef:
|
|
return false;
|
|
}
|
|
}
|
|
return true;
|
|
}
|
|
|
|
void solver::gc_vars(bool_var max_var) {
|
|
init_visited();
|
|
m_aux_literals.reset();
|
|
auto gc_watch = [&](literal lit) {
|
|
auto& wl1 = get_wlist(lit);
|
|
for (auto w : get_wlist(lit)) {
|
|
if (w.is_binary_clause() && w.get_literal().var() < max_var && !is_visited(w.get_literal())) {
|
|
m_aux_literals.push_back(w.get_literal());
|
|
mark_visited(w.get_literal());
|
|
}
|
|
}
|
|
wl1.reset();
|
|
};
|
|
for (unsigned v = max_var; v < num_vars(); ++v) {
|
|
gc_watch(literal(v, false));
|
|
gc_watch(literal(v, true));
|
|
}
|
|
|
|
for (literal lit : m_aux_literals) {
|
|
auto& wl2 = get_wlist(~lit);
|
|
unsigned j = 0;
|
|
for (auto w2 : wl2)
|
|
if (!w2.is_binary_clause() || w2.get_literal().var() < max_var)
|
|
wl2[j++] = w2;
|
|
wl2.shrink(j);
|
|
}
|
|
m_aux_literals.reset();
|
|
|
|
auto gc_clauses = [&](ptr_vector<clause>& clauses) {
|
|
unsigned j = 0;
|
|
for (clause* c : clauses) {
|
|
bool should_remove = false;
|
|
for (auto lit : *c)
|
|
should_remove |= lit.var() >= max_var;
|
|
if (should_remove) {
|
|
SASSERT(!c->on_reinit_stack());
|
|
detach_clause(*c);
|
|
del_clause(*c);
|
|
}
|
|
else {
|
|
clauses[j++] = c;
|
|
}
|
|
}
|
|
clauses.shrink(j);
|
|
};
|
|
gc_clauses(m_learned);
|
|
gc_clauses(m_clauses);
|
|
|
|
if (m_ext)
|
|
m_ext->gc_vars(max_var);
|
|
|
|
unsigned j = 0;
|
|
for (literal lit : m_trail) {
|
|
SASSERT(lvl(lit) == 0);
|
|
if (lit.var() < max_var)
|
|
m_trail[j++] = lit;
|
|
}
|
|
m_trail.shrink(j);
|
|
shrink_vars(max_var);
|
|
}
|
|
|
|
#if 0
|
|
void solver::gc_reinit_stack(unsigned num_scopes) {
|
|
SASSERT (!at_base_lvl());
|
|
collect_clauses_to_gc(num_scopes);
|
|
for (literal lit : m_watch_literals_to_gc) {
|
|
mark_members_of_watch_list(lit);
|
|
shrink_watch_list(lit);
|
|
}
|
|
unsigned j = 0;
|
|
for (clause* c : m_learned)
|
|
if (!c->was_removed())
|
|
m_learned[j++] = c;
|
|
m_learned.shrink(j);
|
|
for (clause* c : m_clauses_to_gc)
|
|
del_clause(*c);
|
|
m_clauses_to_gc.reset();
|
|
}
|
|
|
|
void solver::add_to_gc(literal lit, clause_wrapper const& cw) {
|
|
m_literal2gc_clause.reserve(lit.index()+1);
|
|
m_literal2gc_clause[lit.index()].push_back(cw);
|
|
if (!is_visited(lit)) {
|
|
mark_visited(lit);
|
|
m_watch_literals_to_gc.push_back(lit);
|
|
}
|
|
}
|
|
|
|
void solver::add_to_gc(clause_wrapper const& cw) {
|
|
std::cout << "add-to-gc " << cw << "\n";
|
|
if (cw.is_binary()) {
|
|
add_to_gc(cw[0], cw);
|
|
add_to_gc(cw[1], clause_wrapper(cw[1], cw[0]));
|
|
}
|
|
else if (ENABLE_TERNARY && cw.is_ternary()) {
|
|
SASSERT(cw.is_learned());
|
|
add_to_gc(cw[0], cw);
|
|
add_to_gc(cw[1], cw);
|
|
add_to_gc(cw[2], cw);
|
|
cw.get_clause()->set_removed(true);
|
|
}
|
|
else {
|
|
SASSERT(cw.is_learned());
|
|
add_to_gc(cw[0], cw);
|
|
add_to_gc(cw[1], cw);
|
|
cw.get_clause()->set_removed(true);
|
|
}
|
|
}
|
|
|
|
void solver::insert_ternary_to_delete(literal lit, clause_wrapper const& cw) {
|
|
SASSERT(cw.is_ternary());
|
|
SASSERT(lit == cw[0] || lit == cw[1] || lit == cw[2]);
|
|
literal lit1, lit2;
|
|
if (cw[0] == lit)
|
|
lit1 = cw[1], lit2 = cw[2];
|
|
else if (cw[1] == lit)
|
|
lit1 = cw[0], lit2 = cw[2];
|
|
else
|
|
lit1 = cw[0], lit2 = cw[1];
|
|
insert_ternary_to_delete(lit1, lit2, true);
|
|
}
|
|
|
|
void solver::insert_ternary_to_delete(literal lit1, literal lit2, bool should_delete) {
|
|
if (lit1.index() > lit2.index())
|
|
std::swap(lit1, lit2);
|
|
m_ternary_to_delete.push_back(std::tuple(lit1, lit2, should_delete));
|
|
}
|
|
|
|
bool solver::in_ternary_to_delete(literal lit1, literal lit2) {
|
|
if (lit1.index() > lit2.index())
|
|
std::swap(lit1, lit2);
|
|
bool found = m_ternary_to_delete.contains(std::make_pair(lit1, lit2));
|
|
if (found) std::cout << lit1 << " " << lit2 << "\n";
|
|
return found;
|
|
}
|
|
|
|
|
|
void solver::collect_clauses_to_gc(unsigned num_scopes) {
|
|
unsigned new_lvl = scope_lvl() - num_scopes;
|
|
init_visited();
|
|
m_watch_literals_to_gc.reset();
|
|
unsigned j = m_scopes[new_lvl].m_clauses_to_reinit_lim;
|
|
for (unsigned i = j, sz = m_clauses_to_reinit.size(); i < sz; ++i) {
|
|
auto cw = m_clauses_to_reinit[i];
|
|
if (is_asserting(new_lvl, cw))
|
|
m_clauses_to_reinit[j++] = cw;
|
|
else
|
|
add_to_gc(cw);
|
|
}
|
|
m_clauses_to_reinit.shrink(j);
|
|
SASSERT(m_clauses_to_reinit.size() >= j);
|
|
}
|
|
|
|
void solver::mark_members_of_watch_list(literal lit) {
|
|
init_visited();
|
|
m_ternary_to_delete.reset();
|
|
for (auto const& cw : m_literal2gc_clause[lit.index()]) {
|
|
SASSERT(!cw.is_binary() || lit == cw[0]);
|
|
SASSERT(cw.is_binary() || cw.was_removed());
|
|
if (cw.is_binary())
|
|
mark_visited(cw[1]);
|
|
else if (ENABLE_TERNARY && cw.is_ternary())
|
|
insert_ternary_to_delete(lit, cw);
|
|
}
|
|
}
|
|
|
|
void solver::shrink_watch_list(literal lit) {
|
|
auto& wl = get_wlist((~lit).index());
|
|
unsigned j = 0, sz = wl.size(), end = sz;
|
|
for (unsigned i = 0; i < end; ++i) {
|
|
auto w = wl[i];
|
|
if (w.is_binary_clause() && !is_visited(w.get_literal()))
|
|
wl[j++] = w;
|
|
else if (ENABLE_TERNARY && w.is_ternary_clause())
|
|
insert_ternary_to_delete(w.literal1(), w.literal2(), false);
|
|
else if (w.is_clause() && !get_clause(w).was_removed())
|
|
wl[j++] = w;
|
|
else if (w.is_ext_constraint())
|
|
wl[j++] = w;
|
|
}
|
|
#if 0
|
|
std::sort(m_ternary_to_delete.begin(), m_ternary_to_delete.end());
|
|
int prev = -1;
|
|
unsigned k = 0;
|
|
std::tuple<literal, literal, bool> p = tuple(null_literal, null_literal, false);
|
|
for (unsigned i = 0; i < m_ternary_to_delete.size(); ++i) {
|
|
auto const& t = m_ternary_to_delete[i];
|
|
}
|
|
#endif
|
|
std::cout << "gc-watch-list " << lit << " " << wl.size() << " -> " << j << "\n";
|
|
wl.shrink(j);
|
|
m_literal2gc_clause[lit.index()].reset();
|
|
}
|
|
|
|
|
|
#endif
|
|
|
|
}
|