diff --git a/src/sat/ba_solver.cpp b/src/sat/ba_solver.cpp
index ab2352253..a8a09d3ff 100644
--- a/src/sat/ba_solver.cpp
+++ b/src/sat/ba_solver.cpp
@@ -2761,8 +2761,8 @@ namespace sat {
}
}
- unsigned ba_solver::get_num_non_learned_bin(literal l) {
- return s().m_simplifier.get_num_non_learned_bin(l);
+ unsigned ba_solver::get_num_unblocked_bin(literal l) {
+ return s().m_simplifier.get_num_unblocked_bin(l);
}
/*
@@ -2831,8 +2831,8 @@ namespace sat {
value(lit) == l_undef &&
use_count(lit) == 1 &&
use_count(~lit) == 1 &&
- get_num_non_learned_bin(lit) == 0 &&
- get_num_non_learned_bin(~lit) == 0) {
+ get_num_unblocked_bin(lit) == 0 &&
+ get_num_unblocked_bin(~lit) == 0) {
remove_constraint(c, "unused def");
}
break;
@@ -2876,7 +2876,7 @@ namespace sat {
bool ba_solver::elim_pure(literal lit) {
if (value(lit) == l_undef && !m_cnstr_use_list[lit.index()].empty() &&
- use_count(~lit) == 0 && get_num_non_learned_bin(~lit) == 0) {
+ use_count(~lit) == 0 && get_num_unblocked_bin(~lit) == 0) {
IF_VERBOSE(10, verbose_stream() << "pure literal: " << lit << "\n";);
s().assign(lit, justification());
return true;
@@ -3163,9 +3163,12 @@ namespace sat {
if (w.is_binary_clause() && is_marked(w.get_literal())) {
++m_stats.m_num_bin_subsumes;
// IF_VERBOSE(10, verbose_stream() << c1 << " subsumes (" << lit << " " << w.get_literal() << ")\n";);
- if (!w.is_binary_non_learned_clause()) {
+ if (w.is_learned()) {
c1.set_learned(false);
}
+ else if (w.is_blocked()) {
+ w.set_unblocked();
+ }
}
else {
if (it != it2) {
diff --git a/src/sat/ba_solver.h b/src/sat/ba_solver.h
index 09903f889..16c853423 100644
--- a/src/sat/ba_solver.h
+++ b/src/sat/ba_solver.h
@@ -262,7 +262,7 @@ namespace sat {
void mark_visited(literal l) { m_visited[l.index()] = true; }
void unmark_visited(literal l) { m_visited[l.index()] = false; }
bool is_marked(literal l) const { return m_visited[l.index()] != 0; }
- unsigned get_num_non_learned_bin(literal l);
+ unsigned get_num_unblocked_bin(literal l);
literal get_min_occurrence_literal(card const& c);
void init_use_lists();
void remove_unused_defs();
diff --git a/src/sat/sat_clause.cpp b/src/sat/sat_clause.cpp
index 15c97b509..206dfcf40 100644
--- a/src/sat/sat_clause.cpp
+++ b/src/sat/sat_clause.cpp
@@ -29,6 +29,7 @@ namespace sat {
m_capacity(sz),
m_removed(false),
m_learned(learned),
+ m_blocked(false),
m_used(false),
m_frozen(false),
m_reinit_stack(false),
diff --git a/src/sat/sat_clause.h b/src/sat/sat_clause.h
index 556385696..8fd7b52cf 100644
--- a/src/sat/sat_clause.h
+++ b/src/sat/sat_clause.h
@@ -46,6 +46,7 @@ namespace sat {
unsigned m_used:1;
unsigned m_frozen:1;
unsigned m_reinit_stack:1;
+ unsigned m_blocked;
unsigned m_inact_rounds:8;
unsigned m_glue:8;
unsigned m_psm:8; // transient field used during gc
@@ -86,6 +87,9 @@ namespace sat {
unsigned inact_rounds() const { return m_inact_rounds; }
bool frozen() const { return m_frozen; }
void freeze() { SASSERT(is_learned()); SASSERT(!frozen()); m_frozen = true; }
+ bool is_blocked() const { return m_blocked; }
+ void block() { SASSERT(!m_blocked); SASSERT(!is_learned()); m_blocked = true; }
+ void unblock() { SASSERT(m_blocked); SASSERT(!is_learned()); m_blocked = false; }
void unfreeze() { SASSERT(is_learned()); SASSERT(frozen()); m_frozen = false; }
static var_approx_set approx(unsigned num, literal const * lits);
void set_glue(unsigned glue) { m_glue = glue > 255 ? 255 : glue; }
diff --git a/src/sat/sat_clause_use_list.cpp b/src/sat/sat_clause_use_list.cpp
index 5ee5b4cda..363ef784e 100644
--- a/src/sat/sat_clause_use_list.cpp
+++ b/src/sat/sat_clause_use_list.cpp
@@ -22,17 +22,20 @@ Revision History:
namespace sat {
bool clause_use_list::check_invariant() const {
-#ifdef LAZY_USE_LIST
unsigned sz = 0;
- for (unsigned i = 0; i < m_clauses.size(); i++)
- if (!m_clauses[i]->was_removed())
+ for (clause* c : m_clauses)
+ if (!c->was_removed())
sz++;
SASSERT(sz == m_size);
-#endif
+ unsigned blocked = 0;
+ for (clause* c : m_clauses)
+ if (c->is_blocked())
+ blocked++;
+ SASSERT(blocked == m_num_blocked);
+
return true;
}
-#ifdef LAZY_USE_LIST
void clause_use_list::iterator::consume() {
while (true) {
if (m_i == m_size)
@@ -44,14 +47,11 @@ namespace sat {
m_i++;
}
}
-#endif
clause_use_list::iterator::~iterator() {
-#ifdef LAZY_USE_LIST
while (m_i < m_size)
next();
m_clauses.shrink(m_j);
-#endif
}
};
diff --git a/src/sat/sat_clause_use_list.h b/src/sat/sat_clause_use_list.h
index 121345f21..08b50086a 100644
--- a/src/sat/sat_clause_use_list.h
+++ b/src/sat/sat_clause_use_list.h
@@ -24,30 +24,30 @@ Revision History:
namespace sat {
-#define LAZY_USE_LIST
-
/**
\brief Clause use list with delayed deletion.
*/
class clause_use_list {
clause_vector m_clauses;
-#ifdef LAZY_USE_LIST
unsigned m_size;
-#endif
+ unsigned m_num_blocked;
public:
clause_use_list() {
STRACE("clause_use_list_bug", tout << "[cul_created] " << this << "\n";);
-#ifdef LAZY_USE_LIST
m_size = 0;
-#endif
+ m_num_blocked = 0;
}
unsigned size() const {
-#ifdef LAZY_USE_LIST
return m_size;
-#else
- return m_clauses.size();
-#endif
+ }
+
+ unsigned num_blocked() const {
+ return m_num_blocked;
+ }
+
+ unsigned non_blocked_size() const {
+ return m_size - m_num_blocked;
}
bool empty() const { return size() == 0; }
@@ -57,58 +57,59 @@ namespace sat {
SASSERT(!m_clauses.contains(&c));
SASSERT(!c.was_removed());
m_clauses.push_back(&c);
-#ifdef LAZY_USE_LIST
m_size++;
-#endif
+ if (c.is_blocked()) ++m_num_blocked;
}
void erase_not_removed(clause & c) {
STRACE("clause_use_list_bug", tout << "[cul_erase_not_removed] " << this << " " << &c << "\n";);
-#ifdef LAZY_USE_LIST
SASSERT(m_clauses.contains(&c));
SASSERT(!c.was_removed());
m_clauses.erase(&c);
m_size--;
-#else
- m_clauses.erase(&c);
-#endif
+ if (c.is_blocked()) --m_num_blocked;
}
void erase(clause & c) {
STRACE("clause_use_list_bug", tout << "[cul_erase] " << this << " " << &c << "\n";);
-#ifdef LAZY_USE_LIST
SASSERT(m_clauses.contains(&c));
SASSERT(c.was_removed());
m_size--;
-#else
- m_clauses.erase(&c);
-#endif
+ if (c.is_blocked()) --m_num_blocked;
+ }
+
+ void block(clause const& c) {
+ SASSERT(c.is_blocked());
+ ++m_num_blocked;
+ SASSERT(check_invariant());
+ }
+
+ void unblock(clause const& c) {
+ SASSERT(!c.is_blocked());
+ --m_num_blocked;
+ SASSERT(check_invariant());
}
void reset() {
m_clauses.finalize();
-#ifdef LAZY_USE_LIST
m_size = 0;
-#endif
+ m_num_blocked = 0;
}
bool check_invariant() const;
// iterate & compress
- class iterator {
+ class iterator {
clause_vector & m_clauses;
unsigned m_size;
unsigned m_i;
-#ifdef LAZY_USE_LIST
unsigned m_j;
void consume();
-#endif
+
public:
iterator(clause_vector & v):m_clauses(v), m_size(v.size()), m_i(0) {
-#ifdef LAZY_USE_LIST
m_j = 0;
consume();
-#endif
}
~iterator();
bool at_end() const { return m_i == m_size; }
@@ -117,10 +118,8 @@ namespace sat {
SASSERT(!at_end());
SASSERT(!m_clauses[m_i]->was_removed());
m_i++;
-#ifdef LAZY_USE_LIST
m_j++;
consume();
-#endif
}
};
diff --git a/src/sat/sat_elim_vars.cpp b/src/sat/sat_elim_vars.cpp
index 86954d037..59210a266 100644
--- a/src/sat/sat_elim_vars.cpp
+++ b/src/sat/sat_elim_vars.cpp
@@ -37,13 +37,13 @@ namespace sat{
literal pos_l(v, false);
literal neg_l(v, true);
- unsigned num_bin_pos = simp.get_num_non_learned_bin(pos_l);
+ unsigned num_bin_pos = simp.get_num_unblocked_bin(pos_l);
if (num_bin_pos > m_max_literals) return false;
- unsigned num_bin_neg = simp.get_num_non_learned_bin(neg_l);
+ unsigned num_bin_neg = simp.get_num_unblocked_bin(neg_l);
if (num_bin_neg > m_max_literals) return false;
clause_use_list & pos_occs = simp.m_use_list.get(pos_l);
clause_use_list & neg_occs = simp.m_use_list.get(neg_l);
- unsigned clause_size = num_bin_pos + num_bin_neg + pos_occs.size() + neg_occs.size();
+ unsigned clause_size = num_bin_pos + num_bin_neg + pos_occs.non_blocked_size() + neg_occs.non_blocked_size();
if (clause_size == 0) {
return false;
}
@@ -85,8 +85,8 @@ namespace sat{
// eliminate variable
simp.m_pos_cls.reset();
simp.m_neg_cls.reset();
- simp.collect_clauses(pos_l, simp.m_pos_cls);
- simp.collect_clauses(neg_l, simp.m_neg_cls);
+ simp.collect_clauses(pos_l, simp.m_pos_cls, false);
+ simp.collect_clauses(neg_l, simp.m_neg_cls, false);
model_converter::entry & mc_entry = s.m_mc.mk(model_converter::ELIM_VAR, v);
simp.save_clauses(mc_entry, simp.m_pos_cls);
simp.save_clauses(mc_entry, simp.m_neg_cls);
@@ -122,13 +122,13 @@ namespace sat{
TRACE("elim_vars",
tout << "eliminate " << v << "\n";
for (watched const& w : simp.get_wlist(~pos_l)) {
- if (w.is_binary_non_learned_clause()) {
+ if (w.is_binary_unblocked_clause()) {
tout << pos_l << " " << w.get_literal() << "\n";
}
}
m.display(tout, b1);
for (watched const& w : simp.get_wlist(~neg_l)) {
- if (w.is_binary_non_learned_clause()) {
+ if (w.is_binary_unblocked_clause()) {
tout << neg_l << " " << w.get_literal() << "\n";
}
}
@@ -294,7 +294,7 @@ namespace sat{
bool elim_vars::mark_literals(literal lit) {
watch_list& wl = simp.get_wlist(lit);
for (watched const& w : wl) {
- if (w.is_binary_non_learned_clause()) {
+ if (w.is_binary_unblocked_clause()) {
mark_var(w.get_literal().var());
}
}
@@ -306,6 +306,7 @@ namespace sat{
clause_use_list::iterator it = occs.mk_iterator();
while (!it.at_end()) {
clause const& c = it.curr();
+ if (c.is_blocked()) continue;
bdd cl = m.mk_false();
for (literal l : c) {
cl |= mk_literal(l);
@@ -320,7 +321,7 @@ namespace sat{
bdd result = m.mk_true();
watch_list& wl = simp.get_wlist(~lit);
for (watched const& w : wl) {
- if (w.is_binary_non_learned_clause()) {
+ if (w.is_binary_unblocked_clause()) {
result &= (mk_literal(lit) || mk_literal(w.get_literal()));
}
}
diff --git a/src/sat/sat_local_search.cpp b/src/sat/sat_local_search.cpp
index 5cc19a174..3a9e48182 100644
--- a/src/sat/sat_local_search.cpp
+++ b/src/sat/sat_local_search.cpp
@@ -304,7 +304,7 @@ namespace sat {
watch_list::const_iterator it = wlist.begin();
watch_list::const_iterator end = wlist.end();
for (; it != end; ++it) {
- if (!it->is_binary_non_learned_clause())
+ if (!it->is_binary_unblocked_clause())
continue;
literal l2 = it->get_literal();
if (l1.index() > l2.index())
diff --git a/src/sat/sat_lookahead.cpp b/src/sat/sat_lookahead.cpp
index 4bb7ba180..ff2bac39f 100644
--- a/src/sat/sat_lookahead.cpp
+++ b/src/sat/sat_lookahead.cpp
@@ -965,7 +965,7 @@ namespace sat {
if (m_s.was_eliminated(l.var())) continue;
watch_list const & wlist = m_s.m_watches[l_idx];
for (auto& w : wlist) {
- if (!w.is_binary_non_learned_clause())
+ if (!w.is_binary_clause())
continue;
literal l2 = w.get_literal();
if (l.index() < l2.index() && !m_s.was_eliminated(l2.var()))
diff --git a/src/sat/sat_simplifier.cpp b/src/sat/sat_simplifier.cpp
index cd46f1916..b0ef9e3e9 100644
--- a/src/sat/sat_simplifier.cpp
+++ b/src/sat/sat_simplifier.cpp
@@ -34,26 +34,29 @@ namespace sat {
}
void use_list::insert(clause & c) {
- unsigned sz = c.size();
- for (unsigned i = 0; i < sz; i++) {
- m_use_list[c[i].index()].insert(c);
- }
+ for (literal l : c)
+ m_use_list[l.index()].insert(c);
}
void use_list::erase(clause & c) {
- unsigned sz = c.size();
- for (unsigned i = 0; i < sz; i++) {
- m_use_list[c[i].index()].erase(c);
- }
+ for (literal l : c)
+ m_use_list[l.index()].erase(c);
}
void use_list::erase(clause & c, literal l) {
- unsigned sz = c.size();
- for (unsigned i = 0; i < sz; i++) {
- literal l2 = c[i];
+ for (literal l2 : c)
if (l2 != l)
m_use_list[l2.index()].erase(c);
- }
+ }
+
+ void use_list::block(clause& c) {
+ for (literal l : c)
+ m_use_list[l.index()].block(c);
+ }
+
+ void use_list::unblock(clause& c) {
+ for (literal l : c)
+ m_use_list[l.index()].unblock(c);
}
simplifier::simplifier(solver & _s, params_ref const & p):
@@ -99,9 +102,8 @@ namespace sat {
}
inline void simplifier::remove_clause_core(clause & c) {
- unsigned sz = c.size();
- for (unsigned i = 0; i < sz; i++)
- insert_elim_todo(c[i].var());
+ for (literal l : c)
+ insert_elim_todo(l.var());
m_sub_todo.erase(c);
c.set_removed(true);
TRACE("resolution_bug", tout << "del_clause: " << c << "\n";);
@@ -118,6 +120,20 @@ namespace sat {
m_use_list.erase(c, l);
}
+ inline void simplifier::block_clause(clause & c) {
+#if 1
+ remove_clause(c);
+#else
+ c.block();
+ m_use_list.block(c);
+#endif
+ }
+
+ inline void simplifier::unblock_clause(clause & c) {
+ c.unblock();
+ m_use_list.unblock(c);
+ }
+
inline void simplifier::remove_bin_clause_half(literal l1, literal l2, bool learned) {
SASSERT(s.get_wlist(~l1).contains(watched(l2, learned)));
s.get_wlist(~l1).erase(watched(l2, learned));
@@ -238,10 +254,7 @@ namespace sat {
\brief Eliminate all ternary and clause watches.
*/
void simplifier::cleanup_watches() {
- vector<watch_list>::iterator it = s.m_watches.begin();
- vector<watch_list>::iterator end = s.m_watches.end();
- for (; it != end; ++it) {
- watch_list & wlist = *it;
+ for (watch_list& wlist : s.m_watches) {
watch_list::iterator it2 = wlist.begin();
watch_list::iterator itprev = it2;
watch_list::iterator end2 = wlist.end();
@@ -345,11 +358,9 @@ namespace sat {
\brief Return the variable in c with the minimal number positive+negative occurrences.
*/
bool_var simplifier::get_min_occ_var(clause const & c) const {
- literal l_best = c[0];
- unsigned best = m_use_list.get(l_best).size() + m_use_list.get(~l_best).size();
- unsigned sz = c.size();
- for (unsigned i = 1; i < sz; i++) {
- literal l = c[i];
+ literal l_best = null_literal;
+ unsigned best = UINT_MAX;
+ for (literal l : c) {
unsigned num = m_use_list.get(l).size() + m_use_list.get(~l).size();
if (num < best) {
l_best = l;
@@ -394,6 +405,7 @@ namespace sat {
*/
void simplifier::collect_subsumed1_core(clause const & c1, clause_vector & out, literal_vector & out_lits,
literal target) {
+ if (c1.is_blocked()) return;
clause_use_list const & cs = m_use_list.get(target);
clause_use_list::iterator it = cs.mk_iterator();
while (!it.at_end()) {
@@ -424,7 +436,7 @@ namespace sat {
}
/**
- \brief Perform backward subsumption and self-subsumption resolution using c.
+ \brief Perform backward subsumption and self-subsumption resolution using c1.
*/
void simplifier::back_subsumption1(clause & c1) {
m_bs_cs.reset();
@@ -440,11 +452,13 @@ namespace sat {
// c2 was subsumed
if (c1.is_learned() && !c2.is_learned())
c1.unset_learned();
+ else if (c1.is_blocked() && !c2.is_learned() && !c2.is_blocked())
+ unblock_clause(c1);
TRACE("subsumption", tout << c1 << " subsumed " << c2 << "\n";);
remove_clause(c2);
m_num_subsumed++;
}
- else if (!c2.was_removed()) {
+ else if (!c2.was_removed() && !c1.is_blocked()) {
// subsumption resolution
TRACE("subsumption_resolution", tout << c1 << " sub-ref(" << *l_it << ") " << c2 << "\n";);
elim_lit(c2, *l_it);
@@ -466,11 +480,9 @@ namespace sat {
\brief Return the literal in c with the minimal number of occurrences.
*/
literal simplifier::get_min_occ_var0(clause const & c) const {
- literal l_best = c[0];
- unsigned best = m_use_list.get(l_best).size();
- unsigned sz = c.size();
- for (unsigned i = 1; i < sz; i++) {
- literal l = c[i];
+ literal l_best = null_literal;
+ unsigned best = UINT_MAX;
+ for (literal l : c) {
unsigned num = m_use_list.get(l).size();
if (num < best) {
l_best = l;
@@ -485,21 +497,19 @@ namespace sat {
Otherwise return false
*/
bool simplifier::subsumes0(clause const & c1, clause const & c2) {
- unsigned sz2 = c2.size();
- for (unsigned i = 0; i < sz2; i++)
- mark_visited(c2[i]);
+ for (literal l : c2)
+ mark_visited(l);
bool r = true;
- unsigned sz1 = c1.size();
- for (unsigned i = 0; i < sz1; i++) {
- if (!is_marked(c1[i])) {
+ for (literal l : c1) {
+ if (!is_marked(l)) {
r = false;
break;
}
}
- for (unsigned i = 0; i < sz2; i++)
- unmark_visited(c2[i]);
+ for (literal l : c2)
+ unmark_visited(l);
return r;
}
@@ -508,6 +518,7 @@ namespace sat {
\brief Collect the clauses subsumed by c1 (using the occurrence list of target).
*/
void simplifier::collect_subsumed0_core(clause const & c1, clause_vector & out, literal target) {
+ if (c1.is_blocked()) return;
clause_use_list const & cs = m_use_list.get(target);
clause_use_list::iterator it = cs.mk_iterator();
while (!it.at_end()) {
@@ -540,10 +551,8 @@ namespace sat {
void simplifier::back_subsumption0(clause & c1) {
m_bs_cs.reset();
collect_subsumed0(c1, m_bs_cs);
- clause_vector::iterator it = m_bs_cs.begin();
- clause_vector::iterator end = m_bs_cs.end();
- for (; it != end; ++it) {
- clause & c2 = *(*it);
+ for (clause* cp : m_bs_cs) {
+ clause & c2 = *cp;
// c2 was subsumed
if (c1.is_learned() && !c2.is_learned())
c1.unset_learned();
@@ -951,13 +960,17 @@ namespace sat {
return !s.s.is_assumption(v) && !s.was_eliminated(v) && !s.is_external(v);
}
- void operator()(unsigned num_vars) {
+ void insert_queue(unsigned num_vars) {
for (bool_var v = 0; v < num_vars; v++) {
if (process_var(v)) {
insert(literal(v, false));
insert(literal(v, true));
}
}
+ }
+
+ void block_clauses(unsigned num_vars) {
+ insert_queue(num_vars);
while (!m_queue.empty()) {
s.checkpoint();
if (m_counter < 0)
@@ -965,7 +978,73 @@ namespace sat {
literal l = m_queue.next();
process(l);
}
- cce();
+ }
+
+ void operator()(unsigned num_vars) {
+ block_clauses(num_vars);
+ if (s.m_elim_covered_clauses)
+ cce();
+ }
+
+ void process(literal l) {
+ TRACE("blocked_clause", tout << "processing: " << l << "\n";);
+ model_converter::entry * new_entry = 0;
+ if (!process_var(l.var())) {
+ return;
+ }
+
+ literal blocked = null_literal;
+ m_to_remove.reset();
+ {
+ clause_use_list & occs = s.m_use_list.get(l);
+ clause_use_list::iterator it = occs.mk_iterator();
+ while (!it.at_end()) {
+ clause & c = it.curr();
+ if (c.is_blocked()) continue;
+ m_counter -= c.size();
+ SASSERT(c.contains(l));
+ s.mark_all_but(c, l);
+ if (all_tautology(l)) {
+ block_clause(c, l, new_entry);
+ s.m_num_blocked_clauses++;
+ }
+ s.unmark_all(c);
+ it.next();
+ }
+ }
+ for (clause* c : m_to_remove)
+ s.block_clause(*c);
+
+ {
+ watch_list & wlist = s.get_wlist(~l);
+ m_counter -= wlist.size();
+ watch_list::iterator it = wlist.begin();
+ watch_list::iterator it2 = it;
+ watch_list::iterator end = wlist.end();
+ for (; it != end; ++it) {
+ if (!it->is_binary_clause() || it->is_blocked()) {
+ *it2 = *it;
+ it2++;
+ continue;
+ }
+ literal l2 = it->get_literal();
+ s.mark_visited(l2);
+ if (all_tautology(l)) {
+ block_binary(it, l, new_entry);
+ s.m_num_blocked_clauses++;
+ }
+ else if (s.m_elim_covered_clauses && cce(l, l2, blocked)) {
+ block_covered_binary(it, l, blocked);
+ s.m_num_covered_clauses++;
+ }
+ else {
+ *it2 = *it;
+ it2++;
+ }
+ s.unmark_visited(l2);
+ }
+ wlist.set_end(it2);
+ }
}
//
@@ -976,7 +1055,7 @@ namespace sat {
if (!process_var(l.var())) return false;
bool first = true;
for (watched & w : s.get_wlist(l)) {
- if (w.is_binary_non_learned_clause()) {
+ if (w.is_binary_unblocked_clause()) {
literal lit = w.get_literal();
if (s.is_marked(~lit) && lit != ~l) continue;
if (!first) {
@@ -992,6 +1071,7 @@ namespace sat {
while (!it.at_end()) {
bool tautology = false;
clause & c = it.curr();
+ if (c.is_blocked()) continue;
for (literal lit : c) {
if (s.is_marked(~lit) && lit != ~l) {
tautology = true;
@@ -1007,16 +1087,9 @@ namespace sat {
}
else {
unsigned j = 0;
- unsigned sz = inter.size();
- for (unsigned i = 0; i < sz; ++i) {
- literal lit1 = inter[i];
- for (literal lit2 : c) {
- if (lit1 == lit2) {
- inter[j++] = lit1;
- break;
- }
- }
- }
+ for (literal lit : inter)
+ if (c.contains(lit))
+ inter[j++] = lit;
inter.shrink(j);
if (j == 0) return false;
}
@@ -1052,6 +1125,14 @@ namespace sat {
}
}
+
+ /*
+ * C \/ l ~l \/ lit \/ D_i for i = 1...N all the clauses that have ~l
+ * -------------------------
+ * C \/ l \/ lit
+ *
+ *
+ */
bool add_cla(literal& blocked) {
for (unsigned i = 0; i < m_covered_clause.size(); ++i) {
m_intersection.reset();
@@ -1059,15 +1140,15 @@ namespace sat {
blocked = m_covered_clause[i];
return true;
}
+ if (!m_intersection.empty()) {
+ m_elim_stack.push_back(std::make_pair(m_covered_clause.size(), m_covered_clause[i]));
+ }
for (literal l : m_intersection) {
if (!s.is_marked(l)) {
s.mark_visited(l);
m_covered_clause.push_back(l);
}
}
- if (!m_intersection.empty()) {
- m_elim_stack.push_back(std::make_pair(m_covered_clause.size(), m_covered_clause[i]));
- }
}
return false;
}
@@ -1085,14 +1166,18 @@ namespace sat {
is_tautology = add_cla(blocked);
}
while (m_covered_clause.size() > sz && !is_tautology);
+#if 1
break;
- //if (is_tautology) break;
- //sz = m_covered_clause.size();
- // unsound? add_ala();
+#else
+ // check for soundness?
+ if (is_tautology) break;
+ sz = m_covered_clause.size();
+ add_ala();
+#endif
}
while (m_covered_clause.size() > sz);
for (literal l : m_covered_clause) s.unmark_visited(l);
- // if (is_tautology) std::cout << "taut: " << num_iterations << " " << m_covered_clause.size() << " " << m_elim_stack.size() << "\n";
+ if (is_tautology) std::cout << "taut: " << num_iterations << " " << m_covered_clause.size() << " " << m_elim_stack.size() << "\n";
return is_tautology;
}
@@ -1105,9 +1190,9 @@ namespace sat {
return cla(blocked);
}
- bool cce(literal lit, literal l2, literal& blocked) {
+ bool cce(literal l1, literal l2, literal& blocked) {
m_covered_clause.reset();
- m_covered_clause.push_back(lit);
+ m_covered_clause.push_back(l1);
m_covered_clause.push_back(l2);
return cla(blocked);
}
@@ -1117,79 +1202,17 @@ namespace sat {
literal blocked;
for (clause* cp : s.s.m_clauses) {
clause& c = *cp;
- if (c.was_removed()) continue;
- if (cce(c, blocked)) {
- model_converter::entry * new_entry = 0;
- block_covered_clause(c, blocked, new_entry);
+ if (!c.was_removed() && !c.is_blocked() && cce(c, blocked)) {
+ block_covered_clause(c, blocked);
s.m_num_covered_clauses++;
}
}
for (clause* c : m_to_remove) {
- s.remove_clause(*c);
+ s.block_clause(*c);
}
m_to_remove.reset();
}
- void process(literal l) {
- TRACE("blocked_clause", tout << "processing: " << l << "\n";);
- model_converter::entry * new_entry = 0;
- if (!process_var(l.var())) {
- return;
- }
-
- literal blocked = null_literal;
- m_to_remove.reset();
- {
- clause_use_list & occs = s.m_use_list.get(l);
- clause_use_list::iterator it = occs.mk_iterator();
- while (!it.at_end()) {
- clause & c = it.curr();
- m_counter -= c.size();
- SASSERT(c.contains(l));
- s.mark_all_but(c, l);
- if (all_tautology(l)) {
- block_clause(c, l, new_entry);
- s.m_num_blocked_clauses++;
- }
- s.unmark_all(c);
- it.next();
- }
- }
- for (clause* c : m_to_remove) {
- s.remove_clause(*c);
- }
- {
- watch_list & wlist = s.get_wlist(~l);
- m_counter -= wlist.size();
- watch_list::iterator it = wlist.begin();
- watch_list::iterator it2 = it;
- watch_list::iterator end = wlist.end();
- for (; it != end; ++it) {
- if (!it->is_binary_clause()) {
- *it2 = *it;
- it2++;
- continue;
- }
- literal l2 = it->get_literal();
- s.mark_visited(l2);
- if (all_tautology(l)) {
- block_binary(it, l, new_entry);
- s.m_num_blocked_clauses++;
- }
- else if (cce(l, l2, blocked)) {
- model_converter::entry * blocked_entry = 0;
- block_covered_binary(it, l, blocked, blocked_entry);
- s.m_num_covered_clauses++;
- }
- else {
- *it2 = *it;
- it2++;
- }
- s.unmark_visited(l2);
- }
- wlist.set_end(it2);
- }
- }
void prepare_block_clause(clause& c, literal l, model_converter::entry*& new_entry) {
TRACE("blocked_clause", tout << "new blocked clause: " << c << "\n";);
@@ -1208,7 +1231,8 @@ namespace sat {
mc.insert(*new_entry, c);
}
- void block_covered_clause(clause& c, literal l, model_converter::entry *& new_entry) {
+ void block_covered_clause(clause& c, literal l) {
+ model_converter::entry * new_entry = 0;
prepare_block_clause(c, l, new_entry);
mc.insert(*new_entry, m_covered_clause, m_elim_stack);
}
@@ -1227,7 +1251,8 @@ namespace sat {
mc.insert(*new_entry, l, it->get_literal());
}
- void block_covered_binary(watch_list::iterator it, literal l, literal blocked, model_converter::entry *& new_entry) {
+ void block_covered_binary(watch_list::iterator it, literal l, literal blocked) {
+ model_converter::entry * new_entry = 0;
prepare_block_binary(it, l, blocked, new_entry);
mc.insert(*new_entry, m_covered_clause, m_elim_stack);
}
@@ -1236,7 +1261,7 @@ namespace sat {
watch_list & wlist = s.get_wlist(l);
m_counter -= wlist.size();
for (auto const& w : wlist) {
- if (w.is_binary_non_learned_clause() &&
+ if (w.is_binary_unblocked_clause() &&
!s.is_marked(~w.get_literal()))
return false;
}
@@ -1245,6 +1270,7 @@ namespace sat {
clause_use_list::iterator it = neg_occs.mk_iterator();
while (!it.at_end()) {
clause & c = it.curr();
+ if (c.is_blocked()) continue;
m_counter -= c.size();
unsigned sz = c.size();
unsigned i;
@@ -1300,11 +1326,11 @@ namespace sat {
elim(s.num_vars());
}
- unsigned simplifier::get_num_non_learned_bin(literal l) const {
+ unsigned simplifier::get_num_unblocked_bin(literal l) const {
unsigned r = 0;
watch_list const & wlist = get_wlist(~l);
for (auto & w : wlist) {
- if (w.is_binary_non_learned_clause())
+ if (w.is_binary_unblocked_clause())
r++;
}
return r;
@@ -1315,8 +1341,8 @@ namespace sat {
literal neg_l(v, true);
unsigned num_pos = m_use_list.get(pos_l).size();
unsigned num_neg = m_use_list.get(neg_l).size();
- unsigned num_bin_pos = get_num_non_learned_bin(pos_l);
- unsigned num_bin_neg = get_num_non_learned_bin(neg_l);
+ unsigned num_bin_pos = get_num_unblocked_bin(pos_l);
+ unsigned num_bin_neg = get_num_unblocked_bin(neg_l);
unsigned cost = 2 * num_pos * num_neg + num_pos * num_bin_neg + num_neg * num_bin_pos;
CTRACE("elim_vars_detail", cost == 0, tout << v << " num_pos: " << num_pos << " num_neg: " << num_neg << " num_bin_pos: " << num_bin_pos
<< " num_bin_neg: " << num_bin_neg << " cost: " << cost << "\n";);
@@ -1353,20 +1379,32 @@ namespace sat {
/**
\brief Collect clauses and binary clauses containing l.
*/
- void simplifier::collect_clauses(literal l, clause_wrapper_vector & r) {
+ void simplifier::collect_clauses(literal l, clause_wrapper_vector & r, bool include_blocked) {
clause_use_list const & cs = m_use_list.get(l);
clause_use_list::iterator it = cs.mk_iterator();
while (!it.at_end()) {
- r.push_back(clause_wrapper(it.curr()));
- SASSERT(r.back().size() == it.curr().size());
+ if (!it.curr().is_blocked() || include_blocked) {
+ r.push_back(clause_wrapper(it.curr()));
+ SASSERT(r.back().size() == it.curr().size());
+ }
it.next();
}
watch_list & wlist = get_wlist(~l);
- for (auto & w : wlist) {
- if (w.is_binary_non_learned_clause()) {
- r.push_back(clause_wrapper(l, w.get_literal()));
- SASSERT(r.back().size() == 2);
+ if (include_blocked) {
+ for (auto & w : wlist) {
+ if (w.is_binary_non_learned_clause2()) {
+ r.push_back(clause_wrapper(l, w.get_literal()));
+ SASSERT(r.back().size() == 2);
+ }
+ }
+ }
+ else {
+ for (auto & w : wlist) {
+ if (w.is_binary_unblocked_clause()) {
+ r.push_back(clause_wrapper(l, w.get_literal()));
+ SASSERT(r.back().size() == 2);
+ }
}
}
}
@@ -1503,12 +1541,12 @@ namespace sat {
literal pos_l(v, false);
literal neg_l(v, true);
- unsigned num_bin_pos = get_num_non_learned_bin(pos_l);
- unsigned num_bin_neg = get_num_non_learned_bin(neg_l);
+ unsigned num_bin_pos = get_num_unblocked_bin(pos_l);
+ unsigned num_bin_neg = get_num_unblocked_bin(neg_l);
clause_use_list & pos_occs = m_use_list.get(pos_l);
clause_use_list & neg_occs = m_use_list.get(neg_l);
- unsigned num_pos = pos_occs.size() + num_bin_pos;
- unsigned num_neg = neg_occs.size() + num_bin_neg;
+ unsigned num_pos = pos_occs.non_blocked_size() + num_bin_pos;
+ unsigned num_neg = neg_occs.non_blocked_size() + num_bin_neg;
TRACE("resolution", tout << v << " num_pos: " << num_pos << " neg_pos: " << num_neg << "\n";);
@@ -1520,7 +1558,8 @@ namespace sat {
{
clause_use_list::iterator it = pos_occs.mk_iterator();
while (!it.at_end()) {
- before_lits += it.curr().size();
+ if (!it.curr().is_blocked())
+ before_lits += it.curr().size();
it.next();
}
}
@@ -1528,7 +1567,8 @@ namespace sat {
{
clause_use_list::iterator it2 = neg_occs.mk_iterator();
while (!it2.at_end()) {
- before_lits += it2.curr().size();
+ if (!it2.curr().is_blocked())
+ before_lits += it2.curr().size();
it2.next();
}
}
@@ -1546,8 +1586,8 @@ namespace sat {
m_pos_cls.reset();
m_neg_cls.reset();
- collect_clauses(pos_l, m_pos_cls);
- collect_clauses(neg_l, m_neg_cls);
+ collect_clauses(pos_l, m_pos_cls, false);
+ collect_clauses(neg_l, m_neg_cls, false);
TRACE("resolution_detail", tout << "collecting number of after_clauses\n";);
@@ -1676,6 +1716,7 @@ namespace sat {
void simplifier::updt_params(params_ref const & _p) {
sat_simplifier_params p(_p);
+ m_elim_covered_clauses = p.elim_covered_clauses();
m_elim_blocked_clauses = p.elim_blocked_clauses();
m_elim_blocked_clauses_at = p.elim_blocked_clauses_at();
m_blocked_clause_limit = p.blocked_clause_limit();
@@ -1693,6 +1734,7 @@ namespace sat {
m_subsumption = p.subsumption();
m_subsumption_limit = p.subsumption_limit();
m_elim_vars = p.elim_vars();
+ m_elim_vars_bdd = p.elim_vars_bdd();
}
void simplifier::collect_param_descrs(param_descrs & r) {
diff --git a/src/sat/sat_simplifier.h b/src/sat/sat_simplifier.h
index fdfabb513..d58babfef 100644
--- a/src/sat/sat_simplifier.h
+++ b/src/sat/sat_simplifier.h
@@ -40,6 +40,8 @@ namespace sat {
public:
void init(unsigned num_vars);
void insert(clause & c);
+ void block(clause & c);
+ void unblock(clause & c);
void erase(clause & c);
void erase(clause & c, literal l);
clause_use_list & get(literal l) { return m_use_list[l.index()]; }
@@ -69,6 +71,7 @@ namespace sat {
int m_elim_counter;
// config
+ bool m_elim_covered_clauses;
bool m_elim_blocked_clauses;
unsigned m_elim_blocked_clauses_at;
unsigned m_blocked_clause_limit;
@@ -87,6 +90,7 @@ namespace sat {
bool m_subsumption;
unsigned m_subsumption_limit;
bool m_elim_vars;
+ bool m_elim_vars_bdd;
// stats
unsigned m_num_blocked_clauses;
@@ -119,6 +123,8 @@ namespace sat {
void remove_clause_core(clause & c);
void remove_clause(clause & c);
void remove_clause(clause & c, literal l);
+ void block_clause(clause & c);
+ void unblock_clause(clause & c);
void remove_bin_clause_half(literal l1, literal l2, bool learned);
bool_var get_min_occ_var(clause const & c) const;
@@ -157,10 +163,10 @@ namespace sat {
struct blocked_clause_elim;
void elim_blocked_clauses();
- unsigned get_num_non_learned_bin(literal l) const;
+ unsigned get_num_unblocked_bin(literal l) const;
unsigned get_to_elim_cost(bool_var v) const;
void order_vars_for_elim(bool_var_vector & r);
- void collect_clauses(literal l, clause_wrapper_vector & r);
+ void collect_clauses(literal l, clause_wrapper_vector & r, bool include_blocked);
clause_wrapper_vector m_pos_cls;
clause_wrapper_vector m_neg_cls;
literal_vector m_new_cls;
diff --git a/src/sat/sat_simplifier_params.pyg b/src/sat/sat_simplifier_params.pyg
index ff2944987..9a7812586 100644
--- a/src/sat/sat_simplifier_params.pyg
+++ b/src/sat/sat_simplifier_params.pyg
@@ -2,6 +2,7 @@ def_module_params(module_name='sat',
class_name='sat_simplifier_params',
export=True,
params=(('elim_blocked_clauses', BOOL, False, 'eliminate blocked clauses'),
+ ('elim_covered_clauses', BOOL, False, 'eliminate covered clauses'),
('elim_blocked_clauses_at', UINT, 2, 'eliminate blocked clauses only once at the given simplification round'),
('blocked_clause_limit', UINT, 100000000, 'maximum number of literals visited during blocked clause elimination'),
('resolution', BOOL, True, 'eliminate boolean variables using resolution'),
@@ -16,5 +17,6 @@ def_module_params(module_name='sat',
('resolution.cls_cutoff1', UINT, 100000000, 'limit1 - total number of problems clauses for the second cutoff of Boolean variable elimination'),
('resolution.cls_cutoff2', UINT, 700000000, 'limit2 - total number of problems clauses for the second cutoff of Boolean variable elimination'),
('elim_vars', BOOL, True, 'enable variable elimination during simplification'),
+ ('elim_vars_bdd', BOOL, True, 'enable variable elimination using BDD recompilation during simplification'),
('subsumption', BOOL, True, 'eliminate subsumed clauses'),
('subsumption.limit', UINT, 100000000, 'approx. maximum number of literals visited during subsumption (and subsumption resolution)')))
diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp
index ca1fc7801..1b117b0a7 100644
--- a/src/sat/sat_solver.cpp
+++ b/src/sat/sat_solver.cpp
@@ -117,7 +117,7 @@ namespace sat {
assign(src.m_trail[i], justification());
}
- // copy binary clauses
+ // copy binary clauses that are unblocked.
{
unsigned sz = src.m_watches.size();
for (unsigned l_idx = 0; l_idx < sz; ++l_idx) {
@@ -125,7 +125,7 @@ namespace sat {
if (src.was_eliminated(l.var())) continue;
watch_list const & wlist = src.m_watches[l_idx];
for (auto & wi : wlist) {
- if (!wi.is_binary_non_learned_clause())
+ if (!wi.is_binary_unblocked_clause())
continue;
literal l2 = wi.get_literal();
if (l.index() > l2.index() ||
@@ -142,7 +142,10 @@ namespace sat {
for (clause* c : src.m_clauses) {
buffer.reset();
for (literal l : *c) buffer.push_back(l);
- mk_clause_core(buffer);
+ clause* c1 = mk_clause_core(buffer);
+ if (c1 && c->is_blocked()) {
+ c1->block();
+ }
}
// copy high quality lemmas
for (clause* c : src.m_learned) {
@@ -1558,8 +1561,8 @@ namespace sat {
m_mc(m_model);
TRACE("sat", for (bool_var v = 0; v < num; v++) tout << v << ": " << m_model[v] << "\n";);
-#ifndef _EXTERNAL_RELEASE
- IF_VERBOSE(SAT_VB_LVL, verbose_stream() << "\"checking model\"\n";);
+// #ifndef _EXTERNAL_RELEASE
+ IF_VERBOSE(1, verbose_stream() << "\"checking model\"\n";);
if (!check_model(m_model))
throw solver_exception("check model failed");
@@ -1568,7 +1571,7 @@ namespace sat {
if (!m_clone->check_model(m_model))
throw solver_exception("check model failed (for cloned solver)");
}
-#endif
+// #endif
}
bool solver::check_model(model const & m) const {
@@ -3124,17 +3127,14 @@ namespace sat {
for (unsigned l_idx = 0; l_idx < sz; l_idx++) {
literal l = to_literal(l_idx);
l.neg();
- watch_list const & wlist = m_watches[l_idx];
- watch_list::const_iterator it = wlist.begin();
- watch_list::const_iterator end = wlist.end();
- for (; it != end; ++it) {
- if (!it->is_binary_clause())
+ for (watched const& w : m_watches[l_idx]) {
+ if (!w.is_binary_clause())
continue;
- if (!learned && it->is_learned())
+ if (!learned && w.is_learned())
continue;
- else if (learned && learned_only && !it->is_learned())
+ else if (learned && learned_only && !w.is_learned())
continue;
- literal l2 = it->get_literal();
+ literal l2 = w.get_literal();
if (l.index() > l2.index())
continue;
TRACE("cleanup_bug", tout << "collected: " << l << " " << l2 << "\n";);
@@ -3168,13 +3168,10 @@ namespace sat {
for (unsigned l_idx = 0; l_idx < sz; l_idx++) {
literal l = to_literal(l_idx);
l.neg();
- watch_list const & wlist = m_watches[l_idx];
- watch_list::const_iterator it = wlist.begin();
- watch_list::const_iterator end = wlist.end();
- for (; it != end; ++it) {
- if (!it->is_binary_clause())
+ for (watched const& w : m_watches[l_idx]) {
+ if (!w.is_binary_clause())
continue;
- literal l2 = it->get_literal();
+ literal l2 = w.get_literal();
if (l.index() > l2.index())
continue;
out << "(" << l << " " << l2 << ")\n";
diff --git a/src/sat/sat_solver.h b/src/sat/sat_solver.h
index 58d2824c7..2c5a04104 100644
--- a/src/sat/sat_solver.h
+++ b/src/sat/sat_solver.h
@@ -220,8 +220,8 @@ namespace sat {
protected:
void del_clause(clause & c);
clause * mk_clause_core(unsigned num_lits, literal * lits, bool learned);
- void mk_clause_core(literal_vector const& lits) { mk_clause_core(lits.size(), lits.c_ptr()); }
- void mk_clause_core(unsigned num_lits, literal * lits) { mk_clause_core(num_lits, lits, false); }
+ clause * mk_clause_core(literal_vector const& lits) { return mk_clause_core(lits.size(), lits.c_ptr()); }
+ clause * mk_clause_core(unsigned num_lits, literal * lits) { return mk_clause_core(num_lits, lits, false); }
void mk_clause_core(literal l1, literal l2) { literal lits[2] = { l1, l2 }; mk_clause_core(2, lits); }
void mk_bin_clause(literal l1, literal l2, bool learned);
bool propagate_bin_clause(literal l1, literal l2);
diff --git a/src/sat/sat_watched.h b/src/sat/sat_watched.h
index d1333c314..f18e08999 100644
--- a/src/sat/sat_watched.h
+++ b/src/sat/sat_watched.h
@@ -50,7 +50,7 @@ namespace sat {
SASSERT(is_binary_clause());
SASSERT(get_literal() == l);
SASSERT(is_learned() == learned);
- SASSERT(learned || is_binary_non_learned_clause());
+ SASSERT(learned || is_binary_unblocked_clause());
}
watched(literal l1, literal l2) {
@@ -85,8 +85,15 @@ namespace sat {
literal get_literal() const { SASSERT(is_binary_clause()); return to_literal(static_cast<unsigned>(m_val1)); }
void set_literal(literal l) { SASSERT(is_binary_clause()); m_val1 = l.to_uint(); }
bool is_learned() const { SASSERT(is_binary_clause()); return (m_val2 >> 2) == 1; }
- bool is_binary_non_learned_clause() const { return m_val2 == 0; }
+
+ bool is_binary_unblocked_clause() const { return m_val2 == 0; }
+ bool is_binary_learned_clause() const { return is_binary_clause() && is_learned(); }
+ bool is_binary_non_learned_clause2() const { return is_binary_clause() && !is_learned(); }
+
void mark_not_learned() { SASSERT(is_learned()); m_val2 = static_cast<unsigned>(BINARY); SASSERT(!is_learned()); }
+ void set_blocked() { SASSERT(is_binary_clause()); SASSERT(!is_learned()); m_val2 |= (1 << 3); }
+ bool is_blocked() const { SASSERT(is_binary_clause()); return 0 != (m_val2 & (1 << 3)); }
+ void set_unblocked() { SASSERT(is_binary_clause()); SASSERT(is_blocked()); m_val2 &= ~(1u << 3u); }
bool is_ternary_clause() const { return get_kind() == TERNARY; }
literal get_literal1() const { SASSERT(is_ternary_clause()); return to_literal(static_cast<unsigned>(m_val1)); }
diff --git a/src/shell/dimacs_frontend.cpp b/src/shell/dimacs_frontend.cpp
index c47da9b1f..50c542043 100644
--- a/src/shell/dimacs_frontend.cpp
+++ b/src/shell/dimacs_frontend.cpp
@@ -21,9 +21,9 @@ Revision History:
#include<signal.h>
#include "util/timeout.h"
#include "util/rlimit.h"
+#include "util/gparams.h"
#include "sat/dimacs.h"
#include "sat/sat_solver.h"
-#include "util/gparams.h"
extern bool g_display_statistics;
static sat::solver * g_solver = 0;
@@ -126,6 +126,42 @@ static void track_clauses(sat::solver const& src,
}
}
+void verify_solution(char const * file_name) {
+ params_ref p = gparams::get_module("sat");
+ p.set_bool("produce_models", true);
+ reslimit limit;
+ sat::solver solver(p, limit);
+ std::ifstream in(file_name);
+ if (in.bad() || in.fail()) {
+ std::cerr << "(error \"failed to open file '" << file_name << "'\")" << std::endl;
+ exit(ERR_OPEN_FILE);
+ }
+ parse_dimacs(in, solver);
+
+ sat::model const & m = g_solver->get_model();
+ for (unsigned i = 1; i < m.size(); i++) {
+ sat::literal lit(i, false);
+ switch (m[i]) {
+ case l_false: lit.neg(); break;
+ case l_undef: break;
+ case l_true: break;
+ }
+ solver.mk_clause(1, &lit);
+ }
+ lbool r = solver.check();
+ switch (r) {
+ case l_false:
+ std::cout << "model checking failed\n";
+ break;
+ case l_true:
+ std::cout << "model validated\n";
+ break;
+ default:
+ std::cout << "inconclusive model\n";
+ break;
+ }
+}
+
unsigned read_dimacs(char const * file_name) {
g_start_time = clock();
register_on_timeout_proc(on_timeout);
@@ -164,6 +200,7 @@ unsigned read_dimacs(char const * file_name) {
switch (r) {
case l_true:
std::cout << "sat\n";
+ if (file_name) verify_solution(file_name);
display_model(*g_solver);
break;
case l_undef: