From 4ab27eff78276d38853964e5ca40c2614ecbb463 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 28 Jul 2014 08:31:57 -0700 Subject: [PATCH] refactor weighted-maxsat into separate files Signed-off-by: Nikolaj Bjorner --- src/opt/bcd2.cpp | 408 +++++++++++ src/opt/bcd2.h | 29 + src/opt/dual_maxres.cpp | 429 +++++++++++ src/opt/dual_maxres.h | 32 + src/opt/maxhs.cpp | 561 ++++++++++++++ src/opt/maxhs.h | 29 + src/opt/maxres.cpp | 2 +- src/opt/maxsls.cpp | 63 ++ src/opt/maxsls.h | 36 + src/opt/maxsmt.cpp | 17 +- src/opt/mus.cpp | 15 +- src/opt/pbmax.cpp | 98 +++ src/opt/pbmax.h | 30 + src/opt/weighted_maxsat.cpp | 1384 ----------------------------------- src/opt/weighted_maxsat.h | 51 -- src/opt/wmax.cpp | 130 ++++ src/opt/wmax.h | 30 + src/opt/wpm2.cpp | 251 +++++++ src/opt/wpm2.h | 29 + src/smt/theory_wmaxsat.cpp | 1 - 20 files changed, 2179 insertions(+), 1446 deletions(-) create mode 100644 src/opt/bcd2.cpp create mode 100644 src/opt/bcd2.h create mode 100644 src/opt/dual_maxres.cpp create mode 100644 src/opt/dual_maxres.h create mode 100644 src/opt/maxhs.cpp create mode 100644 src/opt/maxhs.h create mode 100644 src/opt/maxsls.cpp create mode 100644 src/opt/maxsls.h create mode 100644 src/opt/pbmax.cpp create mode 100644 src/opt/pbmax.h delete mode 100644 src/opt/weighted_maxsat.cpp delete mode 100644 src/opt/weighted_maxsat.h create mode 100644 src/opt/wmax.cpp create mode 100644 src/opt/wmax.h create mode 100644 src/opt/wpm2.cpp create mode 100644 src/opt/wpm2.h diff --git a/src/opt/bcd2.cpp b/src/opt/bcd2.cpp new file mode 100644 index 000000000..cb579b9ef --- /dev/null +++ b/src/opt/bcd2.cpp @@ -0,0 +1,408 @@ +/*++ +Copyright (c) 2014 Microsoft Corporation + +Module Name: + + bcd2.cpp + +Abstract: + + bcd2 based MaxSAT. + +Author: + + Nikolaj Bjorner (nbjorner) 2014-4-17 + +Notes: + +--*/ +#include "bcd2.h" +#include "pb_decl_plugin.h" +#include "uint_set.h" +#include "ast_pp.h" + + +namespace opt { + // ------------------------------------------------------ + // Morgado, Heras, Marques-Silva 2013 + // (initial version without model-based optimizations) + // + class bcd2 : public maxsmt_solver_base { + struct wcore { + expr* m_r; + unsigned_vector m_R; + rational m_lower; + rational m_mid; + rational m_upper; + }; + typedef obj_hashtable expr_set; + + pb_util pb; + expr_ref_vector m_soft_aux; + obj_map m_relax2index; // expr |-> index + obj_map m_soft2index; // expr |-> index + expr_ref_vector m_trail; + expr_ref_vector m_soft_constraints; + expr_set m_asm_set; + vector m_cores; + vector m_sigmas; + rational m_den; // least common multiplier of original denominators + bool m_enable_lazy; // enable adding soft constraints lazily (called 'mgbcd2') + unsigned_vector m_lazy_soft; // soft constraints to add lazily. + + void set2asms(expr_set const& set, expr_ref_vector & es) const { + es.reset(); + expr_set::iterator it = set.begin(), end = set.end(); + for (; it != end; ++it) { + es.push_back(m.mk_not(*it)); + } + } + void bcd2_init_soft(vector const& weights, expr_ref_vector const& soft) { + + // normalize weights to be integral: + m_den = rational::one(); + for (unsigned i = 0; i < m_weights.size(); ++i) { + m_den = lcm(m_den, denominator(m_weights[i])); + } + if (!m_den.is_one()) { + for (unsigned i = 0; i < m_weights.size(); ++i) { + m_weights[i] = m_den*m_weights[i]; + SASSERT(m_weights[i].is_int()); + } + } + } + void init_bcd() { + m_trail.reset(); + m_asm_set.reset(); + m_cores.reset(); + m_sigmas.reset(); + m_lazy_soft.reset(); + for (unsigned i = 0; i < m_soft.size(); ++i) { + m_sigmas.push_back(m_weights[i]); + m_soft_aux.push_back(mk_fresh()); + if (m_enable_lazy) { + m_lazy_soft.push_back(i); + } + else { + enable_soft_constraint(i); + } + } + m_upper += rational(1); + } + + void process_sat() { + svector assignment; + update_assignment(assignment); + if (check_lazy_soft(assignment)) { + update_sigmas(); + } + } + + public: + bcd2(opt_solver* s, ast_manager& m, params_ref& p, + vector const& ws, expr_ref_vector const& soft): + maxsmt_solver_base(s, m, p, ws, soft), + pb(m), + m_soft_aux(m), + m_trail(m), + m_soft_constraints(m), + m_enable_lazy(true) { + bcd2_init_soft(ws, soft); + } + + virtual ~bcd2() {} + + virtual lbool operator()() { + expr_ref fml(m), r(m); + lbool is_sat = l_undef; + expr_ref_vector asms(m); + enable_sls(); + solver::scoped_push _scope1(s()); + init(); + init_bcd(); + if (m_cancel) { + normalize_bounds(); + return l_undef; + } + process_sat(); + while (m_lower < m_upper) { + IF_VERBOSE(1, verbose_stream() << "(opt.bcd2 [" << m_lower << ":" << m_upper << "])\n";); + assert_soft(); + solver::scoped_push _scope2(s()); + TRACE("opt", display(tout);); + assert_cores(); + set2asms(m_asm_set, asms); + if (m_cancel) { + normalize_bounds(); + return l_undef; + } + is_sat = s().check_sat(asms.size(), asms.c_ptr()); + switch(is_sat) { + case l_undef: + normalize_bounds(); + return l_undef; + case l_true: + process_sat(); + break; + case l_false: { + ptr_vector unsat_core; + uint_set subC, soft; + s().get_unsat_core(unsat_core); + core2indices(unsat_core, subC, soft); + SASSERT(unsat_core.size() == subC.num_elems() + soft.num_elems()); + if (soft.num_elems() == 0 && subC.num_elems() == 1) { + unsigned s = *subC.begin(); + wcore& c_s = m_cores[s]; + c_s.m_lower = refine(c_s.m_R, c_s.m_mid); + c_s.m_mid = div(c_s.m_lower + c_s.m_upper, rational(2)); + } + else { + wcore c_s; + rational delta = min_of_delta(subC); + rational lower = sum_of_lower(subC); + union_Rs(subC, c_s.m_R); + r = mk_fresh(); + relax(subC, soft, c_s.m_R, delta); + c_s.m_lower = refine(c_s.m_R, lower + delta - rational(1)); + c_s.m_upper = rational::one(); + c_s.m_upper += sum_of_sigmas(c_s.m_R); + c_s.m_mid = div(c_s.m_lower + c_s.m_upper, rational(2)); + c_s.m_r = r; + m_asm_set.insert(r); + subtract(m_cores, subC); + m_relax2index.insert(r, m_cores.size()); + m_cores.push_back(c_s); + } + break; + } + } + m_lower = compute_lower(); + } + normalize_bounds(); + return l_true; + } + + + private: + + void enable_soft_constraint(unsigned i) { + expr_ref fml(m); + expr* r = m_soft_aux[i].get(); + m_soft2index.insert(r, i); + fml = m.mk_or(r, m_soft[i].get()); + m_soft_constraints.push_back(fml); + m_asm_set.insert(r); + SASSERT(m_weights[i].is_int()); + } + + void assert_soft() { + for (unsigned i = 0; i < m_soft_constraints.size(); ++i) { + s().assert_expr(m_soft_constraints[i].get()); + } + m_soft_constraints.reset(); + } + + bool check_lazy_soft(svector const& assignment) { + bool all_satisfied = true; + for (unsigned i = 0; i < m_lazy_soft.size(); ++i) { + unsigned j = m_lazy_soft[i]; + if (!assignment[j]) { + enable_soft_constraint(j); + m_lazy_soft[i] = m_lazy_soft.back(); + m_lazy_soft.pop_back(); + --i; + all_satisfied = false; + } + } + return all_satisfied; + } + + void normalize_bounds() { + m_lower /= m_den; + m_upper /= m_den; + } + + expr* mk_fresh() { + expr* r = mk_fresh_bool("r"); + m_trail.push_back(r); + return r; + } + + void update_assignment(svector& new_assignment) { + expr_ref val(m); + rational new_upper(0); + model_ref model; + new_assignment.reset(); + s().get_model(model); + for (unsigned i = 0; i < m_soft.size(); ++i) { + VERIFY(model->eval(m_soft[i].get(), val)); + new_assignment.push_back(m.is_true(val)); + if (!new_assignment[i]) { + new_upper += m_weights[i]; + } + } + if (new_upper < m_upper) { + m_upper = new_upper; + m_model = model; + m_assignment.reset(); + m_assignment.append(new_assignment); + } + } + + void update_sigmas() { + for (unsigned i = 0; i < m_cores.size(); ++i) { + wcore& c_i = m_cores[i]; + unsigned_vector const& R = c_i.m_R; + c_i.m_upper.reset(); + for (unsigned j = 0; j < R.size(); ++j) { + unsigned r_j = R[j]; + if (!m_assignment[r_j]) { + c_i.m_upper += m_weights[r_j]; + m_sigmas[r_j] = m_weights[r_j]; + } + else { + m_sigmas[r_j].reset(); + } + } + c_i.m_mid = div(c_i.m_lower + c_i.m_upper, rational(2)); + } + } + + /** + * Minimum of two (positive) numbers. Zero is treated as +infinity. + */ + rational min_z(rational const& a, rational const& b) { + if (a.is_zero()) return b; + if (b.is_zero()) return a; + if (a < b) return a; + return b; + } + + rational min_of_delta(uint_set const& subC) { + rational delta(0); + for (uint_set::iterator it = subC.begin(); it != subC.end(); ++it) { + unsigned j = *it; + wcore const& core = m_cores[j]; + rational new_delta = rational(1) + core.m_upper - core.m_mid; + SASSERT(new_delta.is_pos()); + delta = min_z(delta, new_delta); + } + return delta; + } + + rational sum_of_lower(uint_set const& subC) { + rational lower(0); + for (uint_set::iterator it = subC.begin(); it != subC.end(); ++it) { + lower += m_cores[*it].m_lower; + } + return lower; + } + + rational sum_of_sigmas(unsigned_vector const& R) { + rational sum(0); + for (unsigned i = 0; i < R.size(); ++i) { + sum += m_sigmas[R[i]]; + } + return sum; + } + void union_Rs(uint_set const& subC, unsigned_vector& R) { + for (uint_set::iterator it = subC.begin(); it != subC.end(); ++it) { + R.append(m_cores[*it].m_R); + } + } + rational compute_lower() { + rational result(0); + for (unsigned i = 0; i < m_cores.size(); ++i) { + result += m_cores[i].m_lower; + } + return result; + } + void subtract(vector& cores, uint_set const& subC) { + unsigned j = 0; + for (unsigned i = 0; i < cores.size(); ++i) { + if (subC.contains(i)) { + m_asm_set.remove(cores[i].m_r); + } + else { + if (j != i) { + cores[j] = cores[i]; + } + ++j; + } + } + cores.resize(j); + for (unsigned i = 0; i < cores.size(); ++i) { + m_relax2index.insert(cores[i].m_r, i); + } + } + void core2indices(ptr_vector const& core, uint_set& subC, uint_set& soft) { + for (unsigned i = 0; i < core.size(); ++i) { + unsigned j; + expr* a; + VERIFY(m.is_not(core[i], a)); + if (m_relax2index.find(a, j)) { + subC.insert(j); + } + else { + VERIFY(m_soft2index.find(a, j)); + soft.insert(j); + } + } + } + rational refine(unsigned_vector const& idx, rational v) { + return v + rational(1); + } + void relax(uint_set& subC, uint_set& soft, unsigned_vector& R, rational& delta) { + for (uint_set::iterator it = soft.begin(); it != soft.end(); ++it) { + R.push_back(*it); + delta = min_z(delta, m_weights[*it]); + m_asm_set.remove(m_soft_aux[*it].get()); + } + } + void assert_cores() { + for (unsigned i = 0; i < m_cores.size(); ++i) { + assert_core(m_cores[i]); + } + } + void assert_core(wcore const& core) { + expr_ref fml(m); + vector ws; + ptr_vector rs; + rational w(0); + for (unsigned j = 0; j < core.m_R.size(); ++j) { + unsigned idx = core.m_R[j]; + ws.push_back(m_weights[idx]); + w += ws.back(); + rs.push_back(m_soft_aux[idx].get()); + } + w.neg(); + w += core.m_mid; + ws.push_back(w); + rs.push_back(core.m_r); + fml = pb.mk_le(ws.size(), ws.c_ptr(), rs.c_ptr(), core.m_mid); + s().assert_expr(fml); + } + void display(std::ostream& out) { + out << "[" << m_lower << ":" << m_upper << "]\n"; + s().display(out); + out << "\n"; + for (unsigned i = 0; i < m_cores.size(); ++i) { + wcore const& c = m_cores[i]; + out << mk_pp(c.m_r, m) << ": "; + for (unsigned j = 0; j < c.m_R.size(); ++j) { + out << c.m_R[j] << " (" << m_sigmas[c.m_R[j]] << ") "; + } + out << "[" << c.m_lower << ":" << c.m_mid << ":" << c.m_upper << "]\n"; + } + for (unsigned i = 0; i < m_soft.size(); ++i) { + out << mk_pp(m_soft[i].get(), m) << " " << m_weights[i] << "\n"; + } + } + }; + + maxsmt_solver_base* opt::mk_bcd2(ast_manager& m, opt_solver* s, params_ref& p, + vector const& ws, expr_ref_vector const& soft) { + return alloc(bcd2, s, m, p, ws, soft); + } + +} diff --git a/src/opt/bcd2.h b/src/opt/bcd2.h new file mode 100644 index 000000000..db08b15ef --- /dev/null +++ b/src/opt/bcd2.h @@ -0,0 +1,29 @@ +/*++ +Copyright (c) 2014 Microsoft Corporation + +Module Name: + + bcd2.h + +Abstract: + + Bcd2 based MaxSAT. + +Author: + + Nikolaj Bjorner (nbjorner) 2014-4-17 + +Notes: + +--*/ + +#ifndef _BCD2_H_ +#define _BCD2_H_ + +#include "maxsmt.h" + +namespace opt { + maxsmt_solver_base* mk_bcd2(ast_manager& m, opt_solver* s, params_ref& p, + vector const& ws, expr_ref_vector const& soft); +} +#endif diff --git a/src/opt/dual_maxres.cpp b/src/opt/dual_maxres.cpp new file mode 100644 index 000000000..55d347e9e --- /dev/null +++ b/src/opt/dual_maxres.cpp @@ -0,0 +1,429 @@ +/*++ +Copyright (c) 2014 Microsoft Corporation + +Module Name: + + dual_maxsres.cpp + +Abstract: + + MaxRes (weighted) max-sat algorithm + based on dual refinement of bounds. + + MaxRes is a core-guided approach to maxsat. + DualMaxRes extends the core-guided approach by + leveraging both cores and satisfying assignments + to make progress towards a maximal satisfying assignment. + + Given a (minimal) unsatisfiable core for the soft + constraints the approach works like max-res. + Given a (maximal) satisfying subset of the soft constraints + the approach updates the upper bound if the current assignment + improves the current best assignmet. + Furthermore, take the soft constraints that are complements + to the current satisfying subset. + E.g, if F are the hard constraints and + s1,...,sn, t1,..., tm are the soft clauses and + F & s1 & ... & sn is satisfiable, then the complement + of of the current satisfying subset is t1, .., tm. + Update the hard constraint: + F := F & (t1 or ... or tm) + Replace t1, .., tm by m-1 new soft clauses: + t1 & t2, t3 & (t1 or t2), t4 & (t1 or t2 or t3), ..., tn & (t1 or ... t_{n-1}) + Claim: + If k of these soft clauses are satisfied, then k+1 of + the previous soft clauses are satisfied. + If k of these soft clauses are false in the satisfying assignment + for the updated F, then k of the original soft clauses are also false + under the assignment. + In summary: any assignment to the new clauses that satsfies F has the + same cost. + Claim: + If there are no satisfying assignments to F, then the current best assignment + is the optimum. + + +Author: + + Nikolaj Bjorner (nbjorner) 2014-27-7 + +Notes: + +--*/ + +#include "solver.h" +#include "maxsmt.h" +#include "dual_maxres.h" +#include "ast_pp.h" +#include "mus.h" + +using namespace opt; + + +class dual_maxres : public maxsmt_solver_base { + expr_ref_vector m_B; + expr_ref_vector m_asms; + obj_map m_asm2weight; + ptr_vector m_new_core; + mus m_mus; + expr_ref_vector m_trail; + +public: + dual_maxres(ast_manager& m, opt_solver* s, params_ref& p, + vector const& ws, expr_ref_vector const& soft): + maxsmt_solver_base(s, m, p, ws, soft), + m_B(m), m_asms(m), + m_mus(m_s, m), + m_trail(m) + { + } + + virtual ~dual_maxres() {} + + bool is_literal(expr* l) { + return + is_uninterp_const(l) || + (m.is_not(l, l) && is_uninterp_const(l)); + } + + void add_soft(expr* e, rational const& w) { + TRACE("opt", tout << mk_pp(e, m) << "\n";); + expr_ref asum(m), fml(m); + if (is_literal(e)) { + asum = e; + } + else { + asum = mk_fresh_bool("soft"); + fml = m.mk_iff(asum, e); + m_s->assert_expr(fml); + } + new_assumption(asum, w); + m_upper += w; + } + + void new_assumption(expr* e, rational const& w) { + m_asm2weight.insert(e, w); + m_asms.push_back(e); + m_trail.push_back(e); + } + + lbool operator()() { + solver::scoped_push _sc(*m_s.get()); + init(); + init_local(); + lbool was_sat = l_false; + ptr_vector soft_compl; + while (m_lower < m_upper) { + TRACE("opt", + display_vec(tout, m_asms.size(), m_asms.c_ptr()); + m_s->display(tout); + tout << "\n"; + display(tout); + ); + lbool is_sat = m_s->check_sat(0, 0); + 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(soft_compl); + break; + case l_true: + is_sat = process_sat(soft_compl); + break; + } + } + switch (is_sat) { + case l_undef: + return l_undef; + case l_false: + m_lower = m_upper; + return was_sat; + case l_true: + break; + } + } + return was_sat; + } + + lbool process_sat(ptr_vector& softc) { + expr_ref fml(m), tmp(m); + TRACE("opt", display_vec(tout << "softc: ", softc.size(), softc.c_ptr());); + SASSERT(!softc.empty()); // we should somehow stop if all soft are satisfied. + if (softc.empty()) { + return l_false; + } + + remove_soft(softc); + rational w = split_soft(softc); + TRACE("opt", display_vec(tout << " softc: ", softc.size(), softc.c_ptr());); + dual_max_resolve(softc, w); + return l_true; + } + + lbool process_unsat(ptr_vector& core) { + expr_ref fml(m); + TRACE("opt", display_vec(tout << "core: ", core.size(), core.c_ptr());); + SASSERT(!core.empty()); + lbool is_sat = minimize_core(core); + SASSERT(!core.empty()); + if (core.empty()) { + return l_false; + } + if (is_sat != l_true) { + return is_sat; + } + remove_soft(core); + rational w = split_soft(core); + TRACE("opt", display_vec(tout << "minimized core: ", core.size(), core.c_ptr());); + max_resolve(core, w); + m_lower += w; + IF_VERBOSE(1, verbose_stream() << + "(opt.dual_max_res [" << m_lower << ":" << m_upper << "])\n";); + + return is_sat; + } + + // + // 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()) { + soft_compl.reset(); + m_s->get_unsat_core(soft_compl); + 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; + } + } + } + return l_true; + } + + 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); + } + } + 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.dual_max_res [" << m_lower << ":" << m_upper << "])\n";); + } + return num_true; + } + + lbool minimize_core(ptr_vector& core) { + m_mus.reset(); + for (unsigned i = 0; i < core.size(); ++i) { + m_mus.add_soft(core[i], 1, core.c_ptr() + i); + } + unsigned_vector mus_idx; + lbool is_sat = m_mus.get_mus(mus_idx); + if (is_sat != l_true) { + return is_sat; + } + m_new_core.reset(); + for (unsigned i = 0; i < mus_idx.size(); ++i) { + m_new_core.push_back(core[mus_idx[i]]); + } + core.reset(); + core.append(m_new_core); + return l_true; + } + + rational get_weight(expr* e) { + return m_asm2weight.find(e); + } + + + // + // find the minimal weight. + // soft clauses with weight larger than the minimal weight + // are (re)added as soft clauses where the weight is updated + // to subtract the minimal weight. + // + rational split_soft(ptr_vector const& soft) { + + SASSERT(!soft.empty()); + rational w = get_weight(soft[0]); + for (unsigned i = 1; i < soft.size(); ++i) { + rational w2 = get_weight(soft[i]); + if (w2 < w) { + w = w2; + } + } + // add fresh soft clauses for weights that are above w. + for (unsigned i = 0; i < soft.size(); ++i) { + rational w2 = get_weight(soft[i]); + if (w2 > w) { + new_assumption(soft[i], w2 - w); + } + } + return w; + } + + void display_vec(std::ostream& out, unsigned sz, expr* const* args) { + for (unsigned i = 0; i < sz; ++i) { + out << mk_pp(args[i], m) << " "; + } + out << "\n"; + } + + void display(std::ostream& out) { + for (unsigned i = 0; i < m_asms.size(); ++i) { + expr* a = m_asms[i].get(); + out << mk_pp(a, m) << " : " << get_weight(a) << "\n"; + } + } + + void max_resolve(ptr_vector& core, rational const& w) { + SASSERT(!core.empty()); + expr_ref fml(m), asum(m); + app_ref cls(m), d(m); + m_B.reset(); + m_B.append(core.size(), core.c_ptr()); + d = m.mk_true(); + // + // d_0 := true + // d_i := b_{i-1} and d_{i-1} for i = 1...sz-1 + // soft (b_i or !d_i) + // == (b_i or !(!b_{i-1} or d_{i-1})) + // == (b_i or b_0 & b_1 & ... & b_{i-1}) + // + // Soft constraint is satisfied if previous soft constraint + // holds or if it is the first soft constraint to fail. + // + // Soundness of this rule can be established using MaxRes + // + for (unsigned i = 1; i < core.size(); ++i) { + expr* b_i = m_B[i-1].get(); + expr* b_i1 = m_B[i].get(); + d = m.mk_and(b_i, d); + asum = mk_fresh_bool("a"); + cls = m.mk_or(b_i1, d); + fml = m.mk_iff(asum, cls); + new_assumption(asum, w); + m_s->assert_expr(fml); + } + fml = m.mk_not(m.mk_and(m_B.size(), m_B.c_ptr())); + m_s->assert_expr(fml); + } + + // satc are the complements of a (maximal) satisfying assignment. + void dual_max_resolve(ptr_vector& satc, rational const& w) { + SASSERT(!satc.empty()); + expr_ref fml(m), asum(m); + app_ref cls(m), d(m); + m_B.reset(); + m_B.append(satc.size(), satc.c_ptr()); + d = m.mk_false(); + // + // d_0 := false + // d_i := b_{i-1} or d_{i-1} for i = 1...sz-1 + // soft (b_i and d_i) + // == (b_i and (b_0 or b_1 or ... or b_{i-1})) + // + for (unsigned i = 1; i < satc.size(); ++i) { + expr* b_i = m_B[i-1].get(); + expr* b_i1 = m_B[i].get(); + d = m.mk_or(b_i, d); + asum = mk_fresh_bool("a"); + cls = m.mk_and(b_i1, d); + fml = m.mk_iff(asum, cls); + new_assumption(asum, w); + m_s->assert_expr(fml); + } + fml = m.mk_or(m_B.size(), m_B.c_ptr()); + m_s->assert_expr(fml); + } + + void remove_soft(ptr_vector const& soft) { + for (unsigned i = 0; i < m_asms.size(); ++i) { + if (soft.contains(m_asms[i].get())) { + m_asms[i] = m_asms.back(); + m_asms.pop_back(); + --i; + } + } + } + + virtual void set_cancel(bool f) { + maxsmt_solver_base::set_cancel(f); + m_mus.set_cancel(f); + } + + void init_local() { + m_upper.reset(); + m_lower.reset(); + m_asm2weight.reset(); + m_trail.reset(); + for (unsigned i = 0; i < m_soft.size(); ++i) { + add_soft(m_soft[i].get(), m_weights[i]); + } + } + +}; + +opt::maxsmt_solver_base* opt::mk_dual_maxres( + ast_manager& m, opt_solver* s, params_ref& p, + vector const& ws, expr_ref_vector const& soft) { + return alloc(dual_maxres, m, s, p, ws, soft); +} + diff --git a/src/opt/dual_maxres.h b/src/opt/dual_maxres.h new file mode 100644 index 000000000..2bf1c7b18 --- /dev/null +++ b/src/opt/dual_maxres.h @@ -0,0 +1,32 @@ +/*++ +Copyright (c) 2014 Microsoft Corporation + +Module Name: + + dual_maxsres.h + +Abstract: + + MaxRes (weighted) max-sat algorithm + based on dual refinement of bounds. + +Author: + + Nikolaj Bjorner (nbjorner) 2014-27-7 + +Notes: + +--*/ + +#ifndef _DUAL_MAXRES_H_ +#define _DUAL_MAXRES_H_ + +namespace opt { + maxsmt_solver_base* mk_dual_maxres( + ast_manager& m, opt_solver* s, params_ref& p, + vector const& ws, expr_ref_vector const& soft); + + +}; + +#endif diff --git a/src/opt/maxhs.cpp b/src/opt/maxhs.cpp new file mode 100644 index 000000000..35ca630d9 --- /dev/null +++ b/src/opt/maxhs.cpp @@ -0,0 +1,561 @@ +/*++ +Copyright (c) 2014 Microsoft Corporation + +Module Name: + + maxhs.cpp + +Abstract: + + maxhs based MaxSAT. + +Author: + + Nikolaj Bjorner (nbjorner) 2014-4-17 + +Notes: + +--*/ +#include "optsmt.h" +#include "hitting_sets.h" +#include "stopwatch.h" +#include "ast_pp.h" +#include "model_smt2_pp.h" +#include "uint_set.h" +#include "maxhs.h" + +namespace opt { + + class scoped_stopwatch { + double& m_time; + stopwatch m_watch; + public: + scoped_stopwatch(double& time): m_time(time) { + m_watch.start(); + } + ~scoped_stopwatch() { + m_watch.stop(); + m_time += m_watch.get_seconds(); + } + }; + + + // ---------------------------------- + // MaxSatHS+MSS + // variant of MaxSAT-HS (Algorithm 9) + // that also refines upper bound during progressive calls + // to the underlying optimization solver for the soft constraints. + // + + class maxhs : public maxsmt_solver_base { + struct stats { + stats() { reset(); } + void reset() { memset(this, 0, sizeof(*this)); } + unsigned m_num_iterations; + unsigned m_num_core_reductions_success; + unsigned m_num_core_reductions_failure; + unsigned m_num_model_expansions_success; + unsigned m_num_model_expansions_failure; + double m_core_reduction_time; + double m_model_expansion_time; + double m_aux_sat_time; + double m_disjoint_cores_time; + }; + + hitting_sets m_hs; + expr_ref_vector m_aux; // auxiliary (indicator) variables. + obj_map m_aux2index; // expr |-> index + unsigned_vector m_core_activity; // number of times soft constraint is used in a core. + svector m_seed; // clause selected in current model. + svector m_aux_active; // active soft clauses. + ptr_vector m_asms; // assumptions (over aux) + stats m_stats; + bool m_at_lower_bound; + + + public: + maxhs(opt_solver* s, ast_manager& m, params_ref& p, vector const& ws, expr_ref_vector const& soft): + maxsmt_solver_base(s, m, p, ws, soft), + m_aux(m), + m_at_lower_bound(false) { + } + virtual ~maxhs() {} + + virtual void set_cancel(bool f) { + maxsmt_solver_base::set_cancel(f); + m_hs.set_cancel(f); + } + + virtual void collect_statistics(statistics& st) const { + maxsmt_solver_base::collect_statistics(st); + m_hs.collect_statistics(st); + st.update("maxhs-num-iterations", m_stats.m_num_iterations); + st.update("maxhs-num-core-reductions-n", m_stats.m_num_core_reductions_failure); + st.update("maxhs-num-core-reductions-y", m_stats.m_num_core_reductions_success); + st.update("maxhs-num-model-expansions-n", m_stats.m_num_model_expansions_failure); + st.update("maxhs-num-model-expansions-y", m_stats.m_num_model_expansions_success); + st.update("maxhs-core-reduction-time", m_stats.m_core_reduction_time); + st.update("maxhs-model-expansion-time", m_stats.m_model_expansion_time); + st.update("maxhs-aux-sat-time", m_stats.m_aux_sat_time); + st.update("maxhs-disj-core-time", m_stats.m_disjoint_cores_time); + } + + lbool operator()() { + ptr_vector hs; + init(); + init_local(); + if (!disjoint_cores(hs)) { + return l_undef; + } + seed2assumptions(); + while (m_lower < m_upper) { + ++m_stats.m_num_iterations; + IF_VERBOSE(1, verbose_stream() << + "(opt.maxhs [" << m_lower << ":" << m_upper << "])\n";); + TRACE("opt", tout << "(maxhs [" << m_lower << ":" << m_upper << "])\n";); + if (m_cancel) { + return l_undef; + } + + lbool core_found = generate_cores(hs); + switch(core_found) { + case l_undef: + return l_undef; + case l_true: { + lbool is_sat = next_seed(); + switch(is_sat) { + case l_true: + seed2hs(false, hs); + break; + case l_false: + TRACE("opt", tout << "no more seeds\n";); + IF_VERBOSE(1, verbose_stream() << "(opt.maxhs.no-more-seeds)\n";); + m_lower = m_upper; + return l_true; + case l_undef: + return l_undef; + } + break; + } + case l_false: + IF_VERBOSE(1, verbose_stream() << "(opt.maxhs.no-more-cores)\n";); + TRACE("opt", tout << "no more cores\n";); + m_lower = m_upper; + return l_true; + } + } + return l_true; + } + + private: + + unsigned num_soft() const { return m_soft.size(); } + + void init_local() { + unsigned sz = num_soft(); + app_ref fml(m), obj(m); + expr_ref_vector sum(m); + m_asms.reset(); + m_seed.reset(); + m_aux.reset(); + m_aux_active.reset(); + m_aux2index.reset(); + m_core_activity.reset(); + for (unsigned i = 0; i < sz; ++i) { + bool tt = is_true(m_model, m_soft[i].get()); + m_seed.push_back(tt); + m_aux. push_back(mk_fresh(m.mk_bool_sort())); + m_aux_active.push_back(false); + m_core_activity.push_back(0); + m_aux2index.insert(m_aux.back(), i); + if (tt) { + m_asms.push_back(m_aux.back()); + ensure_active(i); + } + } + + for (unsigned i = 0; i < m_weights.size(); ++i) { + m_hs.add_weight(m_weights[i]); + } + TRACE("opt", print_seed(tout);); + } + + + void hs2seed(ptr_vector const& hs) { + for (unsigned i = 0; i < num_soft(); ++i) { + m_seed[i] = true; + } + for (unsigned i = 0; i < hs.size(); ++i) { + m_seed[m_aux2index.find(hs[i])] = false; + } + TRACE("opt", + print_asms(tout << "hitting set: ", hs); + print_seed(tout);); + } + + void seed2hs(bool pos, ptr_vector& hs) { + hs.reset(); + for (unsigned i = 0; i < num_soft(); ++i) { + if (pos == m_seed[i]) { + hs.push_back(m_aux[i].get()); + } + } + TRACE("opt", + print_asms(tout << "hitting set: ", hs); + print_seed(tout);); + + } + + void seed2assumptions() { + seed2hs(true, m_asms); + } + + + // + // Find disjoint cores for soft constraints. + // + bool disjoint_cores(ptr_vector& hs) { + scoped_stopwatch _sw(m_stats.m_disjoint_cores_time); + m_asms.reset(); + svector active(num_soft(), true); + rational lower(0); + update_assumptions(active, lower, hs); + SASSERT(lower.is_zero()); + while (true) { + lbool is_sat = s().check_sat(m_asms.size(), m_asms.c_ptr()); + switch (is_sat) { + case l_true: + if (lower > m_lower) { + m_lower = lower; + } + return true; + case l_false: + if (!shrink()) return false; + block_up(); + update_assumptions(active, lower, hs); + break; + case l_undef: + return false; + } + } + } + + void update_assumptions(svector& active, rational& lower, ptr_vector& hs) { + rational arg_min(0); + expr* e = 0; + for (unsigned i = 0; i < m_asms.size(); ++i) { + unsigned index = m_aux2index.find(m_asms[i]); + active[index] = false; + if (arg_min.is_zero() || arg_min > m_weights[index]) { + arg_min = m_weights[index]; + e = m_asms[i]; + } + } + if (e) { + hs.push_back(e); + lower += arg_min; + } + m_asms.reset(); + for (unsigned i = 0; i < num_soft(); ++i) { + if (active[i]) { + m_asms.push_back(m_aux[i].get()); + ensure_active(i); + } + } + } + + // + // Auxiliary Algorithm 10 for producing cores. + // + lbool generate_cores(ptr_vector& hs) { + bool core = !m_at_lower_bound; + while (true) { + hs2seed(hs); + lbool is_sat = check_subset(); + switch(is_sat) { + case l_undef: + return l_undef; + case l_true: + if (!grow()) return l_undef; + block_down(); + return core?l_true:l_false; + case l_false: + core = true; + if (!shrink()) return l_undef; + block_up(); + find_non_optimal_hitting_set(hs); + break; + } + } + } + + struct lt_activity { + maxhs& hs; + lt_activity(maxhs& hs):hs(hs) {} + bool operator()(expr* a, expr* b) const { + unsigned w1 = hs.m_core_activity[hs.m_aux2index.find(a)]; + unsigned w2 = hs.m_core_activity[hs.m_aux2index.find(b)]; + return w1 < w2; + } + }; + + // + // produce the non-optimal hitting set by using the 10% heuristic. + // of most active cores constraints. + // m_asms contains the current core. + // + void find_non_optimal_hitting_set(ptr_vector& hs) { + std::sort(m_asms.begin(), m_asms.end(), lt_activity(*this)); + for (unsigned i = m_asms.size(); i > 9*m_asms.size()/10;) { + --i; + hs.push_back(m_asms[i]); + } + } + + // + // retrieve the next seed that satisfies state of hs. + // state of hs must be satisfiable before optimization is called. + // + lbool next_seed() { + scoped_stopwatch _sw(m_stats.m_aux_sat_time); + TRACE("opt", tout << "\n";); + + // min c_i*(not x_i) for x_i are soft clauses. + // max c_i*x_i for x_i are soft clauses + + m_at_lower_bound = false; + + lbool is_sat = m_hs.compute_upper(); + + if (is_sat == l_true) { + is_sat = m_hs.compute_lower(); + } + if (is_sat == l_true) { + m_at_lower_bound = m_hs.get_upper() == m_hs.get_lower(); + if (m_hs.get_lower() > m_lower) { + m_lower = m_hs.get_lower(); + } + for (unsigned i = 0; i < num_soft(); ++i) { + m_seed[i] = is_active(i) && !m_hs.get_value(i); + } + TRACE("opt", print_seed(tout);); + } + return is_sat; + } + + // + // check assignment returned by HS with the original + // hard constraints. + // + lbool check_subset() { + TRACE("opt", tout << "\n";); + m_asms.reset(); + for (unsigned i = 0; i < num_soft(); ++i) { + if (m_seed[i]) { + m_asms.push_back(m_aux[i].get()); + ensure_active(i); + } + } + return s().check_sat(m_asms.size(), m_asms.c_ptr()); + } + + // + // extend the current assignment to one that + // satisfies as many soft constraints as possible. + // update the upper bound based on this assignment + // + bool grow() { + scoped_stopwatch _sw(m_stats.m_model_expansion_time); + model_ref mdl; + s().get_model(mdl); + for (unsigned i = 0; i < num_soft(); ++i) { + ensure_active(i); + m_seed[i] = false; + } + for (unsigned i = 0; i < m_asms.size(); ++i) { + m_seed[m_aux2index.find(m_asms[i])] = true; + } + + for (unsigned i = 0; i < num_soft(); ++i) { + if (m_seed[i]) { + // already an assumption + } + else if (is_true(mdl, m_soft[i].get())) { + m_seed[i] = true; + m_asms.push_back(m_aux[i].get()); + } + else { + m_asms.push_back(m_aux[i].get()); + lbool is_sat = s().check_sat(m_asms.size(), m_asms.c_ptr()); + switch(is_sat) { + case l_undef: + return false; + case l_false: + ++m_stats.m_num_model_expansions_failure; + m_asms.pop_back(); + break; + case l_true: + ++m_stats.m_num_model_expansions_success; + s().get_model(mdl); + m_seed[i] = true; + break; + } + } + } + rational upper(0); + for (unsigned i = 0; i < num_soft(); ++i) { + if (!m_seed[i]) { + upper += m_weights[i]; + } + } + if (upper < m_upper) { + m_upper = upper; + m_hs.set_upper(upper); + m_model = mdl; + m_assignment.reset(); + m_assignment.append(m_seed); + TRACE("opt", + tout << "new upper: " << m_upper << "\n"; + model_smt2_pp(tout, m, *(mdl.get()), 0);); + } + DEBUG_CODE( + for (unsigned i = 0; i < num_soft(); ++i) { + SASSERT(is_true(mdl, m_soft[i].get()) == m_seed[i]); + }); + + return true; + } + + // + // remove soft constraints from the current core. + // + bool shrink() { + scoped_stopwatch _sw(m_stats.m_core_reduction_time); + m_asms.reset(); + s().get_unsat_core(m_asms); + TRACE("opt", print_asms(tout, m_asms);); + obj_map asm2index; + for (unsigned i = 0; i < m_asms.size(); ++i) { + asm2index.insert(m_asms[i], i); + } + obj_map::iterator it = asm2index.begin(), end = asm2index.end(); + for (; it != end; ++it) { + unsigned i = it->m_value; + if (i < m_asms.size()) { + expr* tmp = m_asms[i]; + expr* back = m_asms.back(); + m_asms[i] = back; + m_asms.pop_back(); + lbool is_sat = s().check_sat(m_asms.size(), m_asms.c_ptr()); + TRACE("opt", tout << "checking: " << mk_pp(tmp, m) << ": " << is_sat << "\n";); + switch(is_sat) { + case l_true: + ++m_stats.m_num_core_reductions_failure; + // put back literal into core + m_asms.push_back(back); + m_asms[i] = tmp; + break; + case l_false: + // update the core + m_asms.reset(); + ++m_stats.m_num_core_reductions_success; + s().get_unsat_core(m_asms); + TRACE("opt", print_asms(tout, m_asms);); + update_index(asm2index); + break; + case l_undef: + return false; + } + } + } + return true; + } + + void print_asms(std::ostream& out, ptr_vector const& asms) { + for (unsigned j = 0; j < asms.size(); ++j) { + out << mk_pp(asms[j], m) << " "; + } + out << "\n"; + } + + void print_seed(std::ostream& out) { + out << "seed: "; + for (unsigned i = 0; i < num_soft(); ++i) { + out << (m_seed[i]?"1":"0"); + } + out << "\n"; + } + + // + // must include some literal not from asms. + // (furthermore, update upper bound constraint in HS) + // + void block_down() { + uint_set indices; + unsigned_vector c_indices; + for (unsigned i = 0; i < m_asms.size(); ++i) { + indices.insert(m_aux2index.find(m_asms[i])); + } + for (unsigned i = 0; i < num_soft(); ++i) { + if (!indices.contains(i)) { + c_indices.push_back(i); + } + } + m_hs.add_exists_false(c_indices.size(), c_indices.c_ptr()); + } + + // should exclude some literal from core. + void block_up() { + unsigned_vector indices; + for (unsigned i = 0; i < m_asms.size(); ++i) { + unsigned index = m_aux2index.find(m_asms[i]); + m_core_activity[index]++; + indices.push_back(index); + } + m_hs.add_exists_true(indices.size(), indices.c_ptr()); + } + + void update_index(obj_map& asm2index) { + obj_map::iterator it = asm2index.begin(), end = asm2index.end(); + for (; it != end; ++it) { + it->m_value = UINT_MAX; + } + for (unsigned i = 0; i < m_asms.size(); ++i) { + asm2index.find(m_asms[i]) = i; + } + } + + app_ref mk_fresh(sort* s) { + app_ref r(m); + r = m.mk_fresh_const("r", s); + m_mc->insert(r->get_decl()); + return r; + } + + bool is_true(model_ref& mdl, expr* e) { + expr_ref val(m); + VERIFY(mdl->eval(e, val)); + return m.is_true(val); + } + + bool is_active(unsigned i) const { + return m_aux_active[i]; + } + + void ensure_active(unsigned i) { + if (!is_active(i)) { + expr_ref fml(m); + fml = m.mk_implies(m_aux[i].get(), m_soft[i].get()); + s().assert_expr(fml); + m_aux_active[i] = true; + } + } + + }; + + maxsmt_solver_base* opt::mk_maxhs(ast_manager& m, opt_solver* s, params_ref& p, + vector const& ws, expr_ref_vector const& soft) { + return alloc(maxhs, s, m, p, ws, soft); + } + +} diff --git a/src/opt/maxhs.h b/src/opt/maxhs.h new file mode 100644 index 000000000..e08a550bd --- /dev/null +++ b/src/opt/maxhs.h @@ -0,0 +1,29 @@ +/*++ +Copyright (c) 2014 Microsoft Corporation + +Module Name: + + maxhs.h + +Abstract: + + HS-max based MaxSAT. + +Author: + + Nikolaj Bjorner (nbjorner) 2014-4-17 + +Notes: + +--*/ + +#ifndef _HS_MAX_H_ +#define _HS_MAX_H_ + +#include "maxsmt.h" + +namespace opt { + maxsmt_solver_base* mk_maxhs(ast_manager& m, opt_solver* s, params_ref& p, + vector const& ws, expr_ref_vector const& soft); +} +#endif diff --git a/src/opt/maxres.cpp b/src/opt/maxres.cpp index 2ec73bab4..fa0210ee2 100644 --- a/src/opt/maxres.cpp +++ b/src/opt/maxres.cpp @@ -135,7 +135,7 @@ public: m_lower += w; break; } - IF_VERBOSE(1, verbose_stream() << "(opt.max_res lower: " << m_lower << ")\n";); + IF_VERBOSE(1, verbose_stream() << "(opt.max_res [" << m_lower << ":" << m_upper << "])\n";); } return l_true; } diff --git a/src/opt/maxsls.cpp b/src/opt/maxsls.cpp new file mode 100644 index 000000000..c64e0f3fc --- /dev/null +++ b/src/opt/maxsls.cpp @@ -0,0 +1,63 @@ +/*++ +Copyright (c) 2013 Microsoft Corporation + +Module Name: + + maxsls.cpp + +Abstract: + + Weighted SLS MAXSAT module + +Author: + + Nikolaj Bjorner (nbjorner) 2014-4-17 + +Notes: + +--*/ + +#include "maxsls.h" +#include "ast_pp.h" +#include "model_smt2_pp.h" + + +namespace opt { + + class sls : public maxsmt_solver_base { + public: + sls(opt_solver* s, ast_manager& m, params_ref& p, + vector const& ws, expr_ref_vector const& soft): + maxsmt_solver_base(s, m, p, ws, soft) { + } + virtual ~sls() {} + lbool operator()() { + IF_VERBOSE(1, verbose_stream() << "(opt.sls)\n";); + enable_bvsat(); + enable_sls(); + init(); + lbool is_sat = s().check_sat(0, 0); + if (is_sat == l_true) { + s().get_model(m_model); + m_upper.reset(); + for (unsigned i = 0; i < m_soft.size(); ++i) { + expr_ref tmp(m); + m_model->eval(m_soft[i].get(), tmp, true); + m_assignment[i] = m.is_true(tmp); + if (!m_assignment[i]) { + m_upper += m_weights[i]; + } + } + } + return is_sat; + } + + }; + + maxsmt_solver_base* opt::mk_sls(ast_manager& m, opt_solver* s, params_ref& p, + vector const& ws, expr_ref_vector const& soft) { + return alloc(sls, s, m, p, ws, soft); + } + + +}; diff --git a/src/opt/maxsls.h b/src/opt/maxsls.h new file mode 100644 index 000000000..111d6a3b2 --- /dev/null +++ b/src/opt/maxsls.h @@ -0,0 +1,36 @@ +/*++ +Copyright (c) 2013 Microsoft Corporation + +Module Name: + + maxsls.h + +Abstract: + + Weighted SLS MAXSAT module + +Author: + + Nikolaj Bjorner (nbjorner) 2014-4-17 + +Notes: + + Partial, one-round SLS optimizer. Finds the first + local maximum given a resource bound and returns. + +--*/ +#ifndef _OPT_SLS_MAX_SAT_H_ +#define _OPT_SLS_MAX_SAT_H_ + +#include "maxsmt.h" + +namespace opt { + + + maxsmt_solver_base* mk_sls(ast_manager& m, opt_solver* s, params_ref& p, + vector const& ws, expr_ref_vector const& soft); + + +}; + +#endif diff --git a/src/opt/maxsmt.cpp b/src/opt/maxsmt.cpp index 2b20ccbd0..7ae1348ab 100644 --- a/src/opt/maxsmt.cpp +++ b/src/opt/maxsmt.cpp @@ -22,7 +22,13 @@ Notes: #include "fu_malik.h" #include "core_maxsat.h" #include "maxres.h" -#include "weighted_maxsat.h" +#include "dual_maxres.h" +#include "maxhs.h" +#include "bcd2.h" +#include "wpm2.h" +#include "pbmax.h" +#include "wmax.h" +#include "maxsls.h" #include "ast_pp.h" #include "opt_params.hpp" #include "pb_decl_plugin.h" @@ -173,6 +179,9 @@ namespace opt { else if (m_maxsat_engine == symbol("maxres")) { m_msolver = mk_maxres(m, s, m_params, m_weights, m_soft_constraints); } + else if (m_maxsat_engine == symbol("dual-maxres")) { + m_msolver = mk_dual_maxres(m, s, m_params, m_weights, m_soft_constraints); + } else if (m_maxsat_engine == symbol("pbmax")) { m_msolver = mk_pbmax(m, s, m_params, m_weights, m_soft_constraints); } @@ -182,8 +191,8 @@ namespace opt { else if (m_maxsat_engine == symbol("bcd2")) { m_msolver = mk_bcd2(m, s, m_params, m_weights, m_soft_constraints); } - else if (m_maxsat_engine == symbol("hsmax")) { - m_msolver = mk_hsmax(m, s, m_params, m_weights, m_soft_constraints); + else if (m_maxsat_engine == symbol("maxhs")) { + m_msolver = mk_maxhs(m, s, m_params, m_weights, m_soft_constraints); } else if (m_maxsat_engine == symbol("sls")) { // NB: this is experimental one-round version of SLS @@ -196,7 +205,7 @@ namespace opt { m_msolver = alloc(fu_malik, m, *m_s, m_soft_constraints); } else { - if (m_maxsat_engine != symbol::null) { + if (m_maxsat_engine != symbol::null && m_maxsat_engine != symbol("wmax")) { warning_msg("solver %s is not recognized, using default 'wmax'", m_maxsat_engine.str().c_str()); } diff --git a/src/opt/mus.cpp b/src/opt/mus.cpp index 2e71f1bb8..4cfab6376 100644 --- a/src/opt/mus.cpp +++ b/src/opt/mus.cpp @@ -39,8 +39,11 @@ struct mus::imp { expr_ref_vector m_vars; obj_map m_var2idx; volatile bool m_cancel; + bool m_rmr_enabled; - imp(ref& s, ast_manager& m): m_s(s), m(m), m_cls2expr(m), m_vars(m), m_cancel(false) {} + imp(ref& s, ast_manager& m): + m_s(s), m(m), m_cls2expr(m), m_vars(m), m_cancel(false), + m_rmr_enabled(false) {} void reset() { m_cls2expr.reset(); @@ -133,10 +136,12 @@ struct mus::imp { assumptions.push_back(cls); mus.push_back(cls_id); extract_model(model); - sz = core.size(); - core.append(mus); - rmr(core, mus, model); - core.resize(sz); + if (m_rmr_enabled) { + sz = core.size(); + core.append(mus); + rmr(core, mus, model); + core.resize(sz); + } break; default: core_exprs.reset(); diff --git a/src/opt/pbmax.cpp b/src/opt/pbmax.cpp new file mode 100644 index 000000000..fe1d7b70d --- /dev/null +++ b/src/opt/pbmax.cpp @@ -0,0 +1,98 @@ +/*++ +Copyright (c) 2014 Microsoft Corporation + +Module Name: + + pbmax.cpp + +Abstract: + + pb based MaxSAT. + +Author: + + Nikolaj Bjorner (nbjorner) 2014-4-17 + +Notes: + +--*/ +#include "pbmax.h" +#include "pb_decl_plugin.h" +#include "uint_set.h" +#include "ast_pp.h" +#include "model_smt2_pp.h" + + +namespace opt { + + // ---------------------------------- + // incrementally add pseudo-boolean + // lower bounds. + + class pbmax : public maxsmt_solver_base { + public: + pbmax(opt_solver* s, ast_manager& m, params_ref& p, + vector const& ws, expr_ref_vector const& soft): + maxsmt_solver_base(s, m, p, ws, soft) { + } + + virtual ~pbmax() {} + + lbool operator()() { + enable_bvsat(); + enable_sls(); + + TRACE("opt", s().display(tout); tout << "\n"; + for (unsigned i = 0; i < m_soft.size(); ++i) { + tout << mk_pp(m_soft[i].get(), m) << " " << m_weights[i] << "\n"; + } + ); + pb_util u(m); + expr_ref fml(m), val(m); + app_ref b(m); + expr_ref_vector nsoft(m); + init(); + for (unsigned i = 0; i < m_soft.size(); ++i) { + nsoft.push_back(mk_not(m_soft[i].get())); + } + lbool is_sat = l_true; + while (l_true == is_sat) { + TRACE("opt", s().display(tout<<"looping\n"); + model_smt2_pp(tout << "\n", m, *(m_model.get()), 0);); + m_upper.reset(); + for (unsigned i = 0; i < m_soft.size(); ++i) { + VERIFY(m_model->eval(nsoft[i].get(), val)); + m_assignment[i] = !m.is_true(val); + if (!m_assignment[i]) { + m_upper += m_weights[i]; + } + } + IF_VERBOSE(1, verbose_stream() << "(opt.pb [" << m_lower << ":" << m_upper << "])\n";); + TRACE("opt", tout << "new upper: " << m_upper << "\n";); + + fml = u.mk_lt(nsoft.size(), m_weights.c_ptr(), nsoft.c_ptr(), m_upper); + solver::scoped_push _scope2(s()); + s().assert_expr(fml); + is_sat = s().check_sat(0,0); + if (m_cancel) { + is_sat = l_undef; + } + if (is_sat == l_true) { + s().get_model(m_model); + } + } + if (is_sat == l_false) { + is_sat = l_true; + m_lower = m_upper; + } + TRACE("opt", tout << "lower: " << m_lower << "\n";); + return is_sat; + } + }; + + maxsmt_solver_base* opt::mk_pbmax(ast_manager& m, opt_solver* s, params_ref& p, + vector const& ws, expr_ref_vector const& soft) { + return alloc(pbmax, s, m, p, ws, soft); + } + +} diff --git a/src/opt/pbmax.h b/src/opt/pbmax.h new file mode 100644 index 000000000..8dcb43715 --- /dev/null +++ b/src/opt/pbmax.h @@ -0,0 +1,30 @@ +/*++ +Copyright (c) 2014 Microsoft Corporation + +Module Name: + + pbmax.h + +Abstract: + + MaxSAT based on pb theory. + +Author: + + Nikolaj Bjorner (nbjorner) 2014-4-17 + +Notes: + +--*/ + +#ifndef _PBMAX_H_ +#define _PBMAX_H_ + +#include "maxsmt.h" + +namespace opt { + maxsmt_solver_base* mk_pbmax(ast_manager& m, opt_solver* s, params_ref& p, + vector const& ws, expr_ref_vector const& soft); + +} +#endif diff --git a/src/opt/weighted_maxsat.cpp b/src/opt/weighted_maxsat.cpp deleted file mode 100644 index dbd5a060f..000000000 --- a/src/opt/weighted_maxsat.cpp +++ /dev/null @@ -1,1384 +0,0 @@ -/*++ -Copyright (c) 2013 Microsoft Corporation - -Module Name: - - weighted_maxsat.cpp - -Abstract: - - Weighted MAXSAT module - -Author: - - Nikolaj Bjorner (nbjorner) 2014-4-17 - -Notes: - ---*/ - -#include -#include "weighted_maxsat.h" -#include "smt_theory.h" -#include "smt_context.h" -#include "ast_pp.h" -#include "theory_wmaxsat.h" -#include "opt_params.hpp" -#include "pb_decl_plugin.h" -#include "uint_set.h" -#include "model_smt2_pp.h" -#include "cancel_eh.h" -#include "scoped_timer.h" -#include "optsmt.h" -#include "hitting_sets.h" -#include "stopwatch.h" - - -namespace opt { - - class scoped_stopwatch { - double& m_time; - stopwatch m_watch; - public: - scoped_stopwatch(double& time): m_time(time) { - m_watch.start(); - } - ~scoped_stopwatch() { - m_watch.stop(); - m_time += m_watch.get_seconds(); - } - }; - - - // ------------------------------------------------------ - // Morgado, Heras, Marques-Silva 2013 - // (initial version without model-based optimizations) - // - class bcd2 : public maxsmt_solver_base { - struct wcore { - expr* m_r; - unsigned_vector m_R; - rational m_lower; - rational m_mid; - rational m_upper; - }; - typedef obj_hashtable expr_set; - - pb_util pb; - expr_ref_vector m_soft_aux; - obj_map m_relax2index; // expr |-> index - obj_map m_soft2index; // expr |-> index - expr_ref_vector m_trail; - expr_ref_vector m_soft_constraints; - expr_set m_asm_set; - vector m_cores; - vector m_sigmas; - rational m_den; // least common multiplier of original denominators - bool m_enable_lazy; // enable adding soft constraints lazily (called 'mgbcd2') - unsigned_vector m_lazy_soft; // soft constraints to add lazily. - - void set2asms(expr_set const& set, expr_ref_vector & es) const { - es.reset(); - expr_set::iterator it = set.begin(), end = set.end(); - for (; it != end; ++it) { - es.push_back(m.mk_not(*it)); - } - } - void bcd2_init_soft(vector const& weights, expr_ref_vector const& soft) { - - // normalize weights to be integral: - m_den = rational::one(); - for (unsigned i = 0; i < m_weights.size(); ++i) { - m_den = lcm(m_den, denominator(m_weights[i])); - } - if (!m_den.is_one()) { - for (unsigned i = 0; i < m_weights.size(); ++i) { - m_weights[i] = m_den*m_weights[i]; - SASSERT(m_weights[i].is_int()); - } - } - } - void init_bcd() { - m_trail.reset(); - m_asm_set.reset(); - m_cores.reset(); - m_sigmas.reset(); - m_lazy_soft.reset(); - for (unsigned i = 0; i < m_soft.size(); ++i) { - m_sigmas.push_back(m_weights[i]); - m_soft_aux.push_back(mk_fresh()); - if (m_enable_lazy) { - m_lazy_soft.push_back(i); - } - else { - enable_soft_constraint(i); - } - } - m_upper += rational(1); - } - - void process_sat() { - svector assignment; - update_assignment(assignment); - if (check_lazy_soft(assignment)) { - update_sigmas(); - } - } - - public: - bcd2(opt_solver* s, ast_manager& m, params_ref& p, - vector const& ws, expr_ref_vector const& soft): - maxsmt_solver_base(s, m, p, ws, soft), - pb(m), - m_soft_aux(m), - m_trail(m), - m_soft_constraints(m), - m_enable_lazy(true) { - bcd2_init_soft(ws, soft); - } - - virtual ~bcd2() {} - - virtual lbool operator()() { - expr_ref fml(m), r(m); - lbool is_sat = l_undef; - expr_ref_vector asms(m); - enable_sls(); - solver::scoped_push _scope1(s()); - init(); - init_bcd(); - if (m_cancel) { - normalize_bounds(); - return l_undef; - } - process_sat(); - while (m_lower < m_upper) { - IF_VERBOSE(1, verbose_stream() << "(bcd2 [" << m_lower << ":" << m_upper << "])\n";); - assert_soft(); - solver::scoped_push _scope2(s()); - TRACE("opt", display(tout);); - assert_cores(); - set2asms(m_asm_set, asms); - if (m_cancel) { - normalize_bounds(); - return l_undef; - } - is_sat = s().check_sat(asms.size(), asms.c_ptr()); - switch(is_sat) { - case l_undef: - normalize_bounds(); - return l_undef; - case l_true: - process_sat(); - break; - case l_false: { - ptr_vector unsat_core; - uint_set subC, soft; - s().get_unsat_core(unsat_core); - core2indices(unsat_core, subC, soft); - SASSERT(unsat_core.size() == subC.num_elems() + soft.num_elems()); - if (soft.num_elems() == 0 && subC.num_elems() == 1) { - unsigned s = *subC.begin(); - wcore& c_s = m_cores[s]; - c_s.m_lower = refine(c_s.m_R, c_s.m_mid); - c_s.m_mid = div(c_s.m_lower + c_s.m_upper, rational(2)); - } - else { - wcore c_s; - rational delta = min_of_delta(subC); - rational lower = sum_of_lower(subC); - union_Rs(subC, c_s.m_R); - r = mk_fresh(); - relax(subC, soft, c_s.m_R, delta); - c_s.m_lower = refine(c_s.m_R, lower + delta - rational(1)); - c_s.m_upper = rational::one(); - c_s.m_upper += sum_of_sigmas(c_s.m_R); - c_s.m_mid = div(c_s.m_lower + c_s.m_upper, rational(2)); - c_s.m_r = r; - m_asm_set.insert(r); - subtract(m_cores, subC); - m_relax2index.insert(r, m_cores.size()); - m_cores.push_back(c_s); - } - break; - } - } - m_lower = compute_lower(); - } - normalize_bounds(); - return l_true; - } - - - private: - - void enable_soft_constraint(unsigned i) { - expr_ref fml(m); - expr* r = m_soft_aux[i].get(); - m_soft2index.insert(r, i); - fml = m.mk_or(r, m_soft[i].get()); - m_soft_constraints.push_back(fml); - m_asm_set.insert(r); - SASSERT(m_weights[i].is_int()); - } - - void assert_soft() { - for (unsigned i = 0; i < m_soft_constraints.size(); ++i) { - s().assert_expr(m_soft_constraints[i].get()); - } - m_soft_constraints.reset(); - } - - bool check_lazy_soft(svector const& assignment) { - bool all_satisfied = true; - for (unsigned i = 0; i < m_lazy_soft.size(); ++i) { - unsigned j = m_lazy_soft[i]; - if (!assignment[j]) { - enable_soft_constraint(j); - m_lazy_soft[i] = m_lazy_soft.back(); - m_lazy_soft.pop_back(); - --i; - all_satisfied = false; - } - } - return all_satisfied; - } - - void normalize_bounds() { - m_lower /= m_den; - m_upper /= m_den; - } - - expr* mk_fresh() { - expr* r = mk_fresh_bool("r"); - m_trail.push_back(r); - return r; - } - - void update_assignment(svector& new_assignment) { - expr_ref val(m); - rational new_upper(0); - model_ref model; - new_assignment.reset(); - s().get_model(model); - for (unsigned i = 0; i < m_soft.size(); ++i) { - VERIFY(model->eval(m_soft[i].get(), val)); - new_assignment.push_back(m.is_true(val)); - if (!new_assignment[i]) { - new_upper += m_weights[i]; - } - } - if (new_upper < m_upper) { - m_upper = new_upper; - m_model = model; - m_assignment.reset(); - m_assignment.append(new_assignment); - } - } - - void update_sigmas() { - for (unsigned i = 0; i < m_cores.size(); ++i) { - wcore& c_i = m_cores[i]; - unsigned_vector const& R = c_i.m_R; - c_i.m_upper.reset(); - for (unsigned j = 0; j < R.size(); ++j) { - unsigned r_j = R[j]; - if (!m_assignment[r_j]) { - c_i.m_upper += m_weights[r_j]; - m_sigmas[r_j] = m_weights[r_j]; - } - else { - m_sigmas[r_j].reset(); - } - } - c_i.m_mid = div(c_i.m_lower + c_i.m_upper, rational(2)); - } - } - - /** - * Minimum of two (positive) numbers. Zero is treated as +infinity. - */ - rational min_z(rational const& a, rational const& b) { - if (a.is_zero()) return b; - if (b.is_zero()) return a; - if (a < b) return a; - return b; - } - - rational min_of_delta(uint_set const& subC) { - rational delta(0); - for (uint_set::iterator it = subC.begin(); it != subC.end(); ++it) { - unsigned j = *it; - wcore const& core = m_cores[j]; - rational new_delta = rational(1) + core.m_upper - core.m_mid; - SASSERT(new_delta.is_pos()); - delta = min_z(delta, new_delta); - } - return delta; - } - - rational sum_of_lower(uint_set const& subC) { - rational lower(0); - for (uint_set::iterator it = subC.begin(); it != subC.end(); ++it) { - lower += m_cores[*it].m_lower; - } - return lower; - } - - rational sum_of_sigmas(unsigned_vector const& R) { - rational sum(0); - for (unsigned i = 0; i < R.size(); ++i) { - sum += m_sigmas[R[i]]; - } - return sum; - } - void union_Rs(uint_set const& subC, unsigned_vector& R) { - for (uint_set::iterator it = subC.begin(); it != subC.end(); ++it) { - R.append(m_cores[*it].m_R); - } - } - rational compute_lower() { - rational result(0); - for (unsigned i = 0; i < m_cores.size(); ++i) { - result += m_cores[i].m_lower; - } - return result; - } - void subtract(vector& cores, uint_set const& subC) { - unsigned j = 0; - for (unsigned i = 0; i < cores.size(); ++i) { - if (subC.contains(i)) { - m_asm_set.remove(cores[i].m_r); - } - else { - if (j != i) { - cores[j] = cores[i]; - } - ++j; - } - } - cores.resize(j); - for (unsigned i = 0; i < cores.size(); ++i) { - m_relax2index.insert(cores[i].m_r, i); - } - } - void core2indices(ptr_vector const& core, uint_set& subC, uint_set& soft) { - for (unsigned i = 0; i < core.size(); ++i) { - unsigned j; - expr* a; - VERIFY(m.is_not(core[i], a)); - if (m_relax2index.find(a, j)) { - subC.insert(j); - } - else { - VERIFY(m_soft2index.find(a, j)); - soft.insert(j); - } - } - } - rational refine(unsigned_vector const& idx, rational v) { - return v + rational(1); - } - void relax(uint_set& subC, uint_set& soft, unsigned_vector& R, rational& delta) { - for (uint_set::iterator it = soft.begin(); it != soft.end(); ++it) { - R.push_back(*it); - delta = min_z(delta, m_weights[*it]); - m_asm_set.remove(m_soft_aux[*it].get()); - } - } - void assert_cores() { - for (unsigned i = 0; i < m_cores.size(); ++i) { - assert_core(m_cores[i]); - } - } - void assert_core(wcore const& core) { - expr_ref fml(m); - vector ws; - ptr_vector rs; - rational w(0); - for (unsigned j = 0; j < core.m_R.size(); ++j) { - unsigned idx = core.m_R[j]; - ws.push_back(m_weights[idx]); - w += ws.back(); - rs.push_back(m_soft_aux[idx].get()); - } - w.neg(); - w += core.m_mid; - ws.push_back(w); - rs.push_back(core.m_r); - fml = pb.mk_le(ws.size(), ws.c_ptr(), rs.c_ptr(), core.m_mid); - s().assert_expr(fml); - } - void display(std::ostream& out) { - out << "[" << m_lower << ":" << m_upper << "]\n"; - s().display(out); - out << "\n"; - for (unsigned i = 0; i < m_cores.size(); ++i) { - wcore const& c = m_cores[i]; - out << mk_pp(c.m_r, m) << ": "; - for (unsigned j = 0; j < c.m_R.size(); ++j) { - out << c.m_R[j] << " (" << m_sigmas[c.m_R[j]] << ") "; - } - out << "[" << c.m_lower << ":" << c.m_mid << ":" << c.m_upper << "]\n"; - } - for (unsigned i = 0; i < m_soft.size(); ++i) { - out << mk_pp(m_soft[i].get(), m) << " " << m_weights[i] << "\n"; - } - } - }; - - // ---------------------------------- - // MaxSatHS+MSS - // variant of MaxSAT-HS (Algorithm 9) - // that also refines upper bound during progressive calls - // to the underlying optimization solver for the soft constraints. - // - - class hsmax : public maxsmt_solver_base { - struct stats { - stats() { reset(); } - void reset() { memset(this, 0, sizeof(*this)); } - unsigned m_num_iterations; - unsigned m_num_core_reductions_success; - unsigned m_num_core_reductions_failure; - unsigned m_num_model_expansions_success; - unsigned m_num_model_expansions_failure; - double m_core_reduction_time; - double m_model_expansion_time; - double m_aux_sat_time; - double m_disjoint_cores_time; - }; - - hitting_sets m_hs; - expr_ref_vector m_aux; // auxiliary (indicator) variables. - obj_map m_aux2index; // expr |-> index - unsigned_vector m_core_activity; // number of times soft constraint is used in a core. - svector m_seed; // clause selected in current model. - svector m_aux_active; // active soft clauses. - ptr_vector m_asms; // assumptions (over aux) - pb_util pb; - arith_util a; - stats m_stats; - bool m_at_lower_bound; - - - public: - hsmax(opt_solver* s, ast_manager& m, params_ref& p, vector const& ws, expr_ref_vector const& soft): - maxsmt_solver_base(s, m, p, ws, soft), - m_aux(m), - pb(m), - a(m), - m_at_lower_bound(false) { - } - virtual ~hsmax() {} - - virtual void set_cancel(bool f) { - maxsmt_solver_base::set_cancel(f); - m_hs.set_cancel(f); - } - - virtual void collect_statistics(statistics& st) const { - maxsmt_solver_base::collect_statistics(st); - m_hs.collect_statistics(st); - st.update("hsmax-num-iterations", m_stats.m_num_iterations); - st.update("hsmax-num-core-reductions-n", m_stats.m_num_core_reductions_failure); - st.update("hsmax-num-core-reductions-y", m_stats.m_num_core_reductions_success); - st.update("hsmax-num-model-expansions-n", m_stats.m_num_model_expansions_failure); - st.update("hsmax-num-model-expansions-y", m_stats.m_num_model_expansions_success); - st.update("hsmax-core-reduction-time", m_stats.m_core_reduction_time); - st.update("hsmax-model-expansion-time", m_stats.m_model_expansion_time); - st.update("hsmax-aux-sat-time", m_stats.m_aux_sat_time); - st.update("hsmax-disj-core-time", m_stats.m_disjoint_cores_time); - } - - lbool operator()() { - ptr_vector hs; - init(); - init_local(); - if (!disjoint_cores(hs)) { - return l_undef; - } - seed2assumptions(); - while (m_lower < m_upper) { - ++m_stats.m_num_iterations; - IF_VERBOSE(1, verbose_stream() << - "(hsmax [" << m_lower << ":" << m_upper << "])\n";); - TRACE("opt", tout << "(hsmax [" << m_lower << ":" << m_upper << "])\n";); - if (m_cancel) { - return l_undef; - } - - lbool core_found = generate_cores(hs); - switch(core_found) { - case l_undef: - return l_undef; - case l_true: { - lbool is_sat = next_seed(); - switch(is_sat) { - case l_true: - seed2hs(false, hs); - break; - case l_false: - TRACE("opt", tout << "no more seeds\n";); - IF_VERBOSE(1, verbose_stream() << "(maxhs.no-more-seeds)\n";); - m_lower = m_upper; - return l_true; - case l_undef: - return l_undef; - } - break; - } - case l_false: - IF_VERBOSE(1, verbose_stream() << "(maxhs.no-more-cores)\n";); - TRACE("opt", tout << "no more cores\n";); - m_lower = m_upper; - return l_true; - } - } - return l_true; - } - - private: - - unsigned num_soft() const { return m_soft.size(); } - - void init_local() { - unsigned sz = num_soft(); - app_ref fml(m), obj(m); - expr_ref_vector sum(m); - m_asms.reset(); - m_seed.reset(); - m_aux.reset(); - m_aux_active.reset(); - m_aux2index.reset(); - m_core_activity.reset(); - for (unsigned i = 0; i < sz; ++i) { - bool tt = is_true(m_model, m_soft[i].get()); - m_seed.push_back(tt); - m_aux. push_back(mk_fresh(m.mk_bool_sort())); - m_aux_active.push_back(false); - m_core_activity.push_back(0); - m_aux2index.insert(m_aux.back(), i); - if (tt) { - m_asms.push_back(m_aux.back()); - ensure_active(i); - } - } - - for (unsigned i = 0; i < m_weights.size(); ++i) { - m_hs.add_weight(m_weights[i]); - } - TRACE("opt", print_seed(tout);); - } - - - void hs2seed(ptr_vector const& hs) { - for (unsigned i = 0; i < num_soft(); ++i) { - m_seed[i] = true; - } - for (unsigned i = 0; i < hs.size(); ++i) { - m_seed[m_aux2index.find(hs[i])] = false; - } - TRACE("opt", - print_asms(tout << "hitting set: ", hs); - print_seed(tout);); - } - - void seed2hs(bool pos, ptr_vector& hs) { - hs.reset(); - for (unsigned i = 0; i < num_soft(); ++i) { - if (pos == m_seed[i]) { - hs.push_back(m_aux[i].get()); - } - } - TRACE("opt", - print_asms(tout << "hitting set: ", hs); - print_seed(tout);); - - } - - void seed2assumptions() { - seed2hs(true, m_asms); - } - - - // - // Find disjoint cores for soft constraints. - // - bool disjoint_cores(ptr_vector& hs) { - scoped_stopwatch _sw(m_stats.m_disjoint_cores_time); - m_asms.reset(); - svector active(num_soft(), true); - rational lower(0); - update_assumptions(active, lower, hs); - SASSERT(lower.is_zero()); - while (true) { - lbool is_sat = s().check_sat(m_asms.size(), m_asms.c_ptr()); - switch (is_sat) { - case l_true: - if (lower > m_lower) { - m_lower = lower; - } - return true; - case l_false: - if (!shrink()) return false; - block_up(); - update_assumptions(active, lower, hs); - break; - case l_undef: - return false; - } - } - } - - void update_assumptions(svector& active, rational& lower, ptr_vector& hs) { - rational arg_min(0); - expr* e = 0; - for (unsigned i = 0; i < m_asms.size(); ++i) { - unsigned index = m_aux2index.find(m_asms[i]); - active[index] = false; - if (arg_min.is_zero() || arg_min > m_weights[index]) { - arg_min = m_weights[index]; - e = m_asms[i]; - } - } - if (e) { - hs.push_back(e); - lower += arg_min; - } - m_asms.reset(); - for (unsigned i = 0; i < num_soft(); ++i) { - if (active[i]) { - m_asms.push_back(m_aux[i].get()); - ensure_active(i); - } - } - } - - // - // Auxiliary Algorithm 10 for producing cores. - // - lbool generate_cores(ptr_vector& hs) { - bool core = !m_at_lower_bound; - while (true) { - hs2seed(hs); - lbool is_sat = check_subset(); - switch(is_sat) { - case l_undef: - return l_undef; - case l_true: - if (!grow()) return l_undef; - block_down(); - return core?l_true:l_false; - case l_false: - core = true; - if (!shrink()) return l_undef; - block_up(); - find_non_optimal_hitting_set(hs); - break; - } - } - } - - struct lt_activity { - hsmax& hs; - lt_activity(hsmax& hs):hs(hs) {} - bool operator()(expr* a, expr* b) const { - unsigned w1 = hs.m_core_activity[hs.m_aux2index.find(a)]; - unsigned w2 = hs.m_core_activity[hs.m_aux2index.find(b)]; - return w1 < w2; - } - }; - - // - // produce the non-optimal hitting set by using the 10% heuristic. - // of most active cores constraints. - // m_asms contains the current core. - // - void find_non_optimal_hitting_set(ptr_vector& hs) { - std::sort(m_asms.begin(), m_asms.end(), lt_activity(*this)); - for (unsigned i = m_asms.size(); i > 9*m_asms.size()/10;) { - --i; - hs.push_back(m_asms[i]); - } - } - - // - // retrieve the next seed that satisfies state of hs. - // state of hs must be satisfiable before optimization is called. - // - lbool next_seed() { - scoped_stopwatch _sw(m_stats.m_aux_sat_time); - TRACE("opt", tout << "\n";); - - // min c_i*(not x_i) for x_i are soft clauses. - // max c_i*x_i for x_i are soft clauses - - m_at_lower_bound = false; - - lbool is_sat = m_hs.compute_upper(); - - if (is_sat == l_true) { - is_sat = m_hs.compute_lower(); - } - if (is_sat == l_true) { - m_at_lower_bound = m_hs.get_upper() == m_hs.get_lower(); - if (m_hs.get_lower() > m_lower) { - m_lower = m_hs.get_lower(); - } - for (unsigned i = 0; i < num_soft(); ++i) { - m_seed[i] = is_active(i) && !m_hs.get_value(i); - } - TRACE("opt", print_seed(tout);); - } - return is_sat; - } - - // - // check assignment returned by HS with the original - // hard constraints. - // - lbool check_subset() { - TRACE("opt", tout << "\n";); - m_asms.reset(); - for (unsigned i = 0; i < num_soft(); ++i) { - if (m_seed[i]) { - m_asms.push_back(m_aux[i].get()); - ensure_active(i); - } - } - return s().check_sat(m_asms.size(), m_asms.c_ptr()); - } - - // - // extend the current assignment to one that - // satisfies as many soft constraints as possible. - // update the upper bound based on this assignment - // - bool grow() { - scoped_stopwatch _sw(m_stats.m_model_expansion_time); - model_ref mdl; - s().get_model(mdl); - for (unsigned i = 0; i < num_soft(); ++i) { - ensure_active(i); - m_seed[i] = false; - } - for (unsigned i = 0; i < m_asms.size(); ++i) { - m_seed[m_aux2index.find(m_asms[i])] = true; - } - - for (unsigned i = 0; i < num_soft(); ++i) { - if (m_seed[i]) { - // already an assumption - } - else if (is_true(mdl, m_soft[i].get())) { - m_seed[i] = true; - m_asms.push_back(m_aux[i].get()); - } - else { - m_asms.push_back(m_aux[i].get()); - lbool is_sat = s().check_sat(m_asms.size(), m_asms.c_ptr()); - switch(is_sat) { - case l_undef: - return false; - case l_false: - ++m_stats.m_num_model_expansions_failure; - m_asms.pop_back(); - break; - case l_true: - ++m_stats.m_num_model_expansions_success; - s().get_model(mdl); - m_seed[i] = true; - break; - } - } - } - rational upper(0); - for (unsigned i = 0; i < num_soft(); ++i) { - if (!m_seed[i]) { - upper += m_weights[i]; - } - } - if (upper < m_upper) { - m_upper = upper; - m_hs.set_upper(upper); - m_model = mdl; - m_assignment.reset(); - m_assignment.append(m_seed); - TRACE("opt", - tout << "new upper: " << m_upper << "\n"; - model_smt2_pp(tout, m, *(mdl.get()), 0);); - } - DEBUG_CODE( - for (unsigned i = 0; i < num_soft(); ++i) { - SASSERT(is_true(mdl, m_soft[i].get()) == m_seed[i]); - }); - - return true; - } - - // - // remove soft constraints from the current core. - // - bool shrink() { - scoped_stopwatch _sw(m_stats.m_core_reduction_time); - m_asms.reset(); - s().get_unsat_core(m_asms); - TRACE("opt", print_asms(tout, m_asms);); - obj_map asm2index; - for (unsigned i = 0; i < m_asms.size(); ++i) { - asm2index.insert(m_asms[i], i); - } - obj_map::iterator it = asm2index.begin(), end = asm2index.end(); - for (; it != end; ++it) { - unsigned i = it->m_value; - if (i < m_asms.size()) { - expr* tmp = m_asms[i]; - expr* back = m_asms.back(); - m_asms[i] = back; - m_asms.pop_back(); - lbool is_sat = s().check_sat(m_asms.size(), m_asms.c_ptr()); - TRACE("opt", tout << "checking: " << mk_pp(tmp, m) << ": " << is_sat << "\n";); - switch(is_sat) { - case l_true: - ++m_stats.m_num_core_reductions_failure; - // put back literal into core - m_asms.push_back(back); - m_asms[i] = tmp; - break; - case l_false: - // update the core - m_asms.reset(); - ++m_stats.m_num_core_reductions_success; - s().get_unsat_core(m_asms); - TRACE("opt", print_asms(tout, m_asms);); - update_index(asm2index); - break; - case l_undef: - return false; - } - } - } - return true; - } - - void print_asms(std::ostream& out, ptr_vector const& asms) { - for (unsigned j = 0; j < asms.size(); ++j) { - out << mk_pp(asms[j], m) << " "; - } - out << "\n"; - } - - void print_seed(std::ostream& out) { - out << "seed: "; - for (unsigned i = 0; i < num_soft(); ++i) { - out << (m_seed[i]?"1":"0"); - } - out << "\n"; - } - - // - // must include some literal not from asms. - // (furthermore, update upper bound constraint in HS) - // - void block_down() { - uint_set indices; - unsigned_vector c_indices; - for (unsigned i = 0; i < m_asms.size(); ++i) { - indices.insert(m_aux2index.find(m_asms[i])); - } - for (unsigned i = 0; i < num_soft(); ++i) { - if (!indices.contains(i)) { - c_indices.push_back(i); - } - } - m_hs.add_exists_false(c_indices.size(), c_indices.c_ptr()); - } - - // should exclude some literal from core. - void block_up() { - unsigned_vector indices; - for (unsigned i = 0; i < m_asms.size(); ++i) { - unsigned index = m_aux2index.find(m_asms[i]); - m_core_activity[index]++; - indices.push_back(index); - } - m_hs.add_exists_true(indices.size(), indices.c_ptr()); - } - - void update_index(obj_map& asm2index) { - obj_map::iterator it = asm2index.begin(), end = asm2index.end(); - for (; it != end; ++it) { - it->m_value = UINT_MAX; - } - for (unsigned i = 0; i < m_asms.size(); ++i) { - asm2index.find(m_asms[i]) = i; - } - } - - app_ref mk_fresh(sort* s) { - app_ref r(m); - r = m.mk_fresh_const("r", s); - m_mc->insert(r->get_decl()); - return r; - } - - bool is_true(model_ref& mdl, expr* e) { - expr_ref val(m); - VERIFY(mdl->eval(e, val)); - return m.is_true(val); - } - - bool is_active(unsigned i) const { - return m_aux_active[i]; - } - - void ensure_active(unsigned i) { - if (!is_active(i)) { - expr_ref fml(m); - fml = m.mk_implies(m_aux[i].get(), m_soft[i].get()); - s().assert_expr(fml); - m_aux_active[i] = true; - } - } - - }; - - - // ---------------------------------- - // incrementally add pseudo-boolean - // lower bounds. - - class pbmax : public maxsmt_solver_base { - public: - pbmax(opt_solver* s, ast_manager& m, params_ref& p, - vector const& ws, expr_ref_vector const& soft): - maxsmt_solver_base(s, m, p, ws, soft) { - } - - virtual ~pbmax() {} - - lbool operator()() { - enable_bvsat(); - enable_sls(); - - TRACE("opt", s().display(tout); tout << "\n"; - for (unsigned i = 0; i < m_soft.size(); ++i) { - tout << mk_pp(m_soft[i].get(), m) << " " << m_weights[i] << "\n"; - } - ); - pb_util u(m); - expr_ref fml(m), val(m); - app_ref b(m); - expr_ref_vector nsoft(m); - init(); - for (unsigned i = 0; i < m_soft.size(); ++i) { - nsoft.push_back(mk_not(m_soft[i].get())); - } - lbool is_sat = l_true; - while (l_true == is_sat) { - TRACE("opt", s().display(tout<<"looping\n"); - model_smt2_pp(tout << "\n", m, *(m_model.get()), 0);); - m_upper.reset(); - for (unsigned i = 0; i < m_soft.size(); ++i) { - VERIFY(m_model->eval(nsoft[i].get(), val)); - m_assignment[i] = !m.is_true(val); - if (!m_assignment[i]) { - m_upper += m_weights[i]; - } - } - IF_VERBOSE(1, verbose_stream() << "(pb solve with upper bound: " << m_upper << ")\n";); - TRACE("opt", tout << "new upper: " << m_upper << "\n";); - - fml = u.mk_lt(nsoft.size(), m_weights.c_ptr(), nsoft.c_ptr(), m_upper); - solver::scoped_push _scope2(s()); - s().assert_expr(fml); - is_sat = s().check_sat(0,0); - if (m_cancel) { - is_sat = l_undef; - } - if (is_sat == l_true) { - s().get_model(m_model); - } - } - if (is_sat == l_false) { - is_sat = l_true; - m_lower = m_upper; - } - TRACE("opt", tout << "lower: " << m_lower << "\n";); - return is_sat; - } - }; - - // ------------------------------------------------------ - // AAAI 2010 - class wpm2 : public maxsmt_solver_base { - scoped_ptr maxs; - public: - wpm2(opt_solver* s, ast_manager& m, maxsmt_solver_base* _maxs, params_ref& p, - vector const& ws, expr_ref_vector const& soft): - maxsmt_solver_base(s, m, p, ws, soft), maxs(_maxs) { - } - - virtual ~wpm2() {} - - lbool operator()() { - enable_sls(); - IF_VERBOSE(1, verbose_stream() << "(wpm2 solve)\n";); - solver::scoped_push _s(s()); - pb_util u(m); - app_ref fml(m), a(m), b(m), c(m); - expr_ref val(m); - expr_ref_vector block(m), ans(m), al(m), am(m); - obj_map ans_index; - vector amk; - vector sc; - init(); - for (unsigned i = 0; i < m_soft.size(); ++i) { - rational w = m_weights[i]; - - b = mk_fresh_bool("b"); - block.push_back(b); - expr* bb = b; - - a = mk_fresh_bool("a"); - ans.push_back(a); - ans_index.insert(a, i); - fml = m.mk_or(m_soft[i].get(), b, m.mk_not(a)); - s().assert_expr(fml); - - c = mk_fresh_bool("c"); - fml = m.mk_implies(c, u.mk_le(1,&w,&bb,rational(0))); - s().assert_expr(fml); - - sc.push_back(uint_set()); - sc.back().insert(i); - am.push_back(c); - amk.push_back(rational(0)); - } - - while (true) { - expr_ref_vector asms(m); - ptr_vector core; - asms.append(ans); - asms.append(am); - lbool is_sat = s().check_sat(asms.size(), asms.c_ptr()); - TRACE("opt", - tout << "\nassumptions: "; - for (unsigned i = 0; i < asms.size(); ++i) { - tout << mk_pp(asms[i].get(), m) << " "; - } - tout << "\n" << is_sat << "\n"; - tout << "upper: " << m_upper << "\n"; - tout << "lower: " << m_lower << "\n"; - if (is_sat == l_true) { - model_ref mdl; - s().get_model(mdl); - model_smt2_pp(tout, m, *(mdl.get()), 0); - }); - - if (m_cancel && is_sat != l_false) { - is_sat = l_undef; - } - if (is_sat == l_true) { - m_upper = m_lower; - s().get_model(m_model); - for (unsigned i = 0; i < block.size(); ++i) { - VERIFY(m_model->eval(m_soft[i].get(), val)); - TRACE("opt", tout << mk_pp(block[i].get(), m) << " " << val << "\n";); - m_assignment[i] = m.is_true(val); - } - } - if (is_sat != l_false) { - return is_sat; - } - s().get_unsat_core(core); - if (core.empty()) { - return l_false; - } - TRACE("opt", - tout << "core: "; - for (unsigned i = 0; i < core.size(); ++i) { - tout << mk_pp(core[i],m) << " "; - } - tout << "\n";); - uint_set A; - for (unsigned i = 0; i < core.size(); ++i) { - unsigned j; - if (ans_index.find(core[i], j)) { - A.insert(j); - } - } - if (A.empty()) { - return l_false; - } - uint_set B; - rational k(0); - rational old_lower(m_lower); - for (unsigned i = 0; i < sc.size(); ++i) { - uint_set t(sc[i]); - t &= A; - if (!t.empty()) { - B |= sc[i]; - k += amk[i]; - m_lower -= amk[i]; - sc[i] = sc.back(); - sc.pop_back(); - am[i] = am.back(); - am.pop_back(); - amk[i] = amk.back(); - amk.pop_back(); - --i; - } - } - vector ws; - expr_ref_vector bs(m); - for (unsigned i = 0; i < m_soft.size(); ++i) { - if (B.contains(i)) { - ws.push_back(m_weights[i]); - bs.push_back(block[i].get()); - } - } - TRACE("opt", tout << "at most bound: " << k << "\n";); - is_sat = new_bound(al, ws, bs, k); - if (is_sat != l_true) { - return is_sat; - } - m_lower += k; - SASSERT(m_lower > old_lower); - TRACE("opt", tout << "new bound: " << m_lower << "\n";); - expr_ref B_le_k(m), B_ge_k(m); - B_le_k = u.mk_le(ws.size(), ws.c_ptr(), bs.c_ptr(), k); - B_ge_k = u.mk_ge(ws.size(), ws.c_ptr(), bs.c_ptr(), k); - s().assert_expr(B_ge_k); - al.push_back(B_ge_k); - IF_VERBOSE(1, verbose_stream() << "(wpm2 lower bound: " << m_lower << ")\n";); - IF_VERBOSE(2, verbose_stream() << "New lower bound: " << B_ge_k << "\n";); - - c = mk_fresh_bool("c"); - fml = m.mk_implies(c, B_le_k); - s().assert_expr(fml); - sc.push_back(B); - am.push_back(c); - amk.push_back(k); - } - } - - virtual void set_cancel(bool f) { - maxsmt_solver_base::set_cancel(f); - maxs->set_cancel(f); - } - - virtual void collect_statistics(statistics& st) const { - maxsmt_solver_base::collect_statistics(st); - maxs->collect_statistics(st); - } - - private: - lbool new_bound(expr_ref_vector const& al, - vector const& ws, - expr_ref_vector const& bs, - rational& k) { - pb_util u(m); - expr_ref_vector al2(m); - al2.append(al); - // w_j*b_j > k - al2.push_back(m.mk_not(u.mk_le(ws.size(), ws.c_ptr(), bs.c_ptr(), k))); - return bound(al2, ws, bs, k); - } - - // - // minimal k, such that al & w_j*b_j >= k is sat - // minimal k, such that al & 3*x + 4*y >= k is sat - // minimal k, such that al & (or (not x) w3) & (or (not y) w4) - // - lbool bound(expr_ref_vector const& al, - vector const& ws, - expr_ref_vector const& bs, - rational& k) { - expr_ref_vector nbs(m); - opt_solver::scoped_push _sc(maxs->s()); - for (unsigned i = 0; i < al.size(); ++i) { - maxs->add_hard(al[i]); - } - for (unsigned i = 0; i < bs.size(); ++i) { - nbs.push_back(mk_not(bs[i])); - } - TRACE("opt", - maxs->s().display(tout); - tout << "\n"; - for (unsigned i = 0; i < bs.size(); ++i) { - tout << mk_pp(bs[i], m) << " " << ws[i] << "\n"; - }); - maxs->init_soft(ws, nbs); - lbool is_sat = maxs->s().check_sat(0,0); - if (is_sat == l_true) { - maxs->set_model(); - is_sat = (*maxs)(); - } - SASSERT(maxs->get_lower() > k); - k = maxs->get_lower(); - return is_sat; - } - }; - - class sls : public maxsmt_solver_base { - public: - sls(opt_solver* s, ast_manager& m, params_ref& p, - vector const& ws, expr_ref_vector const& soft): - maxsmt_solver_base(s, m, p, ws, soft) { - } - virtual ~sls() {} - lbool operator()() { - IF_VERBOSE(1, verbose_stream() << "(sls solve)\n";); - enable_bvsat(); - enable_sls(); - init(); - lbool is_sat = s().check_sat(0, 0); - if (is_sat == l_true) { - s().get_model(m_model); - m_upper.reset(); - for (unsigned i = 0; i < m_soft.size(); ++i) { - expr_ref tmp(m); - m_model->eval(m_soft[i].get(), tmp, true); - m_assignment[i] = m.is_true(tmp); - if (!m_assignment[i]) { - m_upper += m_weights[i]; - } - } - } - return is_sat; - } - - }; - - - class maxsmt_solver_wbase : public maxsmt_solver_base { - smt::context& ctx; - public: - maxsmt_solver_wbase(opt_solver* s, ast_manager& m, smt::context& ctx, params_ref& p, - vector const& ws, expr_ref_vector const& soft): - maxsmt_solver_base(s, m, p, ws, soft), ctx(ctx) {} - ~maxsmt_solver_wbase() {} - - class scoped_ensure_theory { - smt::theory_wmaxsat* m_wth; - public: - scoped_ensure_theory(maxsmt_solver_wbase& s) { - m_wth = s.ensure_theory(); - } - ~scoped_ensure_theory() { - m_wth->reset(); - } - smt::theory_wmaxsat& operator()() { return *m_wth; } - }; - - smt::theory_wmaxsat* ensure_theory() { - smt::theory_wmaxsat* wth = get_theory(); - if (wth) { - wth->reset(); - } - else { - wth = alloc(smt::theory_wmaxsat, m, m_mc); - ctx.register_plugin(wth); - } - return wth; - } - smt::theory_wmaxsat* get_theory() const { - smt::theory_id th_id = m.get_family_id("weighted_maxsat"); - smt::theory* th = ctx.get_theory(th_id); - if (th) { - return dynamic_cast(th); - } - else { - return 0; - } - } - }; - - // ---------------------------------------------------------- - // weighted max-sat using a custom theory solver for max-sat. - // NB. it is quite similar to pseudo-Boolean propagation. - - - class wmax : public maxsmt_solver_wbase { - public: - wmax(opt_solver* s, ast_manager& m, smt::context& ctx, params_ref& p, - vector const& ws, expr_ref_vector const& soft): - maxsmt_solver_wbase(s, m, ctx, p, ws, soft) {} - virtual ~wmax() {} - - lbool operator()() { - TRACE("opt", tout << "weighted maxsat\n";); - scoped_ensure_theory wth(*this); - solver::scoped_push _s(s()); - lbool is_sat = l_true; - bool was_sat = false; - for (unsigned i = 0; i < m_soft.size(); ++i) { - wth().assert_weighted(m_soft[i].get(), m_weights[i]); - } - solver::scoped_push __s(s()); - while (l_true == is_sat) { - IF_VERBOSE(1, verbose_stream() << "(wmax " << m_upper << ")\n";); - is_sat = s().check_sat(0,0); - if (m_cancel) { - is_sat = l_undef; - } - if (is_sat == l_true) { - if (wth().is_optimal()) { - m_upper = wth().get_min_cost(); - s().get_model(m_model); - } - expr_ref fml = wth().mk_block(); - s().assert_expr(fml); - was_sat = true; - } - } - if (was_sat) { - wth().get_assignment(m_assignment); - } - if (is_sat == l_false && was_sat) { - is_sat = l_true; - } - m_upper = wth().get_min_cost(); - if (is_sat == l_true) { - m_lower = m_upper; - } - TRACE("opt", tout << "min cost: " << m_upper << "\n";); - return is_sat; - } - }; - - - maxsmt_solver_base* opt::mk_bcd2(ast_manager& m, opt_solver* s, params_ref& p, - vector const& ws, expr_ref_vector const& soft) { - return alloc(bcd2, s, m, p, ws, soft); - } - maxsmt_solver_base* opt::mk_pbmax(ast_manager& m, opt_solver* s, params_ref& p, - vector const& ws, expr_ref_vector const& soft) { - return alloc(pbmax, s, m, p, ws, soft); - } - maxsmt_solver_base* opt::mk_hsmax(ast_manager& m, opt_solver* s, params_ref& p, - vector const& ws, expr_ref_vector const& soft) { - return alloc(hsmax, s, m, p, ws, soft); - } - maxsmt_solver_base* opt::mk_sls(ast_manager& m, opt_solver* s, params_ref& p, - vector const& ws, expr_ref_vector const& soft) { - return alloc(hsmax, s, m, p, ws, soft); - } - maxsmt_solver_base* opt::mk_wmax(ast_manager& m, opt_solver* s, params_ref& p, - vector const& ws, expr_ref_vector const& soft) { - return alloc(wmax, s, m, s->get_context(), p, ws, soft); - } - maxsmt_solver_base* opt::mk_wpm2(ast_manager& m, opt_solver* s, params_ref& p, - vector const& ws, expr_ref_vector const& soft) { - - ref s0 = alloc(opt_solver, m, p, symbol()); - // initialize model. - s0->check_sat(0,0); - maxsmt_solver_base* s2 = alloc(pbmax, s0.get(), m, p, ws, soft); - return alloc(wpm2, s, m, s2, p, ws, soft); - } - - -}; diff --git a/src/opt/weighted_maxsat.h b/src/opt/weighted_maxsat.h deleted file mode 100644 index 5343a3b97..000000000 --- a/src/opt/weighted_maxsat.h +++ /dev/null @@ -1,51 +0,0 @@ -/*++ -Copyright (c) 2013 Microsoft Corporation - -Module Name: - - weighted_maxsat.h - -Abstract: - - Weighted MAXSAT module - -Author: - - Nikolaj Bjorner (nbjorner) 2014-4-17 - -Notes: - - Takes solver with hard constraints added. - Returns a maximal satisfying subset of weighted soft_constraints - that are still consistent with the solver state. - ---*/ -#ifndef _OPT_WEIGHTED_MAX_SAT_H_ -#define _OPT_WEIGHTED_MAX_SAT_H_ - -#include "opt_solver.h" -#include "maxsmt.h" - -namespace opt { - - maxsmt_solver_base* mk_bcd2(ast_manager& m, opt_solver* s, params_ref& p, - vector const& ws, expr_ref_vector const& soft); - - maxsmt_solver_base* mk_hsmax(ast_manager& m, opt_solver* s, params_ref& p, - vector const& ws, expr_ref_vector const& soft); - - maxsmt_solver_base* mk_pbmax(ast_manager& m, opt_solver* s, params_ref& p, - vector const& ws, expr_ref_vector const& soft); - - maxsmt_solver_base* mk_wpm2(ast_manager& m, opt_solver* s, params_ref& p, - vector const& ws, expr_ref_vector const& soft); - - maxsmt_solver_base* mk_sls(ast_manager& m, opt_solver* s, params_ref& p, - vector const& ws, expr_ref_vector const& soft); - - maxsmt_solver_base* mk_wmax(ast_manager& m, opt_solver* s, params_ref& p, - vector const& ws, expr_ref_vector const& soft); - -}; - -#endif diff --git a/src/opt/wmax.cpp b/src/opt/wmax.cpp new file mode 100644 index 000000000..8c76b06ba --- /dev/null +++ b/src/opt/wmax.cpp @@ -0,0 +1,130 @@ +/*++ +Copyright (c) 2014 Microsoft Corporation + +Module Name: + + wmax.cpp + +Abstract: + + Theory based MaxSAT. + +Author: + + Nikolaj Bjorner (nbjorner) 2014-4-17 + +Notes: + +--*/ +#include "wmax.h" +#include "uint_set.h" +#include "ast_pp.h" +#include "model_smt2_pp.h" +#include "smt_theory.h" +#include "smt_context.h" +#include "theory_wmaxsat.h" + + +namespace opt { + class maxsmt_solver_wbase : public maxsmt_solver_base { + smt::context& ctx; + public: + maxsmt_solver_wbase(opt_solver* s, ast_manager& m, smt::context& ctx, params_ref& p, + vector const& ws, expr_ref_vector const& soft): + maxsmt_solver_base(s, m, p, ws, soft), ctx(ctx) {} + ~maxsmt_solver_wbase() {} + + class scoped_ensure_theory { + smt::theory_wmaxsat* m_wth; + public: + scoped_ensure_theory(maxsmt_solver_wbase& s) { + m_wth = s.ensure_theory(); + } + ~scoped_ensure_theory() { + m_wth->reset(); + } + smt::theory_wmaxsat& operator()() { return *m_wth; } + }; + + smt::theory_wmaxsat* ensure_theory() { + smt::theory_wmaxsat* wth = get_theory(); + if (wth) { + wth->reset(); + } + else { + wth = alloc(smt::theory_wmaxsat, m, m_mc); + ctx.register_plugin(wth); + } + return wth; + } + smt::theory_wmaxsat* get_theory() const { + smt::theory_id th_id = m.get_family_id("weighted_maxsat"); + smt::theory* th = ctx.get_theory(th_id); + if (th) { + return dynamic_cast(th); + } + else { + return 0; + } + } + }; + + // ---------------------------------------------------------- + // weighted max-sat using a custom theory solver for max-sat. + // NB. it is quite similar to pseudo-Boolean propagation. + + + class wmax : public maxsmt_solver_wbase { + public: + wmax(opt_solver* s, ast_manager& m, smt::context& ctx, params_ref& p, + vector const& ws, expr_ref_vector const& soft): + maxsmt_solver_wbase(s, m, ctx, p, ws, soft) {} + virtual ~wmax() {} + + lbool operator()() { + TRACE("opt", tout << "weighted maxsat\n";); + scoped_ensure_theory wth(*this); + solver::scoped_push _s(s()); + lbool is_sat = l_true; + bool was_sat = false; + for (unsigned i = 0; i < m_soft.size(); ++i) { + wth().assert_weighted(m_soft[i].get(), m_weights[i]); + } + solver::scoped_push __s(s()); + while (l_true == is_sat) { + IF_VERBOSE(1, verbose_stream() << "(opt.wmax [" << m_lower << ":" << m_upper << "])\n";); + is_sat = s().check_sat(0,0); + if (m_cancel) { + is_sat = l_undef; + } + if (is_sat == l_true) { + if (wth().is_optimal()) { + m_upper = wth().get_min_cost(); + s().get_model(m_model); + } + expr_ref fml = wth().mk_block(); + s().assert_expr(fml); + was_sat = true; + } + } + if (was_sat) { + wth().get_assignment(m_assignment); + } + if (is_sat == l_false && was_sat) { + is_sat = l_true; + } + m_upper = wth().get_min_cost(); + if (is_sat == l_true) { + m_lower = m_upper; + } + TRACE("opt", tout << "min cost: " << m_upper << "\n";); + return is_sat; + } + }; + + maxsmt_solver_base* opt::mk_wmax(ast_manager& m, opt_solver* s, params_ref& p, + vector const& ws, expr_ref_vector const& soft) { + return alloc(wmax, s, m, s->get_context(), p, ws, soft); + } + +} diff --git a/src/opt/wmax.h b/src/opt/wmax.h new file mode 100644 index 000000000..bc33eee4a --- /dev/null +++ b/src/opt/wmax.h @@ -0,0 +1,30 @@ +/*++ +Copyright (c) 2014 Microsoft Corporation + +Module Name: + + wmax.h + +Abstract: + + Theory Solver based MaxSAT. + +Author: + + Nikolaj Bjorner (nbjorner) 2014-4-17 + +Notes: + +--*/ + +#ifndef _WMAX_H_ +#define _WMAX_H_ + +#include "maxsmt.h" + +namespace opt { + maxsmt_solver_base* mk_wmax(ast_manager& m, opt_solver* s, params_ref& p, + vector const& ws, expr_ref_vector const& soft); + +} +#endif diff --git a/src/opt/wpm2.cpp b/src/opt/wpm2.cpp new file mode 100644 index 000000000..63418861a --- /dev/null +++ b/src/opt/wpm2.cpp @@ -0,0 +1,251 @@ +/*++ +Copyright (c) 2014 Microsoft Corporation + +Module Name: + + wpm2.cpp + +Abstract: + + wpn2 based MaxSAT. + +Author: + + Nikolaj Bjorner (nbjorner) 2014-4-17 + +Notes: + +--*/ +#include "wpm2.h" +#include "pbmax.h" +#include "pb_decl_plugin.h" +#include "uint_set.h" +#include "ast_pp.h" +#include "model_smt2_pp.h" + + +namespace opt { + + // ------------------------------------------------------ + // AAAI 2010 + class wpm2 : public maxsmt_solver_base { + scoped_ptr maxs; + public: + wpm2(opt_solver* s, ast_manager& m, maxsmt_solver_base* _maxs, params_ref& p, + vector const& ws, expr_ref_vector const& soft): + maxsmt_solver_base(s, m, p, ws, soft), maxs(_maxs) { + } + + virtual ~wpm2() {} + + lbool operator()() { + enable_sls(); + IF_VERBOSE(1, verbose_stream() << "(opt.wpm2)\n";); + solver::scoped_push _s(s()); + pb_util u(m); + app_ref fml(m), a(m), b(m), c(m); + expr_ref val(m); + expr_ref_vector block(m), ans(m), al(m), am(m); + obj_map ans_index; + vector amk; + vector sc; + init(); + for (unsigned i = 0; i < m_soft.size(); ++i) { + rational w = m_weights[i]; + + b = mk_fresh_bool("b"); + block.push_back(b); + expr* bb = b; + + a = mk_fresh_bool("a"); + ans.push_back(a); + ans_index.insert(a, i); + fml = m.mk_or(m_soft[i].get(), b, m.mk_not(a)); + s().assert_expr(fml); + + c = mk_fresh_bool("c"); + fml = m.mk_implies(c, u.mk_le(1,&w,&bb,rational(0))); + s().assert_expr(fml); + + sc.push_back(uint_set()); + sc.back().insert(i); + am.push_back(c); + amk.push_back(rational(0)); + } + + while (true) { + expr_ref_vector asms(m); + ptr_vector core; + asms.append(ans); + asms.append(am); + lbool is_sat = s().check_sat(asms.size(), asms.c_ptr()); + TRACE("opt", + tout << "\nassumptions: "; + for (unsigned i = 0; i < asms.size(); ++i) { + tout << mk_pp(asms[i].get(), m) << " "; + } + tout << "\n" << is_sat << "\n"; + tout << "upper: " << m_upper << "\n"; + tout << "lower: " << m_lower << "\n"; + if (is_sat == l_true) { + model_ref mdl; + s().get_model(mdl); + model_smt2_pp(tout, m, *(mdl.get()), 0); + }); + + if (m_cancel && is_sat != l_false) { + is_sat = l_undef; + } + if (is_sat == l_true) { + m_upper = m_lower; + s().get_model(m_model); + for (unsigned i = 0; i < block.size(); ++i) { + VERIFY(m_model->eval(m_soft[i].get(), val)); + TRACE("opt", tout << mk_pp(block[i].get(), m) << " " << val << "\n";); + m_assignment[i] = m.is_true(val); + } + } + if (is_sat != l_false) { + return is_sat; + } + s().get_unsat_core(core); + if (core.empty()) { + return l_false; + } + TRACE("opt", + tout << "core: "; + for (unsigned i = 0; i < core.size(); ++i) { + tout << mk_pp(core[i],m) << " "; + } + tout << "\n";); + uint_set A; + for (unsigned i = 0; i < core.size(); ++i) { + unsigned j; + if (ans_index.find(core[i], j)) { + A.insert(j); + } + } + if (A.empty()) { + return l_false; + } + uint_set B; + rational k(0); + rational old_lower(m_lower); + for (unsigned i = 0; i < sc.size(); ++i) { + uint_set t(sc[i]); + t &= A; + if (!t.empty()) { + B |= sc[i]; + k += amk[i]; + m_lower -= amk[i]; + sc[i] = sc.back(); + sc.pop_back(); + am[i] = am.back(); + am.pop_back(); + amk[i] = amk.back(); + amk.pop_back(); + --i; + } + } + vector ws; + expr_ref_vector bs(m); + for (unsigned i = 0; i < m_soft.size(); ++i) { + if (B.contains(i)) { + ws.push_back(m_weights[i]); + bs.push_back(block[i].get()); + } + } + TRACE("opt", tout << "at most bound: " << k << "\n";); + is_sat = new_bound(al, ws, bs, k); + if (is_sat != l_true) { + return is_sat; + } + m_lower += k; + SASSERT(m_lower > old_lower); + TRACE("opt", tout << "new bound: " << m_lower << "\n";); + expr_ref B_le_k(m), B_ge_k(m); + B_le_k = u.mk_le(ws.size(), ws.c_ptr(), bs.c_ptr(), k); + B_ge_k = u.mk_ge(ws.size(), ws.c_ptr(), bs.c_ptr(), k); + s().assert_expr(B_ge_k); + al.push_back(B_ge_k); + IF_VERBOSE(1, verbose_stream() << "(opt.wpm2 [" << m_lower << ":" << m_upper << "])\n";); + IF_VERBOSE(2, verbose_stream() << "New lower bound: " << B_ge_k << "\n";); + + c = mk_fresh_bool("c"); + fml = m.mk_implies(c, B_le_k); + s().assert_expr(fml); + sc.push_back(B); + am.push_back(c); + amk.push_back(k); + } + } + + virtual void set_cancel(bool f) { + maxsmt_solver_base::set_cancel(f); + maxs->set_cancel(f); + } + + virtual void collect_statistics(statistics& st) const { + maxsmt_solver_base::collect_statistics(st); + maxs->collect_statistics(st); + } + + private: + lbool new_bound(expr_ref_vector const& al, + vector const& ws, + expr_ref_vector const& bs, + rational& k) { + pb_util u(m); + expr_ref_vector al2(m); + al2.append(al); + // w_j*b_j > k + al2.push_back(m.mk_not(u.mk_le(ws.size(), ws.c_ptr(), bs.c_ptr(), k))); + return bound(al2, ws, bs, k); + } + + // + // minimal k, such that al & w_j*b_j >= k is sat + // minimal k, such that al & 3*x + 4*y >= k is sat + // minimal k, such that al & (or (not x) w3) & (or (not y) w4) + // + lbool bound(expr_ref_vector const& al, + vector const& ws, + expr_ref_vector const& bs, + rational& k) { + expr_ref_vector nbs(m); + opt_solver::scoped_push _sc(maxs->s()); + for (unsigned i = 0; i < al.size(); ++i) { + maxs->add_hard(al[i]); + } + for (unsigned i = 0; i < bs.size(); ++i) { + nbs.push_back(mk_not(bs[i])); + } + TRACE("opt", + maxs->s().display(tout); + tout << "\n"; + for (unsigned i = 0; i < bs.size(); ++i) { + tout << mk_pp(bs[i], m) << " " << ws[i] << "\n"; + }); + maxs->init_soft(ws, nbs); + lbool is_sat = maxs->s().check_sat(0,0); + if (is_sat == l_true) { + maxs->set_model(); + is_sat = (*maxs)(); + } + SASSERT(maxs->get_lower() > k); + k = maxs->get_lower(); + return is_sat; + } + }; + + maxsmt_solver_base* opt::mk_wpm2(ast_manager& m, opt_solver* s, params_ref& p, + vector const& ws, expr_ref_vector const& soft) { + + ref s0 = alloc(opt_solver, m, p, symbol()); + // initialize model. + s0->check_sat(0,0); + maxsmt_solver_base* s2 = mk_pbmax(m, s0.get(), p, ws, soft); + return alloc(wpm2, s, m, s2, p, ws, soft); + } + +} diff --git a/src/opt/wpm2.h b/src/opt/wpm2.h new file mode 100644 index 000000000..efaddc602 --- /dev/null +++ b/src/opt/wpm2.h @@ -0,0 +1,29 @@ +/*++ +Copyright (c) 2014 Microsoft Corporation + +Module Name: + + wpm2.h + +Abstract: + + Wpm2 based MaxSAT. + +Author: + + Nikolaj Bjorner (nbjorner) 2014-4-17 + +Notes: + +--*/ + +#ifndef _WPM2_H_ +#define _WPM2_H_ + +#include "maxsmt.h" + +namespace opt { + maxsmt_solver_base* mk_wpm2(ast_manager& m, opt_solver* s, params_ref& p, + vector const& ws, expr_ref_vector const& soft); +} +#endif diff --git a/src/smt/theory_wmaxsat.cpp b/src/smt/theory_wmaxsat.cpp index 2c33d28da..353ff38a3 100644 --- a/src/smt/theory_wmaxsat.cpp +++ b/src/smt/theory_wmaxsat.cpp @@ -216,7 +216,6 @@ expr_ref theory_wmaxsat::mk_block() { scoped_mpq q(mgr); mgr.set(q, m_zmin_cost, m_den.to_mpq().numerator()); rational rw = rational(q); - IF_VERBOSE(1, verbose_stream() << "(wmaxsat with upper bound: " << rw << ")\n";); m_zmin_cost = weight; m_found_optimal = true; m_cost_save.reset();