From 5f5819f029482eeace9043998c579578f79bf1bf Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 9 Mar 2017 22:44:41 +0100 Subject: [PATCH] fix xor handling, and defaults for cardinality Signed-off-by: Nikolaj Bjorner --- src/ast/rewriter/pb2bv_rewriter.cpp | 8 ++-- src/opt/opt_context.cpp | 11 ++++-- src/sat/card_extension.cpp | 57 ++++++++++++++++++++--------- src/sat/card_extension.h | 10 +++-- src/sat/sat_local_search.cpp | 42 +++++++++++---------- src/sat/sat_lookahead.h | 39 ++++++++++++++++++-- src/tactic/arith/card2bv_tactic.cpp | 1 + src/util/memory_manager.cpp | 1 + 8 files changed, 119 insertions(+), 50 deletions(-) diff --git a/src/ast/rewriter/pb2bv_rewriter.cpp b/src/ast/rewriter/pb2bv_rewriter.cpp index 1afb56c1a..f546ef70b 100644 --- a/src/ast/rewriter/pb2bv_rewriter.cpp +++ b/src/ast/rewriter/pb2bv_rewriter.cpp @@ -419,8 +419,8 @@ struct pb2bv_rewriter::imp { bv(m), m_trail(m), m_args(m), - m_keep_cardinality_constraints(true), - m_min_arity(8) + m_keep_cardinality_constraints(false), + m_min_arity(2) {} bool mk_app(bool full, func_decl * f, unsigned sz, expr * const* args, expr_ref & result) { @@ -618,12 +618,12 @@ struct pb2bv_rewriter::imp { m_fresh(m), m_num_translated(0), m_rw(*this, m) { - m_rw.keep_cardinality_constraints(p.get_bool("keep_cardinality_constraints", true)); + m_rw.keep_cardinality_constraints(p.get_bool("keep_cardinality_constraints", false)); } void updt_params(params_ref const & p) { m_params.append(p); - m_rw.keep_cardinality_constraints(m_params.get_bool("keep_cardinality_constraints", true)); + m_rw.keep_cardinality_constraints(m_params.get_bool("keep_cardinality_constraints", false)); } void collect_param_descrs(param_descrs& r) const { r.insert("keep_cardinality_constraints", CPK_BOOL, "(default: true) retain cardinality constraints (don't bit-blast them) and use built-in cardinality solver"); diff --git a/src/opt/opt_context.cpp b/src/opt/opt_context.cpp index ebe56381a..da02eba6b 100644 --- a/src/opt/opt_context.cpp +++ b/src/opt/opt_context.cpp @@ -270,7 +270,6 @@ namespace opt { #endif solver& s = get_solver(); s.assert_expr(m_hard_constraints); - display_benchmark(); IF_VERBOSE(1, verbose_stream() << "(optimize:check-sat)\n";); lbool is_sat = s.check_sat(0,0); TRACE("opt", tout << "initial search result: " << is_sat << "\n";); @@ -1002,8 +1001,9 @@ namespace opt { TRACE("opt", tout << "Term does not evaluate " << term << "\n";); return false; } - if (!m_arith.is_numeral(val, r)) { - TRACE("opt", tout << "model does not evaluate objective to a value\n";); + unsigned bv_size; + if (!m_arith.is_numeral(val, r) && !m_bv.is_numeral(val, r, bv_size)) { + TRACE("opt", tout << "model does not evaluate objective to a value, but to " << val << "\n";); return false; } if (r != v) { @@ -1199,6 +1199,9 @@ namespace opt { } void context::display_benchmark() { + display(verbose_stream()); + return; + if (opt_params(m_params).dump_benchmarks() && sat_enabled() && m_objectives.size() == 1 && @@ -1208,6 +1211,8 @@ namespace opt { unsigned sz = o.m_terms.size(); inc_sat_display(verbose_stream(), get_solver(), sz, o.m_terms.c_ptr(), o.m_weights.c_ptr()); } + + } void context::display(std::ostream& out) { diff --git a/src/sat/card_extension.cpp b/src/sat/card_extension.cpp index 1100428c5..cb05e5d61 100644 --- a/src/sat/card_extension.cpp +++ b/src/sat/card_extension.cpp @@ -146,7 +146,7 @@ namespace sat { set_conflict(c, lit); break; default: - m_stats.m_num_propagations++; + m_stats.m_num_card_propagations++; m_num_propagations_since_pop++; //TRACE("sat", tout << "#prop: " << m_stats.m_num_propagations << " - " << c.lit() << " => " << lit << "\n";); SASSERT(validate_unit_propagation(c)); @@ -183,8 +183,10 @@ namespace sat { } void card_extension::set_conflict(card& c, literal lit) { + m_stats.m_num_card_conflicts++; TRACE("sat", display(tout, c, true); ); SASSERT(validate_conflict(c)); + SASSERT(value(lit) == l_false); s().set_conflict(justification::mk_ext_justification(c.index()), ~lit); SASSERT(s().inconsistent()); } @@ -223,6 +225,7 @@ namespace sat { if (x.lit() != null_literal && x.lit().sign() == is_true) { x.negate(); } + TRACE("sat", display(tout, x, true);); unsigned sz = x.size(); unsigned j = 0; for (unsigned i = 0; i < sz && j < 2; ++i) { @@ -234,7 +237,16 @@ namespace sat { switch (j) { case 0: if (!parity(x, 0)) { - set_conflict(x, x[0]); + literal_set litset; + for (unsigned i = 0; i < sz; ++i) { + litset.insert(x[i]); + } + literal_vector const& lits = s().m_trail; + unsigned idx = lits.size()-1; + while (!litset.contains(lits[idx])) { + --idx; + } + set_conflict(x, lits[idx]); } break; case 1: @@ -249,14 +261,16 @@ namespace sat { } void card_extension::assign(xor& x, literal lit) { + SASSERT(!s().inconsistent()); switch (value(lit)) { case l_true: break; case l_false: set_conflict(x, lit); + SASSERT(s().inconsistent()); break; default: - m_stats.m_num_propagations++; + m_stats.m_num_xor_propagations++; m_num_propagations_since_pop++; if (s().m_config.m_drat) { svector ps; @@ -269,6 +283,7 @@ namespace sat { ps.push_back(drat::premise(drat::s_ext(), x.lit())); s().m_drat.add(lits, ps); } + TRACE("sat", display(tout << lit << " ", x, true);); s().assign(lit, justification::mk_ext_justification(x.index())); break; } @@ -290,8 +305,11 @@ namespace sat { void card_extension::set_conflict(xor& x, literal lit) { + m_stats.m_num_xor_conflicts++; TRACE("sat", display(tout, x, true); ); + if (value(lit) == l_true) lit.neg(); SASSERT(validate_conflict(x)); + TRACE("sat", display(tout << lit << " ", x, true);); s().set_conflict(justification::mk_ext_justification(x.index()), ~lit); SASSERT(s().inconsistent()); } @@ -332,7 +350,7 @@ namespace sat { assign(x, p ? ~x[0] : x[0]); } else if (!parity(x, 0)) { - set_conflict(x, x[0]); + set_conflict(x, ~x[1]); } return s().inconsistent() ? l_false : l_true; } @@ -410,6 +428,7 @@ namespace sat { m_bound = 0; literal consequent = s().m_not_l; justification js = s().m_conflict; + TRACE("sat", tout << consequent << " " << js << "\n";); m_conflict_lvl = s().get_max_lvl(consequent, js); if (consequent != null_literal) { consequent.neg(); @@ -418,7 +437,6 @@ namespace sat { literal_vector const& lits = s().m_trail; unsigned idx = lits.size()-1; int offset = 1; - DEBUG_CODE(active2pb(m_A);); unsigned init_marks = m_num_marks; @@ -490,17 +508,18 @@ namespace sat { card& c = index2card(index); m_bound += offset * c.k(); process_card(c, offset); + ++m_stats.m_num_card_resolves; } else { // jus.push_back(js); m_lemma.reset(); m_bound += offset; inc_coeff(consequent, offset); - get_xor_antecedents(idx, m_lemma); - // get_antecedents(consequent, index, m_lemma); + get_xor_antecedents(consequent, idx, js, m_lemma); for (unsigned i = 0; i < m_lemma.size(); ++i) { process_antecedent(~m_lemma[i], offset); } + ++m_stats.m_num_xor_resolves; } break; } @@ -666,7 +685,6 @@ namespace sat { CTRACE("sat", s().is_marked(m_lemma[i].var()), tout << "marked: " << m_lemma[i] << "\n";); s().mark(m_lemma[i].var()); } - m_stats.m_num_conflicts++; return true; @@ -797,19 +815,17 @@ namespace sat { The idea is to collect premises based on xor resolvents. Variables that are repeated an even number of times cancel out. */ - void card_extension::get_xor_antecedents(unsigned index, literal_vector& r) { - literal_vector const& lits = s().m_trail; - literal l = lits[index + 1]; + void card_extension::get_xor_antecedents(literal l, unsigned index, justification js, literal_vector& r) { unsigned level = lvl(l); bool_var v = l.var(); - SASSERT(s().m_justification[v].get_kind() == justification::EXT_JUSTIFICATION); - SASSERT(!is_card_index(s().m_justification[v].get_ext_justification_idx())); + SASSERT(js.get_kind() == justification::EXT_JUSTIFICATION); + SASSERT(!is_card_index(js.get_ext_justification_idx())); + TRACE("sat", tout << l << ": " << js << "\n"; tout << s().m_trail << "\n";); unsigned num_marks = 0; unsigned count = 0; while (true) { ++count; - justification js = s().m_justification[v]; if (js.get_kind() == justification::EXT_JUSTIFICATION) { unsigned idx = js.get_ext_justification_idx(); if (is_card_index(idx)) { @@ -838,7 +854,7 @@ namespace sat { r.push_back(l); } while (num_marks > 0) { - l = lits[index]; + l = s().m_trail[index]; v = l.var(); unsigned n = get_parity(v); if (n > 0) { @@ -859,6 +875,7 @@ namespace sat { } --index; --num_marks; + js = s().m_justification[v]; } // now walk the defined literals @@ -874,6 +891,7 @@ namespace sat { reset_parity(lit.var()); } m_parity_trail.reset(); + TRACE("sat", tout << r << "\n";); } void card_extension::get_antecedents(literal l, ext_justification_idx idx, literal_vector & r) { @@ -1274,8 +1292,12 @@ namespace sat { } void card_extension::collect_statistics(statistics& st) const { - st.update("cardinality propagations", m_stats.m_num_propagations); - st.update("cardinality conflicts", m_stats.m_num_conflicts); + st.update("cardinality propagations", m_stats.m_num_card_propagations); + st.update("cardinality conflicts", m_stats.m_num_card_conflicts); + st.update("cardinality resolves", m_stats.m_num_card_resolves); + st.update("xor propagations", m_stats.m_num_xor_propagations); + st.update("xor conflicts", m_stats.m_num_xor_conflicts); + st.update("xor resolves", m_stats.m_num_xor_resolves); } bool card_extension::validate_conflict(card& c) { @@ -1310,6 +1332,7 @@ namespace sat { val += coeff; } } + CTRACE("sat", val >= 0, active2pb(m_A); display(tout, m_A);); return val < 0; } diff --git a/src/sat/card_extension.h b/src/sat/card_extension.h index 1c4aac29b..0d649a97c 100644 --- a/src/sat/card_extension.h +++ b/src/sat/card_extension.h @@ -30,8 +30,12 @@ namespace sat { friend class local_search; struct stats { - unsigned m_num_propagations; - unsigned m_num_conflicts; + unsigned m_num_card_propagations; + unsigned m_num_card_conflicts; + unsigned m_num_card_resolves; + unsigned m_num_xor_propagations; + unsigned m_num_xor_conflicts; + unsigned m_num_xor_resolves; stats() { reset(); } void reset() { memset(this, 0, sizeof(*this)); } }; @@ -172,7 +176,7 @@ namespace sat { bool is_card_index(unsigned idx) const { return 0 == (idx & 0x1); } card& index2card(unsigned idx) const { SASSERT(is_card_index(idx)); return *m_cards[idx >> 1]; } xor& index2xor(unsigned idx) const { SASSERT(!is_card_index(idx)); return *m_xors[idx >> 1]; } - void get_xor_antecedents(unsigned index, literal_vector& r); + void get_xor_antecedents(literal l, unsigned inddex, justification js, literal_vector& r); template diff --git a/src/sat/sat_local_search.cpp b/src/sat/sat_local_search.cpp index 3dc37471e..a93ad12c1 100644 --- a/src/sat/sat_local_search.cpp +++ b/src/sat/sat_local_search.cpp @@ -42,19 +42,21 @@ namespace sat { m_index_in_unsat_stack.resize(num_constraints(), 0); coefficient_in_ob_constraint.resize(num_vars() + 1, 0); - uint_set is_neighbor; - for (bool_var v = 0; v < num_vars(); ++v) { - is_neighbor.reset(); - bool pol = true; - var_info& vi = m_vars[v]; - for (unsigned k = 0; k < 2; pol = !pol, k++) { - for (unsigned i = 0; i < m_vars[v].m_watch[pol].size(); ++i) { - constraint const& c = m_constraints[m_vars[v].m_watch[pol][i]]; - for (unsigned j = 0; j < c.size(); ++j) { - bool_var w = c[j].var(); - if (w == v || is_neighbor.contains(w)) continue; - is_neighbor.insert(w); - vi.m_neighbors.push_back(w); + if (m_config.mode() == local_search_mode::gsat) { + uint_set is_neighbor; + for (bool_var v = 0; v < num_vars(); ++v) { + is_neighbor.reset(); + bool pol = true; + var_info& vi = m_vars[v]; + for (unsigned k = 0; k < 2; pol = !pol, k++) { + for (unsigned i = 0; i < m_vars[v].m_watch[pol].size(); ++i) { + constraint const& c = m_constraints[m_vars[v].m_watch[pol][i]]; + for (unsigned j = 0; j < c.size(); ++j) { + bool_var w = c[j].var(); + if (w == v || is_neighbor.contains(w)) continue; + is_neighbor.insert(w); + vi.m_neighbors.push_back(w); + } } } } @@ -69,7 +71,7 @@ namespace sat { void local_search::init_cur_solution() { for (unsigned v = 0; v < num_vars(); ++v) { // use bias half the time. - if (m_rand() % 100 < 50) { + if (m_rand() % 100 < 10) { m_vars[v].m_value = ((unsigned)(m_rand() % 100) < m_vars[v].m_bias); } } @@ -345,12 +347,12 @@ namespace sat { return check(0, 0); } -#define PROGRESS(tries, flips) \ - if (tries % 10 == 0 || m_unsat_stack.empty()) { \ - IF_VERBOSE(1, verbose_stream() << "(sat-local-search" \ - << " :flips " << flips \ - << " :unsat " << m_unsat_stack.size() \ - << " :time " << (timer.get_seconds() < 0.001 ? 0.0 : timer.get_seconds()) << ")\n";); \ +#define PROGRESS(tries, flips) \ + if (tries % 10 == 0 || m_unsat_stack.empty()) { \ + IF_VERBOSE(1, verbose_stream() << "(sat-local-search" \ + << " :flips " << flips \ + << " :unsat " << m_unsat_stack.size() \ + << " :time " << (timer.get_seconds() < 0.001 ? 0.0 : timer.get_seconds()) << ")\n";); \ } void local_search::walksat() { diff --git a/src/sat/sat_lookahead.h b/src/sat/sat_lookahead.h index 77e562384..420256e59 100644 --- a/src/sat/sat_lookahead.h +++ b/src/sat/sat_lookahead.h @@ -100,7 +100,8 @@ namespace sat { vector m_watches; // literal: watch structure svector m_lits; // literal: attributes. float m_weighted_new_binaries; // metric associated with current lookahead1 literal. - svector m_prefix; // var: prefix where variable participates in propagation + unsigned m_prefix; // where we are in search tree + svector m_vprefix; // var: prefix where variable participates in propagation indexed_uint_set m_freevars; svector m_search_modes; // stack of modes search_mode m_search_mode; // mode of search @@ -131,6 +132,34 @@ namespace sat { } }; + // ---------------------------------------- + // prefix updates. I use low order bits and + // skip bit 0 in a bid to reduce details. + + void flip_prefix() { + if (m_trail_lim.size() < 32) { + unsigned mask = (1 << m_trail_lim.size()); + m_prefix &= mask | (mask - 1); + } + } + + void prune_prefix() { + if (m_trail_lim.size() < 32) { + m_prefix &= (1 << m_trail_lim.size()) - 1; + } + } + + void update_prefix(literal l) { + bool_var x = l.var(); + + unsigned p = m_prefix[x].m_prefix; + if (m_prefix[x].m_length >= m_trail_lim.size() || + ((p | m_prefix) != m_prefix)) { + m_prefix[x].m_length = m_trail_lim.size(); + m_prefix[x].m_prefix = m_prefix; + } + } + // ---------------------------------------- void add_binary(literal l1, literal l2) { @@ -222,6 +251,8 @@ namespace sat { assign(v); // v \/ ~u, u \/ v => v is a unit literal } else if (add_tc1(v, u)) { + update_prefix(u); + update_prefix(v); add_binary(u, v); } } @@ -715,7 +746,7 @@ namespace sat { m_lits.push_back(lit_info()); m_lits.push_back(lit_info()); m_rating.push_back(0); - m_prefix.push_back(prefix()); + m_vprefix.push_back(prefix()); m_freevars.insert(v); } @@ -1154,7 +1185,8 @@ namespace sat { bool backtrack(literal_vector& trail) { if (trail.empty()) return false; - pop(); + pop(); + flip_prefix(); assign(~trail.back()); propagate(); trail.pop_back(); @@ -1221,6 +1253,7 @@ namespace sat { } std::ostream& display(std::ostream& out) const { + out << std::hex << "Prefix: " << m_prefix << std::dec << "\n"; display_values(out); display_binary(out); display_clauses(out); diff --git a/src/tactic/arith/card2bv_tactic.cpp b/src/tactic/arith/card2bv_tactic.cpp index 096e52981..e5a3eec80 100644 --- a/src/tactic/arith/card2bv_tactic.cpp +++ b/src/tactic/arith/card2bv_tactic.cpp @@ -48,6 +48,7 @@ public: } virtual void collect_param_descrs(param_descrs & r) { + r.insert("keep_cardinality_constraints", CPK_BOOL, "(default: true) retain cardinality constraints for solver"); } diff --git a/src/util/memory_manager.cpp b/src/util/memory_manager.cpp index 76069ce44..6bd4ec64f 100644 --- a/src/util/memory_manager.cpp +++ b/src/util/memory_manager.cpp @@ -282,6 +282,7 @@ void * memory::allocate(size_t s) { if (g_memory_thread_alloc_size > SYNCH_THRESHOLD) { synchronize_counters(true); } + return static_cast(r) + 1; // we return a pointer to the location after the extra field }