diff --git a/src/opt/maxcore.cpp b/src/opt/maxcore.cpp index f23954506..20cc028aa 100644 --- a/src/opt/maxcore.cpp +++ b/src/opt/maxcore.cpp @@ -85,7 +85,6 @@ public: s_primal_dual, s_primal_binary, s_rc2, - s_rc2tot, s_primal_binary_rc2 }; private: @@ -136,6 +135,7 @@ private: bool m_enable_lns = false; // enable LNS improvements unsigned m_lns_conflicts = 1000; // number of conflicts used for LNS improvement bool m_enable_core_rotate = false; // enable core rotation + bool m_use_totalizer = true; // use totalizer instead of cardinality encoding std::string m_trace_id; typedef ptr_vector exprs; @@ -165,9 +165,6 @@ public: case s_rc2: m_trace_id = "rc2"; break; - case s_rc2tot: - m_trace_id = "rc2tot"; - break; case s_primal_binary_rc2: m_trace_id = "rc2bin"; break; @@ -177,7 +174,10 @@ public: } } - ~maxcore() override {} + ~maxcore() override { + for (auto& [k,t] : m_totalizers) + dealloc(t); + } bool is_literal(expr* l) { return @@ -374,7 +374,6 @@ public: case s_primal: case s_primal_binary: case s_rc2: - case s_rc2tot: case s_primal_binary_rc2: return mus_solver(); case s_primal_dual: @@ -567,7 +566,6 @@ public: bin_max_resolve(core, w); break; case strategy_t::s_rc2: - case strategy_t::s_rc2tot: max_resolve_rc2(core, w); break; case strategy_t::s_primal_binary_rc2: @@ -820,7 +818,7 @@ public: } expr* mk_atmost(expr_ref_vector const& es, unsigned bound, rational const& weight) { - if (m_st == strategy_t::s_rc2tot) + if (m_use_totalizer) return mk_atmost_tot(es, bound, weight); pb_util pb(m); expr_ref am(pb.mk_at_most_k(es, bound), m); @@ -1064,6 +1062,7 @@ public: m_enable_lns = p.enable_lns(); m_enable_core_rotate = p.enable_core_rotate(); m_lns_conflicts = p.lns_conflicts(); + m_use_totalizer = p.rc2_totalizer(); if (m_c.num_objectives() > 1) m_add_upper_bound_block = false; } @@ -1152,10 +1151,6 @@ opt::maxsmt_solver_base* opt::mk_rc2( return alloc(maxcore, c, id, soft, maxcore::s_rc2); } -opt::maxsmt_solver_base* opt::mk_rc2tot( - maxsat_context& c, unsigned id, vector& soft) { - return alloc(maxcore, c, id, soft, maxcore::s_rc2tot); -} opt::maxsmt_solver_base* opt::mk_rc2bin( maxsat_context& c, unsigned id, vector& soft) { diff --git a/src/opt/maxcore.h b/src/opt/maxcore.h index f64184e7f..2038c5e98 100644 --- a/src/opt/maxcore.h +++ b/src/opt/maxcore.h @@ -23,8 +23,6 @@ namespace opt { maxsmt_solver_base* mk_rc2(maxsat_context& c, unsigned id, vector& soft); - maxsmt_solver_base* mk_rc2tot(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); diff --git a/src/opt/maxsmt.cpp b/src/opt/maxsmt.cpp index a6eb17aa5..3d0834472 100644 --- a/src/opt/maxsmt.cpp +++ b/src/opt/maxsmt.cpp @@ -193,8 +193,6 @@ namespace opt { m_msolver = mk_maxres_binary(m_c, m_index, m_soft); else if (maxsat_engine == symbol("rc2")) m_msolver = mk_rc2(m_c, m_index, m_soft); - else if (maxsat_engine == symbol("rc2tot")) - m_msolver = mk_rc2tot(m_c, m_index, m_soft); else if (maxsat_engine == symbol("rc2bin")) m_msolver = mk_rc2bin(m_c, m_index, m_soft); else if (maxsat_engine == symbol("pd-maxres")) diff --git a/src/opt/opt_params.pyg b/src/opt/opt_params.pyg index 93ecddbe4..df3ab0925 100644 --- a/src/opt/opt_params.pyg +++ b/src/opt/opt_params.pyg @@ -19,6 +19,7 @@ def_module_params('opt', ('pb.compile_equality', BOOL, False, 'compile arithmetical equalities into pseudo-Boolean equality (instead of two inequalites)'), ('pp.wcnf', BOOL, False, 'print maxsat benchmark into wcnf format'), ('maxlex.enable', BOOL, True, 'enable maxlex heuristic for lexicographic MaxSAT problems'), + ('rc2.totalizer', BOOL, True, 'use totalizer for rc2 encoding'), ('maxres.hill_climb', BOOL, True, 'give preference for large weight cores'), ('maxres.add_upper_bound_block', BOOL, False, 'restict upper bound with constraint'), ('maxres.max_num_cores', UINT, 200, 'maximal number of cores per round'), diff --git a/src/opt/totalizer.cpp b/src/opt/totalizer.cpp index 1e4618b24..41d730560 100644 --- a/src/opt/totalizer.cpp +++ b/src/opt/totalizer.cpp @@ -37,7 +37,7 @@ namespace opt { expr_ref c(m), def(m); expr_ref_vector ors(m), clause(m); for (unsigned i = k; i > 0 && !lits.get(i - 1); --i) { - if (l->m_literals.size() + r->m_literals.size() < i) { + if (l->size() + r->size() < i) { lits[i - 1] = m.mk_false(); continue; } @@ -55,9 +55,9 @@ namespace opt { for (unsigned j1 = 0; j1 <= i; ++j1) { unsigned j2 = i - j1; - if (j1 > l->m_literals.size()) + if (j1 > l->size()) continue; - if (j2 > r->m_literals.size()) + if (j2 > r->size()) continue; clause.reset(); if (0 < j1) { @@ -93,37 +93,27 @@ namespace opt { node* left = trees[i]; node* right = trees[i + 1]; expr_ref_vector ls(m); - ls.resize(left->m_literals.size() + right->m_literals.size()); + ls.resize(left->size() + right->size()); node* n = alloc(node, ls); n->m_left = left; n->m_right = right; trees.push_back(n); } - m_tree = trees.back(); + m_root = trees.back(); } totalizer::~totalizer() { - ptr_vector trees; - trees.push_back(m_tree); - while (!trees.empty()) { - node* n = trees.back(); - trees.pop_back(); - if (n->m_left) - trees.push_back(n->m_left); - if (n->m_right) - trees.push_back(n->m_right); - dealloc(n); - } + dealloc(m_root); } expr* totalizer::at_least(unsigned k) { if (k == 0) return m.mk_true(); - if (m_tree->m_literals.size() < k) + if (m_root->size() < k) return m.mk_false(); - SASSERT(1 <= k && k <= m_tree->m_literals.size()); - ensure_bound(m_tree, k); - return m_tree->m_literals.get(k - 1); + SASSERT(1 <= k && k <= m_root->size()); + ensure_bound(m_root, k); + return m_root->m_literals.get(k - 1); } } diff --git a/src/opt/totalizer.h b/src/opt/totalizer.h index eba4474d0..3d26fa2e6 100644 --- a/src/opt/totalizer.h +++ b/src/opt/totalizer.h @@ -26,11 +26,17 @@ namespace opt { node* m_right = nullptr; expr_ref_vector m_literals; node(expr_ref_vector& l): m_literals(l) {} + ~node() { + dealloc(m_left); + dealloc(m_right); + } + unsigned size() const { return m_literals.size(); } + }; ast_manager& m; expr_ref_vector m_literals; - node* m_tree = nullptr; + node* m_root = nullptr; expr_ref_vector m_clauses; vector> m_defs;