From 180b0d4ec915c84b770bb609fae4e462118cde50 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 12 Aug 2014 19:24:31 -0700 Subject: [PATCH] add sls Signed-off-by: Nikolaj Bjorner --- src/opt/pb_sls.cpp | 44 ++-------------- src/sat/sat_mus.cpp | 60 +++++++++++++++++++--- src/sat/sat_mus.h | 3 ++ src/sat/sat_sls.cpp | 96 +++++++++++++++++++++++++++++++++++ src/sat/sat_sls.h | 60 ++++++++++++++++++++++ src/sat/sat_solver.cpp | 8 ++- src/shell/dimacs_frontend.cpp | 4 +- src/test/hilbert_basis.cpp | 30 +++++++++++ 8 files changed, 252 insertions(+), 53 deletions(-) create mode 100644 src/sat/sat_sls.cpp create mode 100644 src/sat/sat_sls.h 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 e7eecfe4a..5f9154e05 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(); @@ -59,7 +61,7 @@ namespace sat { literal lit = core.back(); core.pop_back(); unsigned sz = mus.size(); - //mus.push_back(~lit); // TBD: measure + mus.push_back(~lit); // TBD: measure mus.append(core); lbool is_sat = s.check(mus.size(), mus.c_ptr()); mus.resize(sz); @@ -76,9 +78,9 @@ namespace sat { } sz = core.size(); core.append(mus); - rmr(); + measure_mr(); + // rmr(); core.resize(sz); - IF_VERBOSE(2, verbose_stream() << "(sat.mus.new " << mus << " " << core << ")\n";); break; } case l_false: @@ -86,7 +88,6 @@ namespace sat { if (new_core.contains(~lit)) { break; } - IF_VERBOSE(2, verbose_stream() << "(sat.mus.new " << new_core << ")\n";); core.reset(); for (unsigned i = 0; i < new_core.size(); ++i) { literal lit = new_core[i]; @@ -99,9 +100,27 @@ namespace sat { } TRACE("sat", tout << "new core: " << mus << "\n";); set_core(); + IF_VERBOSE(2, verbose_stream() << "(sat.mus.new " << m_core << ")\n";); 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() { model& model = s.m_model; literal lit = m_mus.back(); @@ -146,16 +165,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(); @@ -163,15 +199,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/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;