diff --git a/src/opt/maxcore.cpp b/src/opt/maxcore.cpp index 46e4c5a7d..70bf38d87 100644 --- a/src/opt/maxcore.cpp +++ b/src/opt/maxcore.cpp @@ -9,10 +9,12 @@ Abstract: Core based (weighted) max-sat algorithms: - - mu: max-sat algorithm by Nina and Bacchus, AAAI 2014. - - mus-mss: based on dual refinement of bounds. - - binary: binary versino of maxres - - rc2: implementaion of rc2 heuristic using cardinality constraints + - mu: max-sat algorithm by Nina and Bacchus, AAAI 2014. + - mus-mss: based on dual refinement of bounds. + - binary: binary version of maxres + - rc2: implementaion of rc2 heuristic using cardinality constraints + - rc2-binary: hybrid of rc2 and binary maxres. Perform one step of binary maxres. + If there are more than 16 soft constraints create a cardinality constraint. MaxRes is a core-guided approach to maxsat. @@ -78,7 +80,8 @@ public: s_primal, s_primal_dual, s_primal_binary, - s_rc2 + s_rc2, + s_primal_binary_rc2 }; private: struct stats { @@ -157,6 +160,9 @@ public: case s_rc2: m_trace_id = "rc2"; break; + case s_primal_binary_rc2: + m_trace_id = "rc2bin"; + break; default: UNREACHABLE(); break; @@ -360,6 +366,7 @@ public: case s_primal: case s_primal_binary: case s_rc2: + case s_primal_binary_rc2: return mus_solver(); case s_primal_dual: return primal_dual_solver(); @@ -553,6 +560,9 @@ public: case strategy_t::s_rc2: max_resolve_rc2(core, w); break; + case strategy_t::s_primal_binary_rc2: + max_resolve_rc2bin(core, w); + break; default: max_resolve(core, w); break; @@ -717,10 +727,9 @@ public: m_defs.push_back(fml); } } - - - void bin_max_resolve(exprs const& _core, rational w) { - expr_ref_vector core(m, _core.size(), _core.data()); + + void bin_resolve(exprs const& _core, rational weight, expr_ref_vector& us) { + expr_ref_vector core(m, _core.size(), _core.data()), fmls(m); expr_ref fml(m), cls(m); for (unsigned i = 0; i + 1 < core.size(); i += 2) { expr* a = core.get(i); @@ -739,13 +748,19 @@ public: add(fml); update_model(v, cls); m_defs.push_back(fml); - new_assumption(u, w); + us.push_back(u); core.push_back(v); } - s().assert_expr(m.mk_not(core.back())); + s().assert_expr(m.mk_not(core.back())); } - + void bin_max_resolve(exprs const& _core, rational w) { + expr_ref_vector core(m, _core.size(), _core.data()), us(m); + expr_ref fml(m), cls(m); + bin_resolve(_core, w, us); + for (expr* u : us) + new_assumption(u, w); + } // rc2, using cardinality constraints @@ -785,10 +800,8 @@ public: return r; } - void max_resolve_rc2(exprs const& core, rational weight) { - expr_ref_vector ncore(m); + void weaken_bounds(exprs const& core) { for (expr* f : core) { - ncore.push_back(mk_not(m, f)); bound_info b; if (!m_bounds.find(f, b)) continue; @@ -800,6 +813,15 @@ public: new_assumption(amk, b.weight); m_unfold_upper -= b.weight; } + } + + void max_resolve_rc2(exprs const& core, rational weight) { + expr_ref_vector ncore(m); + for (expr* f : core) + ncore.push_back(mk_not(m, f)); + + weaken_bounds(core); + if (core.size() > 1) { m_unfold_upper += rational(core.size() - 2) * weight; expr* am = mk_atmost(ncore, 1, weight); @@ -807,6 +829,31 @@ public: } } + /** + * \brief hybrid of rc2 and binary resolution. + * Create us := u1, .., u_n, where core has size n + 1 + * If the core is of size at most 16 just use us as soft constraints + * Otherwise introduce a single soft constraint, the conjunction of us. + */ + + void max_resolve_rc2bin(exprs const& core, rational weight) { + weaken_bounds(core); + expr_ref_vector us(m); + bin_resolve(core, weight, us); + if (us.size() <= 15) { + for (auto* u : us) + new_assumption(u, weight); + } + else if (us.size() > 15) { + expr_ref_vector ncore(m); + for (expr* f : us) + ncore.push_back(mk_not(m, f)); + m_unfold_upper += rational(us.size() - 1) * weight; + expr* am = mk_atmost(ncore, 0, weight); + new_assumption(am, weight); + } + } + // cs is a correction set (a complement of a (maximal) satisfying assignment). void cs_max_resolve(exprs const& cs, rational const& w) { @@ -1062,6 +1109,11 @@ opt::maxsmt_solver_base* opt::mk_rc2( return alloc(maxcore, c, id, soft, maxcore::s_rc2); } +opt::maxsmt_solver_base* opt::mk_rc2bin( + maxsat_context& c, unsigned id, vector& soft) { + return alloc(maxcore, c, id, soft, maxcore::s_primal_binary_rc2); +} + opt::maxsmt_solver_base* opt::mk_maxres_binary( maxsat_context& c, unsigned id, vector& soft) { return alloc(maxcore, c, id, soft, maxcore::s_primal_binary); diff --git a/src/opt/maxcore.h b/src/opt/maxcore.h index 2dba613a7..2038c5e98 100644 --- a/src/opt/maxcore.h +++ b/src/opt/maxcore.h @@ -23,6 +23,8 @@ namespace opt { maxsmt_solver_base* mk_rc2(maxsat_context& c, unsigned id, vector& soft); + maxsmt_solver_base* mk_rc2bin(maxsat_context& c, unsigned id, vector& soft); + maxsmt_solver_base* mk_maxres(maxsat_context& c, unsigned id, vector& soft); maxsmt_solver_base* mk_maxres_binary(maxsat_context& c, unsigned id, vector& soft); diff --git a/src/opt/maxsmt.cpp b/src/opt/maxsmt.cpp index 6064ef899..3d0834472 100644 --- a/src/opt/maxsmt.cpp +++ b/src/opt/maxsmt.cpp @@ -185,27 +185,22 @@ namespace opt { symbol const& maxsat_engine = m_c.maxsat_engine(); IF_VERBOSE(1, verbose_stream() << "(maxsmt)\n";); TRACE("opt_verbose", s().display(tout << "maxsmt\n") << "\n";); - if (optp.maxlex_enable() && is_maxlex(m_soft)) { + if (optp.maxlex_enable() && is_maxlex(m_soft)) m_msolver = mk_maxlex(m_c, m_index, m_soft); - } - else if (m_soft.empty() || maxsat_engine == symbol("maxres") || maxsat_engine == symbol::null) { + else if (m_soft.empty() || maxsat_engine == symbol("maxres") || maxsat_engine == symbol::null) m_msolver = mk_maxres(m_c, m_index, m_soft); - } - else if (maxsat_engine == symbol("maxres-bin")) { + else if (maxsat_engine == symbol("maxres-bin")) m_msolver = mk_maxres_binary(m_c, m_index, m_soft); - } - else if (maxsat_engine == symbol("rc2")) { + else if (maxsat_engine == symbol("rc2")) m_msolver = mk_rc2(m_c, m_index, m_soft); - } - else if (maxsat_engine == symbol("pd-maxres")) { + else if (maxsat_engine == symbol("rc2bin")) + m_msolver = mk_rc2bin(m_c, m_index, m_soft); + else if (maxsat_engine == symbol("pd-maxres")) m_msolver = mk_primal_dual_maxres(m_c, m_index, m_soft); - } - else if (maxsat_engine == symbol("wmax")) { + else if (maxsat_engine == symbol("wmax")) m_msolver = mk_wmax(m_c, m_soft, m_index); - } - else if (maxsat_engine == symbol("sortmax")) { + else if (maxsat_engine == symbol("sortmax")) m_msolver = mk_sortmax(m_c, m_soft, m_index); - } else { auto str = maxsat_engine.str(); warning_msg("solver %s is not recognized, using default 'maxres'", str.c_str());