diff --git a/src/opt/pb_sls.cpp b/src/opt/pb_sls.cpp index a702b6b7b..05bdd5cf8 100644 --- a/src/opt/pb_sls.cpp +++ b/src/opt/pb_sls.cpp @@ -20,49 +20,11 @@ Notes: #include "smt_literal.h" #include "ast_pp.h" #include "th_rewriter.h" +#include "sat_sls.h" namespace smt { struct pb_sls::imp { - struct index_set { - unsigned_vector m_elems; - unsigned_vector m_index; - - unsigned num_elems() const { return m_elems.size(); } - - void reset() { m_elems.reset(); m_index.reset(); } - - bool empty() const { return m_elems.empty(); } - - bool contains(unsigned idx) const { - return - (idx < m_index.size()) && - (m_index[idx] < m_elems.size()) && - (m_elems[m_index[idx]] == idx); - } - - void insert(unsigned idx) { - m_index.reserve(idx+1); - if (!contains(idx)) { - m_index[idx] = m_elems.size(); - m_elems.push_back(idx); - } - } - - void remove(unsigned idx) { - if (!contains(idx)) return; - unsigned pos = m_index[idx]; - m_elems[pos] = m_elems.back(); - m_index[m_elems[pos]] = pos; - m_elems.pop_back(); - } - - unsigned choose(random_gen& rnd) const { - SASSERT(!empty()); - return m_elems[rnd(num_elems())]; - } - }; - struct clause { literal_vector m_lits; scoped_mpz_vector m_weights; @@ -112,8 +74,8 @@ namespace smt { expr_ref_vector m_trail; obj_map m_decl2var; // map declarations to Boolean variables. ptr_vector m_var2decl; // reverse map - index_set m_hard_false; // list of hard clauses that are false. - index_set m_soft_false; // list of soft clauses that are false. + sat::index_set m_hard_false; // list of hard clauses that are false. + sat::index_set m_soft_false; // list of soft clauses that are false. unsigned m_max_flips; // maximal number of flips unsigned m_non_greedy_percent; // percent of moves to do non-greedy style random_gen m_rng; diff --git a/src/sat/sat_mus.cpp b/src/sat/sat_mus.cpp index 835777b47..a3685869a 100644 --- a/src/sat/sat_mus.cpp +++ b/src/sat/sat_mus.cpp @@ -36,6 +36,7 @@ namespace sat { m_core.append(m_mus); s.m_core.reset(); s.m_core.append(m_core); + m_model.reset(); } lbool mus::operator()() { @@ -46,11 +47,12 @@ namespace sat { literal_vector& core = m_core; literal_vector& mus = m_mus; core.append(s.get_core()); + while (!core.empty()) { TRACE("sat", tout << "core: " << core << "\n"; - tout << "mus: " << mus << "\n";); + tout << "mus: " << mus << "\n";); if (s.m_cancel) { set_core(); @@ -76,7 +78,8 @@ namespace sat { } sz = core.size(); core.append(mus); - rmr(); + measure_mr(); + // rmr(); core.resize(sz); break; } @@ -97,10 +100,31 @@ namespace sat { } TRACE("sat", tout << "new core: " << mus << "\n";); set_core(); +<<<<<<< HEAD IF_VERBOSE(2, verbose_stream() << "(sat.mus.new " << core << ")\n";); +======= + IF_VERBOSE(2, verbose_stream() << "(sat.mus.new " << m_core << ")\n";); +>>>>>>> 180b0d4ec915c84b770bb609fae4e462118cde50 return l_true; } + void mus::measure_mr() { + model const& m2 = s.get_model(); + if (!m_model.empty()) { + unsigned n = 0; + for (unsigned i = 0; i < m_model.size(); ++i) { + if (m2[i] != m_model[i]) ++n; + } + std::cout << "model diff: " << n << " out of " << m_model.size() << "\n"; + } + m_model.reset(); + m_model.append(m2); + } + + // + // TBD: eager model rotation allows rotating the same clause + // several times with respect to different models. + // void mus::rmr() { return; #if 0 @@ -148,16 +172,33 @@ namespace sat { watch_list const& wlist = s.get_wlist(lit); watch_list::const_iterator it = wlist.begin(); watch_list::const_iterator end = wlist.end(); - for (; it != end; ++it) { + unsigned num_cand = 0; + for (; it != end && num_cand <= 1; ++it) { switch (it->get_kind()) { case watched::BINARY: + if (it->is_learned()) { + break; + } lit2 = it->get_literal(); + if (value_at(lit2, model) == l_true) { + break; + } + IF_VERBOSE(1, verbose_stream() << "(" << ~lit << " " << lit2 << ") ";); TRACE("sat", tout << ~lit << " " << lit2 << "\n";); + ++num_cand; break; case watched::TERNARY: lit2 = it->get_literal1(); lit3 = it->get_literal2(); - TRACE("sat", tout << ~lit << " " << lit2 << " " << lit3 << "\n";); + if (value_at(lit2, model) == l_true) { + break; + } + if (value_at(lit3, model) == l_true) { + break; + } + + IF_VERBOSE(1, verbose_stream() << "(" << ~lit << " " << lit2 << " " << lit3 << ") ";); + ++num_cand; break; case watched::CLAUSE: { clause_offset cls_off = it->get_clause_offset(); @@ -165,15 +206,23 @@ namespace sat { if (c.is_learned()) { break; } + ++num_cand; + IF_VERBOSE(1, verbose_stream() << c << " ";); TRACE("sat", tout << c << "\n";); break; } case watched::EXT_CONSTRAINT: TRACE("sat", tout << "external constraint - should avoid rmr\n";); - m_toswap.resize(sz); return; } } + if (num_cand > 1) { + m_toswap.resize(sz); + } + else { + IF_VERBOSE(1, verbose_stream() << "wlist size: " << num_cand << " " << m_core.size() << "\n";); + } + } } diff --git a/src/sat/sat_mus.h b/src/sat/sat_mus.h index b2643ade6..964bddfe5 100644 --- a/src/sat/sat_mus.h +++ b/src/sat/sat_mus.h @@ -24,6 +24,8 @@ namespace sat { literal_vector m_core; literal_vector m_mus; literal_vector m_toswap; + model m_model; + solver& s; public: mus(solver& s); @@ -32,6 +34,7 @@ namespace sat { private: lbool mus2(); void rmr(); + void measure_mr(); bool has_single_unsat(literal& assumption_lit); void find_swappable(literal lit); void reset(); diff --git a/src/sat/sat_sls.cpp b/src/sat/sat_sls.cpp new file mode 100644 index 000000000..128152952 --- /dev/null +++ b/src/sat/sat_sls.cpp @@ -0,0 +1,96 @@ +/*++ +Copyright (c) 2014 Microsoft Corporation + +Module Name: + + sat_sls.cpp + +Abstract: + + SLS for clauses in SAT solver + +Author: + + Nikolaj Bjorner (nbjorner) 2014-12-8 + +Notes: + +--*/ + +#include "sat_sls.h" + +namespace sat { + + bool index_set::contains(unsigned idx) const { + return + (idx < m_index.size()) && + (m_index[idx] < m_elems.size()) && + (m_elems[m_index[idx]] == idx); + } + + void index_set::insert(unsigned idx) { + m_index.reserve(idx+1); + if (!contains(idx)) { + m_index[idx] = m_elems.size(); + m_elems.push_back(idx); + } + } + + void index_set::remove(unsigned idx) { + if (!contains(idx)) return; + unsigned pos = m_index[idx]; + m_elems[pos] = m_elems.back(); + m_index[m_elems[pos]] = pos; + m_elems.pop_back(); + } + + unsigned index_set::choose(random_gen& rnd) const { + SASSERT(!empty()); + return m_elems[rnd(num_elems())]; + } + + sls::sls(solver& s): s(s) { + + } + + sls::~sls() { + + } + +#if 0 + bool_var sls::pick_flip() { + unsigned clause_idx = m_false.choose(m_rand); + clause const& c = m_clauses[clause_idx]; + unsigned result = UINT_MAX; + m_min_vars.reset(); + for (unsigned i = 0; i < c.size(); ++i) { + + } + } + + void sls::flip(bool_var v) { + + } + + bool sls::local_search() { + for (unsigned i = 0; !m_false.empty() && i < m_max_flips; ++i) { + flip(pick_flip()); + } + return m_false.empty(); + } + +#endif + + lbool sls::operator()() { +#if 0 + for (unsigned i = 0; i < m_max_tries; ++i) { + if (local_search()) { + return l_true; + } + } +#endif + return l_undef; + } + +}; + diff --git a/src/sat/sat_sls.h b/src/sat/sat_sls.h new file mode 100644 index 000000000..80f660317 --- /dev/null +++ b/src/sat/sat_sls.h @@ -0,0 +1,60 @@ +/*++ +Copyright (c) 2014 Microsoft Corporation + +Module Name: + + sat_sls.h + +Abstract: + + SLS for clauses in SAT solver + +Author: + + Nikolaj Bjorner (nbjorner) 2014-12-8 + +Notes: + +--*/ +#ifndef _SAT_SLS_H_ +#define _SAT_SLS_H_ + +#include "util.h" +#include "sat_simplifier.h" + +namespace sat { + + class index_set { + unsigned_vector m_elems; + unsigned_vector m_index; + public: + unsigned num_elems() const { return m_elems.size(); } + void reset() { m_elems.reset(); m_index.reset(); } + bool empty() const { return m_elems.empty(); } + bool contains(unsigned idx) const; + void insert(unsigned idx); + void remove(unsigned idx); + unsigned choose(random_gen& rnd) const; + }; + + class sls { + solver& s; + random_gen m_rand; + unsigned m_max_tries; + unsigned m_max_flips; + index_set m_false; + use_list m_use_list; + vector m_clauses; + public: + sls(solver& s); + ~sls(); + lbool operator()(); + private: + bool local_search(); + bool_var pick_flip(); + void flip(bool_var v); + }; + +}; + +#endif diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp index 870544d92..25ad62361 100644 --- a/src/sat/sat_solver.cpp +++ b/src/sat/sat_solver.cpp @@ -48,6 +48,8 @@ namespace sat { m_scope_lvl(0), m_params(p) { m_config.updt_params(p); + m_conflicts_since_gc = 0; + m_next_simplify = 0; } solver::~solver() { @@ -924,10 +926,8 @@ namespace sat { m_conflicts_since_restart = 0; m_restart_threshold = m_config.m_restart_initial; m_luby_idx = 1; - m_conflicts_since_gc = 0; m_gc_threshold = m_config.m_gc_initial; m_min_d_tk = 1.0; - m_next_simplify = 0; m_stopwatch.reset(); m_stopwatch.start(); m_core.reset(); @@ -1667,6 +1667,10 @@ namespace sat { } reset_unmark(old_size); if (m_config.m_minimize_core) { + // TBD: + // apply optional clause minimization by detecting subsumed literals. + // initial experiment suggests it has no effect. + m_mus(); // ignore return value on cancelation. } } diff --git a/src/shell/dimacs_frontend.cpp b/src/shell/dimacs_frontend.cpp index 879c5f212..abaa2eace 100644 --- a/src/shell/dimacs_frontend.cpp +++ b/src/shell/dimacs_frontend.cpp @@ -101,7 +101,7 @@ static void track_clauses(sat::solver const& src, sat::clause * const * end = src.end_clauses(); svector bin_clauses; src.collect_bin_clauses(bin_clauses, false); - tracking_clauses.reserve(2*src.num_vars() + (end - it) + bin_clauses.size()); + tracking_clauses.reserve(2*src.num_vars() + static_cast(end - it) + bin_clauses.size()); for (sat::bool_var v = 1; v < src.num_vars(); ++v) { if (src.value(v) != l_undef) { @@ -114,7 +114,7 @@ static void track_clauses(sat::solver const& src, for (; it != end; ++it) { lits.reset(); sat::clause& cls = *(*it); - lits.append(cls.end()-cls.begin(), cls.begin()); + lits.append(static_cast(cls.end()-cls.begin()), cls.begin()); track_clause(dst, lits, assumptions, tracking_clauses); } for (unsigned i = 0; i < bin_clauses.size(); ++i) { diff --git a/src/tactic/arith/card2bv_tactic.cpp b/src/tactic/arith/card2bv_tactic.cpp index a433dd307..ea4bd4aed 100644 --- a/src/tactic/arith/card2bv_tactic.cpp +++ b/src/tactic/arith/card2bv_tactic.cpp @@ -22,6 +22,7 @@ Notes: #include"ast_smt2_pp.h" #include"expr_substitution.h" #include"card2bv_tactic.h" +#include"pb_rewriter.h" namespace pb { unsigned card2bv_rewriter::get_num_bits(func_decl* f) { @@ -58,43 +59,8 @@ namespace pb { return BR_DONE; } else if (f->get_family_id() == pb.get_family_id()) { - expr_ref zero(m), a(m), b(m); - expr_ref_vector es(m); - unsigned bw = get_num_bits(f); - zero = bv.mk_numeral(rational(0), bw); - for (unsigned i = 0; i < sz; ++i) { - es.push_back(m.mk_ite(args[i], bv.mk_numeral(pb.get_coeff(f, i), bw), zero)); - } - switch (es.size()) { - case 0: a = zero; break; - case 1: a = es[0].get(); break; - default: - a = es[0].get(); - for (unsigned i = 1; i < es.size(); ++i) { - a = bv.mk_bv_add(a, es[i].get()); - } - break; - } - b = bv.mk_numeral(pb.get_k(f), bw); - - switch (f->get_decl_kind()) { - case OP_AT_MOST_K: - case OP_PB_LE: - UNREACHABLE(); - result = bv.mk_ule(a, b); - return BR_DONE; - case OP_AT_LEAST_K: - UNREACHABLE(); - case OP_PB_GE: - result = bv.mk_ule(b, a); - return BR_DONE; - case OP_PB_EQ: - result = m.mk_eq(a, b); - return BR_DONE; - default: - UNREACHABLE(); - } - return BR_FAILED; + // return mk_shannon(f, sz, args, result); + return mk_bv(f, sz, args, result); } // NSB: review // we should remove this code and rely on a layer above to deal with @@ -136,6 +102,62 @@ namespace pb { return BR_FAILED; } + + br_status card2bv_rewriter::mk_bv(func_decl * f, unsigned sz, expr * const* args, expr_ref & result) { + expr_ref zero(m), a(m), b(m); + expr_ref_vector es(m); + unsigned bw = get_num_bits(f); + zero = bv.mk_numeral(rational(0), bw); + for (unsigned i = 0; i < sz; ++i) { + es.push_back(m.mk_ite(args[i], bv.mk_numeral(pb.get_coeff(f, i), bw), zero)); + } + switch (es.size()) { + case 0: a = zero; break; + case 1: a = es[0].get(); break; + default: + a = es[0].get(); + for (unsigned i = 1; i < es.size(); ++i) { + a = bv.mk_bv_add(a, es[i].get()); + } + break; + } + b = bv.mk_numeral(pb.get_k(f), bw); + + switch (f->get_decl_kind()) { + case OP_AT_MOST_K: + case OP_PB_LE: + UNREACHABLE(); + result = bv.mk_ule(a, b); + break; + case OP_AT_LEAST_K: + UNREACHABLE(); + case OP_PB_GE: + result = bv.mk_ule(b, a); + break; + case OP_PB_EQ: + result = m.mk_eq(a, b); + break; + default: + UNREACHABLE(); + } + return BR_DONE; + } + + br_status card2bv_rewriter::mk_shannon(func_decl * f, unsigned sz, expr * const* args, expr_ref & result) { + pb_rewriter rw(m); + if (sz == 0) { + rw.mk_app_core(f, sz, args, result); + return BR_DONE; + } + expr_ref r1(m), r2(m); + ptr_vector new_args(sz, args); + new_args[0] = m.mk_true(); + rw.mk_app_core(f, sz, new_args.c_ptr(), r1); + new_args[0] = m.mk_false(); + rw.mk_app_core(f, sz, new_args.c_ptr(), r2); + result = m.mk_ite(args[0], r1, r2); + return BR_REWRITE_FULL; + } }; template class rewriter_tpl; diff --git a/src/tactic/arith/card2bv_tactic.h b/src/tactic/arith/card2bv_tactic.h index 90bafbf53..e1fa6dbde 100644 --- a/src/tactic/arith/card2bv_tactic.h +++ b/src/tactic/arith/card2bv_tactic.h @@ -35,6 +35,8 @@ namespace pb { pb_util pb; bv_util bv; unsigned get_num_bits(func_decl* f); + br_status mk_bv(func_decl * f, unsigned sz, expr * const* args, expr_ref & result); + br_status mk_shannon(func_decl * f, unsigned sz, expr * const* args, expr_ref & result); public: card2bv_rewriter(ast_manager& m); br_status mk_app_core(func_decl * f, unsigned sz, expr * const* args, expr_ref & result); diff --git a/src/test/hilbert_basis.cpp b/src/test/hilbert_basis.cpp index 4752dd78d..60af1eae8 100644 --- a/src/test/hilbert_basis.cpp +++ b/src/test/hilbert_basis.cpp @@ -540,6 +540,33 @@ static void tst19() { saturate_basis(hb); } +static void test_A_5_5_3() { + hilbert_basis hb; + for (unsigned i = 0; i < 15; ++i) { + vector v; + for (unsigned j = 0; j < 5; ++j) { + for (unsigned k = 0; k < 15; ++k) { + v.push_back(rational(k == i)); + } + } + hb.add_ge(v, R(0)); + } + for (unsigned i = 1; i <= 15; ++i) { + vector v; + for (unsigned k = 1; k <= 5; ++k) { + for (unsigned l = 1; l <= 5; ++l) { + for (unsigned j = 1; j <= 3; ++j) { + bool one = ((j*k <= i) && (((i - j) % 3) == 0); // fixme + v.push_back(rational(one)); + } + } + } + hb.add_ge(v, R(0)); + } + // etc. + saturate_basis(hb); +} + void tst_hilbert_basis() { std::cout << "hilbert basis test\n"; // tst3(); @@ -547,6 +574,9 @@ void tst_hilbert_basis() { g_use_ordered_support = true; + test_A_5_5_3(); + return; + tst18(); return;