From bc6b3007de3727a284cf5f19c268d52cf4e75313 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 13 Jan 2017 20:53:22 -0800 Subject: [PATCH] remove unused features related to weighted check-sat Signed-off-by: Nikolaj Bjorner --- contrib/cmake/src/sat/CMakeLists.txt | 2 - src/opt/maxres.cpp | 12 +- src/opt/pb_sls.cpp | 46 +- src/sat/sat_bceq.cpp | 530 -------------------- src/sat/sat_bceq.h | 89 ---- src/sat/sat_config.cpp | 2 - src/sat/sat_config.h | 2 - src/sat/sat_mus.cpp | 37 +- src/sat/sat_mus.h | 2 - src/sat/sat_params.pyg | 2 - src/sat/sat_sls.cpp | 686 -------------------------- src/sat/sat_sls.h | 115 ----- src/sat/sat_solver.cpp | 143 +----- src/sat/sat_solver.h | 16 +- src/sat/sat_solver/inc_sat_solver.cpp | 29 +- src/sat/sat_solver/inc_sat_solver.h | 1 - 16 files changed, 58 insertions(+), 1656 deletions(-) delete mode 100644 src/sat/sat_bceq.cpp delete mode 100644 src/sat/sat_bceq.h delete mode 100644 src/sat/sat_sls.cpp delete mode 100644 src/sat/sat_sls.h diff --git a/contrib/cmake/src/sat/CMakeLists.txt b/contrib/cmake/src/sat/CMakeLists.txt index cfc3835c1..3eec21ec3 100644 --- a/contrib/cmake/src/sat/CMakeLists.txt +++ b/contrib/cmake/src/sat/CMakeLists.txt @@ -2,7 +2,6 @@ z3_add_component(sat SOURCES dimacs.cpp sat_asymm_branch.cpp - sat_bceq.cpp sat_clause.cpp sat_clause_set.cpp sat_clause_use_list.cpp @@ -16,7 +15,6 @@ z3_add_component(sat sat_probing.cpp sat_scc.cpp sat_simplifier.cpp - sat_sls.cpp sat_solver.cpp sat_watched.cpp COMPONENT_DEPENDENCIES diff --git a/src/opt/maxres.cpp b/src/opt/maxres.cpp index 54e7f351c..83f0849b2 100644 --- a/src/opt/maxres.cpp +++ b/src/opt/maxres.cpp @@ -302,17 +302,7 @@ public: } lbool check_sat(unsigned sz, expr* const* asms) { - if (m_st == s_primal_dual && m_c.sat_enabled()) { - rational max_weight = m_upper; - vector weights; - for (unsigned i = 0; i < sz; ++i) { - weights.push_back(get_weight(asms[i])); - } - return inc_sat_check_sat(s(), sz, asms, weights.c_ptr(), max_weight); - } - else { - return s().check_sat(sz, asms); - } + return s().check_sat(sz, asms); } void found_optimum() { diff --git a/src/opt/pb_sls.cpp b/src/opt/pb_sls.cpp index 95b489394..32c144652 100644 --- a/src/opt/pb_sls.cpp +++ b/src/opt/pb_sls.cpp @@ -20,9 +20,49 @@ Notes: #include "smt_literal.h" #include "ast_pp.h" #include "th_rewriter.h" -#include "sat_sls.h" +#include "sat_types.h" namespace smt { + + class index_set { + + unsigned_vector m_elems; + unsigned_vector m_index; + public: + unsigned num_elems() const { return m_elems.size(); } + unsigned operator[](unsigned idx) const { return m_elems[idx]; } + 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 pb_sls::imp { struct clause { @@ -73,8 +113,8 @@ namespace smt { expr_ref_vector m_trail; obj_map m_decl2var; // map declarations to Boolean variables. ptr_vector m_var2decl; // reverse map - 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. + index_set m_hard_false; // list of hard clauses that are false. + 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_bceq.cpp b/src/sat/sat_bceq.cpp deleted file mode 100644 index fa0309327..000000000 --- a/src/sat/sat_bceq.cpp +++ /dev/null @@ -1,530 +0,0 @@ -/*++ -Copyright (c) 2014 Microsoft Corporation - -Module Name: - - sat_bceq.cpp - -Abstract: - - Find equivalent literals based on blocked clause decomposition. - -Author: - - Nikolaj Bjorner (nbjorner) 2014-09-27. - - -Revision History: - ---*/ -#include"sat_bceq.h" -#include"sat_solver.h" -#include"trace.h" -#include"bit_vector.h" -#include"map.h" -#include"sat_elim_eqs.h" - -namespace sat { - - void bceq::use_list::init(unsigned num_vars) { - m_clauses.reset(); - m_clauses.resize(2*num_vars); - } - - void bceq::use_list::insert(clause& c) { - unsigned sz = c.size(); - for (unsigned i = 0; i < sz; i++) { - m_clauses[c[i].index()].push_back(&c); - } - } - - void bceq::use_list::erase(clause& c) { - unsigned sz = c.size(); - for (unsigned i = 0; i < sz; i++) { - m_clauses[c[i].index()].erase(&c); - } - } - - ptr_vector& bceq::use_list::get(literal lit) { - return m_clauses[lit.index()]; - } - - bceq::bceq(solver & s): - m_solver(s) { - } - - void bceq::register_clause(clause* cls) { - m_clauses.setx(cls->id(), cls, 0); - } - - void bceq::unregister_clause(clause* cls) { - m_clauses.setx(cls->id(), 0, 0); - } - - void bceq::init() { - m_clauses.reset(); - m_bin_clauses.reset(); - m_L.reset(); - m_R.reset(); - m_L_blits.reset(); - m_R_blits.reset(); - m_bce_use_list.reset(); - clause * const* it = m_solver.begin_clauses(); - clause * const* end = m_solver.end_clauses(); - for (; it != end; ++it) { - clause* cls = *it; - if (!cls->was_removed()) { - m_use_list->insert(*cls); - register_clause(cls); - } - } - bin_clauses bc; - m_solver.collect_bin_clauses(bc, false); // exclude roots. - literal lits[2]; - for (unsigned i = 0; i < bc.size(); ++i) { - lits[0] = bc[i].first; - lits[1] = bc[i].second; - clause* cls = m_solver.m_cls_allocator.mk_clause(2, lits, false); - m_use_list->insert(*cls); - m_bin_clauses.push_back(cls); - register_clause(cls); - } - TRACE("sat", - for (unsigned i = 0; i < m_clauses.size(); ++i) { - clause const* cls = m_clauses[i]; - if (cls) tout << *cls << "\n"; - }); - } - - void bceq::pure_decompose() { - // while F != empty - // pick a clause and variable x in clause. - // get use list U1 of x and U2 of ~x - // assume |U1| >= |U2| - // add U1 to clause set. - for (unsigned i = 0; i < m_clauses.size(); ++i) { - clause* cls = m_clauses[i]; - if (cls) { - SASSERT(i == cls->id()); - pure_decompose((*cls)[0]); - SASSERT(!m_clauses[i]); - } - } - m_L.reverse(); - m_L_blits.reverse(); - } - - void bceq::pure_decompose(literal lit) { - clause_use_list& pos = m_use_list->get(lit); - clause_use_list& neg = m_use_list->get(~lit); - unsigned sz1 = m_L.size(); - unsigned sz2 = m_R.size(); - pure_decompose(pos, m_L); - pure_decompose(neg, m_R); - unsigned delta1 = m_L.size() - sz1; - unsigned delta2 = m_R.size() - sz2; - if (delta1 < delta2) { - m_L_blits.resize(sz1+delta2, ~lit); - m_R_blits.resize(sz2+delta1, lit); - for (unsigned i = 0; i < delta1; ++i) { - std::swap(m_L[sz1 + i], m_R[sz2 + i]); - } - for (unsigned i = delta1; i < delta2; ++i) { - m_L.push_back(m_R[sz2 + i]); - } - m_R.resize(sz2 + delta1); - std::swap(delta1, delta2); - } - else { - m_L_blits.resize(sz1+delta1, lit); - m_R_blits.resize(sz2+delta2, ~lit); - } - TRACE("bceq", tout << lit << " " << "pos: " << delta1 << " " << "neg: " << delta2 << "\n";); - } - - void bceq::pure_decompose(clause_use_list& uses, svector& clauses) { - unsigned sz = uses.size(); - for (unsigned i = 0; i < sz; ++i) { - clause& cls = *uses[i]; - if (!cls.was_removed() && m_clauses[cls.id()]) { - clauses.push_back(&cls); - m_clauses[cls.id()] = 0; - } - } - } - - void bceq::post_decompose() { - m_marked.reset(); - m_marked.resize(2*m_solver.num_vars(), false); - use_list ul; - use_list* save = m_use_list; - m_use_list = &ul; - ul.init(m_solver.num_vars()); - for (unsigned i = 0; i < m_L.size(); ++i) { - ul.insert(*m_L[i]); - } - - // cheap pass: add clauses from R in order - // such that they are blocked with respect to - // predecessors. - m_removed.reset(); - for (unsigned i = 0; i < m_R.size(); ++i) { - literal lit = find_blocked(*m_R[i]); - if (lit != null_literal) { - m_L.push_back(m_R[i]); - m_L_blits.push_back(lit); - ul.insert(*m_R[i]); - m_R[i] = m_R.back(); - m_R_blits[i] = m_R_blits.back(); - m_R.pop_back(); - m_R_blits.pop_back(); - --i; - } - } - // expensive pass: add clauses from R as long - // as BCE produces the empty set of clauses. - m_bce_use_list.init(m_solver.num_vars()); - for (unsigned i = 0; i < m_L.size(); ++i) { - m_bce_use_list.insert(*m_L[i]); - } - for (unsigned i = 0; i < m_R.size(); ++i) { - if (bce(*m_R[i])) { - m_R[i] = m_R.back(); - m_R_blits[i] = m_R_blits.back(); - m_R.pop_back(); - m_R_blits.pop_back(); - --i; - } - } - m_use_list = save; - } - - - // Note: replay blocked clause elimination: - // Suppose C u { c1 } is blocked. - // annotate each clause by blocking literal. - // for new clause c2, check if C u { c2 } is blocked. - // For each c in C record which literal it is blocked. - // (Order the clauses in C by block ordering) - // l | c is blocked, - // -> c2 contains ~l => check if c c2 is blocked - // - bool bceq::bce(clause& cls0) { - IF_VERBOSE(1, verbose_stream() << "bce " << m_L.size() << " " << m_R.size() << " " << cls0 << "\n";); - unsigned_vector& live_clauses = m_live_clauses; - live_clauses.reset(); - m_use_list = &m_bce_use_list; - m_bce_use_list.insert(cls0); - svector& clauses = m_L; - literal_vector& blits = m_L_blits; - clauses.push_back(&cls0); - blits.push_back(null_literal); - bool removed = false; - m_removed.reset(); - for (unsigned i = 0; i < clauses.size(); ++i) { - clause& cls1 = *clauses[i]; - literal lit = find_blocked(cls1); - if (lit == null_literal) { - live_clauses.push_back(i); - } - else { - m_removed.setx(cls1.id(), true, false); - removed = true; - } - } - while (removed) { - removed = false; - //std::cout << live_clauses.size() << " "; - for (unsigned i = 0; i < live_clauses.size(); ++i) { - clause& cls1 = *clauses[live_clauses[i]]; - literal lit = find_blocked(cls1); - if (lit != null_literal) { - m_removed.setx(cls1.id(), true, false); - removed = true; - live_clauses[i] = live_clauses.back(); - live_clauses.pop_back(); - --i; - } - } - } - //std::cout << "\n"; - m_bce_use_list.erase(cls0); - clauses.pop_back(); - blits.pop_back(); - return live_clauses.empty(); - } - - literal bceq::find_blocked(clause const& cls) { - TRACE("bceq", tout << cls << "\n";); - - unsigned sz = cls.size(); - for (unsigned i = 0; i < sz; ++i) { - m_marked[(~cls[i]).index()] = true; - } - literal result = null_literal; - for (unsigned i = 0; i < sz; ++i) { - literal lit = cls[i]; - if (is_blocked(lit)) { - TRACE("bceq", tout << "is blocked " << lit << " : " << cls << "\n";); - result = lit; - break; - } - } - for (unsigned i = 0; i < sz; ++i) { - m_marked[(~cls[i]).index()] = false; - } - return result; - } - - bool bceq::is_blocked(literal lit) const { - clause_use_list& uses = m_use_list->get(~lit); - unsigned sz = uses.size(); - for (unsigned i = 0; i < sz; ++i) { - clause const& cls = *uses[i]; - unsigned sz = cls.size(); - bool is_axiom = m_removed.get(cls.id(), false); - for (unsigned i = 0; !is_axiom && i < sz; ++i) { - is_axiom = m_marked[cls[i].index()] && cls[i] != ~lit; - } - - TRACE("bceq", tout << "resolvent " << lit << " : " << cls << " " << (is_axiom?"axiom":"non-axiom") << "\n";); - if (!is_axiom) { - return false; - } - } - return true; - } - - - void bceq::init_rbits() { - m_rbits.reset(); - for (unsigned i = 0; i < m_solver.num_vars(); ++i) { - uint64 lo = m_rand() + (m_rand() << 16); - uint64 hi = m_rand() + (m_rand() << 16); - m_rbits.push_back(lo + (hi << 32ULL)); - } - } - - void bceq::init_reconstruction_stack() { - m_rstack.reset(); - m_bstack.reset(); - // decomposition already creates a blocked stack in the proper order. - m_rstack.append(m_L); - m_bstack.append(m_L_blits); - } - - uint64 bceq::eval_clause(clause const& cls) const { - uint64 b = 0; - unsigned sz = cls.size(); - for (unsigned i = 0; i < sz; ++i) { - literal lit = cls[i]; - uint64 val = m_rbits[lit.var()]; - if (lit.sign()) { - val = ~val; - } - b |= val; - } - return b; - } - - void bceq::sat_sweep() { - init_rbits(); - init_reconstruction_stack(); - for (unsigned i = 0; i < m_rstack.size(); ++i) { - clause const& cls = *m_rstack[i]; - literal block_lit = m_bstack[i]; - uint64 b = eval_clause(cls); - // v = 0, b = 0 -> v := 1 - // v = 0, b = 1 -> v := 0 - // v = 1, b = 0 -> v := 0 - // v = 1, b = 1 -> v := 1 - m_rbits[block_lit.var()] ^= ~b; - - } - DEBUG_CODE(verify_sweep();); - } - - void bceq::verify_sweep() { - DEBUG_CODE( - for (unsigned i = 0; i < m_L.size(); ++i) { - uint64 b = eval_clause(*m_L[i]); - SASSERT((~b) == 0); - }); - } - - struct u64_hash { unsigned operator()(uint64 u) const { return (unsigned)u; } }; - - struct u64_eq { bool operator()(uint64 u1, uint64 u2) const { return u1 == u2; } }; - - void bceq::extract_partition() { - unsigned num_vars = m_solver.num_vars(); - map table; - union_find<> union_find(m_union_find_ctx); - for (unsigned i = 0; i < num_vars; ++i) { - m_s->mk_var(true, true); - union_find.mk_var(); - } - for (unsigned i = 0; i < m_L.size(); ++i) { - m_s->mk_clause(m_L[i]->size(), m_L[i]->begin()); - } - for (unsigned i = 0; i < num_vars; ++i) { - uint64 val = m_rbits[i]; - unsigned index; - if (table.find(val, index)) { - union_find.merge(i, index); - } - else if (table.find(~val, index)) { - union_find.merge(i, index); - } - else { - table.insert(val, i); - } - } - TRACE("sat", union_find.display(tout);); - - // - // Preliminary version: - // A more appropriate is to walk each pair, - // and refine partition based on SAT results. - // - for (unsigned i = 0; i < num_vars; ++i) { - if (!union_find.is_root(i)) continue; - unsigned v = union_find.next(i); - unsigned last_v = UINT_MAX; - if (!m_solver.was_eliminated(i)) { - last_v = i; - } - while (v != i) { - if (!m_solver.was_eliminated(v)) { - if (last_v != UINT_MAX) { - if (check_equality(v, last_v)) { - // last_v was eliminated. - - } - else { - // TBD: refine partition. - } - } - last_v = v; - } - v = union_find.next(v); - } - } - } - - bool bceq::check_equality(unsigned v1, unsigned v2) { - TRACE("sat", tout << "check: " << v1 << " = " << v2 << "\n";); - uint64 val1 = m_rbits[v1]; - uint64 val2 = m_rbits[v2]; - literal l1 = literal(v1, false); - literal l2 = literal(v2, false); - if (val1 != val2) { - SASSERT(val1 == ~val2); - l2.neg(); - } - if (is_already_equiv(l1, l2)) { - TRACE("sat", tout << "Already equivalent: " << l1 << " " << l2 << "\n";); - return false; - } - - literal lits[2]; - lits[0] = l1; - lits[1] = ~l2; - lbool is_sat = m_s->check(2, lits); - if (is_sat == l_false) { - lits[0] = ~l1; - lits[1] = l2; - is_sat = m_s->check(2, lits); - } - if (is_sat == l_false) { - TRACE("sat", tout << "Found equivalent: " << l1 << " " << l2 << "\n";); - assert_equality(l1, l2); - } - else { - TRACE("sat", tout << "Not equivalent: " << l1 << " " << l2 << "\n";); - // TBD: if is_sat == l_true, then refine partition. - } - return is_sat == l_false; - } - - bool bceq::is_already_equiv(literal l1, literal l2) { - watch_list const& w1 = m_solver.get_wlist(l1); - bool found = false; - for (unsigned i = 0; !found && i < w1.size(); ++i) { - watched const& w = w1[i]; - found = w.is_binary_clause() && w.get_literal() == ~l2; - } - if (!found) return false; - found = false; - watch_list const& w2 = m_solver.get_wlist(~l1); - for (unsigned i = 0; !found && i < w2.size(); ++i) { - watched const& w = w2[i]; - found = w.is_binary_clause() && w.get_literal() == l2; - } - return found; - } - - void bceq::assert_equality(literal l1, literal l2) { - if (l2.sign()) { - l1.neg(); - l2.neg(); - } - literal_vector roots; - bool_var_vector vars; - for (unsigned i = 0; i < m_solver.num_vars(); ++i) { - roots.push_back(literal(i, false)); - } - roots[l2.var()] = l1; - vars.push_back(l2.var()); - elim_eqs elim(m_solver); - IF_VERBOSE(1, - for (unsigned i = 0; i < vars.size(); ++i) { - verbose_stream() << "var: " << vars[i] << " root: " << roots[vars[i]] << "\n"; - }); - elim(roots, vars); - } - - void bceq::cleanup() { - m_solver.del_clauses(m_bin_clauses.begin(), m_bin_clauses.end()); - m_bin_clauses.reset(); - } - - - void bceq::operator()() { - if (!m_solver.m_config.m_bcd) return; - flet _disable_bcd(m_solver.m_config.m_bcd, false); - flet _disable_min(m_solver.m_config.m_core_minimize, false); - flet _disable_opt(m_solver.m_config.m_optimize_model, false); - flet _bound_maxc(m_solver.m_config.m_max_conflicts, 1500); - - use_list ul; - solver s(m_solver.m_params, m_solver.rlimit(), 0); - s.m_config.m_bcd = false; - s.m_config.m_core_minimize = false; - s.m_config.m_optimize_model = false; - s.m_config.m_max_conflicts = 1500; - m_use_list = &ul; - m_s = &s; - ul.init(m_solver.num_vars()); - init(); - pure_decompose(); - post_decompose(); - IF_VERBOSE(1, verbose_stream() << "Decomposed set " << m_L.size() << " rest: " << m_R.size() << "\n";); - - TRACE("sat", - tout << "Decomposed set " << m_L.size() << "\n"; - for (unsigned i = 0; i < m_L.size(); ++i) { - clause const* cls = m_L[i]; - if (cls) tout << *cls << "\n"; - } - tout << "remainder " << m_R.size() << "\n"; - for (unsigned i = 0; i < m_R.size(); ++i) { - clause const* cls = m_R[i]; - if (cls) tout << *cls << "\n"; - } - ); - sat_sweep(); - extract_partition(); - cleanup(); - } -}; diff --git a/src/sat/sat_bceq.h b/src/sat/sat_bceq.h deleted file mode 100644 index c9d01e78b..000000000 --- a/src/sat/sat_bceq.h +++ /dev/null @@ -1,89 +0,0 @@ -/*++ -Copyright (c) 2014 Microsoft Corporation - -Module Name: - - sat_bceq.h - -Abstract: - - Find equivalent literals based on blocked clause decomposition. - -Author: - - Nikolaj Bjorner (nbjorner) 2014-09-27. - -Revision History: - ---*/ -#ifndef SAT_BCEQ_H_ -#define SAT_BCEQ_H_ - -#include"sat_types.h" -#include"union_find.h" - - -namespace sat { - class solver; - - class bceq { - typedef ptr_vector clause_use_list; - class use_list { - vector > m_clauses; - public: - use_list() {} - void init(unsigned num_vars); - void reset() { m_clauses.reset(); } - void erase(clause& c); - void insert(clause& c); - ptr_vector& get(literal lit); - }; - typedef std::pair bin_clause; - typedef svector bin_clauses; - solver & m_solver; - use_list* m_use_list; - use_list m_bce_use_list; - solver* m_s; - random_gen m_rand; - svector m_clauses; - svector m_L; - svector m_R; - literal_vector m_L_blits; - literal_vector m_R_blits; - svector m_bin_clauses; - svector m_rbits; - svector m_rstack; // stack of blocked clauses - literal_vector m_bstack; // stack of blocking literals - svector m_marked; - svector m_removed; // set of clauses removed (not considered in clause set during BCE) - union_find_default_ctx m_union_find_ctx; - unsigned_vector m_live_clauses; - - void init(); - void register_clause(clause* cls); - void unregister_clause(clause* cls); - void pure_decompose(); - void pure_decompose(literal lit); - void pure_decompose(ptr_vector& uses, svector& clauses); - void post_decompose(); - literal find_blocked(clause const& cls); - bool bce(clause& cls); - bool is_blocked(literal lit) const; - void init_rbits(); - void init_reconstruction_stack(); - void sat_sweep(); - void cleanup(); - uint64 eval_clause(clause const& cls) const; - void verify_sweep(); - void extract_partition(); - bool check_equality(unsigned v1, unsigned v2); - bool is_already_equiv(literal l1, literal l2); - void assert_equality(literal l1, literal l2); - public: - bceq(solver & s); - void operator()(); - }; - -}; - -#endif diff --git a/src/sat/sat_config.cpp b/src/sat/sat_config.cpp index 7e0a7c50c..4e01bfe55 100644 --- a/src/sat/sat_config.cpp +++ b/src/sat/sat_config.cpp @@ -111,8 +111,6 @@ namespace sat { m_minimize_lemmas = p.minimize_lemmas(); m_core_minimize = p.core_minimize(); m_core_minimize_partial = p.core_minimize_partial(); - m_optimize_model = p.optimize_model(); - m_bcd = p.bcd(); m_dyn_sub_res = p.dyn_sub_res(); } diff --git a/src/sat/sat_config.h b/src/sat/sat_config.h index 1cdabddef..910ca0360 100644 --- a/src/sat/sat_config.h +++ b/src/sat/sat_config.h @@ -72,8 +72,6 @@ namespace sat { bool m_dyn_sub_res; bool m_core_minimize; bool m_core_minimize_partial; - bool m_optimize_model; - bool m_bcd; symbol m_always_true; diff --git a/src/sat/sat_mus.cpp b/src/sat/sat_mus.cpp index 7b3277b6c..380b8ee94 100644 --- a/src/sat/sat_mus.cpp +++ b/src/sat/sat_mus.cpp @@ -20,11 +20,10 @@ Notes: #include "sat_solver.h" #include "sat_mus.h" -#include "sat_sls.h" namespace sat { - mus::mus(solver& s):s(s), m_is_active(false), m_best_value(0), m_restart(0), m_max_restarts(0) {} + mus::mus(solver& s):s(s), m_is_active(false),m_restart(0), m_max_restarts(0) {} mus::~mus() {} @@ -32,7 +31,6 @@ namespace sat { m_core.reset(); m_mus.reset(); m_model.reset(); - m_best_value = 0; m_max_restarts = (s.m_stats.m_restart - m_restart) + 10; m_restart = s.m_stats.m_restart; } @@ -45,21 +43,13 @@ namespace sat { } void mus::update_model() { - double new_value = s.m_wsls.evaluate_model(s.m_model); if (m_model.empty()) { m_model.append(s.m_model); - m_best_value = new_value; - } - else if (m_best_value > new_value) { - m_model.reset(); - m_model.append(s.m_model); - m_best_value = new_value; } } lbool mus::operator()() { flet _disable_min(s.m_config.m_core_minimize, false); - flet _disable_opt(s.m_config.m_optimize_model, false); flet _is_active(m_is_active, true); IF_VERBOSE(3, verbose_stream() << "(sat.mus " << s.get_core() << ")\n";); reset(); @@ -120,9 +110,6 @@ namespace sat { SASSERT(value_at(lit, s.get_model()) == l_false); mus.push_back(lit); update_model(); - if (!core.empty()) { - // mr(); // TBD: measure - } break; } case l_false: @@ -262,27 +249,5 @@ namespace sat { IF_VERBOSE(3, verbose_stream() << "core verification: " << is_sat << " " << core << "\n";); } - void mus::mr() { - sls sls(s); - literal_vector tabu; - tabu.append(m_mus); - tabu.append(m_core); - bool reuse_model = false; - for (unsigned i = m_mus.size(); i < tabu.size(); ++i) { - tabu[i] = ~tabu[i]; - lbool is_sat = sls(tabu.size(), tabu.c_ptr(), reuse_model); - tabu[i] = ~tabu[i]; - if (is_sat == l_true) { - m_mus.push_back(tabu[i]); - m_core.erase(tabu[i]); - IF_VERBOSE(3, verbose_stream() << "in core " << tabu[i] << "\n";); - reuse_model = true; - } - else { - IF_VERBOSE(3, verbose_stream() << "NOT in core " << tabu[i] << "\n";); - reuse_model = false; - } - } - } } diff --git a/src/sat/sat_mus.h b/src/sat/sat_mus.h index 617bbc757..74f6d75f0 100644 --- a/src/sat/sat_mus.h +++ b/src/sat/sat_mus.h @@ -26,7 +26,6 @@ namespace sat { literal_vector m_mus; bool m_is_active; model m_model; // model obtained during minimal unsat core - double m_best_value; unsigned m_restart; unsigned m_max_restarts; @@ -41,7 +40,6 @@ namespace sat { lbool mus1(); lbool mus2(); lbool qx(literal_set& assignment, literal_set& support, bool has_support); - void mr(); void reset(); void set_core(); void update_model(); diff --git a/src/sat/sat_params.pyg b/src/sat/sat_params.pyg index de1759486..21a50bea2 100644 --- a/src/sat/sat_params.pyg +++ b/src/sat/sat_params.pyg @@ -22,6 +22,4 @@ def_module_params('sat', ('dyn_sub_res', BOOL, True, 'dynamic subsumption resolution for minimizing learned clauses'), ('core.minimize', BOOL, False, 'minimize computed core'), ('core.minimize_partial', BOOL, False, 'apply partial (cheap) core minimization'), - ('optimize_model', BOOL, False, 'enable optimization of soft constraints'), - ('bcd', BOOL, False, 'enable blocked clause decomposition for equality extraction'), ('dimacs.core', BOOL, False, 'extract core from DIMACS benchmarks'))) diff --git a/src/sat/sat_sls.cpp b/src/sat/sat_sls.cpp deleted file mode 100644 index 7efc0ce0b..000000000 --- a/src/sat/sat_sls.cpp +++ /dev/null @@ -1,686 +0,0 @@ -/*++ -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" -#include "sat_solver.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) { - m_prob_choose_min_var = 43; - m_clause_generation = 0; - } - - sls::~sls() { - for (unsigned i = 0; i < m_bin_clauses.size(); ++i) { - m_alloc.del_clause(m_bin_clauses[i]); - } - } - - lbool sls::operator()(unsigned sz, literal const* tabu, bool reuse_model) { - init(sz, tabu, reuse_model); - unsigned i; - for (i = 0; !m_false.empty() && !s.canceled() && i < m_max_tries; ++i) { - flip(); - } - IF_VERBOSE(2, verbose_stream() << "tries " << i << "\n";); - if (m_false.empty()) { - SASSERT(s.check_model(m_model)); - return l_true; - } - return l_undef; - } - - void sls::init(unsigned sz, literal const* tabu, bool reuse_model) { - bool same_generation = (m_clause_generation == s.m_stats.m_non_learned_generation); - if (!same_generation) { - init_clauses(); - init_use(); - IF_VERBOSE(0, verbose_stream() << s.m_stats.m_non_learned_generation << " " << m_clause_generation << "\n";); - } - if (!reuse_model) { - init_model(); - } - init_tabu(sz, tabu); - m_clause_generation = s.m_stats.m_non_learned_generation; - - m_max_tries = 10*(s.num_vars() + m_clauses.size()); - - } - - void sls::init_clauses() { - for (unsigned i = 0; i < m_bin_clauses.size(); ++i) { - m_alloc.del_clause(m_bin_clauses[i]); - } - m_bin_clauses.reset(); - m_clauses.reset(); - clause * const * it = s.begin_clauses(); - clause * const * end = s.end_clauses(); - for (; it != end; ++it) { - m_clauses.push_back(*it); - } - svector bincs; - s.collect_bin_clauses(bincs, false); - literal lits[2]; - for (unsigned i = 0; i < bincs.size(); ++i) { - lits[0] = bincs[i].first; - lits[1] = bincs[i].second; - clause* cl = m_alloc.mk_clause(2, lits, false); - m_clauses.push_back(cl); - m_bin_clauses.push_back(cl); - } - } - - void sls::init_model() { - m_num_true.reset(); - m_model.reset(); - m_model.append(s.get_model()); - unsigned sz = m_clauses.size(); - for (unsigned i = 0; i < sz; ++i) { - clause const& c = *m_clauses[i]; - unsigned n = 0; - unsigned csz = c.size(); - for (unsigned j = 0; j < csz; ++j) { - lbool val = value_at(c[j], m_model); - switch (val) { - case l_true: - ++n; - break; - case l_undef: - ++n; - m_model[c[j].var()] = c[j].sign()?l_false:l_true; - SASSERT(value_at(c[j], m_model) == l_true); - break; - default: - break; - } - } - m_num_true.push_back(n); - if (n == 0) { - m_false.insert(i); - } - } - } - - void sls::init_tabu(unsigned sz, literal const* tabu) { - // our main use is where m_model satisfies all the hard constraints. - // SASSERT(s.check_model(m_model)); - // SASSERT(m_false.empty()); - // ASSERT: m_num_true is correct count. - m_tabu.reset(); - m_tabu.resize(s.num_vars(), false); - for (unsigned i = 0; i < sz; ++i) { - literal lit = tabu[i]; - if (s.m_level[lit.var()] == 0) continue; - if (value_at(lit, m_model) == l_false) { - flip(lit); - } - m_tabu[lit.var()] = true; - } - for (unsigned i = 0; i < s.m_trail.size(); ++i) { - literal lit = s.m_trail[i]; - if (s.m_level[lit.var()] > 0) break; - if (value_at(lit, m_model) != l_true) { - flip(lit); - } - m_tabu[lit.var()] = true; - } - } - - void sls::init_use() { - m_use_list.reset(); - m_use_list.resize(s.num_vars()*2); - unsigned sz = m_clauses.size(); - for (unsigned i = 0; i < sz; ++i) { - clause const& c = *m_clauses[i]; - unsigned csz = c.size(); - for (unsigned j = 0; j < csz; ++j) { - m_use_list[c[j].index()].push_back(i); - } - } - DEBUG_CODE(check_use_list();); - } - - unsigned_vector const& sls::get_use(literal lit) { - SASSERT(lit.index() < m_use_list.size()); - return m_use_list[lit.index()]; - } - - unsigned sls::get_break_count(literal lit, unsigned min_break) { - SASSERT(value_at(lit, m_model) == l_false); - unsigned result = 0; - unsigned_vector const& uses = get_use(~lit); - unsigned sz = uses.size(); - for (unsigned i = 0; i < sz; ++i) { - if (m_num_true[uses[i]] == 1) { - ++result; - if (result > min_break) return result; - } - } - return result; - } - - bool sls::pick_flip(literal& lit) { - unsigned clause_idx = m_false.choose(m_rand); - clause const& c = *m_clauses[clause_idx]; - SASSERT(!c.satisfied_by(m_model)); - unsigned min_break = UINT_MAX; - unsigned sz = c.size(); - m_min_vars.reset(); - for (unsigned i = 0; i < sz; ++i) { - lit = c[i]; - if (m_tabu[lit.var()]) continue; - unsigned break_count = get_break_count(lit, min_break); - if (break_count < min_break) { - min_break = break_count; - m_min_vars.reset(); - m_min_vars.push_back(lit); - } - else if (break_count == min_break) { - m_min_vars.push_back(lit); - } - } - if (min_break == 0 || (!m_min_vars.empty() && m_rand(100) >= m_prob_choose_min_var)) { - lit = m_min_vars[m_rand(m_min_vars.size())]; - return true; - } - else if (min_break == UINT_MAX) { - return false; - } - else { - lit = c[m_rand(c.size())]; - return !m_tabu[lit.var()]; - } - } - - void sls::flip() { - literal lit; - if (pick_flip(lit)) { - flip(lit); - } - } - - void sls::flip(literal lit) { - //IF_VERBOSE(0, verbose_stream() << lit << " ";); - SASSERT(value_at(lit, m_model) == l_false); - SASSERT(!m_tabu[lit.var()]); - m_model[lit.var()] = lit.sign()?l_false:l_true; - SASSERT(value_at(lit, m_model) == l_true); - unsigned_vector const& use1 = get_use(lit); - unsigned sz = use1.size(); - for (unsigned i = 0; i < sz; ++i) { - unsigned cl = use1[i]; - m_num_true[cl]++; - SASSERT(m_num_true[cl] <= m_clauses[cl]->size()); - if (m_num_true[cl] == 1) m_false.remove(cl); - } - unsigned_vector const& use2 = get_use(~lit); - sz = use2.size(); - for (unsigned i = 0; i < sz; ++i) { - unsigned cl = use2[i]; - SASSERT(m_num_true[cl] > 0); - m_num_true[cl]--; - if (m_num_true[cl] == 0) m_false.insert(cl); - } - } - - void sls::check_invariant() { - DEBUG_CODE( - for (unsigned i = 0; i < m_clauses.size(); ++i) { - clause const& c = *m_clauses[i]; - bool is_sat = c.satisfied_by(m_model); - SASSERT(is_sat != m_false.contains(i)); - SASSERT(is_sat == (m_num_true[i] > 0)); - }); - } - - void sls::check_use_list() { - DEBUG_CODE( - for (unsigned i = 0; i < m_clauses.size(); ++i) { - clause const& c = *m_clauses[i]; - for (unsigned j = 0; j < c.size(); ++j) { - unsigned idx = c[j].index(); - SASSERT(m_use_list[idx].contains(i)); - } - } - - for (unsigned i = 0; i < m_use_list.size(); ++i) { - literal lit = to_literal(i); - for (unsigned j = 0; j < m_use_list[i].size(); ++j) { - clause const& c = *m_clauses[m_use_list[i][j]]; - bool found = false; - for (unsigned k = 0; !found && k < c.size(); ++k) { - found = c[k] == lit; - } - SASSERT(found); - } - }); - } - - void sls::display(std::ostream& out) const { - out << "Model\n"; - for (bool_var v = 0; v < m_model.size(); ++v) { - out << v << ": " << m_model[v] << "\n"; - } - out << "Clauses\n"; - unsigned sz = m_false.num_elems(); - for (unsigned i = 0; i < sz; ++i) { - out << *m_clauses[m_false[i]] << "\n"; - } - for (unsigned i = 0; i < m_clauses.size(); ++i) { - if (m_false.contains(i)) continue; - clause const& c = *m_clauses[i]; - out << c << " " << m_num_true[i] << "\n"; - } - bool has_tabu = false; - for (unsigned i = 0; !has_tabu && i < m_tabu.size(); ++i) { - has_tabu = m_tabu[i]; - } - if (has_tabu) { - out << "Tabu: "; - for (unsigned i = 0; i < m_tabu.size(); ++i) { - if (m_tabu[i]) { - literal lit(i, false); - if (value_at(lit, m_model) == l_false) lit.neg(); - out << lit << " "; - } - } - out << "\n"; - } - } - - - wsls::wsls(solver& s): - sls(s) - { - m_smoothing_probability = 1; // 1/1000 - } - - wsls::~wsls() {} - - void wsls::set_soft(unsigned sz, literal const* lits, double const* weights) { - m_soft.reset(); - m_weights.reset(); - m_soft.append(sz, lits); - m_weights.append(sz, weights); - } - - void wsls::opt(unsigned sz, literal const* tabu, bool reuse_model) { - init(sz, tabu, reuse_model); - - // - // Initialize m_clause_weights, m_hscore, m_sscore. - // - m_best_value = m_false.empty()?evaluate_model(m_model):-1.0; - m_best_model.reset(); - m_clause_weights.reset(); - m_hscore.reset(); - m_sscore.reset(); - m_H.reset(); - m_S.reset(); - m_best_model.append(s.get_model()); - m_clause_weights.resize(m_clauses.size(), 1); - m_sscore.resize(s.num_vars(), 0.0); - m_hscore.resize(s.num_vars(), 0); - for (unsigned i = 0; i < m_soft.size(); ++i) { - literal lit = m_soft[i]; - m_sscore[lit.var()] = m_weights[i]; - if (value_at(lit, m_model) == l_true) { - m_sscore[lit.var()] = -m_sscore[lit.var()]; - } - } - for (bool_var i = 0; i < s.num_vars(); ++i) { - m_hscore[i] = compute_hscore(i); - refresh_scores(i); - } - DEBUG_CODE(check_invariant();); - unsigned i = 0; - for (; !s.canceled() && m_best_value > 0 && i < m_max_tries; ++i) { - wflip(); - if (m_false.empty()) { - double val = evaluate_model(m_model); - if (val < m_best_value || m_best_value < 0.0) { - m_best_value = val; - m_best_model.reset(); - m_best_model.append(m_model); - s.set_model(m_best_model); - IF_VERBOSE(1, verbose_stream() << "new value: " << val << " @ " << i << "\n";); - if (i*2 > m_max_tries) { - m_max_tries *= 2; - } - } - } - } - TRACE("sat", display(tout);); - IF_VERBOSE(0, verbose_stream() << "tries " << i << "\n";); - } - - void wsls::wflip() { - literal lit; - if (pick_wflip(lit)) { - // IF_VERBOSE(0, verbose_stream() << lit << " ";); - wflip(lit); - } - } - - bool wsls::pick_wflip(literal & lit) { - unsigned idx; - if (!m_H.empty()) { - idx = m_H.choose(m_rand); - lit = literal(idx, false); - if (value_at(lit, m_model) == l_true) lit.neg(); - SASSERT(value_at(lit, m_model) == l_false); - TRACE("sat", tout << "flip H(" << m_H.num_elems() << ") " << lit << "\n";); - } - else if (!m_S.empty()) { - double score = 0.0; - m_min_vars.reset(); - for (unsigned i = 0; i < m_S.num_elems(); ++i) { - unsigned v = m_S[i]; - SASSERT(m_sscore[v] > 0.0); - if (m_sscore[v] > score) { - m_min_vars.reset(); - m_min_vars.push_back(literal(v, false)); - score = m_sscore[v]; - } - else if (m_sscore[v] == score) { - m_min_vars.push_back(literal(v, false)); - } - } - lit = m_min_vars[m_rand(m_min_vars.size())]; // pick with largest sscore. - SASSERT(value_at(lit, m_model) == l_false); - TRACE("sat", tout << "flip S(" << m_min_vars.size() << "," << score << ") " << lit << "\n";); - } - else { - update_hard_weights(); - if (!m_false.empty()) { - unsigned cls_idx = m_false.choose(m_rand); - clause const& c = *m_clauses[cls_idx]; - lit = c[m_rand(c.size())]; - TRACE("sat", tout << "flip hard(" << m_false.num_elems() << "," << c.size() << ") " << lit << "\n";); - } - else { - m_min_vars.reset(); - for (unsigned i = 0; i < m_soft.size(); ++i) { - lit = m_soft[i]; - if (value_at(lit, m_model) == l_false) { - m_min_vars.push_back(lit); - } - } - if (m_min_vars.empty()) { - SASSERT(m_best_value == 0.0); - UNREACHABLE(); // we should have exited the main loop before. - return false; - } - else { - lit = m_min_vars[m_rand(m_min_vars.size())]; - } - TRACE("sat", tout << "flip soft(" << m_min_vars.size() << ", " << m_sscore[lit.var()] << ") " << lit << "\n";); - - } - SASSERT(value_at(lit, m_model) == l_false); - } - return !m_tabu[lit.var()]; - } - - void wsls::wflip(literal lit) { - flip(lit); - unsigned v = lit.var(); - m_sscore[v] = -m_sscore[v]; - m_hscore[v] = compute_hscore(v); - refresh_scores(v); - recompute_hscores(lit); - } - - void wsls::update_hard_weights() { - unsigned csz = m_clauses.size(); - if (m_smoothing_probability >= m_rand(1000)) { - for (unsigned i = 0; i < csz; ++i) { - if (m_clause_weights[i] > 1 && !m_false.contains(i)) { - --m_clause_weights[i]; - if (m_num_true[i] == 1) { - clause const& c = *m_clauses[i]; - unsigned sz = c.size(); - for (unsigned j = 0; j < sz; ++j) { - if (value_at(c[j], m_model) == l_true) { - ++m_hscore[c[j].var()]; - refresh_scores(c[j].var()); - break; - } - } - } - } - } - } - else { - for (unsigned i = 0; i < csz; ++i) { - if (m_false.contains(i)) { - ++m_clause_weights[i]; - clause const& c = *m_clauses[i]; - unsigned sz = c.size(); - for (unsigned j = 0; j < sz; ++j) { - ++m_hscore[c[j].var()]; - refresh_scores(c[j].var()); - } - } - } - } - DEBUG_CODE(check_invariant();); - } - - double wsls::evaluate_model(model& mdl) { - SASSERT(m_false.empty()); - double result = 0.0; - for (unsigned i = 0; i < m_soft.size(); ++i) { - literal lit = m_soft[i]; - if (value_at(lit, mdl) != l_true) { - result += m_weights[i]; - } - } - return result; - } - - int wsls::compute_hscore(bool_var v) { - literal lit(v, false); - if (value_at(lit, m_model) == l_false) { - lit.neg(); - } - SASSERT(value_at(lit, m_model) == l_true); - int hs = 0; - unsigned_vector const& use1 = get_use(~lit); - unsigned sz = use1.size(); - for (unsigned i = 0; i < sz; ++i) { - unsigned cl = use1[i]; - if (m_num_true[cl] == 0) { - SASSERT(m_false.contains(cl)); - hs += m_clause_weights[cl]; - } - else { - SASSERT(!m_false.contains(cl)); - } - } - unsigned_vector const& use2 = get_use(lit); - sz = use2.size(); - for (unsigned i = 0; i < sz; ++i) { - unsigned cl = use2[i]; - if (m_num_true[cl] == 1) { - SASSERT(!m_false.contains(cl)); - hs -= m_clause_weights[cl]; - } - } - return hs; - } - - void wsls::recompute_hscores(literal lit) { - SASSERT(value_at(lit, m_model) == l_true); - TRACE("sat", tout << lit.var() << " := " << m_hscore[lit.var()] << "\n";); - unsigned_vector const& use1 = get_use(lit); - unsigned sz = use1.size(); - for (unsigned i = 0; i < sz; ++i) { - unsigned cl = use1[i]; - TRACE("sat", tout << *m_clauses[cl] << " " << m_num_true[cl] << "\n";); - SASSERT(m_num_true[cl] > 0); - if (m_num_true[cl] == 1) { - // num_true 0 -> 1 - // other literals don't have upside any more. - // subtract one from all other literals - adjust_all_values(lit, cl, -static_cast(m_clause_weights[cl])); - } - else if (m_num_true[cl] == 2) { - // num_true 1 -> 2, previous critical literal is no longer critical - adjust_pivot_value(lit, cl, +m_clause_weights[cl]); - } - } - unsigned_vector const& use2 = get_use(~lit); - sz = use2.size(); - for (unsigned i = 0; i < sz; ++i) { - unsigned cl = use2[i]; - TRACE("sat", tout << *m_clauses[cl] << " " << m_num_true[cl] << "\n";); - if (m_num_true[cl] == 0) { - // num_true 1 -> 0 - // all variables became critical. - adjust_all_values(~lit, cl, +m_clause_weights[cl]); - } - else if (m_num_true[cl] == 1) { - adjust_pivot_value(~lit, cl, -static_cast(m_clause_weights[cl])); - } - // else n+1 -> n >= 2 - } - } - - void wsls::adjust_all_values(literal lit, unsigned cl, int delta) { - clause const& c = *m_clauses[cl]; - unsigned sz = c.size(); - TRACE("sat", tout << lit << " " << c << " delta: " << delta << " nt: " << m_num_true[cl] << "\n";); - for (unsigned i = 0; i < sz; ++i) { - literal lit2 = c[i]; - if (lit2 != lit) { - TRACE("sat", tout << lit2.var() << " := " << m_hscore[lit2.var()] << "\n";); - m_hscore[lit2.var()] += delta; - TRACE("sat", tout << lit2.var() << " := " << m_hscore[lit2.var()] << "\n";); - refresh_scores(lit2.var()); - } - } - } - - void wsls::adjust_pivot_value(literal lit, unsigned cl, int delta) { - clause const& c = *m_clauses[cl]; - unsigned csz = c.size(); - for (unsigned j = 0; j < csz; ++j) { - literal lit2 = c[j]; - if (lit2 != lit && value_at(lit2, m_model) == l_true) { - TRACE("sat", tout << lit2.var() << " := " << m_hscore[lit2.var()] << "\n";); - m_hscore[lit2.var()] += delta; - TRACE("sat", tout << lit2.var() << " := " << m_hscore[lit2.var()] << "\n";); - refresh_scores(lit2.var()); - break; - } - } - } - - void wsls::refresh_scores(bool_var v) { - if (m_hscore[v] > 0 && !m_tabu[v] && m_sscore[v] == 0) { - m_H.insert(v); - } - else { - m_H.remove(v); - } - if (m_sscore[v] > 0) { - if (m_hscore[v] == 0 && !m_tabu[v]) { - m_S.insert(v); - } - else { - m_S.remove(v); - } - } - else if (m_sscore[v] < 0) { - m_S.remove(v); - } - } - - void wsls::check_invariant() { - sls::check_invariant(); - // The hscore is the reward for flipping the truth value of variable v. - // hscore(v) = Sum weight(c) for num_true(c) = 0 and v in c - // - Sum weight(c) for num_true(c) = 1 and (v in c, M(v) or !v in c and !M(v)) - DEBUG_CODE( - for (unsigned v = 0; v < s.num_vars(); ++v) { - int hs = compute_hscore(v); - CTRACE("sat", hs != m_hscore[v], display(tout << v << " - computed: " << hs << " - assigned: " << m_hscore[v] << "\n");); - SASSERT(m_hscore[v] == hs); - } - - // The score(v) is the reward on soft clauses for flipping v. - for (unsigned j = 0; j < m_soft.size(); ++j) { - unsigned v = m_soft[j].var(); - double ss = (l_true == value_at(m_soft[j], m_model))?(-m_weights[j]):m_weights[j]; - SASSERT(m_sscore[v] == ss); - } - - // m_H are values such that m_hscore > 0 and sscore = 0. - for (bool_var v = 0; v < m_hscore.size(); ++v) { - SASSERT((m_hscore[v] > 0 && !m_tabu[v] && m_sscore[v] == 0) == m_H.contains(v)); - } - - // m_S are values such that hscore = 0, sscore > 0 - for (bool_var v = 0; v < m_sscore.size(); ++v) { - SASSERT((m_hscore[v] == 0 && m_sscore[v] > 0 && !m_tabu[v]) == m_S.contains(v)); - }); - } - - void wsls::display(std::ostream& out) const { - sls::display(out); - out << "Best model\n"; - for (bool_var v = 0; v < m_best_model.size(); ++v) { - out << v << ": " << m_best_model[v] << " h: " << m_hscore[v]; - if (m_sscore[v] != 0.0) out << " s: " << m_sscore[v]; - out << "\n"; - } - } - -}; - diff --git a/src/sat/sat_sls.h b/src/sat/sat_sls.h deleted file mode 100644 index f1bf55543..000000000 --- a/src/sat/sat_sls.h +++ /dev/null @@ -1,115 +0,0 @@ -/*++ -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(); } - unsigned operator[](unsigned idx) const { return m_elems[idx]; } - 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 { - protected: - solver& s; - random_gen m_rand; - unsigned m_max_tries; - unsigned m_prob_choose_min_var; // number between 0 and 99. - unsigned m_clause_generation; - ptr_vector m_clauses; // vector of all clauses. - index_set m_false; // clauses currently false - vector m_use_list; // use lists for literals - unsigned_vector m_num_true; // per clause, count of # true literals - svector m_min_vars; // literals with smallest break count - model m_model; // current model - clause_allocator m_alloc; // clause allocator - clause_vector m_bin_clauses; // binary clauses - svector m_tabu; // variables that cannot be swapped - public: - sls(solver& s); - virtual ~sls(); - lbool operator()(unsigned sz, literal const* tabu, bool reuse_model); - void set_max_tries(unsigned mx) { m_max_tries = mx; } - virtual void display(std::ostream& out) const; - protected: - void init(unsigned sz, literal const* tabu, bool reuse_model); - void init_tabu(unsigned sz, literal const* tabu); - void init_model(); - void init_use(); - void init_clauses(); - unsigned_vector const& get_use(literal lit); - void flip(literal lit); - virtual void check_invariant(); - void check_use_list(); - private: - bool pick_flip(literal& lit); - void flip(); - unsigned get_break_count(literal lit, unsigned min_break); - }; - - /** - \brief sls with weighted soft clauses. - */ - class wsls : public sls { - unsigned_vector m_clause_weights; - svector m_hscore; - svector m_sscore; - literal_vector m_soft; - svector m_weights; - double m_best_value; - model m_best_model; - index_set m_H, m_S; - unsigned m_smoothing_probability; - public: - wsls(solver& s); - virtual ~wsls(); - void set_soft(unsigned sz, literal const* lits, double const* weights); - bool has_soft() const { return !m_soft.empty(); } - void opt(unsigned sz, literal const* tabu, bool reuse_model); - virtual void display(std::ostream& out) const; - double evaluate_model(model& mdl); - private: - void wflip(); - void wflip(literal lit); - void update_hard_weights(); - bool pick_wflip(literal & lit); - virtual void check_invariant(); - void refresh_scores(bool_var v); - int compute_hscore(bool_var v); - void recompute_hscores(literal lit); - void adjust_all_values(literal lit, unsigned cl, int delta); - void adjust_pivot_value(literal lit, unsigned cl, int delta); - }; - -}; - -#endif diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp index 10c97b296..1ed343efa 100644 --- a/src/sat/sat_solver.cpp +++ b/src/sat/sat_solver.cpp @@ -20,7 +20,6 @@ Revision History: #include"sat_integrity_checker.h" #include"luby.h" #include"trace.h" -#include"sat_bceq.h" #include"max_cliques.h" // define to update glue during propagation @@ -42,7 +41,6 @@ namespace sat { m_asymm_branch(*this, p), m_probing(*this, p), m_mus(*this), - m_wsls(*this), m_inconsistent(false), m_num_frozen(0), m_activity_inc(128), @@ -55,7 +53,6 @@ namespace sat { m_conflicts = 0; m_next_simplify = 0; m_num_checkpoints = 0; - m_initializing_preferred = false; } solver::~solver() { @@ -713,7 +710,7 @@ namespace sat { // Search // // ----------------------- - lbool solver::check(unsigned num_lits, literal const* lits, double const* weights, double max_weight) { + lbool solver::check(unsigned num_lits, literal const* lits) { pop_to_base_level(); IF_VERBOSE(2, verbose_stream() << "(sat.sat-solver)\n";); SASSERT(scope_lvl() == 0); @@ -728,7 +725,7 @@ namespace sat { init_search(); propagate(false); if (inconsistent()) return l_false; - init_assumptions(num_lits, lits, weights, max_weight); + init_assumptions(num_lits, lits); propagate(false); if (check_inconsistent()) return l_false; cleanup(); @@ -914,12 +911,11 @@ namespace sat { } } - void solver::init_assumptions(unsigned num_lits, literal const* lits, double const* weights, double max_weight) { + void solver::init_assumptions(unsigned num_lits, literal const* lits) { if (num_lits == 0 && m_user_scope_literals.empty()) { return; } - retry_init_assumptions: reset_assumptions(); push(); @@ -943,16 +939,6 @@ namespace sat { assign(nlit, justification()); } - if (weights && !inconsistent()) { - if (m_config.m_optimize_model) { - m_wsls.set_soft(num_lits, lits, weights); - } - if (!init_weighted_assumptions(num_lits, lits, weights, max_weight)) { - goto retry_init_assumptions; - } - return; - } - for (unsigned i = 0; !inconsistent() && i < num_lits; ++i) { literal lit = lits[i]; SASSERT(is_external(lit.var())); @@ -962,109 +948,6 @@ namespace sat { } - bool solver::init_weighted_assumptions(unsigned num_lits, literal const* lits, double const* weights, double max_weight) { - flet _min1(m_config.m_core_minimize, false); - m_weight = 0; - m_blocker.reset(); - svector values; - unsigned num_cores = 0; - for (unsigned i = 0; !inconsistent() && i < num_lits; ++i) { - literal lit = lits[i]; - SASSERT(is_external(lit.var())); - TRACE("sat", tout << "propagate: " << lit << " " << value(lit) << "\n";); - SASSERT(m_scope_lvl == 1); - add_assumption(lit); - switch(value(lit)) { - case l_undef: - values.push_back(l_true); - assign(lit, justification()); - if (num_cores*2 >= num_lits) { - break; - } - propagate(false); - if (inconsistent()) { - flet _init(m_initializing_preferred, true); - while (inconsistent()) { - if (!resolve_conflict()) { - return true; - } - propagate(true); - } - if (m_scope_lvl == 0) { - return false; - } - // backjump to last consistent assumption: - unsigned j; - m_weight = 0; - m_blocker.reset(); - for (j = 0; j < i && value(lits[j]) == values[j]; ++j) { - if (values[j] == l_false) { - m_weight += weights[j]; - m_blocker.push_back(lits[j]); - } - } - SASSERT(value(lits[j]) != values[j]); - SASSERT(j <= i); - SASSERT(j == 0 || value(lits[j-1]) == values[j-1]); - for (unsigned k = i; k >= j; --k) { - if (is_assumption(lits[k])) { - pop_assumption(); - } - } - values.resize(j); - TRACE("sat", tout << "backjump " << (i - j + 1) << " steps " << num_cores << "\n";); - i = j - 1; - } - break; - - case l_false: - ++num_cores; - values.push_back(l_false); - SASSERT(!inconsistent()); - set_conflict(justification(), ~lit); - m_conflict_lvl = scope_lvl(); - resolve_conflict_for_unsat_core(); - IF_VERBOSE(3, verbose_stream() << "(sat.core: " << m_core << ")\n";); - update_min_core(); - SASSERT(m_min_core_valid); - m_weight += weights[i]; - if (m_weight <= max_weight) { - m_blocker.push_back(lit); - } - TRACE("sat", tout << "core: " << m_core << "\nassumptions: " << m_assumptions << "\n";); - SASSERT(m_core.size() <= m_assumptions.size()); - SASSERT(m_assumptions.size() <= i+1); - if (m_core.size() <= 3) { - m_inconsistent = true; - TRACE("opt", tout << "found small core: " << m_core << "\n";); - IF_VERBOSE(11, verbose_stream() << "(sat.core: " << m_core << ")\n";); - return true; - } - pop_assumption(); - m_inconsistent = false; - break; - case l_true: - values.push_back(l_true); - SASSERT(m_justification[lit.var()].get_kind() != justification::NONE || lvl(lit) == 0); - break; - } - } - TRACE("sat", tout << "initialized\n";); - IF_VERBOSE(11, verbose_stream() << "(sat.blocker: " << m_blocker << "\nCore: " << m_min_core << ")\n";); - if (m_weight >= max_weight) { - // block the current correction set candidate. - ++m_stats.m_blocked_corr_sets; - TRACE("opt", tout << "blocking soft correction set: " << m_blocker << "\n";); - IF_VERBOSE(11, verbose_stream() << "blocking " << m_blocker << "\n";); - pop_to_base_level(); - mk_clause_core(m_blocker); - return false; - } - return true; - } - - - void solver::update_min_core() { if (!m_min_core_valid || m_core.size() < m_min_core.size()) { m_min_core.reset(); @@ -1148,11 +1031,6 @@ namespace sat { m_min_core_valid = false; m_min_core.reset(); TRACE("sat", display(tout);); - - if (m_config.m_bcd) { - bceq bc(*this); - bc(); - } } /** @@ -1244,9 +1122,6 @@ namespace sat { m_model[v] = value(v); } TRACE("sat_mc_bug", m_mc.display(tout);); - if (m_config.m_optimize_model) { - m_wsls.opt(0, 0, false); - } m_mc(m_model); TRACE("sat", for (bool_var v = 0; v < num; v++) tout << v << ": " << m_model[v] << "\n";); @@ -1673,10 +1548,6 @@ namespace sat { if (m_not_l == literal()) tout << "null literal\n"; else tout << m_not_l << "\n";); - if (m_initializing_preferred) { - SASSERT(m_conflict_lvl <= 1); - return resolve_conflict_for_init(); - } if (m_conflict_lvl <= 1 && tracking_assumptions()) { resolve_conflict_for_unsat_core(); return false; @@ -3184,10 +3055,10 @@ namespace sat { if (asms.empty()) { bool_var v = mk_var(true, false); literal lit(v, false); - init_assumptions(1, &lit, 0, 0); + init_assumptions(1, &lit); } else { - init_assumptions(asms.size(), asms.c_ptr(), 0, 0); + init_assumptions(asms.size(), asms.c_ptr()); } propagate(false); if (check_inconsistent()) return l_false; @@ -3249,10 +3120,10 @@ namespace sat { if (asms.empty()) { bool_var v = mk_var(true, false); literal lit(v, false); - init_assumptions(1, &lit, 0, 0); + init_assumptions(1, &lit); } else { - init_assumptions(asms.size(), asms.c_ptr(), 0, 0); + init_assumptions(asms.size(), asms.c_ptr()); } propagate(false); if (check_inconsistent()) return l_false; diff --git a/src/sat/sat_solver.h b/src/sat/sat_solver.h index 1700dfb7e..d89afd898 100644 --- a/src/sat/sat_solver.h +++ b/src/sat/sat_solver.h @@ -33,7 +33,6 @@ Revision History: #include"sat_iff3_finder.h" #include"sat_probing.h" #include"sat_mus.h" -#include"sat_sls.h" #include"params.h" #include"statistics.h" #include"stopwatch.h" @@ -86,7 +85,6 @@ namespace sat { asymm_branch m_asymm_branch; probing m_probing; mus m_mus; // MUS for minimal core extraction - wsls m_wsls; // SLS facility for MaxSAT use bool m_inconsistent; // A conflict is usually a single justification. That is, a justification // for false. If m_not_l is not null_literal, then m_conflict is a @@ -141,9 +139,6 @@ namespace sat { friend class probing; friend class iff3_finder; friend class mus; - friend class sls; - friend class wsls; - friend class bceq; friend struct mk_stat; public: solver(params_ref const & p, reslimit& l, extension * ext); @@ -280,10 +275,7 @@ namespace sat { // // ----------------------- public: - lbool check(unsigned num_lits = 0, literal const* lits = 0) { - return check(num_lits, lits, 0, 0); - } - lbool check(unsigned num_lits, literal const* lits, double const* weights, double max_weight); + lbool check(unsigned num_lits = 0, literal const* lits = 0); model const & get_model() const { return m_model; } bool model_is_current() const { return m_model_is_current; } @@ -311,11 +303,7 @@ namespace sat { literal_vector m_min_core; bool m_min_core_valid; - literal_vector m_blocker; - double m_weight; - bool m_initializing_preferred; - void init_assumptions(unsigned num_lits, literal const* lits, double const* weights, double max_weight); - bool init_weighted_assumptions(unsigned num_lits, literal const* lits, double const* weights, double max_weight); + void init_assumptions(unsigned num_lits, literal const* lits); void reassert_min_core(); void update_min_core(); void resolve_weighted(); diff --git a/src/sat/sat_solver/inc_sat_solver.cpp b/src/sat/sat_solver/inc_sat_solver.cpp index b7ce92108..33d10f428 100644 --- a/src/sat/sat_solver/inc_sat_solver.cpp +++ b/src/sat/sat_solver/inc_sat_solver.cpp @@ -105,13 +105,8 @@ public: virtual void set_progress_callback(progress_callback * callback) {} - virtual lbool check_sat(unsigned num_assumptions, expr * const * assumptions) { - return check_sat(num_assumptions, assumptions, 0, 0); - } - void display_weighted(std::ostream& out, unsigned sz, expr * const * assumptions, unsigned const* weights) { - m_weights.reset(); if (weights != 0) { for (unsigned i = 0; i < sz; ++i) m_weights.push_back(weights[i]); } @@ -131,15 +126,11 @@ public: for (unsigned i = 0; i < m_asms.size(); ++i) { nweights.push_back((unsigned) m_weights[i]); } + m_weights.reset(); m_solver.display_wcnf(out, m_asms.size(), m_asms.c_ptr(), nweights.c_ptr()); } - lbool check_sat(unsigned sz, expr * const * assumptions, double const* weights, double max_weight) { - m_weights.reset(); - if (weights != 0) { - m_weights.append(sz, weights); - } - SASSERT(m_weights.empty() == (m_weights.c_ptr() == 0)); + virtual lbool check_sat(unsigned sz, expr * const * assumptions) { m_solver.pop_to_base_level(); dep2asm_t dep2asm; m_model = 0; @@ -148,10 +139,10 @@ public: r = internalize_assumptions(sz, assumptions, dep2asm); if (r != l_true) return r; - r = m_solver.check(m_asms.size(), m_asms.c_ptr(), m_weights.c_ptr(), max_weight); + r = m_solver.check(m_asms.size(), m_asms.c_ptr()); switch (r) { case l_true: - if (sz > 0 && !weights) { + if (sz > 0) { check_assumptions(dep2asm); } break; @@ -675,18 +666,6 @@ solver* mk_inc_sat_solver(ast_manager& m, params_ref const& p) { } -lbool inc_sat_check_sat(solver& _s, unsigned sz, expr*const* soft, rational const* _weights, rational const& max_weight) { - inc_sat_solver& s = dynamic_cast(_s); - vector weights; - for (unsigned i = 0; _weights && i < sz; ++i) { - weights.push_back(_weights[i].get_double()); - } - params_ref p; - p.set_bool("minimize_core", false); - s.updt_params(p); - return s.check_sat(sz, soft, weights.c_ptr(), max_weight.get_double()); -} - void inc_sat_display(std::ostream& out, solver& _s, unsigned sz, expr*const* soft, rational const* _weights) { inc_sat_solver& s = dynamic_cast(_s); vector weights; diff --git a/src/sat/sat_solver/inc_sat_solver.h b/src/sat/sat_solver/inc_sat_solver.h index 028f71b06..4b0bea50e 100644 --- a/src/sat/sat_solver/inc_sat_solver.h +++ b/src/sat/sat_solver/inc_sat_solver.h @@ -24,7 +24,6 @@ Notes: solver* mk_inc_sat_solver(ast_manager& m, params_ref const& p); -lbool inc_sat_check_sat(solver& s, unsigned sz, expr*const* soft, rational const* weights, rational const& max_weight); void inc_sat_display(std::ostream& out, solver& s, unsigned sz, expr*const* soft, rational const* _weights);