mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-06 06:03:23 +00:00
Code Activity

Merge branch 'opt' of https://github.com/NikolajBjorner/z3 into opt

Browse source
This commit is contained in:
Miguel Angelo Da Terra Neves 2017-12-01 11:02:35 -08:00
commit 2e042a8bea
13 changed files with 304 additions and 158 deletions
Download patch file Download diff file Expand all files Collapse all files

49
src/sat/ba_solver.cpp
View file

@ -216,10 +216,10 @@ namespace sat {
// ---------------------------- // ----------------------------
// card // card
bool ba_solver::init_watch(card& c, bool is_true) { bool ba_solver::init_watch(card& c) {
clear_watch(c); clear_watch(c);
literal root = c.lit(); literal root = c.lit();
if (root != null_literal && root.sign() == is_true) { if (root != null_literal && value(root) == l_false) {
c.negate(); c.negate();
root.neg(); root.neg();
} }
@ -352,7 +352,7 @@ namespace sat {
IF_VERBOSE(100, display(verbose_stream() << "nullify tracking literal\n", p, true);); IF_VERBOSE(100, display(verbose_stream() << "nullify tracking literal\n", p, true););
SASSERT(lvl(p.lit()) == 0); SASSERT(lvl(p.lit()) == 0);
nullify_tracking_literal(p); nullify_tracking_literal(p);
init_watch(p, true); init_watch(p);
} }
SASSERT(p.lit() == null_literal || value(p.lit()) != l_false); SASSERT(p.lit() == null_literal || value(p.lit()) != l_false);
@ -379,7 +379,7 @@ namespace sat {
} }
else if (true_val == 0 && num_false == 0) { else if (true_val == 0 && num_false == 0) {
if (p.lit() == null_literal || value(p.lit()) == l_true) { if (p.lit() == null_literal || value(p.lit()) == l_true) {
init_watch(p, true); init_watch(p);
} }
} }
else if (true_val >= p.k()) { else if (true_val >= p.k()) {
@ -431,7 +431,7 @@ namespace sat {
return; return;
} }
else if (p.lit() == null_literal || value(p.lit()) == l_true) { else if (p.lit() == null_literal || value(p.lit()) == l_true) {
init_watch(p, true); init_watch(p);
} }
else { else {
SASSERT(value(p.lit()) == l_undef); SASSERT(value(p.lit()) == l_undef);
@ -510,13 +510,13 @@ namespace sat {
// watch a prefix of literals, such that the slack of these is >= k // watch a prefix of literals, such that the slack of these is >= k
bool ba_solver::init_watch(pb& p, bool is_true) { bool ba_solver::init_watch(pb& p) {
clear_watch(p); clear_watch(p);
if (p.lit() != null_literal && p.lit().sign() == is_true) { if (p.lit() != null_literal && value(p.lit()) == l_false) {
p.negate(); p.negate();
} }
SASSERT(p.lit() == null_literal || value(p.lit()) == l_true); VERIFY(p.lit() == null_literal || value(p.lit()) == l_true);
unsigned sz = p.size(), bound = p.k(); unsigned sz = p.size(), bound = p.k();
// put the non-false literals into the head. // put the non-false literals into the head.
@ -548,7 +548,7 @@ namespace sat {
if (slack < bound) { if (slack < bound) {
literal lit = p[j].second; literal lit = p[j].second;
SASSERT(value(lit) == l_false); VERIFY(value(lit) == l_false);
for (unsigned i = j + 1; i < sz; ++i) { for (unsigned i = j + 1; i < sz; ++i) {
if (lvl(lit) < lvl(p[i].second)) { if (lvl(lit) < lvl(p[i].second)) {
lit = p[i].second; lit = p[i].second;
@ -826,7 +826,7 @@ namespace sat {
SASSERT(p.well_formed()); SASSERT(p.well_formed());
if (p.lit() == null_literal || value(p.lit()) == l_true) { if (p.lit() == null_literal || value(p.lit()) == l_true) {
init_watch(p, true); init_watch(p);
} }
} }
} }
@ -909,9 +909,9 @@ namespace sat {
return odd; return odd;
} }
bool ba_solver::init_watch(xor& x, bool is_true) { bool ba_solver::init_watch(xor& x) {
clear_watch(x); clear_watch(x);
if (x.lit() != null_literal && x.lit().sign() == is_true) { if (x.lit() != null_literal && value(x.lit()) == l_false) {
x.negate(); x.negate();
} }
TRACE("ba", display(tout, x, true);); TRACE("ba", display(tout, x, true););
@ -1566,7 +1566,7 @@ namespace sat {
m_constraint_to_reinit.push_back(c); m_constraint_to_reinit.push_back(c);
} }
else if (lit == null_literal) { else if (lit == null_literal) {
init_watch(*c, true); init_watch(*c);
} }
else { else {
if (m_solver) m_solver->set_external(lit.var()); if (m_solver) m_solver->set_external(lit.var());
@ -1577,12 +1577,12 @@ namespace sat {
} }
bool ba_solver::init_watch(constraint& c, bool is_true) { bool ba_solver::init_watch(constraint& c) {
if (inconsistent()) return false; if (inconsistent()) return false;
switch (c.tag()) { switch (c.tag()) {
case card_t: return init_watch(c.to_card(), is_true); case card_t: return init_watch(c.to_card());
case pb_t: return init_watch(c.to_pb(), is_true); case pb_t: return init_watch(c.to_pb());
case xor_t: return init_watch(c.to_xor(), is_true); case xor_t: return init_watch(c.to_xor());
} }
UNREACHABLE(); UNREACHABLE();
return false; return false;
@ -1642,7 +1642,7 @@ namespace sat {
constraint& c = index2constraint(idx); constraint& c = index2constraint(idx);
TRACE("ba", tout << l << "\n";); TRACE("ba", tout << l << "\n";);
if (c.lit() != null_literal && l.var() == c.lit().var()) { if (c.lit() != null_literal && l.var() == c.lit().var()) {
init_watch(c, !l.sign()); init_watch(c);
return true; return true;
} }
else if (c.lit() != null_literal && value(c.lit()) != l_true) { else if (c.lit() != null_literal && value(c.lit()) != l_true) {
@ -2358,7 +2358,7 @@ namespace sat {
unsigned sz = m_constraint_to_reinit_last_sz; unsigned sz = m_constraint_to_reinit_last_sz;
for (unsigned i = sz; i < m_constraint_to_reinit.size(); ++i) { for (unsigned i = sz; i < m_constraint_to_reinit.size(); ++i) {
constraint* c = m_constraint_to_reinit[i]; constraint* c = m_constraint_to_reinit[i];
if (!init_watch(*c, true) && !s().at_base_lvl()) { if (!init_watch(*c) && !s().at_base_lvl()) {
m_constraint_to_reinit[sz++] = c; m_constraint_to_reinit[sz++] = c;
} }
} }
@ -2677,7 +2677,7 @@ namespace sat {
} }
else { else {
if (c.lit() == null_literal || value(c.lit()) == l_true) { if (c.lit() == null_literal || value(c.lit()) == l_true) {
init_watch(c, true); init_watch(c);
} }
SASSERT(c.lit() == null_literal || is_watched(c.lit(), c)); SASSERT(c.lit() == null_literal || is_watched(c.lit(), c));
SASSERT(c.well_formed()); SASSERT(c.well_formed());
@ -2753,10 +2753,7 @@ namespace sat {
recompile(c); recompile(c);
} }
else { else {
// review for potential incompleteness: if c.lit() == l_false, do propagations happen? if (c.lit() == null_literal || value(c.lit()) != l_undef) init_watch(c);
if (c.lit() == null_literal || value(c.lit()) == l_true) {
init_watch(c, true);
}
SASSERT(c.well_formed()); SASSERT(c.well_formed());
} }
} }
@ -2870,7 +2867,6 @@ namespace sat {
s().set_external(v); s().set_external(v);
} }
} }
IF_VERBOSE(10, verbose_stream() << "non-external variables converted: " << ext << "\n";);
return ext; return ext;
} }
@ -2897,7 +2893,6 @@ namespace sat {
++pure_literals; ++pure_literals;
} }
} }
IF_VERBOSE(10, verbose_stream() << "pure literals converted: " << pure_literals << " " << inconsistent() << "\n";);
return pure_literals; return pure_literals;
} }
@ -3119,7 +3114,7 @@ namespace sat {
} }
} }
c2.set_size(c2.size() - 1); c2.set_size(c2.size() - 1);
init_watch(c2, true); init_watch(c2);
m_simplify_change = true; m_simplify_change = true;
#endif #endif
} }

8
src/sat/ba_solver.h
View file

@ -296,7 +296,7 @@ namespace sat {
void watch_literal(wliteral w, pb& p); void watch_literal(wliteral w, pb& p);
bool is_watched(literal l, constraint const& c) const; bool is_watched(literal l, constraint const& c) const;
void add_constraint(constraint* c); void add_constraint(constraint* c);
bool init_watch(constraint& c, bool is_true); bool init_watch(constraint& c);
void init_watch(bool_var v); void init_watch(bool_var v);
void clear_watch(constraint& c); void clear_watch(constraint& c);
lbool add_assign(constraint& c, literal l); lbool add_assign(constraint& c, literal l);
@ -320,7 +320,7 @@ namespace sat {
// cardinality // cardinality
bool init_watch(card& c, bool is_true); bool init_watch(card& c);
lbool add_assign(card& c, literal lit); lbool add_assign(card& c, literal lit);
void clear_watch(card& c); void clear_watch(card& c);
void reset_coeffs(); void reset_coeffs();
@ -334,7 +334,7 @@ namespace sat {
// xor specific functionality // xor specific functionality
void clear_watch(xor& x); void clear_watch(xor& x);
bool init_watch(xor& x, bool is_true); bool init_watch(xor& x);
bool parity(xor const& x, unsigned offset) const; bool parity(xor const& x, unsigned offset) const;
lbool add_assign(xor& x, literal alit); lbool add_assign(xor& x, literal alit);
void get_xor_antecedents(literal l, unsigned index, justification js, literal_vector& r); void get_xor_antecedents(literal l, unsigned index, justification js, literal_vector& r);
@ -345,7 +345,7 @@ namespace sat {
// pb functionality // pb functionality
unsigned m_a_max; unsigned m_a_max;
bool init_watch(pb& p, bool is_true); bool init_watch(pb& p);
lbool add_assign(pb& p, literal alit); lbool add_assign(pb& p, literal alit);
void add_index(pb& p, unsigned index, literal lit); void add_index(pb& p, unsigned index, literal lit);
void clear_watch(pb& p); void clear_watch(pb& p);

55
src/sat/sat_asymm_branch.cpp
View file

@ -59,7 +59,7 @@ namespace sat {
} }
}; };
void asymm_branch::process(clause_vector& clauses) { void asymm_branch::process(scc& scc, clause_vector& clauses) {
int64 limit = -m_asymm_branch_limit; int64 limit = -m_asymm_branch_limit;
std::stable_sort(clauses.begin(), clauses.end(), clause_size_lt()); std::stable_sort(clauses.begin(), clauses.end(), clause_size_lt());
m_counter -= clauses.size(); m_counter -= clauses.size();
@ -83,8 +83,9 @@ namespace sat {
} }
s.checkpoint(); s.checkpoint();
clause & c = *(*it); clause & c = *(*it);
if (!process(c)) if (m_asymm_branch_sampled ? !process_sampled(scc, c) : !process(c)) {
continue; // clause was removed continue; // clause was removed
}
*it2 = *it; *it2 = *it;
++it2; ++it2;
} }
@ -103,7 +104,7 @@ namespace sat {
void asymm_branch::operator()(bool force) { void asymm_branch::operator()(bool force) {
++m_calls; ++m_calls;
if (m_calls <= 1) if (m_calls <= m_asymm_branch_delay)
return; return;
if (!m_asymm_branch && !m_asymm_branch_all) if (!m_asymm_branch && !m_asymm_branch_all)
return; return;
@ -118,9 +119,27 @@ namespace sat {
TRACE("asymm_branch_detail", s.display(tout);); TRACE("asymm_branch_detail", s.display(tout););
report rpt(*this); report rpt(*this);
svector<char> saved_phase(s.m_phase); svector<char> saved_phase(s.m_phase);
if (m_asymm_branch_sampled) {
scc scc(s, m_params);
while (true) {
unsigned elim = m_elim_literals;
scc.init_big(true);
process(scc, s.m_clauses);
process(scc, s.m_learned);
s.propagate(false);
if (s.m_inconsistent)
break;
std::cout << m_elim_literals - elim << "\n";
if (m_elim_literals == elim)
break;
}
}
else {
scc scc(s, m_params);
m_counter = 0; m_counter = 0;
process(s.m_clauses); process(scc, s.m_clauses);
m_counter = -m_counter; m_counter = -m_counter;
}
s.m_phase = saved_phase; s.m_phase = saved_phase;
m_asymm_branch_limit *= 2; m_asymm_branch_limit *= 2;
if (m_asymm_branch_limit > UINT_MAX) if (m_asymm_branch_limit > UINT_MAX)
@ -145,12 +164,6 @@ namespace sat {
return true; return true;
} }
void asymm_branch::setup_big() {
scc scc(s, m_params);
vector<literal_vector> const& big = scc.get_big(true); // include learned binary clauses
}
struct asymm_branch::compare_left { struct asymm_branch::compare_left {
scc& s; scc& s;
compare_left(scc& s): s(s) {} compare_left(scc& s): s(s) {}
@ -206,6 +219,7 @@ namespace sat {
right = right2; right = right2;
} }
} }
if (m_to_delete.empty()) {
right = scc.get_right(m_neg[0]); right = scc.get_right(m_neg[0]);
for (unsigned i = 1; i < m_neg.size(); ++i) { for (unsigned i = 1; i < m_neg.size(); ++i) {
literal lit = m_neg[i]; literal lit = m_neg[i];
@ -218,7 +232,21 @@ namespace sat {
right = right2; right = right2;
} }
} }
}
if (!m_to_delete.empty()) { if (!m_to_delete.empty()) {
#if 0
std::cout << "delete " << m_to_delete << "\n";
std::cout << "pos\n";
for (literal l : m_pos) {
std::cout << l << ": " << scc.get_left(l) << " " << scc.get_right(l) << "\n";
}
std::cout << "neg\n";
for (literal l : m_neg) {
std::cout << l << ": " << scc.get_left(l) << " " << scc.get_right(l) << "\n";
}
std::cout << "\n";
#endif
unsigned j = 0; unsigned j = 0;
for (unsigned i = 0; i < c.size(); ++i) { for (unsigned i = 0; i < c.size(); ++i) {
if (!m_to_delete.contains(c[i])) { if (!m_to_delete.contains(c[i])) {
@ -283,12 +311,12 @@ namespace sat {
} }
} }
new_sz = j; new_sz = j;
m_elim_literals += c.size() - new_sz;
// std::cout << "cleanup: " << c.id() << ": " << literal_vector(new_sz, c.begin()) << " delta: " << (c.size() - new_sz) << " " << skip_idx << " " << new_sz << "\n"; // std::cout << "cleanup: " << c.id() << ": " << literal_vector(new_sz, c.begin()) << " delta: " << (c.size() - new_sz) << " " << skip_idx << " " << new_sz << "\n";
return re_attach(scoped_d, c, new_sz); return re_attach(scoped_d, c, new_sz);
} }
bool asymm_branch::re_attach(scoped_detach& scoped_d, clause& c, unsigned new_sz) { bool asymm_branch::re_attach(scoped_detach& scoped_d, clause& c, unsigned new_sz) {
m_elim_literals += c.size() - new_sz;
switch(new_sz) { switch(new_sz) {
case 0: case 0:
s.set_conflict(justification()); s.set_conflict(justification());
@ -315,8 +343,9 @@ namespace sat {
} }
} }
bool asymm_branch::process2(scc& scc, clause & c) { bool asymm_branch::process_sampled(scc& scc, clause & c) {
scoped_detach scoped_d(s, c); scoped_detach scoped_d(s, c);
sort(scc, c);
if (uhte(scc, c)) { if (uhte(scc, c)) {
scoped_d.del_clause(); scoped_d.del_clause();
return false; return false;
@ -372,6 +401,8 @@ namespace sat {
void asymm_branch::updt_params(params_ref const & _p) { void asymm_branch::updt_params(params_ref const & _p) {
sat_asymm_branch_params p(_p); sat_asymm_branch_params p(_p);
m_asymm_branch = p.asymm_branch(); m_asymm_branch = p.asymm_branch();
m_asymm_branch_delay = p.asymm_branch_delay();
m_asymm_branch_sampled = p.asymm_branch_sampled();
m_asymm_branch_limit = p.asymm_branch_limit(); m_asymm_branch_limit = p.asymm_branch_limit();
m_asymm_branch_all = p.asymm_branch_all(); m_asymm_branch_all = p.asymm_branch_all();
if (m_asymm_branch_limit > UINT_MAX) if (m_asymm_branch_limit > UINT_MAX)

8
src/sat/sat_asymm_branch.h
View file

@ -39,6 +39,8 @@ namespace sat {
// config // config
bool m_asymm_branch; bool m_asymm_branch;
unsigned m_asymm_branch_delay;
bool m_asymm_branch_sampled;
bool m_asymm_branch_all; bool m_asymm_branch_all;
int64 m_asymm_branch_limit; int64 m_asymm_branch_limit;
@ -60,9 +62,9 @@ namespace sat {
bool process(clause & c); bool process(clause & c);
bool process2(scc& scc, clause & c); bool process_sampled(scc& scc, clause & c);
void process(clause_vector & c); void process(scc& scc, clause_vector & c);
bool process_all(clause & c); bool process_all(clause & c);
@ -72,8 +74,6 @@ namespace sat {
bool propagate_literal(clause const& c, literal l); bool propagate_literal(clause const& c, literal l);
void setup_big();
public: public:
asymm_branch(solver & s, params_ref const & p); asymm_branch(solver & s, params_ref const & p);

2
src/sat/sat_asymm_branch_params.pyg
View file

@ -2,5 +2,7 @@ def_module_params(module_name='sat',
class_name='sat_asymm_branch_params', class_name='sat_asymm_branch_params',
export=True, export=True,
params=(('asymm_branch', BOOL, True, 'asymmetric branching'), params=(('asymm_branch', BOOL, True, 'asymmetric branching'),
('asymm_branch.delay', UINT, 1, 'number of simplification rounds to wait until invoking asymmetric branch simplification'),
('asymm_branch.sampled', BOOL, False, 'use sampling based asymmetric branching based on binary implication graph'),
('asymm_branch.limit', UINT, 100000000, 'approx. maximum number of literals visited during asymmetric branching'), ('asymm_branch.limit', UINT, 100000000, 'approx. maximum number of literals visited during asymmetric branching'),
('asymm_branch.all', BOOL, False, 'asymmetric branching on all literals per clause'))) ('asymm_branch.all', BOOL, False, 'asymmetric branching on all literals per clause')))

100
src/sat/sat_lookahead.cpp
View file

@ -20,6 +20,7 @@ Notes:
#include "sat/sat_solver.h" #include "sat/sat_solver.h"
#include "sat/sat_extension.h" #include "sat/sat_extension.h"
#include "sat/sat_lookahead.h" #include "sat/sat_lookahead.h"
#include "sat/sat_scc.h"
#include "util/union_find.h" #include "util/union_find.h"
namespace sat { namespace sat {
@ -2013,6 +2014,11 @@ namespace sat {
return true; return true;
} }
void lookahead::update_cube_statistics(statistics& st) {
st.update("lh cube cutoffs", m_cube_state.m_cutoffs);
st.update("lh cube conflicts", m_cube_state.m_conflicts);
}
lbool lookahead::cube(bool_var_vector const& vars, literal_vector& lits, unsigned backtrack_level) { lbool lookahead::cube(bool_var_vector const& vars, literal_vector& lits, unsigned backtrack_level) {
scoped_ext _scoped_ext(*this); scoped_ext _scoped_ext(*this);
lits.reset(); lits.reset();
@ -2031,6 +2037,7 @@ namespace sat {
unsigned depth = 0; unsigned depth = 0;
unsigned init_trail = m_trail.size(); unsigned init_trail = m_trail.size();
m_cube_state.reset_stats();
if (!is_first) { if (!is_first) {
goto pick_up_work; goto pick_up_work;
} }
@ -2042,6 +2049,7 @@ namespace sat {
if (inconsistent()) { if (inconsistent()) {
TRACE("sat", tout << "inconsistent: " << m_cube_state.m_cube << "\n";); TRACE("sat", tout << "inconsistent: " << m_cube_state.m_cube << "\n";);
m_cube_state.m_freevars_threshold = m_freevars.size(); m_cube_state.m_freevars_threshold = m_freevars.size();
m_cube_state.inc_conflict();
if (!backtrack(m_cube_state.m_cube, m_cube_state.m_is_decision)) return l_false; if (!backtrack(m_cube_state.m_cube, m_cube_state.m_is_decision)) return l_false;
continue; continue;
} }
@ -2062,6 +2070,7 @@ namespace sat {
(m_config.m_cube_cutoff == 0 && m_freevars.size() < m_cube_state.m_freevars_threshold)) {*/ (m_config.m_cube_cutoff == 0 && m_freevars.size() < m_cube_state.m_freevars_threshold)) {*/
m_cube_state.m_freevars_threshold *= (1.0 - pow(m_config.m_cube_fraction, depth)); m_cube_state.m_freevars_threshold *= (1.0 - pow(m_config.m_cube_fraction, depth));
set_conflict(); set_conflict();
m_cube_state.inc_cutoff();
#if 0 #if 0
// return cube of all literals, not just the ones in the main cube // return cube of all literals, not just the ones in the main cube
lits.append(m_trail.size() - init_trail, m_trail.c_ptr() + init_trail); lits.append(m_trail.size() - init_trail, m_trail.c_ptr() + init_trail);
@ -2308,15 +2317,86 @@ namespace sat {
void lookahead::add_hyper_binary() { void lookahead::add_hyper_binary() {
unsigned num_lits = m_s.num_vars() * 2;
#if 0
std::cout << "binary trail size: " << m_binary_trail.size() << "\n"; std::cout << "binary trail size: " << m_binary_trail.size() << "\n";
std::cout << "Are windfalls still on the trail at base level?\n"; std::cout << "Are windfalls still on the trail at base level?\n";
unsigned num_lits = m_s.num_vars() * 2; #endif
unsigned disconnected1 = 0;
unsigned disconnected2 = 0;
#if 1
typedef std::pair<unsigned, unsigned> u_pair;
hashtable<u_pair, pair_hash<unsigned_hash, unsigned_hash>, default_eq<u_pair> > imp;
for (unsigned idx = 0; idx < num_lits; ++idx) {
literal u = get_parent(to_literal(idx));
if (null_literal != u) {
for (watched const& w : m_s.m_watches[idx]) {
if (!w.is_binary_clause()) continue;
literal v = get_parent(w.get_literal());
if (null_literal != v) {
imp.insert(std::make_pair(u.index(), v.index()));
}
}
}
}
scc scc(m_s, m_s.m_params);
scc.init_big(true);
svector<std::pair<literal, literal>> candidates;
unsigned_vector bin_size(num_lits); unsigned_vector bin_size(num_lits);
for (unsigned idx : m_binary_trail) { for (unsigned idx : m_binary_trail) {
bin_size[idx]++; bin_size[idx]++;
} }
for (unsigned idx = 0; idx < num_lits; ++idx) {
literal u = to_literal(idx);
if (u != get_parent(u)) continue;
if (m_s.was_eliminated(u.var())) continue;
literal_vector const& lits = m_binary[idx];
for (unsigned sz = bin_size[idx]; sz > 0; --sz) {
literal v = lits[lits.size() - sz];
if (v != get_parent(v)) continue;
if (m_s.was_eliminated(v.var())) continue;
if (imp.contains(std::make_pair(u.index(), v.index()))) continue;
if (scc.reaches(u, v)) continue;
candidates.push_back(std::make_pair(u, v));
}
}
for (unsigned i = 0; i < 5; ++i) {
scc.init_big(true);
unsigned k = 0;
union_find_default_ctx ufctx;
union_find<union_find_default_ctx> uf(ufctx);
for (unsigned i = 0; i < num_lits; ++i) uf.mk_var();
for (unsigned j = 0; j < candidates.size(); ++j) {
literal u = candidates[j].first;
literal v = candidates[j].second;
if (!scc.reaches(u, v)) {
if (uf.find(u.index()) != uf.find(v.index())) {
++disconnected1;
uf.merge(u.index(), v.index());
uf.merge((~u).index(), (~v).index());
m_s.mk_clause(~u, v, true);
}
else {
candidates[k] = candidates[j];
++k;
}
}
}
std::cout << candidates.size() << " -> " << k << "\n";
if (k == candidates.size()) break;
candidates.shrink(k);
}
std::cout << "candidates: " << candidates.size() << "\n";
#endif
#if 0
union_find_default_ctx ufctx; union_find_default_ctx ufctx;
union_find<union_find_default_ctx> uf(ufctx); union_find<union_find_default_ctx> uf(ufctx);
for (unsigned i = 0; i < num_lits; ++i) uf.mk_var(); for (unsigned i = 0; i < num_lits; ++i) uf.mk_var();
@ -2333,21 +2413,25 @@ namespace sat {
} }
} }
unsigned disconnected = 0;
for (unsigned i = 0; i < m_binary.size(); ++i) { for (unsigned i = 0; i < m_binary.size(); ++i) {
literal u = to_literal(i); literal u = to_literal(i);
if (u == get_parent(u)) { if (u == get_parent(u) && !m_s.was_eliminated(u.var())) {
for (literal v : m_binary[i]) { for (literal v : m_binary[i]) {
if (v == get_parent(v) && uf.find(u.index()) != uf.find(v.index())) { if (v == get_parent(v) &&
++disconnected; !m_s.was_eliminated(v.var()) &&
uf.find(u.index()) != uf.find(v.index())) {
++disconnected2;
uf.merge(u.index(), v.index()); uf.merge(u.index(), v.index());
m_s.mk_clause(~u, v, true); // m_s.mk_clause(~u, v, true);
} }
} }
} }
} }
IF_VERBOSE(10, verbose_stream() << "(sat-lookahead :bca " << disconnected << ")\n";); #endif
m_stats.m_bca += disconnected;
IF_VERBOSE(10, verbose_stream() << "(sat-lookahead :bca " << disconnected1 << " " << disconnected2 << ")\n";);
//IF_VERBOSE(10, verbose_stream() << "(sat-lookahead :bca " << disconnected << ")\n";);
//m_stats.m_bca += disconnected;
} }
void lookahead::normalize_parents() { void lookahead::normalize_parents() {

8
src/sat/sat_lookahead.h
View file

@ -171,13 +171,19 @@ namespace sat {
svector<bool> m_is_decision; svector<bool> m_is_decision;
literal_vector m_cube; literal_vector m_cube;
double m_freevars_threshold; double m_freevars_threshold;
unsigned m_conflicts;
unsigned m_cutoffs;
cube_state() { reset(); } cube_state() { reset(); }
void reset() { void reset() {
m_first = true; m_first = true;
m_is_decision.reset(); m_is_decision.reset();
m_cube.reset(); m_cube.reset();
m_freevars_threshold = 0; m_freevars_threshold = 0;
reset_stats();
} }
void reset_stats() { m_conflicts = 0; m_cutoffs = 0; }
void inc_conflict() { ++m_conflicts; }
void inc_cutoff() { ++m_cutoffs; }
}; };
config m_config; config m_config;
@ -577,6 +583,8 @@ namespace sat {
lbool cube(bool_var_vector const& vars, literal_vector& lits, unsigned backtrack_level); lbool cube(bool_var_vector const& vars, literal_vector& lits, unsigned backtrack_level);
void update_cube_statistics(statistics& st);
literal select_lookahead(literal_vector const& assumptions, bool_var_vector const& vars); literal select_lookahead(literal_vector const& assumptions, bool_var_vector const& vars);
/** /**
\brief simplify set of clauses by extracting units from a lookahead at base level. \brief simplify set of clauses by extracting units from a lookahead at base level.

120
src/sat/sat_scc.cpp
View file

@ -234,17 +234,7 @@ namespace sat {
return to_elim.size(); return to_elim.size();
} }
// shuffle vertices to obtain different DAG traversal each time void scc::init_big(bool learned) {
void scc::shuffle(literal_vector& lits) {
unsigned sz = lits.size();
if (sz > 1) {
for (unsigned i = sz; i-- > 0; ) {
std::swap(lits[i], lits[m_rand(i+1)]);
}
}
}
vector<literal_vector> const& scc::get_big(bool learned) {
unsigned num_lits = m_solver.num_vars() * 2; unsigned num_lits = m_solver.num_vars() * 2;
m_dag.reset(); m_dag.reset();
m_roots.reset(); m_roots.reset();
@ -263,53 +253,21 @@ namespace sat {
edges.push_back(v); edges.push_back(v);
} }
} }
shuffle(edges); shuffle<literal>(edges.size(), edges.c_ptr(), m_rand);
} }
return m_dag; init_dfs_num(learned);
} }
void scc::get_dfs_num(bool learned) { struct scc::pframe {
unsigned num_lits = m_solver.num_vars() * 2; literal m_parent;
SASSERT(m_left.size() == num_lits); literal m_child;
SASSERT(m_right.size() == num_lits); pframe(literal p, literal c):
literal_vector todo; m_parent(p), m_child(c) {}
// retrieve literals that have no predecessors literal child() const { return m_child; }
for (unsigned l_idx = 0; l_idx < num_lits; l_idx++) { literal parent() const { return m_parent; }
literal u(to_literal(l_idx)); };
if (m_roots[u.index()]) todo.push_back(u);
}
shuffle(todo);
int dfs_num = 0;
while (!todo.empty()) {
literal u = todo.back();
int& d = m_left[u.index()];
// already visited
if (d > 0) {
if (m_right[u.index()] < 0) {
m_right[u.index()] = dfs_num;
}
todo.pop_back();
}
// visited as child:
else if (d < 0) {
d = -d;
for (literal v : m_dag[u.index()]) {
if (m_left[v.index()] == 0) {
m_left[v.index()] = - d - 1;
m_root[v.index()] = m_root[u.index()];
m_parent[v.index()] = u;
todo.push_back(v);
}
}
}
// new root.
else {
d = --dfs_num;
}
}
}
unsigned scc::reduce_tr(bool learned) { void scc::init_dfs_num(bool learned) {
unsigned num_lits = m_solver.num_vars() * 2; unsigned num_lits = m_solver.num_vars() * 2;
m_left.reset(); m_left.reset();
m_right.reset(); m_right.reset();
@ -317,11 +275,61 @@ namespace sat {
m_parent.reset(); m_parent.reset();
m_left.resize(num_lits, 0); m_left.resize(num_lits, 0);
m_right.resize(num_lits, -1); m_right.resize(num_lits, -1);
m_root.resize(num_lits, null_literal);
m_parent.resize(num_lits, null_literal);
for (unsigned i = 0; i < num_lits; ++i) { for (unsigned i = 0; i < num_lits; ++i) {
m_root[i] = to_literal(i); m_root[i] = to_literal(i);
m_parent[i] = to_literal(i); m_parent[i] = to_literal(i);
} }
get_dfs_num(learned); svector<pframe> todo;
// retrieve literals that have no predecessors
for (unsigned l_idx = 0; l_idx < num_lits; l_idx++) {
literal u(to_literal(l_idx));
if (m_roots[u.index()]) {
todo.push_back(pframe(null_literal, u));
}
}
shuffle<pframe>(todo.size(), todo.c_ptr(), m_rand);
int dfs_num = 0;
while (!todo.empty()) {
literal u = todo.back().child();
if (m_left[u.index()] > 0) {
// already visited
if (m_right[u.index()] < 0) {
m_right[u.index()] = ++dfs_num;
}
todo.pop_back();
}
else {
SASSERT(m_left[u.index()] == 0);
m_left[u.index()] = ++dfs_num;
for (literal v : m_dag[u.index()]) {
if (m_left[v.index()] == 0) {
todo.push_back(pframe(u, v));
}
}
literal p = todo.back().parent();
if (p != null_literal) {
m_root[u.index()] = m_root[p.index()];
m_parent[u.index()] = p;
}
}
}
for (unsigned i = 0; i < num_lits; ++i) {
if (m_right[i] < 0) {
VERIFY(m_left[i] == 0);
m_left[i] = ++dfs_num;
m_right[i] = ++dfs_num;
}
}
for (unsigned i = 0; i < num_lits; ++i) {
VERIFY(m_left[i] < m_right[i]);
}
}
unsigned scc::reduce_tr(bool learned) {
unsigned num_lits = m_solver.num_vars() * 2;
init_big(learned);
unsigned idx = 0; unsigned idx = 0;
unsigned elim = m_num_elim_bin; unsigned elim = m_num_elim_bin;
for (watch_list & wlist : m_solver.m_watches) { for (watch_list & wlist : m_solver.m_watches) {
@ -333,7 +341,7 @@ namespace sat {
watched& w = *it; watched& w = *it;
if (learned ? w.is_binary_learned_clause() : w.is_binary_unblocked_clause()) { if (learned ? w.is_binary_learned_clause() : w.is_binary_unblocked_clause()) {
literal v = w.get_literal(); literal v = w.get_literal();
if (m_left[u.index()] + 1 < m_left[v.index()]) { if (reaches(u, v) && u != get_parent(v)) {
++m_num_elim_bin; ++m_num_elim_bin;
} }
else { else {

14
src/sat/sat_scc.h
View file

@ -44,10 +44,13 @@ namespace sat {
svector<int> m_left, m_right; svector<int> m_left, m_right;
literal_vector m_root, m_parent; literal_vector m_root, m_parent;
void shuffle(literal_vector& lits);
void reduce_tr(); void reduce_tr();
unsigned reduce_tr(bool learned); unsigned reduce_tr(bool learned);
void init_dfs_num(bool learned);
struct pframe;
public: public:
scc(solver & s, params_ref const & p); scc(solver & s, params_ref const & p);
@ -60,17 +63,14 @@ namespace sat {
void reset_statistics(); void reset_statistics();
/* /*
\brief retrieve binary implication graph \brief create binary implication graph and associated data-structures to check transitivity.
*/ */
vector<literal_vector> const& get_big(bool learned); void init_big(bool learned);
int get_left(literal l) const { return m_left[l.index()]; } int get_left(literal l) const { return m_left[l.index()]; }
int get_right(literal l) const { return m_right[l.index()]; } int get_right(literal l) const { return m_right[l.index()]; }
literal get_parent(literal l) const { return m_parent[l.index()]; } literal get_parent(literal l) const { return m_parent[l.index()]; }
literal get_root(literal l) const { return m_root[l.index()]; } literal get_root(literal l) const { return m_root[l.index()]; }
bool reaches(literal u, literal v) const { return m_left[u.index()] < m_left[v.index()] && m_right[v.index()] < m_right[u.index()]; }
void get_dfs_num(bool learned);
}; };
}; };

51
src/sat/sat_simplifier.cpp
View file

@ -958,6 +958,8 @@ namespace sat {
literal_vector m_covered_clause; literal_vector m_covered_clause;
literal_vector m_intersection; literal_vector m_intersection;
literal_vector m_new_intersection;
svector<bool> m_in_intersection;
sat::model_converter::elim_stackv m_elim_stack; sat::model_converter::elim_stackv m_elim_stack;
unsigned m_ala_qhead; unsigned m_ala_qhead;
@ -967,6 +969,7 @@ namespace sat {
m_counter(limit), m_counter(limit),
mc(_mc), mc(_mc),
m_queue(l, wlist) { m_queue(l, wlist) {
m_in_intersection.resize(s.s.num_vars() * 2, false);
} }
void insert(literal l) { void insert(literal l) {
@ -1066,13 +1069,26 @@ namespace sat {
s.block_clause(*c); s.block_clause(*c);
} }
void reset_intersection() {
for (literal l : m_intersection) m_in_intersection[l.index()] = false;
m_intersection.reset();
}
void add_intersection(literal lit) {
m_intersection.push_back(lit);
m_in_intersection[lit.index()] = true;
}
// //
// Resolve intersection // Resolve intersection
// Find literals that are in the intersection of all resolvents with l. // Find literals that are in the intersection of all resolvents with l.
// //
bool resolution_intersection(literal l, literal_vector& inter, bool adding) { bool resolution_intersection(literal l, bool adding) {
if (!process_var(l.var())) return false; if (!process_var(l.var())) return false;
bool first = true; bool first = true;
reset_intersection();
for (watched & w : s.get_wlist(l)) { for (watched & w : s.get_wlist(l)) {
// when adding a blocked clause, then all non-learned clauses have to be considered for the // when adding a blocked clause, then all non-learned clauses have to be considered for the
// resolution intersection. // resolution intersection.
@ -1083,11 +1099,12 @@ namespace sat {
continue; // tautology continue; // tautology
} }
if (!first || s.is_marked(lit)) { if (!first || s.is_marked(lit)) {
inter.reset(); reset_intersection();
return false; // intersection is empty or does not add anything new. return false; // intersection is empty or does not add anything new.
} }
first = false; first = false;
inter.push_back(lit); SASSERT(m_intersection.empty());
add_intersection(lit);
} }
} }
clause_use_list & neg_occs = s.m_use_list.get(~l); clause_use_list & neg_occs = s.m_use_list.get(~l);
@ -1103,20 +1120,22 @@ namespace sat {
} }
if (!tautology) { if (!tautology) {
if (first) { if (first) {
for (literal lit : c) { for (literal lit : c)
if (lit != ~l && !s.is_marked(lit)) inter.push_back(lit); if (lit != ~l && !s.is_marked(lit))
} add_intersection(lit);
first = false; first = false;
if (inter.empty()) return false;
} }
else { else {
unsigned j = 0; m_new_intersection.reset();
for (literal lit : inter) for (literal lit : c)
if (c.contains(lit)) if (m_in_intersection[lit.index()])
inter[j++] = lit; m_new_intersection.push_back(lit);
inter.shrink(j); reset_intersection();
if (j == 0) return false; for (literal lit : m_new_intersection)
add_intersection(lit);
} }
if (m_intersection.empty())
return false;
} }
} }
return first; return first;
@ -1176,8 +1195,7 @@ namespace sat {
*/ */
bool add_cla(literal& blocked) { bool add_cla(literal& blocked) {
for (unsigned i = 0; i < m_covered_clause.size(); ++i) { for (unsigned i = 0; i < m_covered_clause.size(); ++i) {
m_intersection.reset(); if (resolution_intersection(m_covered_clause[i], false)) {
if (resolution_intersection(m_covered_clause[i], m_intersection, false)) {
blocked = m_covered_clause[i]; blocked = m_covered_clause[i];
return true; return true;
} }
@ -1404,8 +1422,7 @@ namespace sat {
Then the following binary clause is blocked: l \/ ~l' Then the following binary clause is blocked: l \/ ~l'
*/ */
void bca(literal l) { void bca(literal l) {
m_intersection.reset(); if (resolution_intersection(l, true)) {
if (resolution_intersection(l, m_intersection, true)) {
// this literal is pure. // this literal is pure.
return; return;
} }

2
src/sat/sat_simplifier_params.pyg
View file

@ -2,7 +2,7 @@ def_module_params(module_name='sat',
class_name='sat_simplifier_params', class_name='sat_simplifier_params',
export=True, export=True,
params=(('elim_blocked_clauses', BOOL, False, 'eliminate blocked clauses'), params=(('elim_blocked_clauses', BOOL, False, 'eliminate blocked clauses'),
('abce', BOOL, BOOL, False, 'eliminate blocked clauses using asymmmetric literals'), ('abce', BOOL, False, 'eliminate blocked clauses using asymmmetric literals'),
('cce', BOOL, False, 'eliminate covered clauses'), ('cce', BOOL, False, 'eliminate covered clauses'),
('acce', BOOL, False, 'eliminate covered clauses using asymmetric added literals'), ('acce', BOOL, False, 'eliminate covered clauses using asymmetric added literals'),
('elim_blocked_clauses_at', UINT, 2, 'eliminate blocked clauses only once at the given simplification round'), ('elim_blocked_clauses_at', UINT, 2, 'eliminate blocked clauses only once at the given simplification round'),

1
src/sat/sat_solver.cpp
View file

@ -859,6 +859,7 @@ namespace sat {
m_cuber = alloc(lookahead, *this); m_cuber = alloc(lookahead, *this);
} }
lbool result = m_cuber->cube(vars, lits, backtrack_level); lbool result = m_cuber->cube(vars, lits, backtrack_level);
m_cuber->update_cube_statistics(m_aux_stats);
if (result == l_false) { if (result == l_false) {
dealloc(m_cuber); dealloc(m_cuber);
m_cuber = nullptr; m_cuber = nullptr;