From e5aa79ba6a1f1e5e5ba38716c71247ccb70c0391 Mon Sep 17 00:00:00 2001 From: TheRealNebus Date: Mon, 19 Feb 2018 13:29:15 +0000 Subject: [PATCH] disjoint cores --- src/opt/mss_solver.cpp | 221 +++++++++++++++++++++++++++++------------ src/opt/opt_params.pyg | 3 +- 2 files changed, 161 insertions(+), 63 deletions(-) diff --git a/src/opt/mss_solver.cpp b/src/opt/mss_solver.cpp index d27b6300c..1ac351855 100755 --- a/src/opt/mss_solver.cpp +++ b/src/opt/mss_solver.cpp @@ -11,45 +11,85 @@ class mss_solver: public maxsmt_solver_base { private: typedef ptr_vector exprs; + typedef obj_hashtable expr_set; mss m_mss; unsigned m_index; - expr_ref_vector m_asms; + exprs m_asms; + unsigned m_mss_found; + vector m_cores; + unsigned m_core_idx; + model_ref m_last_model; + exprs m_mss_trail; + exprs m_mcs_trail; + unsigned_vector m_mss_trail_lim; + unsigned_vector m_mcs_trail_lim; unsigned m_max_mss; + bool m_disjoint_cores; public: mss_solver(maxsat_context& c, unsigned id, weights_t& ws, expr_ref_vector const& soft): maxsmt_solver_base(c, ws, soft), m_mss(c.get_solver(), m), m_index(id), - m_asms(m), - m_max_mss(UINT_MAX) { + m_mss_found(0), + m_core_idx(0), + m_max_mss(UINT_MAX), + m_disjoint_cores(false) { } virtual ~mss_solver() {} virtual lbool operator()() { if (!init()) return l_undef; - init_asms(); - lbool is_sat = check_sat(m_asms); - if (is_sat == l_undef) return l_undef; - if (is_sat == l_true) { - IF_VERBOSE(2, verbose_stream() << "(opt.mss-solver :mss " << m_asms.size() << " :mcs " << 0 << ")\n";); - model_ref mdl; - s().get_model(mdl); - update_assignment(mdl.get()); - return l_true; + init_local(); + lbool is_sat = disjoint_cores(); + if (is_sat != l_true) return is_sat; + if (m_cores.size() == 0) return l_true; + update_model(); + exprs asms; + while (true) { + exprs mss, mcs; + mss.append(m_cores[m_core_idx]); + is_sat = cld(m_last_model, mss, mcs); + if (is_sat == l_undef || m.canceled()) return l_undef; + SASSERT(is_sat == l_true); + update_trails(mss, mcs); + if (m_core_idx < m_cores.size()-1) { + m_core_idx++; + } + else { + IF_VERBOSE(2, verbose_stream() << "(opt.mss-solver :mss " << m_mss_trail.size() + m_asms.size() << " :mcs " << m_mcs_trail.size() << ")\n";); + if (++m_mss_found >= m_max_mss) return l_true; + asms.push_back(relax_and_assert(m.mk_or(m_mcs_trail.size(), m_mcs_trail.c_ptr()))); + is_sat = backtrack(asms); + if (is_sat == l_false) { + SASSERT(m_core_idx == 0); + is_sat = disjoint_cores(asms); + } + if (is_sat == l_undef) return l_undef; + if (is_sat == l_false) return l_true; + } } - return enumerate_mss(); + return l_true; } virtual void updt_params(params_ref& p) { maxsmt_solver_base::updt_params(p); opt_params _p(p); m_max_mss = _p.mss_max(); + m_disjoint_cores = _p.mss_disjoint_cores(); } private: - void init_asms() { + void init_local() { + m_cores.reset(); + m_core_idx = 0; + m_mss_found = 0; + m_last_model.reset(); + m_mss_trail.reset(); + m_mcs_trail.reset(); + m_mss_trail_lim.reset(); + m_mcs_trail_lim.reset(); m_asms.reset(); for (unsigned i = 0; i < m_soft.size(); ++i) { expr* e = m_soft[i]; @@ -74,42 +114,84 @@ private: return is_uninterp_const(l) || (m.is_not(l, l) && is_uninterp_const(l)); } - lbool enumerate_mss() { - expr_ref_vector asms(m); - for (unsigned i = 0; i < m_max_mss; ++i) { - exprs mss, mcs; - lbool is_sat = next_mss(asms, mss, mcs); - if (is_sat == l_false && i == 0) return l_false; - if (is_sat == l_undef && i == 0) return l_undef; - if (is_sat == l_false || is_sat == l_undef) return l_true; - asms.push_back(relax_and_assert(m.mk_or(mcs.size(), mcs.c_ptr()))); + lbool disjoint_cores(exprs const& asms) { + expr_set asm_lits, core_lits; + for (unsigned i = 0; i < asms.size(); ++i) { + asm_lits.insert(asms[i]); } - return l_true; + lbool is_sat = l_false; + exprs core; + while (is_sat == l_false) { + exprs tmp_asms; + tmp_asms.append(asms); + tmp_asms.append(m_asms); + is_sat = check_sat(tmp_asms); + if (is_sat == l_true) { + update_model(); + } + else if (is_sat == l_false) { + core.reset(); + s().get_unsat_core(core); + for (unsigned i = 0; i < core.size();) { + if (asm_lits.contains(core[i])) { + core[i] = core.back(); + core.pop_back(); + } + else { + core_lits.insert(core[i]); + ++i; + } + } + if (core.empty()) { + IF_VERBOSE(2, verbose_stream() << "(opt.mss-solver empty core)\n";); + return l_false; + } + if (m_disjoint_cores) { + m_cores.push_back(core); + IF_VERBOSE(2, verbose_stream() << "(opt.mss-solver :core-size " << core.size() << " :num-cores " << m_cores.size() << ")\n";); + for (unsigned i = 0; i < m_asms.size();) { + if (core_lits.contains(m_asms[i]) || !m_disjoint_cores) { + m_asms[i] = m_asms.back(); + m_asms.pop_back(); + } + else { + ++i; + } + } + } + else { + m_cores.push_back(m_asms); + m_asms.reset(); + } + } + } + IF_VERBOSE(2, verbose_stream() << "(opt.mss-solver :num-cores " << m_cores.size() << ")\n";); + // TODO: update m_lower? + return is_sat; } - lbool next_mss(expr_ref_vector const& asms, exprs& mss, exprs& mcs) { - mss.reset(); - mcs.reset(); - lbool is_sat = check_sat(asms); - if (is_sat != l_true) return is_sat; - model_ref mdl; - s().get_model(mdl); - update_assignment(mdl.get()); - vector dummy; - push_exprs(mss, m_asms); - push_exprs(mss, asms); - is_sat = cld(mdl.get(), mss, mcs); - if (is_sat == l_true) { - IF_VERBOSE(2, verbose_stream() << "(opt.mss-solver :mss " << mss.size() - asms.size() << " :mcs " << mcs.size() << ")\n";); + lbool disjoint_cores() { + return disjoint_cores(exprs()); + } + + lbool backtrack(exprs& asms) { + SASSERT(m_mss_trail_lim.size() == m_mcs_trail_lim.size()); + lbool is_sat = l_false; + while (is_sat == l_false && m_core_idx > 0) { + m_core_idx--; + m_mss_trail.resize(m_mss_trail_lim.back()); + m_mss_trail_lim.pop_back(); + m_mcs_trail.resize(m_mcs_trail_lim.back()); + m_mcs_trail_lim.pop_back(); + exprs tmp_asms; + tmp_asms.append(asms); + get_trail_asms(tmp_asms); + is_sat = check_sat(tmp_asms); + if (is_sat == l_true) { + update_model(); + } } - /*is_sat = m_mss(mdl.get(), dummy, mss, mcs); - SASSERT(is_sat != l_false); - if (is_sat == l_true) { - mdl.reset(); - m_mss.get_model(mdl); - update_assignment(mdl.get()); - IF_VERBOSE(2, verbose_stream() << "(opt.mss-solver :mss " << mss.size() - asms.size() << " :mcs " << mcs.size() << ")\n";); - }*/ + IF_VERBOSE(2, verbose_stream() << "(opt.mss-solver :backtrack-lvl " << m_core_idx << ")\n";); return is_sat; } @@ -118,19 +200,19 @@ private: undef.append(mss); update_sat(initial_model, sat, undef); lbool is_sat = l_true; - while (is_sat == l_true) { + while (is_sat == l_true && !undef.empty()) { expr_ref asum = relax_and_assert(m.mk_or(undef.size(), undef.c_ptr())); - sat.push_back(asum); - is_sat = check_sat(sat); - sat.pop_back(); + exprs asms; + asms.append(sat); + get_trail_asms(asms); + asms.push_back(asum); + is_sat = check_sat(asms); if (is_sat == l_true) { - model_ref mdl; - s().get_model(mdl); - update_sat(mdl, sat, undef); - update_assignment(mdl.get()); + update_model(); + update_sat(m_last_model, sat, undef); } } - if (is_sat == l_false) { + if (is_sat == l_false || undef.empty()) { mss.reset(); mcs.reset(); mss.append(sat); @@ -140,6 +222,26 @@ private: return is_sat; } + void get_trail_asms(exprs& asms) { + asms.append(m_mss_trail); + for (unsigned i = 0; i < m_mcs_trail.size(); ++i) { + asms.push_back(m.mk_not(m_mcs_trail[i])); + } + } + + void update_trails(exprs const& mss, exprs const& mcs) { + m_mss_trail_lim.push_back(m_mss_trail.size()); + m_mcs_trail_lim.push_back(m_mcs_trail.size()); + m_mss_trail.append(mss); + m_mcs_trail.append(mcs); + } + + void update_model() { + m_last_model.reset(); + s().get_model(m_last_model); + update_assignment(m_last_model.get()); + } + void update_sat(model_ref mdl, exprs& sat, exprs& undef) { for (unsigned i = 0; i < undef.size();) { if (is_true(mdl.get(), undef[i])) { @@ -160,12 +262,7 @@ private: } lbool check_sat() { - expr_ref_vector dummy(m); - return check_sat(dummy); - } - - lbool check_sat(expr_ref_vector const& asms) { - return s().check_sat(asms); + return check_sat(exprs()); } lbool check_sat(exprs const& asms) { @@ -186,7 +283,7 @@ private: for (unsigned i = 0; i < m_soft.size(); ++i) { m_assignment[i] = is_true(m_soft[i]); } - // TODO: DEBUG verify assignment + // TODO: DEBUG verify assignment? m_upper = upper; trace_bounds("mss-solver"); } diff --git a/src/opt/opt_params.pyg b/src/opt/opt_params.pyg index 4cb22389d..41548452a 100644 --- a/src/opt/opt_params.pyg +++ b/src/opt/opt_params.pyg @@ -21,7 +21,8 @@ def_module_params('opt', ('maxres.max_correction_set_size', UINT, 3, 'allow generating correction set constraints up to maximal size'), ('maxres.wmax', BOOL, False, 'use weighted theory solver to constrain upper bounds'), ('maxres.pivot_on_correction_set', BOOL, True, 'reduce soft constraints if the current correction set is smaller than current core'), - ('mss.max', UINT, UINT_MAX, 'maximum number of MSS to enumerate') + ('mss.max', UINT, UINT_MAX, 'maximum number of MSS to enumerate'), + ('mss.disjoint_cores', BOOL, True, 'partition soft based on disjoint cores') ))