From 66f0de6785c07278a852184ed6a1544393bf637f Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 25 Jun 2017 16:26:47 -0700 Subject: [PATCH] added in-processing features to card/pb Signed-off-by: Nikolaj Bjorner --- src/sat/card_extension.cpp | 655 ++++++++++++++++++++++++++++---- src/sat/card_extension.h | 37 +- src/sat/sat_elim_eqs.cpp | 4 +- src/sat/sat_extension.h | 3 + src/sat/sat_local_search.cpp | 6 +- src/sat/sat_model_converter.cpp | 59 +-- src/sat/sat_parallel.cpp | 13 +- src/sat/sat_simplifier.cpp | 75 ++-- src/sat/sat_simplifier.h | 1 + src/sat/sat_solver.cpp | 15 +- src/sat/sat_solver.h | 2 + 11 files changed, 706 insertions(+), 164 deletions(-) diff --git a/src/sat/card_extension.cpp b/src/sat/card_extension.cpp index 4f8f2d1d3..85d812cc3 100644 --- a/src/sat/card_extension.cpp +++ b/src/sat/card_extension.cpp @@ -41,6 +41,28 @@ namespace sat { SASSERT(m_size >= m_k && m_k > 0); } + std::ostream& operator<<(std::ostream& out, card_extension::card const& c) { + if (c.lit() != null_literal) { + out << c.lit() << " == "; + } + for (literal l : c) { + out << l << " "; + } + return out << " >= " << c.k(); + } + + std::ostream& operator<<(std::ostream& out, card_extension::pb const& p) { + if (p.lit() != null_literal) { + out << p.lit() << " == "; + } + for (card_extension::wliteral wl : p) { + if (wl.first != 1) out << wl.first << " * "; + out << wl.second << " "; + } + return out << " >= " << p.k(); + } + + card_extension::pb::pb(unsigned index, literal lit, svector const& wlits, unsigned k): m_index(index), m_lit(lit), @@ -204,6 +226,7 @@ namespace sat { void card_extension::copy_pb(card_extension& result) { for (pb* p : m_pbs) { + if (!p) continue; svector wlits; for (wliteral w : *p) { wlits.push_back(w); @@ -366,13 +389,12 @@ namespace sat { p.swap(num_watch, index); if (slack < bound + m_a_max) { - TRACE("sat", display(tout, p, false); for(auto j : m_pb_undef) tout << j << "\n";); + TRACE("sat", tout << p; for(auto j : m_pb_undef) tout << j << "\n";); literal_vector to_assign; while (!m_pb_undef.empty()) { index1 = m_pb_undef.back(); if (index1 == num_watch) index1 = index; // it was swapped with index above. literal lit = p[index1].second; - if (value(lit) != l_undef) std::cout << "not undef: " << index1 << " " << lit << " " << value(lit) << "\n"; SASSERT(value(lit) == l_undef); TRACE("sat", tout << index1 << " " << lit << "\n";); if (slack >= bound + p[index1].first) { @@ -484,12 +506,12 @@ namespace sat { return; } if (p.lit() == null_literal) { - unsigned max_sum = p.max_sum(); - unsigned sz = p.size(); - for (unsigned i = 0; i < sz; ++i) { - wliteral wl = p[i]; - if (p.k() > max_sum - wl.first) { - std::cout << "unit literal\n"; + for (wliteral wl : p) { + if (p.k() > p.max_sum() - wl.first) { + TRACE("sat", + tout << "unit literal " << wl.second << "\n"; + display(tout, p, true);); + s().assign(wl.second, justification()); } } } @@ -498,12 +520,11 @@ namespace sat { void card_extension::simplify(pb& p) { s().pop_to_base_level(); if (p.lit() != null_literal && value(p.lit()) == l_false) { + TRACE("sat", tout << "pb: flip sign " << p << "\n";); return; init_watch(p, !p.lit().sign()); - std::cout << "pb: flip sign\n"; } if (p.lit() != null_literal && value(p.lit()) == l_true) { - std::cout << "literal is assigned at base level " << s().at_base_lvl() << "\n"; SASSERT(lvl(p.lit()) == 0); nullify_tracking_literal(p); } @@ -522,9 +543,9 @@ namespace sat { // no op } else if (true_val >= p.k()) { - std::cout << "tautology\n"; + // std::cout << "tautology\n"; if (p.lit() != null_literal) { - std::cout << "tautology at level 0\n"; + // std::cout << "tautology at level 0\n"; s().assign(p.lit(), justification()); } remove_constraint(p); @@ -534,19 +555,19 @@ namespace sat { s().assign(~p.lit(), justification()); } else { - std::cout << "unsat during simplification\n"; + IF_VERBOSE(0, verbose_stream() << "unsat during simplification\n";); s().set_conflict(justification()); } remove_constraint(p); } else if (slack + true_val == p.k()) { - std::cout << "unit propagation\n"; + // std::cout << "unit propagation\n"; literal_vector lits(p.literals()); unit_propagation_simplification(p.lit(), lits); remove_constraint(p); } else { - std::cout << "pb value at base: " << true_val << " false: " << num_false << " size: " << p.size() << " k: " << p.k() << "\n"; + // std::cout << "pb value at base: " << true_val << " false: " << num_false << " size: " << p.size() << " k: " << p.k() << "\n"; unsigned sz = p.size(); clear_watch(p); for (unsigned i = 0; i < sz; ++i) { @@ -556,10 +577,10 @@ namespace sat { --i; } } - std::cout << "new size: " << sz << " old size " << p.size() << "\n"; + // std::cout << "new size: " << sz << " old size " << p.size() << "\n"; p.update_size(sz); p.update_k(p.k() - true_val); - // display(std::cout, c, true); + // display(verbose_stream(), c, true); if (p.lit() == null_literal) { init_watch(p, true); } @@ -568,6 +589,7 @@ namespace sat { // c will be watched once c.lit() is assigned. } simplify2(p); + m_simplify_change = true; } } @@ -1397,11 +1419,8 @@ namespace sat { break; } } - if (coeff == 0) { - - std::cout << l << " coeff: " << coeff << "\n"; - display(std::cout, p, true); - } + + CTRACE("sat", coeff == 0, display(tout << l << " coeff: " << coeff << "\n", p, true);); SASSERT(coeff > 0); unsigned slack = p.slack() - coeff; @@ -1415,10 +1434,9 @@ namespace sat { } for (; i < p.size(); ++i) { literal lit = p[i].second; - if (l_false != value(lit)) { - std::cout << l << " index: " << i << " slack: " << slack << " h: " << h << " coeff: " << coeff << "\n"; - display(std::cout, p, true); - } + CTRACE("sat", l_false != value(lit), + tout << l << " index: " << i << " slack: " << slack << " h: " << h << " coeff: " << coeff << "\n"; + display(tout, p, true);); SASSERT(l_false == value(lit)); r.push_back(~lit); } @@ -1496,6 +1514,8 @@ namespace sat { void card_extension::simplify(card& c) { SASSERT(c.lit() == null_literal || value(c.lit()) != l_false); if (c.lit() != null_literal && value(c.lit()) == l_false) { + return; +#if 0 std::ofstream ous("unit.txt"); s().display(ous); s().display_watches(ous); @@ -1503,15 +1523,13 @@ namespace sat { exit(1); return; init_watch(c, !c.lit().sign()); - std::cout << "card: flip sign\n"; +#endif } if (c.lit() != null_literal && value(c.lit()) == l_true) { - std::cout << "literal is assigned at base level " << value(c.lit()) << " " << s().at_base_lvl() << "\n"; SASSERT(lvl(c.lit()) == 0); nullify_tracking_literal(c); } if (c.lit() == null_literal && c.k() == 1) { - std::cout << "create clause\n"; literal_vector lits; for (literal l : c) lits.push_back(l); s().mk_clause(lits); @@ -1535,31 +1553,29 @@ namespace sat { return; } else if (num_true >= c.k()) { - std::cout << "tautology\n"; if (c.lit() != null_literal) { - std::cout << "tautology at level 0\n"; s().assign(c.lit(), justification()); } remove_constraint(c); } else if (num_false + c.k() > c.size()) { if (c.lit() != null_literal) { - std::cout << "falsity at level 0\n"; s().assign(~c.lit(), justification()); remove_constraint(c); } else { - std::cout << "unsat during simplification\n"; + IF_VERBOSE(1, verbose_stream() << "(sat detected unsat)\n";); } } else if (num_false + c.k() == c.size()) { - std::cout << "unit propagations : " << c.size() - num_false - num_true << "\n"; + TRACE("sat", tout << "unit propagations : " << c.size() - num_false - num_true << "\n";); literal_vector lits(c.literals()); unit_propagation_simplification(c.lit(), lits); remove_constraint(c); } else { - std::cout << "literals assigned at base: " << num_true + num_false << " " << c.size() << " k: " << c.k() << "\n"; + TRACE("sat", tout << "literals assigned at base: " << num_true + num_false << " " << c.size() << " k: " << c.k() << "\n";); + unsigned sz = c.size(); clear_watch(c); for (unsigned i = 0; i < sz; ++i) { @@ -1569,7 +1585,6 @@ namespace sat { --i; } } - std::cout << "new size: " << sz << " old size " << c.size() << "\n"; c.update_size(sz); c.update_k(c.k() - num_true); if (c.lit() == null_literal) { @@ -1579,6 +1594,7 @@ namespace sat { SASSERT(value(c.lit()) == l_undef); // c will be watched once c.lit() is assigned. } + m_simplify_change = true; } } @@ -1696,51 +1712,551 @@ namespace sat { void card_extension::simplify() { s().pop_to_base_level(); - for (card* c : m_cards) { - if (c) simplify(*c); - } - for (pb* p : m_pbs) { - if (p) simplify(*p); - } - for (xor* x : m_xors) { - if (x) simplify(*x); - } - gc(); + unsigned trail_sz; + do { + m_simplify_change = false; + trail_sz = s().init_trail_size(); + for (card* c : m_cards) { + if (c) simplify(*c); + } + for (pb* p : m_pbs) { + if (p) simplify(*p); + } + for (xor* x : m_xors) { + if (x) simplify(*x); + } + gc(); + } + while (m_simplify_change || trail_sz < s().init_trail_size()); + // or could create queue of constraints that are affected } + bool card_extension::set_root(literal l, literal r) { + for (unsigned i = m_roots.size(); i < 2 * s().num_vars(); ++i) { + m_roots.push_back(to_literal(i)); + } + m_roots[l.index()] = r; + m_roots[(~l).index()] = ~r; + return true; + } + + void card_extension::flush_roots() { + if (m_roots.empty()) return; + m_visited.resize(s().num_vars()*2, false); + for (card* c : m_cards) { + if (c) flush_roots(*c); + } + for (pb* p : m_pbs) { + if (p) flush_roots(*p); + } + for (xor* x : m_xors) { + if (x) flush_roots(*x); + } + + // display(std::cout << "flush roots\n"); + } + + void card_extension::flush_roots(card& c) { + bool found = c.lit() != null_literal && m_roots[c.lit().index()] != c.lit(); + for (literal l : c) { + if (found) break; + found = m_roots[l.index()] != l; + } + if (!found) return; + clear_watch(c); + // this could create duplicate literals + for (unsigned i = 0; i < c.size(); ++i) { + c[i] = m_roots[c[i].index()]; + } + bool found_dup = false; + for (literal l : c) { + if (is_marked(l)) { + found_dup = true; + } + else { + mark_visited(l); + mark_visited(~l); + } + } + for (literal l : c) { + unmark_visited(l); + unmark_visited(~l); + } + if (found_dup) { + recompile(c); + return; + } + + if (c.lit() != null_literal && m_roots[c.lit().index()] != c.lit()) { + literal r = m_roots[c.lit().index()]; + nullify_tracking_literal(c); + c.update_literal(r); + get_wlist(r).push_back(c.index()); + get_wlist(~r).push_back(c.index()); + } + + if (c.lit() == null_literal || value(c.lit()) == l_true) { + init_watch(c, true); + } + } + + void card_extension::recompile(card& c) { + m_count.resize(2*s().num_vars(), 0); + for (literal l : c) { + ++m_count[l.index()]; + } + unsigned k = c.k(); + bool is_card = true; + unsigned sz = c.size(); + for (unsigned i = 0; i < sz && 0 < k; ++i) { + literal l = c[i]; + while (k > 0 && + m_count[l.index()] > 0 && + m_count[(~l).index()] > 0) { + --m_count[l.index()]; + --m_count[(~l).index()]; + --k; + } + unsigned w = m_count[l.index()]; + if (w > 0) { + is_card &= w == 1; + } + else { + c.swap(i, sz - 1); + --sz; + --i; + } + } + c.update_size(sz); + c.update_k(k); + + svector wlits; + if (!is_card) { + for (literal l : c) { + unsigned w = m_count[l.index()]; + if (w > 0) { + wlits.push_back(wliteral(w, l)); + } + } + } + + // clear counts: + for (literal l : c) { + m_count[l.index()] = 0; + } + + if (k == 0) { + remove_constraint(c); + return; + } + + literal root = null_literal; + if (c.lit() != null_literal) root = m_roots[c.lit().index()]; + + if (!is_card) { + TRACE("sat", tout << "replacing by pb: " << c << "\n";); + remove_constraint(c); + add_pb_ge(root, wlits, k); + } + else { + if (c.lit() != root) { + nullify_tracking_literal(c); + c.update_literal(root); + get_wlist(root).push_back(c.index()); + get_wlist(~root).push_back(c.index()); + } + if (c.lit() == null_literal || value(c.lit()) == l_true) { + init_watch(c, true); + } + } + + } + + void card_extension::recompile(pb& p) { + m_count.resize(2*s().num_vars(), 0); + for (wliteral wl : p) { + m_count[wl.second.index()] += wl.first; + } + unsigned k = p.k(); + unsigned sz = p.size(); + for (unsigned i = 0; i < sz && 0 < k; ++i) { + wliteral wl = p[i]; + literal l = wl.second; + if (m_count[l.index()] >= m_count[(~l).index()]) { + if (k < m_count[(~l).index()]) { + k = 0; + break; + } + k -= m_count[(~l).index()]; + m_count[l.index()] -= m_count[(~l).index()]; + } + unsigned w = m_count[l.index()]; + if (w == 0) { + p.swap(i, sz - 1); + --sz; + --i; + } + else { + p[i] = wliteral(w, l); + } + } + // clear counts: + for (wliteral wl : p) { + m_count[wl.second.index()] = 0; + } + + if (k == 0) { + remove_constraint(p); + return; + } + + p.update_size(sz); + p.update_k(k); + + literal root = null_literal; + if (p.lit() != null_literal) root = m_roots[p.lit().index()]; + + // std::cout << "simplified " << p << "\n"; + if (p.lit() != root) { + nullify_tracking_literal(p); + p.update_literal(root); + get_wlist(root).push_back(p.index()); + get_wlist(~root).push_back(p.index()); + } + if (p.lit() == null_literal || value(p.lit()) == l_true) { + init_watch(p, true); + } + } + + void card_extension::flush_roots(pb& p) { + bool found = p.lit() != null_literal && m_roots[p.lit().index()] != p.lit(); + for (wliteral wl : p) { + if (found) break; + found = m_roots[wl.second.index()] != wl.second; + } + if (!found) return; + clear_watch(p); + // this could create duplicate literals + for (unsigned i = 0; i < p.size(); ++i) { + p[i].second = m_roots[p[i].second.index()]; + } + if (p.lit() != null_literal && m_roots[p.lit().index()] != p.lit()) { + literal r = m_roots[p.lit().index()]; + nullify_tracking_literal(p); + p.update_literal(r); + get_wlist(r).push_back(p.index()); + get_wlist(~r).push_back(p.index()); + } + + bool found_dup = false; + for (wliteral wl : p) { + if (is_marked(wl.second)) { + found_dup = true; + // std::cout << "Dup: " << wl.second << "\n"; + } + else { + mark_visited(wl.second); + mark_visited(~(wl.second)); + } + } + for (wliteral wl : p) { + unmark_visited(wl.second); + unmark_visited(~(wl.second)); + } + if (found_dup) { + // std::cout << "FOUND DUP " << p << "\n"; + recompile(p); + return; + } + // review for potential incompleteness: if p.lit() == l_false, do propagations happen? + if (p.lit() == null_literal || value(p.lit()) == l_true) { + init_watch(p, true); + } + } + + void card_extension::flush_roots(xor& x) { + NOT_IMPLEMENTED_YET(); + } + + + unsigned card_extension::get_num_non_learned_bin(literal l) { + return s().m_simplifier.get_num_non_learned_bin(l); + } + + /* + \brief garbage collection. + This entails + - finding pure literals, + - setting literals that are not used in the extension to non-external. + - subsumption + - resolution + - blocked literals + */ void card_extension::gc() { // remove constraints where indicator literal isn't used. - sat::use_list use_list; - use_list.init(s().num_vars()); - svector var_used(s().num_vars(), false); - for (clause* c : s().m_clauses) if (!c->frozen()) use_list.insert(*c); - for (card* c : m_cards) if (c) for (literal l : *c) var_used[l.var()] = true; - for (pb* p : m_pbs) if (p) for (wliteral wl : *p) var_used[wl.second.var()] = true; - for (xor* x : m_xors) if (x) for (literal l : *x) var_used[l.var()] = true; + m_visited.resize(s().num_vars()*2, false); + m_clause_use_list.init(s().num_vars()); + m_var_used.reset(); + m_var_used.resize(s().num_vars(), false); + m_card_use_list.reset(); + m_card_use_list.resize(2*s().num_vars(), false); + for (clause* c : s().m_clauses) if (!c->frozen()) m_clause_use_list.insert(*c); + for (card* c : m_cards) { + if (c) { + if (c->lit() != null_literal) { + m_card_use_list[c->lit().index()].push_back(c->index()); + m_card_use_list[(~c->lit()).index()].push_back(c->index()); + for (literal l : *c) m_card_use_list[(~l).index()].push_back(c->index()); + + } + for (literal l : *c) { + m_var_used[l.var()] = true; + m_card_use_list[l.index()].push_back(c->index()); + } + } + } + for (pb* p : m_pbs) { + if (p) { + if (p->lit() != null_literal) { + m_card_use_list[p->lit().index()].push_back(p->index()); + m_card_use_list[(~p->lit()).index()].push_back(p->index()); + for (wliteral wl : *p) m_card_use_list[(~wl.second).index()].push_back(p->index()); + } + for (wliteral wl : *p) { + literal l = wl.second; + m_var_used[l.var()] = true; + m_card_use_list[l.index()].push_back(p->index()); + } + } + } + for (xor* x : m_xors) { + if (x) { + m_card_use_list[x->lit().index()].push_back(x->index()); + m_card_use_list[(~x->lit()).index()].push_back(x->index()); + m_var_used[x->lit().var()] = true; + for (literal l : *x) { + m_var_used[l.var()] = true; + m_card_use_list[l.index()].push_back(x->index()); + m_card_use_list[(~l).index()].push_back(x->index()); + } + } + } for (card* c : m_cards) { - if (c && c->lit() != null_literal && !var_used[c->lit().var()] && use_list.get(c->lit()).empty() && use_list.get(~c->lit()).empty()) { + if (c && c->lit() != null_literal && + !m_var_used[c->lit().var()] && + m_clause_use_list.get(c->lit()).empty() && + m_clause_use_list.get(~c->lit()).empty() && + get_num_non_learned_bin(c->lit()) == 0 && + get_num_non_learned_bin(~c->lit()) == 0) { remove_constraint(*c); } } for (pb* p : m_pbs) { - if (p && p->lit() != null_literal && !var_used[p->lit().var()] && use_list.get(p->lit()).empty() && use_list.get(~p->lit()).empty()) { + if (p && p->lit() != null_literal && + !m_var_used[p->lit().var()] && + m_clause_use_list.get(p->lit()).empty() && + m_clause_use_list.get(~p->lit()).empty() && + get_num_non_learned_bin(p->lit()) == 0 && + get_num_non_learned_bin(~p->lit()) == 0) { remove_constraint(*p); } } // take ownership of interface variables - for (card* c : m_cards) if (c && c->lit() != null_literal) var_used[c->lit().var()] = true; - for (pb* p : m_pbs) if (p && p->lit() != null_literal) var_used[p->lit().var()] = true; + for (card* c : m_cards) if (c && c->lit() != null_literal) m_var_used[c->lit().var()] = true; + for (pb* p : m_pbs) if (p && p->lit() != null_literal) m_var_used[p->lit().var()] = true; + // set variables to be non-external if they are not used in theory constraints. unsigned ext = 0; for (unsigned v = 0; v < s().num_vars(); ++v) { - if (s().is_external(v) && !var_used[v]) { + if (s().is_external(v) && !m_var_used[v]) { s().set_non_external(v); ++ext; } } - std::cout << "non-external variables " << ext << "\n"; + // eliminate pure literals + unsigned pure_literals = 0; + for (unsigned v = 0; v < s().num_vars(); ++v) { + if (!m_var_used[v]) continue; + literal lit(v, false); + if (!m_card_use_list[lit.index()].empty() && m_card_use_list[(~lit).index()].empty() && m_clause_use_list.get(~lit).empty() && + get_num_non_learned_bin(~lit) == 0) { + s().assign(lit, justification()); + ++pure_literals; + continue; + } + lit.neg(); + if (!m_card_use_list[lit.index()].empty() && m_card_use_list[(~lit).index()].empty() && m_clause_use_list.get(~lit).empty() && get_num_non_learned_bin(~lit) == 0) { + s().assign(lit, justification()); + ++pure_literals; + } + } + IF_VERBOSE(10, + verbose_stream() << "non-external variables converted: " << ext << "\n"; + verbose_stream() << "pure literals converted: " << pure_literals << "\n";); + + m_cleanup_clauses = false; + for (card* c : m_cards) { + if (c && c->k() > 1) { + subsumption(*c); + } + } + if (m_cleanup_clauses) { + clause_vector::iterator it = s().m_clauses.begin(); + clause_vector::iterator end = s().m_clauses.end(); + clause_vector::iterator it2 = it; + for (; it != end; ++it) { + clause* c = *it; + if (c->was_removed()) { + s().detach_clause(*c); + s().del_clause(*c); + } + else { + if (it2 != it) { + *it2 = *it; + } + ++it2; + } + } + s().m_clauses.set_end(it2); + } + } + + /* + \brief subsumption between two cardinality constraints + - A >= k subsumes A + B >= k' for k' <= k + - A + A' >= k subsumes A + B >= k' for k' + |A'| <= k + - A + lit >= k self subsumes A + ~lit + B >= k' into A + B >= k' for k' <= k + - TBD: consider version that generalizes self-subsumption to more than one literal + A + ~L + B >= k' => A + B >= k' if A + A' + L >= k and k' + |L| + |A'| <= k + */ + bool card_extension::subsumes(card& c1, card& c2, literal_vector & comp) { + if (c2.lit() != null_literal) return false; // perhaps support this? + + unsigned c2_exclusive = 0; + unsigned common = 0; + comp.empty(); + for (literal l : c2) { + if (is_marked(l)) { + ++common; + } + else if (!is_marked(~l)) { + ++c2_exclusive; + } + else { + comp.push_back(l); + } + } + + unsigned c1_exclusive = c1.size() - common - comp.size(); + + return c1_exclusive + c2.k() + comp.size() <= c1.k(); + } + + bool card_extension::subsumes(card& c1, clause& c2, literal_vector & comp) { + unsigned c2_exclusive = 0; + unsigned common = 0; + comp.reset(); + for (literal l : c2) { + if (is_marked(l)) { + ++common; + } + else if (!is_marked(~l)) { + ++c2_exclusive; + } + else { + comp.push_back(l); + } + } + + if (!comp.empty()) { + // self-subsumption is TBD. + return false; + } + unsigned c1_exclusive = c1.size() - common - comp.size(); + if (c1_exclusive + 1 <= c1.k()) { + return true; + } + + return false; + } + + literal card_extension::get_min_occurrence_literal(card const& c) { + unsigned occ_count = UINT_MAX; + literal lit = null_literal; + for (literal l : c) { + unsigned occ_count1 = m_card_use_list[l.index()].size(); + if (occ_count1 < occ_count) { + lit = l; + occ_count = occ_count1; + } + } + return lit; + } + + void card_extension::subsumption(card& c1) { + if (c1.lit() != null_literal) { + return; + } + literal lit = get_min_occurrence_literal(c1); + literal_vector slit; + // maybe index over (~lit) to catch self-subsumption. + + for (literal l : c1) mark_visited(l); + + for (unsigned index : m_card_use_list[lit.index()]) { + if (!is_card_index(index) || index == c1.index()) { + continue; + } + // c2 could be null + card* c = m_cards[index2position(index)]; + if (!c) continue; + card& c2 = *c; + + SASSERT(c1.index() != c2.index()); + if (subsumes(c1, c2, slit)) { + if (slit.empty()) { + TRACE("sat", tout << "subsume cardinality\n" << c1.index() << ":" << c1 << "\n" << c2.index() << ":" << c2 << "\n";); + remove_constraint(c2); + } + else { + TRACE("sat", tout << "self subsume carinality\n";); +#if 0 + clear_watch(c2); + for (unsigned i = 0; i < c2.size(); ++i) { + if (slit == c2[i]) { + c2.swap(i, c2.size() -1); + break; + } + } + c2.update_size(c2.size() - 1); + init_watch(c2, true); + m_simplify_change = true; +#endif + } + } + } + + // same for clauses... + clause_use_list::iterator it = m_clause_use_list.get(lit).mk_iterator(); + while (!it.at_end()) { + clause& c2 = it.curr(); + if (!c2.was_removed() && subsumes(c1, c2, slit)) { + if (slit.empty()) { + TRACE("sat", tout << "remove\n" << c1 << "\n" << c2 << "\n";); + c2.set_removed(true); + m_cleanup_clauses = true; + } + else { + // remove literal slit from c2. + TRACE("sat", tout << "TBD remove literals " << slit << " from " << c2 << "\n";); + } + } + it.next(); + } + + for (literal l : c1) unmark_visited(l); } void card_extension::clauses_modifed() {} @@ -1749,6 +2265,7 @@ namespace sat { void card_extension::copy_card(card_extension& result) { for (card* c : m_cards) { + if (!c) continue; literal_vector lits; for (literal l : *c) lits.push_back(l); result.add_at_least(c->lit(), lits, c->k()); @@ -1864,10 +2381,10 @@ namespace sat { std::ostream& card_extension::display(std::ostream& out) const { for (card* c : m_cards) { - if (c) display(out, *c, false); + if (c) out << *c << "\n"; } for (pb* p : m_pbs) { - if (p) display(out, *p, false); + if (p) out << *p << "\n"; } for (xor* x : m_xors) { if (x) display(out, *x, false); @@ -2092,7 +2609,7 @@ namespace sat { unsigned coeff; if (coeffs.find(lit.index(), coeff)) { if (coeff > m_C.m_coeffs[i] && m_C.m_coeffs[i] < m_C.m_k) { - std::cout << i << ": " << m_C.m_coeffs[i] << " " << m_C.m_k << "\n"; + IF_VERBOSE(0, verbose_stream() << i << ": " << m_C.m_coeffs[i] << " " << m_C.m_k << "\n";); goto violated; } coeffs.remove(lit.index()); @@ -2105,13 +2622,13 @@ namespace sat { return true; violated: - display(std::cout, m_A); - display(std::cout, m_B); - display(std::cout, m_C); - u_map::iterator it = coeffs.begin(), end = coeffs.end(); - for (; it != end; ++it) { - std::cout << to_literal(it->m_key) << ": " << it->m_value << "\n"; - } + IF_VERBOSE(0, + display(verbose_stream(), m_A); + display(verbose_stream(), m_B); + display(verbose_stream(), m_C); + for (auto& e : coeffs) { + verbose_stream() << to_literal(e.m_key) << ": " << e.m_value << "\n"; + }); return false; } diff --git a/src/sat/card_extension.h b/src/sat/card_extension.h index 64553795b..c3f8e430f 100644 --- a/src/sat/card_extension.h +++ b/src/sat/card_extension.h @@ -59,6 +59,7 @@ namespace sat { unsigned index() const { return m_index; } literal lit() const { return m_lit; } literal operator[](unsigned i) const { return m_lits[i]; } + literal& operator[](unsigned i) { return m_lits[i]; } literal const* begin() const { return m_lits; } literal const* end() const { return static_cast(m_lits) + m_size; } unsigned k() const { return m_k; } @@ -67,9 +68,12 @@ namespace sat { void negate(); void update_size(unsigned sz) { SASSERT(sz <= m_size); m_size = sz; } void update_k(unsigned k) { m_k = k; } + void update_literal(literal l) { m_lit = l; } void nullify_literal() { m_lit = null_literal; } - literal_vector literals() const { return literal_vector(m_size, m_lits); } + literal_vector literals() const { return literal_vector(m_size, m_lits); } }; + + friend std::ostream& operator<<(std::ostream& out, card const& c); typedef std::pair wliteral; @@ -89,6 +93,7 @@ namespace sat { unsigned index() const { return m_index; } literal lit() const { return m_lit; } wliteral operator[](unsigned i) const { return m_wlits[i]; } + wliteral& operator[](unsigned i) { return m_wlits[i]; } wliteral const* begin() const { return m_wlits; } wliteral const* end() const { return static_cast(m_wlits) + m_size; } @@ -102,11 +107,14 @@ namespace sat { void swap(unsigned i, unsigned j) { std::swap(m_wlits[i], m_wlits[j]); } void negate(); void update_size(unsigned sz) { m_size = sz; update_max_sum(); } - void update_k(unsigned k) { m_k = k; } + void update_k(unsigned k) { m_k = k; } + void update_literal(literal l) { m_lit = l; } void nullify_literal() { m_lit = null_literal; } literal_vector literals() const { literal_vector lits; for (auto wl : *this) lits.push_back(wl.second); return lits; } }; + friend std::ostream& operator<<(std::ostream& out, pb const& p); + class xor { unsigned m_index; literal m_lit; @@ -168,8 +176,26 @@ namespace sat { void clear_index_trail_back(); solver& s() const { return *m_solver; } + + // simplification routines + svector m_visited; + vector> m_card_use_list; + use_list m_clause_use_list; + svector m_var_used; + bool m_simplify_change; + bool m_cleanup_clauses; + literal_vector m_roots; + unsigned_vector m_count; void gc(); + bool subsumes(card& c1, card& c2, literal_vector& comp); + bool subsumes(card& c1, clause& c2, literal_vector& comp); + 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); + literal get_min_occurrence_literal(card const& c); + void subsumption(card& c1); // cardinality void init_watch(card& c); @@ -189,6 +215,8 @@ namespace sat { void nullify_tracking_literal(card& c); void remove_constraint(card& c); void unit_propagation_simplification(literal lit, literal_vector const& lits); + void flush_roots(card& c); + void recompile(card& c); // xor specific functionality void copy_xor(card_extension& result); @@ -203,6 +231,7 @@ namespace sat { void get_xor_antecedents(literal l, unsigned index, justification js, literal_vector& r); void get_xor_antecedents(literal l, xor const& x, literal_vector & r); void simplify(xor& x); + void flush_roots(xor& x); bool is_card_index(unsigned idx) const { return 0x0 == (idx & 0x3); } @@ -231,6 +260,8 @@ namespace sat { bool is_cardinality(pb const& p); void nullify_tracking_literal(pb& p); void remove_constraint(pb& p); + void flush_roots(pb& p); + void recompile(pb& p); inline lbool value(literal lit) const { return m_lookahead ? m_lookahead->value(lit) : m_solver->value(lit); } inline unsigned lvl(literal lit) const { return m_solver->lvl(lit); } @@ -301,6 +332,8 @@ namespace sat { virtual void simplify(); virtual void clauses_modifed(); virtual lbool get_phase(bool_var v); + virtual bool set_root(literal l, literal r); + virtual void flush_roots(); virtual std::ostream& display(std::ostream& out) const; virtual std::ostream& display_justification(std::ostream& out, ext_justification_idx idx) const; virtual void collect_statistics(statistics& st) const; diff --git a/src/sat/sat_elim_eqs.cpp b/src/sat/sat_elim_eqs.cpp index b9b7dbd85..f51b8c42d 100644 --- a/src/sat/sat_elim_eqs.cpp +++ b/src/sat/sat_elim_eqs.cpp @@ -189,7 +189,8 @@ namespace sat { literal l(v, false); literal r = roots[v]; SASSERT(v != r.var()); - if (m_solver.is_external(v)) { + if (m_solver.is_external(v) && !m_solver.set_root(l, r)) { + std::cout << "skip: " << l << " == " << r << "\n"; // cannot really eliminate v, since we have to notify extension of future assignments m_solver.mk_bin_clause(~l, r, false); m_solver.mk_bin_clause(l, ~r, false); @@ -201,6 +202,7 @@ namespace sat { mc.insert(e, ~l, r); mc.insert(e, l, ~r); } + m_solver.flush_roots(); } } diff --git a/src/sat/sat_extension.h b/src/sat/sat_extension.h index 44a704f80..d3a58810c 100644 --- a/src/sat/sat_extension.h +++ b/src/sat/sat_extension.h @@ -42,6 +42,9 @@ namespace sat { virtual void push() = 0; virtual void pop(unsigned n) = 0; virtual void simplify() = 0; + // have a way to replace l by r in all constraints + virtual bool set_root(literal l, literal r) { return false; } + virtual void flush_roots() {} virtual void clauses_modifed() = 0; virtual lbool get_phase(bool_var v) = 0; virtual std::ostream& display(std::ostream& out) const = 0; diff --git a/src/sat/sat_local_search.cpp b/src/sat/sat_local_search.cpp index 5372011ed..e42076de4 100644 --- a/src/sat/sat_local_search.cpp +++ b/src/sat/sat_local_search.cpp @@ -394,6 +394,7 @@ namespace sat { << " :flips " << flips \ << " :noise " << m_noise \ << " :unsat " << /*m_unsat_stack.size()*/ m_best_unsat \ + << " :constraints " << m_constraints.size() \ << " :time " << (timer.get_seconds() < 0.001 ? 0.0 : timer.get_seconds()) << ")\n";); \ } @@ -419,7 +420,7 @@ namespace sat { } total_flips += step; PROGRESS(tries, total_flips); - if (m_par && tries % 20 == 0) { + if (m_par && tries % 1 == 0) { m_par->get_phase(*this); reinit(); } @@ -489,7 +490,7 @@ namespace sat { result = l_undef; } IF_VERBOSE(1, verbose_stream() << "(sat-local-search " << result << ")\n";); - IF_VERBOSE(2, display(verbose_stream());); + IF_VERBOSE(20, display(verbose_stream());); return result; } @@ -810,7 +811,6 @@ namespace sat { constraint const& c = m_constraints[m_unsat_stack[m_rand() % m_unsat_stack.size()]]; // a random unsat constraint // Within c, from all slack increasing var, choose the oldest one unsigned c_size = c.size(); - //std::cout << "rd\t"; for (unsigned i = 0; i < c_size; ++i) { bool_var v = c[i].var(); if (is_true(c[i]) && time_stamp(v) < time_stamp(best_var)) diff --git a/src/sat/sat_model_converter.cpp b/src/sat/sat_model_converter.cpp index 81de935b1..c6f340f2e 100644 --- a/src/sat/sat_model_converter.cpp +++ b/src/sat/sat_model_converter.cpp @@ -34,8 +34,7 @@ namespace sat { } model_converter& model_converter::operator=(model_converter const& other) { - reset(); - m_entries.append(other.m_entries); + copy(other); return *this; } @@ -50,10 +49,7 @@ namespace sat { // and the following procedure flips its value. bool sat = false; bool var_sign = false; - literal_vector::const_iterator it2 = it->m_clauses.begin(); - literal_vector::const_iterator end2 = it->m_clauses.end(); - for (; it2 != end2; ++it2) { - literal l = *it2; + for (literal l : it->m_clauses) { if (l == null_literal) { // end of clause if (!sat) { @@ -80,9 +76,7 @@ namespace sat { DEBUG_CODE({ // all clauses must be satisfied bool sat = false; - it2 = it->m_clauses.begin(); - for (; it2 != end2; ++it2) { - literal l = *it2; + for (literal l : it->m_clauses) { if (l == null_literal) { SASSERT(sat); sat = false; @@ -145,10 +139,7 @@ namespace sat { SASSERT(c.contains(e.var())); SASSERT(m_entries.begin() <= &e); SASSERT(&e < m_entries.end()); - unsigned sz = c.size(); - for (unsigned i = 0; i < sz; i++) { - e.m_clauses.push_back(c[i]); - } + for (literal l : c) e.m_clauses.push_back(l); e.m_clauses.push_back(null_literal); TRACE("sat_mc_bug", tout << "adding: " << c << "\n";); } @@ -168,10 +159,10 @@ namespace sat { SASSERT(m_entries.begin() <= &e); SASSERT(&e < m_entries.end()); unsigned sz = c.size(); - for (unsigned i = 0; i < sz; i++) + for (unsigned i = 0; i < sz; ++i) e.m_clauses.push_back(c[i]); e.m_clauses.push_back(null_literal); - TRACE("sat_mc_bug", tout << "adding (wrapper): "; for (unsigned i = 0; i < c.size(); i++) tout << c[i] << " "; tout << "\n";); + TRACE("sat_mc_bug", tout << "adding (wrapper): "; for (literal l : c) tout << l << " "; tout << "\n";); } bool model_converter::check_invariant(unsigned num_vars) const { @@ -186,12 +177,10 @@ namespace sat { it2++; for (; it2 != end; ++it2) { SASSERT(it2->var() != it->var()); - literal_vector::const_iterator it3 = it2->m_clauses.begin(); - literal_vector::const_iterator end3 = it2->m_clauses.end(); - for (; it3 != end3; ++it3) { - CTRACE("sat_model_converter", it3->var() == it->var(), tout << "var: " << it->var() << "\n"; display(tout);); - SASSERT(it3->var() != it->var()); - SASSERT(*it3 == null_literal || it3->var() < num_vars); + for (literal l : it2->m_clauses) { + CTRACE("sat_model_converter", l.var() == it->var(), tout << "var: " << it->var() << "\n"; display(tout);); + SASSERT(l.var() != it->var()); + SASSERT(l == null_literal || l.var() < num_vars); } } } @@ -201,28 +190,24 @@ namespace sat { void model_converter::display(std::ostream & out) const { out << "(sat::model-converter"; - vector::const_iterator it = m_entries.begin(); - vector::const_iterator end = m_entries.end(); - for (; it != end; ++it) { - out << "\n (" << (it->get_kind() == ELIM_VAR ? "elim" : "blocked") << " " << it->var(); + for (auto & entry : m_entries) { + out << "\n (" << (entry.get_kind() == ELIM_VAR ? "elim" : "blocked") << " " << entry.var(); bool start = true; - literal_vector::const_iterator it2 = it->m_clauses.begin(); - literal_vector::const_iterator end2 = it->m_clauses.end(); - for (; it2 != end2; ++it2) { + for (literal l : entry.m_clauses) { if (start) { out << "\n ("; start = false; } else { - if (*it2 != null_literal) + if (l != null_literal) out << " "; } - if (*it2 == null_literal) { + if (l == null_literal) { out << ")"; start = true; continue; } - out << *it2; + out << l; } out << ")"; } @@ -230,18 +215,12 @@ namespace sat { } void model_converter::copy(model_converter const & src) { - vector::const_iterator it = src.m_entries.begin(); - vector::const_iterator end = src.m_entries.end(); - for (; it != end; ++it) - m_entries.push_back(*it); + reset(); + m_entries.append(src.m_entries); } void model_converter::collect_vars(bool_var_set & s) const { - vector::const_iterator it = m_entries.begin(); - vector::const_iterator end = m_entries.end(); - for (; it != end; ++it) { - s.insert(it->m_var); - } + for (entry const & e : m_entries) s.insert(e.m_var); } }; diff --git a/src/sat/sat_parallel.cpp b/src/sat/sat_parallel.cpp index 0b9a5bcb3..21f98cd6a 100644 --- a/src/sat/sat_parallel.cpp +++ b/src/sat/sat_parallel.cpp @@ -127,7 +127,7 @@ namespace sat { void parallel::exchange(solver& s, literal_vector const& in, unsigned& limit, literal_vector& out) { - if (s.m_par_syncing_clauses) return; + if (s.get_config().m_num_threads == 1 || s.m_par_syncing_clauses) return; flet _disable_sync_clause(s.m_par_syncing_clauses, true); #pragma omp critical (par_solver) { @@ -147,11 +147,11 @@ namespace sat { } void parallel::share_clause(solver& s, literal l1, literal l2) { - if (s.m_par_syncing_clauses) return; + if (s.get_config().m_num_threads == 1 || s.m_par_syncing_clauses) return; flet _disable_sync_clause(s.m_par_syncing_clauses, true); + IF_VERBOSE(3, verbose_stream() << s.m_par_id << ": share " << l1 << " " << l2 << "\n";); #pragma omp critical (par_solver) { - IF_VERBOSE(3, verbose_stream() << s.m_par_id << ": share " << l1 << " " << l2 << "\n";); m_pool.begin_add_vector(s.m_par_id, 2); m_pool.add_vector_elem(l1.index()); m_pool.add_vector_elem(l2.index()); @@ -160,13 +160,13 @@ namespace sat { } void parallel::share_clause(solver& s, clause const& c) { - if (!enable_add(c) || s.m_par_syncing_clauses) return; + if (s.get_config().m_num_threads == 1 || !enable_add(c) || s.m_par_syncing_clauses) return; flet _disable_sync_clause(s.m_par_syncing_clauses, true); unsigned n = c.size(); unsigned owner = s.m_par_id; + IF_VERBOSE(3, verbose_stream() << owner << ": share " << c << "\n";); #pragma omp critical (par_solver) { - IF_VERBOSE(3, verbose_stream() << owner << ": share " << c << "\n";); m_pool.begin_add_vector(owner, n); for (unsigned i = 0; i < n; ++i) { m_pool.add_vector_elem(c[i].index()); @@ -229,7 +229,8 @@ namespace sat { break; } } - if (90 * m_num_clauses > 100 * s.m_clauses.size() && !m_solver_copy) { + IF_VERBOSE(1, verbose_stream() << "set phase: " << m_num_clauses << " " << s.m_clauses.size() << " " << m_solver_copy << "\n";); + if (m_num_clauses == 0 || (m_num_clauses > s.m_clauses.size())) { // time to update local search with new clauses. // there could be multiple local search engines runing at the same time. IF_VERBOSE(1, verbose_stream() << "(sat-parallel refresh local search " << m_num_clauses << " -> " << s.m_clauses.size() << ")\n";); diff --git a/src/sat/sat_simplifier.cpp b/src/sat/sat_simplifier.cpp index 4750f8e76..9c31f4005 100644 --- a/src/sat/sat_simplifier.cpp +++ b/src/sat/sat_simplifier.cpp @@ -354,17 +354,15 @@ namespace sat { Otherwise return false */ bool simplifier::subsumes1(clause const & c1, clause const & c2, literal & l) { - unsigned sz2 = c2.size(); - for (unsigned i = 0; i < sz2; i++) - mark_visited(c2[i]); + for (literal lit : c2) + mark_visited(lit); bool r = true; l = null_literal; - unsigned sz1 = c1.size(); - for (unsigned i = 0; i < sz1; i++) { - if (!is_marked(c1[i])) { - if (l == null_literal && is_marked(~c1[i])) { - l = ~c1[i]; + for (literal lit : c1) { + if (!is_marked(lit)) { + if (l == null_literal && is_marked(~lit)) { + l = ~lit; } else { l = null_literal; @@ -374,8 +372,8 @@ namespace sat { } } - for (unsigned i = 0; i < sz2; i++) - unmark_visited(c2[i]); + for (literal lit : c2) + unmark_visited(lit); return r; } @@ -964,40 +962,37 @@ namespace sat { if (!process_var(l.var())) { return; } + + m_to_remove.reset(); { - 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)) { - TRACE("blocked_clause", tout << "new blocked clause: " << c << "\n";); - if (new_entry == 0) - new_entry = &(mc.mk(model_converter::BLOCK_LIT, l.var())); - m_to_remove.push_back(&c); - s.m_num_blocked_clauses++; - mc.insert(*new_entry, c); - unsigned sz = c.size(); - for (unsigned i = 0; i < sz; i++) { - literal lit = c[i]; - if (lit != l && process_var(lit.var())) { - m_queue.decreased(~lit); - } + 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)) { + TRACE("blocked_clause", tout << "new blocked clause: " << c << "\n";); + if (new_entry == 0) + new_entry = &(mc.mk(model_converter::BLOCK_LIT, l.var())); + m_to_remove.push_back(&c); + s.m_num_blocked_clauses++; + mc.insert(*new_entry, c); + unsigned sz = c.size(); + for (unsigned i = 0; i < sz; i++) { + literal lit = c[i]; + if (lit != l && process_var(lit.var())) { + m_queue.decreased(~lit); } } - s.unmark_all(c); - it.next(); } - } - clause_vector::iterator it = m_to_remove.begin(); - clause_vector::iterator end = m_to_remove.end(); - for (; it != end; ++it) { - s.remove_clause(*(*it)); - } + s.unmark_all(c); + it.next(); + } + } + for (clause* c : m_to_remove) { + s.remove_clause(*c); } { watch_list & wlist = s.get_wlist(~l); diff --git a/src/sat/sat_simplifier.h b/src/sat/sat_simplifier.h index 0f0b1d71e..6429ce6eb 100644 --- a/src/sat/sat_simplifier.h +++ b/src/sat/sat_simplifier.h @@ -47,6 +47,7 @@ namespace sat { }; class simplifier { + friend class card_extension; solver & s; unsigned m_num_calls; use_list m_use_list; diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp index 2aa944087..4e34579a7 100644 --- a/src/sat/sat_solver.cpp +++ b/src/sat/sat_solver.cpp @@ -1072,9 +1072,8 @@ namespace sat { \brief import lemmas/units from parallel sat solvers. */ void solver::exchange_par() { - if (m_par && at_search_lvl()) m_par->set_phase(*this); - if (m_par && at_base_lvl()) m_par->get_clauses(*this); - if (m_par && at_base_lvl()) { + if (m_par && at_base_lvl() && m_config.m_num_threads > 1) m_par->get_clauses(*this); + if (m_par && at_base_lvl() && m_config.m_num_threads > 1) { // SASSERT(scope_lvl() == search_lvl()); // TBD: import also dependencies of assumptions. unsigned sz = init_trail_size(); @@ -1463,7 +1462,17 @@ namespace sat { } #endif + if (m_par) m_par->set_phase(*this); + + } + + bool solver::set_root(literal l, literal r) { + return !m_ext || m_ext->set_root(l, r); + } + + void solver::flush_roots() { + if (m_ext) m_ext->flush_roots(); } void solver::sort_watch_lits() { diff --git a/src/sat/sat_solver.h b/src/sat/sat_solver.h index c534ae828..eb7dd9c70 100644 --- a/src/sat/sat_solver.h +++ b/src/sat/sat_solver.h @@ -315,6 +315,8 @@ namespace sat { config const& get_config() const { return m_config; } extension* get_extension() const { return m_ext.get(); } void set_extension(extension* e); + bool set_root(literal l, literal r); + void flush_roots(); typedef std::pair bin_clause; protected: watch_list & get_wlist(literal l) { return m_watches[l.index()]; }