From d429e72e922643ab6368846a03799c0c02cdb7d6 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 3 Aug 2014 18:50:21 -0700 Subject: [PATCH] v2 of dual maxres engine Signed-off-by: Nikolaj Bjorner --- src/opt/inc_sat_solver.cpp | 6 +- src/opt/maxres.cpp | 195 ++++++++++++++++++++----------------- src/opt/maxsmt.cpp | 8 +- src/opt/maxsmt.h | 1 + src/opt/mss.cpp | 166 +++++++++++++++++++++++-------- src/opt/mss.h | 16 +-- 6 files changed, 253 insertions(+), 139 deletions(-) diff --git a/src/opt/inc_sat_solver.cpp b/src/opt/inc_sat_solver.cpp index c307ef6ae..f8979edce 100644 --- a/src/opt/inc_sat_solver.cpp +++ b/src/opt/inc_sat_solver.cpp @@ -89,7 +89,7 @@ public: m_solver.pop_to_base_level(); dep2asm_t dep2asm; - m_model.reset(); + m_model = 0; lbool r = internalize_formulas(); if (r != l_true) return r; r = internalize_assumptions(num_assumptions, assumptions, dep2asm); @@ -161,7 +161,7 @@ public: r.append(m_core.size(), m_core.c_ptr()); } virtual void get_model(model_ref & m) { - if (!m_model) { + if (!m_model.get()) { extract_model(); } m = m_model; @@ -275,6 +275,7 @@ private: // bit-blasting model converter. void extract_model() { + TRACE("sat", tout << "retrieve model\n";); model_ref md = alloc(model, m); sat::model const & ll_m = m_solver.get_model(); atom2bool_var::iterator it = m_map.begin(); @@ -300,6 +301,7 @@ private: if (m_mc) { (*m_mc)(m_model); } + SASSERT(m_model); // IF_VERBOSE(0, model_smt2_pp(verbose_stream(), m, *(m_model.get()), 0);); } diff --git a/src/opt/maxres.cpp b/src/opt/maxres.cpp index 7e8df3e18..5e7dac0f7 100644 --- a/src/opt/maxres.cpp +++ b/src/opt/maxres.cpp @@ -58,10 +58,10 @@ Notes: #include "maxres.h" #include "ast_pp.h" #include "mus.h" +#include "mss.h" using namespace opt; - class maxres : public maxsmt_solver_base { public: enum strategy_t { @@ -75,8 +75,10 @@ private: obj_map m_asm2weight; ptr_vector m_new_core; mus m_mus; + mss m_mss; expr_ref_vector m_trail; strategy_t m_st; + rational m_max_upper; public: maxres(ast_manager& m, opt_solver* s, params_ref& p, @@ -85,6 +87,7 @@ public: maxsmt_solver_base(s, m, p, ws, soft), m_B(m), m_asms(m), m_mus(m_s, m), + m_mss(m_s, m), m_trail(m), m_st(st) { @@ -168,7 +171,6 @@ public: default: break; } - IF_VERBOSE(1, verbose_stream() << "(opt.max_res [" << m_lower << ":" << m_upper << "])\n";); } return l_true; } @@ -179,8 +181,7 @@ public: init_local(); enable_bvsat(); enable_sls(); - lbool was_sat = l_false; - ptr_vector soft_compl; + ptr_vector mcs; vector > cores; while (m_lower < m_upper) { TRACE("opt", @@ -189,37 +190,38 @@ public: tout << "\n"; display(tout); ); - lbool is_sat = m_s->check_sat(0, 0); + lbool is_sat = try_improve_bound(cores, mcs); if (m_cancel) { return l_undef; } - if (is_sat == l_true) { - was_sat = l_true; - is_sat = extend_model(soft_compl); - switch (is_sat) { - case l_undef: - break; - case l_false: - is_sat = process_unsat(); - break; - case l_true: - is_sat = process_sat(soft_compl); - break; - } - } switch (is_sat) { case l_undef: return l_undef; case l_false: + SASSERT(cores.empty() && mcs.empty()); m_lower = m_upper; - return was_sat; - case l_true: + return l_true; + case l_true: + SASSERT(cores.empty() || mcs.empty()); + SASSERT(!cores.empty() || !mcs.empty()); + for (unsigned i = 0; is_sat == l_true && i < cores.size(); ++i) { + is_sat = process_unsat(cores[i]); + } + if (is_sat == l_true && !mcs.empty()) { + is_sat = process_sat(mcs); + } + if (is_sat != l_true) { + return is_sat; + } break; } } - return was_sat; + m_lower = m_lower; + return l_true; } + + lbool mss_solver() { NOT_IMPLEMENTED_YET(); return l_undef; @@ -314,6 +316,7 @@ public: fml = m.mk_not(m.mk_and(m_B.size(), m_B.c_ptr())); m_s->assert_expr(fml); m_lower += w; + IF_VERBOSE(1, verbose_stream() << "(opt.maxres [" << m_lower << ":" << m_upper << "])\n";); return l_true; } @@ -422,6 +425,7 @@ public: // cs is a correction set (a complement of a (maximal) satisfying assignment). void cs_max_resolve(ptr_vector& cs, rational const& w) { + TRACE("opt", display_vec(tout << "correction set: ", cs.size(), cs.c_ptr());); SASSERT(!cs.empty()); expr_ref fml(m), asum(m); app_ref cls(m), d(m), dd(m); @@ -437,6 +441,7 @@ public: // asm => b_i // asm => d_{i-1} or b_{i-1} // d_i => d_{i-1} or b_{i-1} + // for (unsigned i = 1; i < cs.size(); ++i) { expr* b_i = m_B[i-1].get(); expr* b_i1 = m_B[i].get(); @@ -460,82 +465,89 @@ public: m_s->assert_expr(fml); } - // - // The hard constraints are satisfiable. - // Extend the current model to satisfy as many - // soft constraints as possible until either - // hitting an unsatisfiable subset of size < 1/2*#assumptions, - // or producing a maximal satisfying assignment exceeding - // number of soft constraints >= 1/2*#assumptions. - // In both cases, soft constraints that are not satisfied - // is <= 1/2*#assumptions. In this way, the new modified assumptions - // account for at most 1/2 of the current assumptions. - // The core reduction algorithms also need to take into account - // at most 1/2 of the assumptions for minimization. - // - - lbool extend_model(ptr_vector& soft_compl) { - ptr_vector asms; - model_ref mdl; - expr_ref tmp(m); - m_s->get_model(mdl); - unsigned num_true = update_model(mdl, asms, soft_compl); - for (unsigned j = 0; j < m_asms.size(); ++j) { - expr* fml = m_asms[j].get(); - VERIFY(mdl->eval(fml, tmp)); - if (m.is_false(tmp)) { - asms.push_back(fml); - lbool is_sat = m_s->check_sat(asms.size(), asms.c_ptr()); - asms.pop_back(); - switch (is_sat) { - case l_false: - if (num_true*2 < m_asms.size()) { - return l_false; - } - break; - case l_true: - m_s->get_model(mdl); - num_true = update_model(mdl, asms, soft_compl); - break; - case l_undef: - return l_undef; + lbool try_improve_bound(vector >& cores, ptr_vector& mcs) { + cores.reset(); + mcs.reset(); + ptr_vector core; + expr_ref_vector asms(m_asms); + while (true) { + rational upper = m_max_upper; + unsigned sz = 0; + for (unsigned i = 0; m_upper <= upper && i < asms.size(); ++i, ++sz) { + upper -= get_weight(asms[i].get()); + } + lbool is_sat = m_s->check_sat(sz, asms.c_ptr()); + switch (is_sat) { + case l_true: { + ptr_vector lits; + lits.append(asms.size(), asms.c_ptr()); + set_mus(false); + is_sat = m_mss(cores, lits); + set_mus(true); + if (is_sat != l_true) { + return is_sat; } + m_mss.get_model(m_model); // last model is best way to reduce search space. + update_assignment(); + if (cores.empty() || asms.size() < cores.back().size()) { + cores.reset(); + mcs.append(asms.size(), asms.c_ptr()); + } + return l_true; + } + case l_undef: + return l_undef; + case l_false: + core.reset(); + m_s->get_unsat_core(core); + is_sat = minimize_core(core); + if (is_sat != l_true) { + break; + } + if (core.empty()) { + cores.reset(); + mcs.reset(); + return l_false; + } + cores.push_back(core); + if (core.size() >= 3) { + return l_true; + } + // + // check arithmetic: cannot improve upper bound + // + if (m_upper <= upper) { + return l_true; + } + + remove_soft(core, asms); + break; } } - return l_true; + + return l_undef; } - unsigned update_model(model_ref& mdl, ptr_vector& asms, ptr_vector& soft_compl) { - expr_ref tmp(m); - asms.reset(); - soft_compl.reset(); - rational weight = m_lower; - unsigned num_true = 0; - for (unsigned i = 0; i < m_asms.size(); ++i) { - expr* fml = m_asms[i].get(); - VERIFY(mdl->eval(fml, tmp)); - SASSERT(m.is_false(tmp) || m.is_true(tmp)); - if (m.is_false(tmp)) { - weight += get_weight(fml); - soft_compl.push_back(fml); - } - else { - ++num_true; - asms.push_back(fml); + + void update_assignment() { + rational upper(0); + for (unsigned i = 0; i < m_soft.size(); ++i) { + expr_ref tmp(m); + expr* n = m_soft[i].get(); + VERIFY(m_model->eval(n, tmp)); + CTRACE("opt", !m.is_true(tmp) && !m.is_false(tmp), + tout << mk_pp(n, m) << " |-> " << mk_pp(tmp, m) << "\n";); + + m_assignment[i] = m.is_true(tmp); + if (!m_assignment[i]) { + upper += m_weights[i]; } } - if (weight < m_upper) { - m_upper = weight; - m_model = mdl; - for (unsigned i = 0; i < m_soft.size(); ++i) { - expr_ref tmp(m); - VERIFY(m_model->eval(m_soft[i].get(), tmp)); - m_assignment[i] = m.is_true(tmp); - } - IF_VERBOSE(1, verbose_stream() << - "(opt.mus-mss_max_res [" << m_lower << ":" << m_upper << "])\n";); - } - return num_true; + SASSERT(upper <= m_upper); + m_upper = upper; + IF_VERBOSE(1, verbose_stream() << + "(opt.maxres [" << m_lower << ":" << m_upper << "])\n";); + } void remove_soft(ptr_vector const& core, expr_ref_vector& asms) { @@ -564,6 +576,7 @@ public: for (unsigned i = 0; i < m_soft.size(); ++i) { add_soft(m_soft[i].get(), m_weights[i]); } + m_max_upper = m_upper; } }; diff --git a/src/opt/maxsmt.cpp b/src/opt/maxsmt.cpp index d6663099d..eb0a65ce9 100644 --- a/src/opt/maxsmt.cpp +++ b/src/opt/maxsmt.cpp @@ -138,8 +138,6 @@ namespace opt { m_s = sat_solver; } - - void maxsmt_solver_base::enable_bvsat() { if (m_enable_sat && !m_sat_enabled && probe_bv()) { enable_inc_bvsat(); @@ -159,6 +157,12 @@ namespace opt { } } + void maxsmt_solver_base::set_mus(bool f) { + params_ref p; + p.set_bool("minimize_core", f); + m_s->updt_params(p); + } + app* maxsmt_solver_base::mk_fresh_bool(char const* name) { app* result = m.mk_fresh_const(name, m.mk_bool_sort()); m_mc->insert(result->get_decl()); diff --git a/src/opt/maxsmt.h b/src/opt/maxsmt.h index 138670693..df03499c9 100644 --- a/src/opt/maxsmt.h +++ b/src/opt/maxsmt.h @@ -94,6 +94,7 @@ namespace opt { void init(); expr* mk_not(expr* e); bool probe_bv(); + void set_mus(bool f); void enable_bvsat(); void enable_sls(); app* mk_fresh_bool(char const* name); diff --git a/src/opt/mss.cpp b/src/opt/mss.cpp index d0780c916..8a5bcdfe5 100644 --- a/src/opt/mss.cpp +++ b/src/opt/mss.cpp @@ -27,35 +27,74 @@ Notes: namespace opt { - mss::mss(solver& s, ast_manager& m): s(s), m(m), m_cancel(false) { + mss::mss(ref& s, ast_manager& m): m_s(s), m(m), m_cancel(false) { } mss::~mss() { - } - + } - void mss::check_parameters(vector const& cores, exprs& literals) { + bool mss::check_result() { + lbool is_sat = m_s->check_sat(m_mss.size(), m_mss.c_ptr()); + if (is_sat == l_undef) return true; + SASSERT(is_sat == l_true); + if (is_sat == l_false) return false; + expr_set::iterator it = m_mcs.begin(), end = m_mcs.end(); + for (; it != end; ++it) { + m_mss.push_back(*it); + is_sat = m_s->check_sat(m_mss.size(), m_mss.c_ptr()); + m_mss.pop_back(); + if (is_sat == l_undef) return true; + SASSERT(is_sat == l_false); + if (is_sat == l_true) return false; + } + return true; + } + + void mss::initialize(vector& cores, exprs& literals) { expr* n; + expr_set lits, core_lits; for (unsigned i = 0; i < literals.size(); ++i) { n = literals[i]; + lits.insert(n); m.is_not(n, n); if (!is_uninterp_const(n)) { throw default_exception("arguments have to be uninterpreted literals"); } } - // cores are disjoint - // cores are a subset of literals - // literals not in cores evaluate to true in current model - } - - /** - \brief Move literals satisfied in todo into mss. - Precondition: the solver state is satisfiable. - */ - void mss::update_model() { + exprs rest_core; expr_ref tmp(m); - s.get_model(m_model); - update_set(m_todo); + // + // the last core is a dummy core. It contains literals that + // did not occur in previous cores and did not evaluate to true + // in the current model. + // + for (unsigned i = 0; i < cores.size(); ++i) { + exprs const& core = cores[i]; + for (unsigned j = 0; j < core.size(); ++j) { + expr* n = core[j]; + if (!core_lits.contains(n)) { + core_lits.insert(n); + VERIFY(m_model->eval(n, tmp)); + if (m.is_true(tmp)) { + m_mss.push_back(n); + } + } + } + } + for (unsigned i = 0; i < literals.size(); ++i) { + expr* n = literals[i]; + if (!core_lits.contains(n)) { + VERIFY(m_model->eval(n, tmp)); + if (m.is_true(tmp)) { + m_mss.push_back(n); + } + else { + rest_core.push_back(n); + core_lits.insert(n); + } + } + } + cores.push_back(rest_core); } void mss::update_set(exprs& lits) { @@ -69,7 +108,7 @@ namespace opt { continue; } VERIFY(m_model->eval(n, tmp)); - if (m.is_false(tmp)) { + if (!m.is_true(tmp)) { if (j != i) { lits[j] = lits[i]; } @@ -83,33 +122,44 @@ namespace opt { } - lbool mss::operator()(vector const& cores, exprs& literals) { + lbool mss::operator()(vector const& _cores, exprs& literals) { m_mss.reset(); m_mcs.reset(); - m_todo.reset(); - m_todo.append(literals); - check_parameters(cores, literals); - update_model(); + m_s->get_model(m_model); + SASSERT(m_model); + vector cores(_cores); + TRACE("opt", + for (unsigned i = 0; i < cores.size(); ++i) { + display_vec(tout << "core: ", cores[i].size(), cores[i].c_ptr()); + } + display_vec(tout << "lits: ", literals.size(), literals.c_ptr()); + ); + initialize(cores, literals); + TRACE("opt", display(tout);); lbool is_sat = l_true; for (unsigned i = 0; is_sat == l_true && i < cores.size(); ++i) { - is_sat = process_core(cores[i]); + bool has_mcs = false; + bool is_last = i + 1 < cores.size(); + SASSERT(check_invariant()); + update_set(cores[i]); + is_sat = process_core(1, cores[i], has_mcs, is_last); } if (is_sat == l_true) { + SASSERT(check_invariant()); + TRACE("opt", display(tout);); literals.reset(); literals.append(m_mss); + SASSERT(check_result()); } return is_sat; } + - lbool mss::process_core(exprs const& _core) { - // at least one literal in core is false in current model. - // pick literals in core that are not yet in mss. - exprs core(_core); - update_set(core); - return process_core(1, core); - } - - lbool mss::process_core(unsigned sz, exprs& core) { + // + // at least one literal in core is false in current model. + // pick literals in core that are not yet in mss. + // + lbool mss::process_core(unsigned sz, exprs& core, bool& has_mcs, bool is_last) { TRACE("opt", tout << "process: " << sz << " out of " << core.size() << " literals\n";); SASSERT(sz > 0); if (core.empty()) { @@ -118,18 +168,25 @@ namespace opt { if (m_cancel) { return l_undef; } + if (sz == 1 && is_last && !has_mcs) { + // there has to be at least one false + // literal in the core. + m_mcs.insert(core[0]); + return l_true; + } sz = std::min(sz, core.size()); unsigned sz_save = m_mss.size(); m_mss.append(sz, core.c_ptr()); - lbool is_sat = s.check_sat(m_mss.size(), m_mss.c_ptr()); + lbool is_sat = m_s->check_sat(m_mss.size(), m_mss.c_ptr()); m_mss.resize(sz_save); switch (is_sat) { case l_true: - update_model(); + m_s->get_model(m_model); update_set(core); - return process_core(2*sz, core); + return process_core(2*sz, core, has_mcs, is_last); case l_false: if (sz == 1) { + has_mcs = true; m_mcs.insert(core[0]); core[0] = core.back(); core.pop_back(); @@ -138,12 +195,12 @@ namespace opt { exprs core2; core2.append(core.size()-sz, core.c_ptr()+sz); core.resize(sz); - is_sat = process_core(sz, core2); + is_sat = process_core(sz, core2, has_mcs, false); if (is_sat != l_true) { return is_sat; } } - return process_core(1, core); + return process_core(1, core, has_mcs, is_last); case l_undef: return l_undef; } @@ -151,8 +208,41 @@ namespace opt { return l_true; } + void mss::display_vec(std::ostream& out, unsigned sz, expr* const* args) const { + for (unsigned i = 0; i < sz; ++i) { + out << mk_pp(args[i], m) << " "; + } + out << "\n"; + } + void mss::display(std::ostream& out) const { - + expr_set::iterator it = m_mcs.begin(), end = m_mcs.end(); + out << "mcs:\n"; + for (; it != end; ++it) { + out << mk_pp(*it, m) << "\n"; + } + out << "\n"; + out << "mss:\n"; + for (unsigned i = 0; i < m_mss.size(); ++i) { + out << mk_pp(m_mss[i], m) << "\n"; + } + out << "\n"; + if (m_model) { + model_smt2_pp(out, m, *(m_model.get()), 0); + } + } + + bool mss::check_invariant() const { + if (!m_model) return true; + expr_ref tmp(m); + for (unsigned i = 0; i < m_mss.size(); ++i) { + expr* n = m_mss[i]; + VERIFY(m_model->eval(n, tmp)); + CTRACE("opt", !m.is_true(tmp), tout << mk_pp(n, m) << " |-> " << mk_pp(tmp, m) << "\n";); + SASSERT(!m.is_false(tmp)); + } + + return true; } } diff --git a/src/opt/mss.h b/src/opt/mss.h index 2e5d82df2..c434cd952 100644 --- a/src/opt/mss.h +++ b/src/opt/mss.h @@ -21,30 +21,34 @@ Notes: namespace opt { class mss { - solver& s; + ref& m_s; ast_manager& m; volatile bool m_cancel; typedef ptr_vector exprs; typedef obj_hashtable expr_set; exprs m_mss; expr_set m_mcs; - exprs m_todo; model_ref m_model; public: - mss(solver& s, ast_manager& m); + mss(ref& s, ast_manager& m); ~mss(); - lbool operator()(vector > const& cores, ptr_vector& literals); + lbool operator()(vector const& cores, exprs& literals); void set_cancel(bool f) { m_cancel = f; } + void get_model(model_ref& mdl) { mdl = m_model; } + private: - void check_parameters(vector const& cores, exprs& literals); + void initialize(vector& cores, exprs& literals); + bool check_result(); void update_model(); void update_set(exprs& lits); lbool process_core(exprs const& _core); - lbool process_core(unsigned sz, exprs& core); + lbool process_core(unsigned sz, exprs& core, bool& has_mcs, bool is_last); void display(std::ostream& out) const; + void display_vec(std::ostream& out, unsigned sz, expr* const* args) const; + bool check_invariant() const; }; };