diff --git a/src/opt/opt_solver.cpp b/src/opt/opt_solver.cpp index ef11b8b91..cd4e167dc 100644 --- a/src/opt/opt_solver.cpp +++ b/src/opt/opt_solver.cpp @@ -41,7 +41,7 @@ namespace opt { m_context(mgr, m_params), m(mgr), m_dump_benchmarks(false), - m_fm(m) { + m_fm(alloc(filter_model_converter, m)) { m_logic = l; if (m_logic != symbol::null) m_context.set_logic(m_logic); @@ -231,20 +231,20 @@ namespace opt { if (typeid(smt::theory_inf_arith) == typeid(opt)) { smt::theory_inf_arith& th = dynamic_cast(opt); - return expr_ref(th.mk_ge(m_fm, v, val), m); + return expr_ref(th.mk_ge(mc(), v, val), m); } if (typeid(smt::theory_mi_arith) == typeid(opt)) { smt::theory_mi_arith& th = dynamic_cast(opt); SASSERT(val.is_finite()); - return expr_ref(th.mk_ge(m_fm, v, val.get_numeral()), m); + return expr_ref(th.mk_ge(mc(), v, val.get_numeral()), m); } if (typeid(smt::theory_i_arith) == typeid(opt)) { SASSERT(val.is_finite()); SASSERT(val.get_infinitesimal().is_zero()); smt::theory_i_arith& th = dynamic_cast(opt); - return expr_ref(th.mk_ge(m_fm, v, val.get_rational()), m); + return expr_ref(th.mk_ge(mc(), v, val.get_rational()), m); } // difference logic? diff --git a/src/opt/opt_solver.h b/src/opt/opt_solver.h index 74d75a806..5ac794ab4 100644 --- a/src/opt/opt_solver.h +++ b/src/opt/opt_solver.h @@ -50,7 +50,7 @@ namespace opt { bool m_dump_benchmarks; static unsigned m_dump_count; statistics m_stats; - filter_model_converter m_fm; + ref m_fm; public: opt_solver(ast_manager & m, params_ref const & p, symbol const & l); virtual ~opt_solver(); @@ -82,7 +82,8 @@ namespace opt { inf_eps const & get_objective_value(unsigned obj_index); expr_ref mk_ge(unsigned obj_index, inf_eps const& val); - filter_model_converter& mc() { return m_fm; } + filter_model_converter& mc() { return *(m_fm.get()); } + ref& mc_ref() { return m_fm; } static opt_solver& to_opt(solver& s); bool dump_benchmarks(); diff --git a/src/opt/weighted_maxsat.cpp b/src/opt/weighted_maxsat.cpp index ebe332ad3..5cf69b16b 100644 --- a/src/opt/weighted_maxsat.cpp +++ b/src/opt/weighted_maxsat.cpp @@ -21,6 +21,7 @@ Notes: #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" @@ -36,440 +37,31 @@ Notes: #include "bvsls_opt_engine.h" #include "nnf_tactic.h" -namespace smt { - - class theory_weighted_maxsat : public theory { - struct stats { - unsigned m_num_blocks; - void reset() { memset(this, 0, sizeof(*this)); } - stats() { reset(); } - }; - - opt::opt_solver& s; - mutable unsynch_mpz_manager m_mpz; - app_ref_vector m_vars; // Auxiliary variables per soft clause - expr_ref_vector m_fmls; // Formulas per soft clause - app_ref m_min_cost_atom; // atom tracking modified lower bound - app_ref_vector m_min_cost_atoms; - bool_var m_min_cost_bv; // max cost Boolean variable - vector m_rweights; // weights of theory variables. - scoped_mpz_vector m_zweights; - scoped_mpz_vector m_old_values; - svector m_costs; // set of asserted theory variables - svector m_cost_save; // set of asserted theory variables - rational m_rcost; // current sum of asserted costs - rational m_rmin_cost; // current maximal cost assignment. - scoped_mpz m_zcost; // current sum of asserted costs - scoped_mpz m_zmin_cost; // current maximal cost assignment. - bool m_found_optimal; - u_map m_bool2var; // bool_var -> theory_var - svector m_var2bool; // theory_var -> bool_var - bool m_propagate; - bool m_normalize; - rational m_den; // lcm of denominators for rational weights. - svector m_assigned; - stats m_stats; - - public: - theory_weighted_maxsat(ast_manager& m, opt::opt_solver& s): - theory(m.mk_family_id("weighted_maxsat")), - s(s), - m_vars(m), - m_fmls(m), - m_min_cost_atom(m), - m_min_cost_atoms(m), - m_zweights(m_mpz), - m_old_values(m_mpz), - m_zcost(m_mpz), - m_zmin_cost(m_mpz), - m_found_optimal(false), - m_propagate(false), - m_normalize(false) - {} - - virtual ~theory_weighted_maxsat() { - m_old_values.reset(); - } - - /** - \brief return the complement of variables that are currently assigned. - */ - void get_assignment(svector& result) { - result.reset(); - - if (!m_found_optimal) { - for (unsigned i = 0; i < m_vars.size(); ++i) { - result.push_back(false); - } - } - else { - std::sort(m_cost_save.begin(), m_cost_save.end()); - for (unsigned i = 0, j = 0; i < m_vars.size(); ++i) { - if (j < m_cost_save.size() && m_cost_save[j] == i) { - result.push_back(false); - ++j; - } - else { - result.push_back(true); - } - } - } - TRACE("opt", - tout << "cost save: "; - for (unsigned i = 0; i < m_cost_save.size(); ++i) { - tout << m_cost_save[i] << " "; - } - tout << "\nvars: "; - for (unsigned i = 0; i < m_vars.size(); ++i) { - tout << mk_pp(m_vars[i].get(), get_manager()) << " "; - } - tout << "\nassignment: "; - for (unsigned i = 0; i < result.size(); ++i) { - tout << result[i] << " "; - } - tout << "\n";); - - } - - virtual void init_search_eh() { - m_propagate = true; - } - - bool_var assert_weighted(expr* fml, rational const& w) { - context & ctx = get_context(); - ast_manager& m = get_manager(); - app_ref var(m), wfml(m); - var = m.mk_fresh_const("w", m.mk_bool_sort()); - s.mc().insert(var->get_decl()); - wfml = m.mk_or(var, fml); - ctx.assert_expr(wfml); - m_rweights.push_back(w); - m_vars.push_back(var); - m_fmls.push_back(fml); - m_assigned.push_back(false); - m_rmin_cost += w; - m_normalize = true; - return register_var(var, true); - } - - bool_var register_var(app* var, bool attach) { - context & ctx = get_context(); - ast_manager& m = get_manager(); - bool_var bv; - SASSERT(!ctx.e_internalized(var)); - enode* x = ctx.mk_enode(var, false, true, true); - if (ctx.b_internalized(var)) { - bv = ctx.get_bool_var(var); - } - else { - bv = ctx.mk_bool_var(var); - } - ctx.set_enode_flag(bv, true); - if (attach) { - ctx.set_var_theory(bv, get_id()); - theory_var v = mk_var(x); - ctx.attach_th_var(x, this, v); - m_bool2var.insert(bv, v); - SASSERT(v == m_var2bool.size()); - m_var2bool.push_back(bv); - SASSERT(ctx.bool_var2enode(bv)); - } - return bv; - } - - rational const& get_min_cost() { - unsynch_mpq_manager mgr; - scoped_mpq q(mgr); - mgr.set(q, m_zmin_cost, m_den.to_mpq().numerator()); - m_rmin_cost = rational(q); - return m_rmin_cost; - } - - expr* set_min_cost(rational const& c) { - m_normalize = true; - ast_manager& m = get_manager(); - std::ostringstream strm; - strm << "cost <= " << c; - m_rmin_cost = c; - m_min_cost_atom = m.mk_fresh_const(strm.str().c_str(), m.mk_bool_sort()); - m_min_cost_atoms.push_back(m_min_cost_atom); - s.mc().insert(m_min_cost_atom->get_decl()); - - m_min_cost_bv = register_var(m_min_cost_atom, false); - - return m_min_cost_atom; - } - - // scoped_mpz leaks. - - class numeral_trail : public trail { - typedef scoped_mpz T; - T & m_value; - scoped_mpz_vector& m_old_values; - - // numeral_trail(numeral_trail const& nt); - - public: - numeral_trail(T & value, scoped_mpz_vector& old): - m_value(value), - m_old_values(old) { - old.push_back(value); - } - - virtual ~numeral_trail() { - } - - virtual void undo(context & ctx) { - m_value = m_old_values.back(); - m_old_values.shrink(m_old_values.size() - 1); - } - }; - - virtual void assign_eh(bool_var v, bool is_true) { - TRACE("opt", tout << "Assign " << mk_pp(m_vars[m_bool2var[v]].get(), get_manager()) << " " << is_true << "\n";); - if (is_true) { - if (m_normalize) normalize(); - context& ctx = get_context(); - theory_var tv = m_bool2var[v]; - if (m_assigned[tv]) return; - scoped_mpz w(m_mpz); - w = m_zweights[tv]; - ctx.push_trail(numeral_trail(m_zcost, m_old_values)); - ctx.push_trail(push_back_vector >(m_costs)); - ctx.push_trail(value_trail(m_assigned[tv])); - m_zcost += w; - m_costs.push_back(tv); - m_assigned[tv] = true; - if (m_zcost > m_zmin_cost) { - block(); - } - } - } - - virtual final_check_status final_check_eh() { - if (m_normalize) normalize(); - return FC_DONE; - } - - virtual bool use_diseqs() const { - return false; - } - - virtual bool build_models() const { - return false; - } - - void reset() { - reset_eh(); - } - - virtual void reset_eh() { - theory::reset_eh(); - m_vars.reset(); - m_fmls.reset(); - m_rweights.reset(); - m_costs.reset(); - m_rmin_cost.reset(); - m_rcost.reset(); - m_zweights.reset(); - m_zcost.reset(); - m_zmin_cost.reset(); - m_cost_save.reset(); - m_bool2var.reset(); - m_var2bool.reset(); - m_min_cost_atom = 0; - m_min_cost_atoms.reset(); - m_propagate = false; - m_found_optimal = false; - m_assigned.reset(); - } - - virtual theory * mk_fresh(context * new_ctx) { return 0; } - virtual bool internalize_atom(app * atom, bool gate_ctx) { return false; } - virtual bool internalize_term(app * term) { return false; } - virtual void new_eq_eh(theory_var v1, theory_var v2) { } - virtual void new_diseq_eh(theory_var v1, theory_var v2) { } - - virtual void collect_statistics(::statistics & st) const { - st.update("wmaxsat num blocks", m_stats.m_num_blocks); - } - - virtual bool can_propagate() { - return m_propagate; - } - - virtual void propagate() { - context& ctx = get_context(); - for (unsigned i = 0; m_propagate && i < m_vars.size(); ++i) { - bool_var bv = m_var2bool[i]; - lbool asgn = ctx.get_assignment(bv); - if (asgn == l_true) { - assign_eh(bv, true); - } - } - m_propagate = false; - } - - bool is_optimal() const { - return !m_found_optimal || m_zcost < m_zmin_cost; - } - - expr_ref mk_block() { - ++m_stats.m_num_blocks; - ast_manager& m = get_manager(); - expr_ref_vector disj(m); - compare_cost compare_cost(*this); - svector costs(m_costs); - std::sort(costs.begin(), costs.end(), compare_cost); - scoped_mpz weight(m_mpz); - m_mpz.reset(weight); - for (unsigned i = 0; i < costs.size() && m_mpz.lt(weight, m_zmin_cost); ++i) { - weight += m_zweights[costs[i]]; - disj.push_back(m.mk_not(m_vars[costs[i]].get())); - } - if (m_min_cost_atom) { - disj.push_back(m.mk_not(m_min_cost_atom)); - } - if (is_optimal()) { - unsynch_mpq_manager mgr; - 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(); - m_cost_save.append(m_costs); - TRACE("opt", - tout << "costs: "; - for (unsigned i = 0; i < m_costs.size(); ++i) { - tout << mk_pp(get_enode(m_costs[i])->get_owner(), get_manager()) << " "; - } - tout << "\n"; - get_context().display(tout); - ); - } - expr_ref result(m.mk_or(disj.size(), disj.c_ptr()), m); - TRACE("opt", - tout << result << " weight: " << weight << "\n"; - tout << "cost: " << m_zcost << " min-cost: " << m_zmin_cost << "\n";); - return result; - } - - expr_ref mk_optimal_block(svector const& ws, rational const& weight) { - ast_manager& m = get_manager(); - expr_ref_vector disj(m); - rational new_w = weight*m_den; - m_zmin_cost = new_w.to_mpq().numerator(); - m_cost_save.reset(); - for (unsigned i = 0; i < ws.size(); ++i) { - bool_var bv = ws[i]; - theory_var v = m_bool2var[bv]; - m_cost_save.push_back(v); - disj.push_back(m.mk_not(m_vars[v].get())); - } - if (m_min_cost_atom) { - disj.push_back(m.mk_not(m_min_cost_atom)); - } - expr_ref result(m.mk_or(disj.size(), disj.c_ptr()), m); - return result; - } - - - private: - - void block() { - if (m_vars.empty()) { - return; - } - ++m_stats.m_num_blocks; - ast_manager& m = get_manager(); - context& ctx = get_context(); - literal_vector lits; - compare_cost compare_cost(*this); - svector costs(m_costs); - std::sort(costs.begin(), costs.end(), compare_cost); - - scoped_mpz weight(m_mpz); - m_mpz.reset(weight); - for (unsigned i = 0; i < costs.size() && weight < m_zmin_cost; ++i) { - weight += m_zweights[costs[i]]; - lits.push_back(~literal(m_var2bool[costs[i]])); - } - if (m_min_cost_atom) { - lits.push_back(~literal(m_min_cost_bv)); - } - TRACE("opt", - tout << "block: "; - for (unsigned i = 0; i < lits.size(); ++i) { - expr_ref tmp(m); - ctx.literal2expr(lits[i], tmp); - tout << tmp << " "; - } - tout << "\n"; - ); - - ctx.mk_th_axiom(get_id(), lits.size(), lits.c_ptr()); - } - - - void normalize() { - m_den = rational::one(); - for (unsigned i = 0; i < m_rweights.size(); ++i) { - m_den = lcm(m_den, denominator(m_rweights[i])); - } - m_den = lcm(m_den, denominator(m_rmin_cost)); - SASSERT(!m_den.is_zero()); - m_zweights.reset(); - for (unsigned i = 0; i < m_rweights.size(); ++i) { - rational r = m_rweights[i]*m_den; - SASSERT(r.is_int()); - mpq const& q = r.to_mpq(); - m_zweights.push_back(q.numerator()); - } - rational r = m_rcost* m_den; - m_zcost = r.to_mpq().numerator(); - r = m_rmin_cost * m_den; - m_zmin_cost = r.to_mpq().numerator(); - m_normalize = false; - } - - class compare_cost { - theory_weighted_maxsat& m_th; - public: - compare_cost(theory_weighted_maxsat& t):m_th(t) {} - bool operator() (theory_var v, theory_var w) const { - return m_th.m_mpz.gt(m_th.m_zweights[v], m_th.m_zweights[w]); - } - }; - }; - -} - namespace opt { struct wmaxsmt::imp { ast_manager& m; - opt_solver& s; - expr_ref_vector m_soft; - svector m_assignment; - vector m_weights; - rational m_upper; - rational m_lower; - model_ref m_model; - symbol m_engine; - bool m_print_all_models; + opt_solver& s; // solver state that contains hard constraints + expr_ref_vector m_soft; // set of soft constraints + vector m_weights; // their weights + svector m_assignment; // truth assignment to soft constrsaints + rational m_upper; // current upper bound for wmaxsmt + rational m_lower; // current lower bound for wmaxsmt + model_ref m_model; // current best model is stored here. + symbol m_engine; // config + bool m_print_all_models; // config + params_ref m_params; // config volatile bool m_cancel; - params_ref m_params; - opt_solver m_solver; - ref m_sat_solver; - scoped_ptr m_imp; - smt::pb_sls m_sls; - bvsls_opt_engine m_bvsls; + opt_solver m_solver; // used for recursively calling maxsmt + scoped_ptr m_imp; // + ref m_sat_solver; // used for maxsmt over QF_BV + smt::pb_sls m_sls; // used for sls improvement of assignment + bvsls_opt_engine m_bvsls; // used for bvsls improvements of assignment imp(ast_manager& m, opt_solver& s, expr_ref_vector const& soft_constraints, vector const& weights): - m(m), s(s), m_soft(soft_constraints), m_weights(weights), m_print_all_models(false), m_cancel(false), + m(m), s(s), m_soft(soft_constraints), + m_weights(weights), m_print_all_models(false), m_cancel(false), m_solver(m, m_params, symbol("bound")), m_sls(m), m_bvsls(m, m_params) @@ -490,25 +82,25 @@ namespace opt { m_upper.reset(); } - smt::theory_weighted_maxsat* get_theory() const { + smt::theory_wmaxsat* get_theory() const { smt::context& ctx = s.get_context(); 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); + return dynamic_cast(th); } else { return 0; } } - smt::theory_weighted_maxsat* ensure_theory() { - smt::theory_weighted_maxsat* wth = get_theory(); + smt::theory_wmaxsat* ensure_theory() { + smt::theory_wmaxsat* wth = get_theory(); if (wth) { wth->reset(); } else { - wth = alloc(smt::theory_weighted_maxsat, m, s); + wth = alloc(smt::theory_wmaxsat, m, s.mc_ref()); s.get_context().register_plugin(wth); } return wth; @@ -566,6 +158,7 @@ namespace opt { m_sat_solver->set_cancel(f); } m_sls.set_cancel(f); + m_bvsls.set_cancel(f); m_cancel = f; m_solver.set_cancel(f); m_imp->m_cancel = f; @@ -581,7 +174,7 @@ namespace opt { class scoped_ensure_theory { - smt::theory_weighted_maxsat* m_wth; + smt::theory_wmaxsat* m_wth; public: scoped_ensure_theory(imp& i) { m_wth = i.ensure_theory(); @@ -589,7 +182,7 @@ namespace opt { ~scoped_ensure_theory() { m_wth->reset(); } - smt::theory_weighted_maxsat& operator()() { return *m_wth; } + smt::theory_wmaxsat& operator()() { return *m_wth; } }; lbool incremental_solve() { @@ -809,7 +402,7 @@ namespace opt { lbool conditional_solve(expr* cond) { IF_VERBOSE(1, verbose_stream() << "(wmaxsat.conditional solve)\n";); - smt::theory_weighted_maxsat& wth = *get_theory(); + smt::theory_wmaxsat& wth = *get_theory(); bool was_sat = false; lbool is_sat = l_true; while (l_true == is_sat) { @@ -1533,54 +1126,14 @@ namespace opt { }; #if 0 -// The case m_lower = 0, m_upper = 1 is not handled correctly. -// cost becomes 0 - - lbool bisection_solve() { - IF_VERBOSE(3, verbose_stream() << "(bisection solve)\n";); - 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; - expr_ref_vector bounds(m); - for (unsigned i = 0; i < m_soft.size(); ++i) { - wth().assert_weighted(m_soft[i].get(), m_weights[i]); - } - solver::scoped_push __s(s); - m_lower = rational::zero(); - m_upper = wth().get_min_cost(); - while (m_lower < m_upper && is_sat != l_undef) { - rational cost = div(m_upper + m_lower, rational(2)); - - bounds.push_back(wth().set_min_cost(cost)); - is_sat = s.check_sat_core(1,bounds.c_ptr()+bounds.size()-1); - if (m_cancel) { - is_sat = l_undef; - } - switch(is_sat) { - case l_true: { - if (wth().is_optimal()) { - updt_model(s); - } - expr_ref fml = wth().mk_block(); - s.assert_expr(fml); - m_upper = wth().get_min_cost(); - IF_VERBOSE(1, verbose_stream() << "(wmaxsat.bwmax max cost: " << m_upper << ")\n";); - break; - } - case l_false: { - m_lower = cost; - IF_VERBOSE(1, verbose_stream() << "(wmaxsat.bwmax min cost: " << m_lower << ")\n";); - break; - } - case l_undef: - break; - } - } - if (was_sat) { - is_sat = l_true; - } - return is_sat; - } + class base_solver { + opt_solver& s; + public: + base_solver(opt_solver& s): s(s) {} + virutal void assert_soft(expr* e, rational const& w) = 0; + virtual void get_model(model_ref& m) = 0; + virtual void block() = 0; + virtual lbool check() = 0; + virtual void get_core(ptr_vector& core) { UNREACHABLE(); } + }; #endif diff --git a/src/smt/theory_wmaxsat.cpp b/src/smt/theory_wmaxsat.cpp new file mode 100644 index 000000000..92b1b4626 --- /dev/null +++ b/src/smt/theory_wmaxsat.cpp @@ -0,0 +1,338 @@ +/*++ +Copyright (c) 2013 Microsoft Corporation + +Module Name: + + theory_wmaxsat.h + +Abstract: + + Weighted Max-SAT theory plugin. + +Author: + + Nikolaj Bjorner (nbjorner) 2013-11-05 + +Notes: + +--*/ + +#include +#include "smt_context.h" +#include "ast_pp.h" +#include "theory_wmaxsat.h" + +namespace smt { + +theory_wmaxsat::theory_wmaxsat(ast_manager& m, ref& mc): + theory(m.mk_family_id("weighted_maxsat")), + m_mc(mc), + m_vars(m), + m_fmls(m), + m_min_cost_atom(m), + m_min_cost_atoms(m), + m_zweights(m_mpz), + m_old_values(m_mpz), + m_zcost(m_mpz), + m_zmin_cost(m_mpz), + m_found_optimal(false), + m_propagate(false), + m_normalize(false) +{} + +theory_wmaxsat::~theory_wmaxsat() { + m_old_values.reset(); +} + +/** + \brief return the complement of variables that are currently assigned. +*/ +void theory_wmaxsat::get_assignment(svector& result) { + result.reset(); + + if (!m_found_optimal) { + for (unsigned i = 0; i < m_vars.size(); ++i) { + result.push_back(false); + } + } + else { + std::sort(m_cost_save.begin(), m_cost_save.end()); + for (unsigned i = 0, j = 0; i < m_vars.size(); ++i) { + if (j < m_cost_save.size() && m_cost_save[j] == i) { + result.push_back(false); + ++j; + } + else { + result.push_back(true); + } + } + } + TRACE("opt", + tout << "cost save: "; + for (unsigned i = 0; i < m_cost_save.size(); ++i) { + tout << m_cost_save[i] << " "; + } + tout << "\nvars: "; + for (unsigned i = 0; i < m_vars.size(); ++i) { + tout << mk_pp(m_vars[i].get(), get_manager()) << " "; + } + tout << "\nassignment: "; + for (unsigned i = 0; i < result.size(); ++i) { + tout << result[i] << " "; + } + tout << "\n";); + +} + +void theory_wmaxsat::init_search_eh() { + m_propagate = true; +} + +bool_var theory_wmaxsat::assert_weighted(expr* fml, rational const& w) { + context & ctx = get_context(); + ast_manager& m = get_manager(); + app_ref var(m), wfml(m); + var = m.mk_fresh_const("w", m.mk_bool_sort()); + m_mc->insert(var->get_decl()); + wfml = m.mk_or(var, fml); + ctx.assert_expr(wfml); + m_rweights.push_back(w); + m_vars.push_back(var); + m_fmls.push_back(fml); + m_assigned.push_back(false); + m_rmin_cost += w; + m_normalize = true; + return register_var(var, true); +} + +bool_var theory_wmaxsat::register_var(app* var, bool attach) { + context & ctx = get_context(); + ast_manager& m = get_manager(); + bool_var bv; + SASSERT(!ctx.e_internalized(var)); + enode* x = ctx.mk_enode(var, false, true, true); + if (ctx.b_internalized(var)) { + bv = ctx.get_bool_var(var); + } + else { + bv = ctx.mk_bool_var(var); + } + ctx.set_enode_flag(bv, true); + if (attach) { + ctx.set_var_theory(bv, get_id()); + theory_var v = mk_var(x); + ctx.attach_th_var(x, this, v); + m_bool2var.insert(bv, v); + SASSERT(v == m_var2bool.size()); + m_var2bool.push_back(bv); + SASSERT(ctx.bool_var2enode(bv)); + } + return bv; +} + +rational const& theory_wmaxsat::get_min_cost() { + unsynch_mpq_manager mgr; + scoped_mpq q(mgr); + mgr.set(q, m_zmin_cost, m_den.to_mpq().numerator()); + m_rmin_cost = rational(q); + return m_rmin_cost; +} + +expr* theory_wmaxsat::set_min_cost(rational const& c) { + m_normalize = true; + ast_manager& m = get_manager(); + std::ostringstream strm; + strm << "cost <= " << c; + m_rmin_cost = c; + m_min_cost_atom = m.mk_fresh_const(strm.str().c_str(), m.mk_bool_sort()); + m_min_cost_atoms.push_back(m_min_cost_atom); + m_mc->insert(m_min_cost_atom->get_decl()); + + m_min_cost_bv = register_var(m_min_cost_atom, false); + + return m_min_cost_atom; +} + +void theory_wmaxsat::assign_eh(bool_var v, bool is_true) { + TRACE("opt", tout << "Assign " << mk_pp(m_vars[m_bool2var[v]].get(), get_manager()) << " " << is_true << "\n";); + if (is_true) { + if (m_normalize) normalize(); + context& ctx = get_context(); + theory_var tv = m_bool2var[v]; + if (m_assigned[tv]) return; + scoped_mpz w(m_mpz); + w = m_zweights[tv]; + ctx.push_trail(numeral_trail(m_zcost, m_old_values)); + ctx.push_trail(push_back_vector >(m_costs)); + ctx.push_trail(value_trail(m_assigned[tv])); + m_zcost += w; + m_costs.push_back(tv); + m_assigned[tv] = true; + if (m_zcost > m_zmin_cost) { + block(); + } + } +} + +final_check_status theory_wmaxsat::final_check_eh() { + if (m_normalize) normalize(); + return FC_DONE; +} + + +void theory_wmaxsat::reset_eh() { + theory::reset_eh(); + m_vars.reset(); + m_fmls.reset(); + m_rweights.reset(); + m_costs.reset(); + m_rmin_cost.reset(); + m_rcost.reset(); + m_zweights.reset(); + m_zcost.reset(); + m_zmin_cost.reset(); + m_cost_save.reset(); + m_bool2var.reset(); + m_var2bool.reset(); + m_min_cost_atom = 0; + m_min_cost_atoms.reset(); + m_propagate = false; + m_found_optimal = false; + m_assigned.reset(); +} + + +void theory_wmaxsat::propagate() { + context& ctx = get_context(); + for (unsigned i = 0; m_propagate && i < m_vars.size(); ++i) { + bool_var bv = m_var2bool[i]; + lbool asgn = ctx.get_assignment(bv); + if (asgn == l_true) { + assign_eh(bv, true); + } + } + m_propagate = false; +} + +bool theory_wmaxsat::is_optimal() const { + return !m_found_optimal || m_zcost < m_zmin_cost; +} + +expr_ref theory_wmaxsat::mk_block() { + ++m_stats.m_num_blocks; + ast_manager& m = get_manager(); + expr_ref_vector disj(m); + compare_cost compare_cost(*this); + svector costs(m_costs); + std::sort(costs.begin(), costs.end(), compare_cost); + scoped_mpz weight(m_mpz); + m_mpz.reset(weight); + for (unsigned i = 0; i < costs.size() && m_mpz.lt(weight, m_zmin_cost); ++i) { + weight += m_zweights[costs[i]]; + disj.push_back(m.mk_not(m_vars[costs[i]].get())); + } + if (m_min_cost_atom) { + disj.push_back(m.mk_not(m_min_cost_atom)); + } + if (is_optimal()) { + unsynch_mpq_manager mgr; + 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(); + m_cost_save.append(m_costs); + TRACE("opt", + tout << "costs: "; + for (unsigned i = 0; i < m_costs.size(); ++i) { + tout << mk_pp(get_enode(m_costs[i])->get_owner(), get_manager()) << " "; + } + tout << "\n"; + get_context().display(tout); + ); + } + expr_ref result(m.mk_or(disj.size(), disj.c_ptr()), m); + TRACE("opt", + tout << result << " weight: " << weight << "\n"; + tout << "cost: " << m_zcost << " min-cost: " << m_zmin_cost << "\n";); + return result; +} + +expr_ref theory_wmaxsat::mk_optimal_block(svector const& ws, rational const& weight) { + ast_manager& m = get_manager(); + expr_ref_vector disj(m); + rational new_w = weight*m_den; + m_zmin_cost = new_w.to_mpq().numerator(); + m_cost_save.reset(); + for (unsigned i = 0; i < ws.size(); ++i) { + bool_var bv = ws[i]; + theory_var v = m_bool2var[bv]; + m_cost_save.push_back(v); + disj.push_back(m.mk_not(m_vars[v].get())); + } + if (m_min_cost_atom) { + disj.push_back(m.mk_not(m_min_cost_atom)); + } + expr_ref result(m.mk_or(disj.size(), disj.c_ptr()), m); + return result; +} + +void theory_wmaxsat::block() { + if (m_vars.empty()) { + return; + } + ++m_stats.m_num_blocks; + ast_manager& m = get_manager(); + context& ctx = get_context(); + literal_vector lits; + compare_cost compare_cost(*this); + svector costs(m_costs); + std::sort(costs.begin(), costs.end(), compare_cost); + + scoped_mpz weight(m_mpz); + m_mpz.reset(weight); + for (unsigned i = 0; i < costs.size() && weight < m_zmin_cost; ++i) { + weight += m_zweights[costs[i]]; + lits.push_back(~literal(m_var2bool[costs[i]])); + } + if (m_min_cost_atom) { + lits.push_back(~literal(m_min_cost_bv)); + } + TRACE("opt", + tout << "block: "; + for (unsigned i = 0; i < lits.size(); ++i) { + expr_ref tmp(m); + ctx.literal2expr(lits[i], tmp); + tout << tmp << " "; + } + tout << "\n"; + ); + + ctx.mk_th_axiom(get_id(), lits.size(), lits.c_ptr()); +} + + +void theory_wmaxsat::normalize() { + m_den = rational::one(); + for (unsigned i = 0; i < m_rweights.size(); ++i) { + m_den = lcm(m_den, denominator(m_rweights[i])); + } + m_den = lcm(m_den, denominator(m_rmin_cost)); + SASSERT(!m_den.is_zero()); + m_zweights.reset(); + for (unsigned i = 0; i < m_rweights.size(); ++i) { + rational r = m_rweights[i]*m_den; + SASSERT(r.is_int()); + mpq const& q = r.to_mpq(); + m_zweights.push_back(q.numerator()); + } + rational r = m_rcost* m_den; + m_zcost = r.to_mpq().numerator(); + r = m_rmin_cost * m_den; + m_zmin_cost = r.to_mpq().numerator(); + m_normalize = false; +} + +}; diff --git a/src/smt/theory_wmaxsat.h b/src/smt/theory_wmaxsat.h new file mode 100644 index 000000000..21f7fd907 --- /dev/null +++ b/src/smt/theory_wmaxsat.h @@ -0,0 +1,129 @@ +/*++ +Copyright (c) 2013 Microsoft Corporation + +Module Name: + + theory_wmaxsat.h + +Abstract: + + Weighted Max-SAT theory plugin. + +Author: + + Nikolaj Bjorner (nbjorner) 2013-11-05 + +Notes: + +--*/ + +#include "smt_theory.h" +#include "smt_clause.h" +#include "filter_model_converter.h" + +namespace smt { + class theory_wmaxsat : public theory { + struct stats { + unsigned m_num_blocks; + void reset() { memset(this, 0, sizeof(*this)); } + stats() { reset(); } + }; + ref m_mc; + mutable unsynch_mpz_manager m_mpz; + app_ref_vector m_vars; // Auxiliary variables per soft clause + expr_ref_vector m_fmls; // Formulas per soft clause + app_ref m_min_cost_atom; // atom tracking modified lower bound + app_ref_vector m_min_cost_atoms; + bool_var m_min_cost_bv; // max cost Boolean variable + vector m_rweights; // weights of theory variables. + scoped_mpz_vector m_zweights; + scoped_mpz_vector m_old_values; + svector m_costs; // set of asserted theory variables + svector m_cost_save; // set of asserted theory variables + rational m_rcost; // current sum of asserted costs + rational m_rmin_cost; // current maximal cost assignment. + scoped_mpz m_zcost; // current sum of asserted costs + scoped_mpz m_zmin_cost; // current maximal cost assignment. + bool m_found_optimal; + u_map m_bool2var; // bool_var -> theory_var + svector m_var2bool; // theory_var -> bool_var + bool m_propagate; + bool m_normalize; + rational m_den; // lcm of denominators for rational weights. + svector m_assigned; + stats m_stats; + public: + theory_wmaxsat(ast_manager& m, ref& mc); + virtual ~theory_wmaxsat(); + void get_assignment(svector& result); + virtual void init_search_eh(); + bool_var assert_weighted(expr* fml, rational const& w); + bool_var register_var(app* var, bool attach); + rational const& get_min_cost(); + expr* set_min_cost(rational const& c); + class numeral_trail : public trail { + typedef scoped_mpz T; + T & m_value; + scoped_mpz_vector& m_old_values; + public: + numeral_trail(T & value, scoped_mpz_vector& old): + m_value(value), + m_old_values(old) { + old.push_back(value); + } + + virtual ~numeral_trail() { + } + + virtual void undo(context & ctx) { + m_value = m_old_values.back(); + m_old_values.shrink(m_old_values.size() - 1); + } + }; + virtual void assign_eh(bool_var v, bool is_true); + virtual final_check_status final_check_eh(); + virtual bool use_diseqs() const { + return false; + } + virtual bool build_models() const { + return false; + } + void reset() { + reset_eh(); + } + virtual void reset_eh(); + virtual theory * mk_fresh(context * new_ctx) { return 0; } + virtual bool internalize_atom(app * atom, bool gate_ctx) { return false; } + virtual bool internalize_term(app * term) { return false; } + virtual void new_eq_eh(theory_var v1, theory_var v2) { } + virtual void new_diseq_eh(theory_var v1, theory_var v2) { } + + virtual void collect_statistics(::statistics & st) const { + st.update("wmaxsat num blocks", m_stats.m_num_blocks); + } + virtual bool can_propagate() { + return m_propagate; + } + + virtual void propagate(); + bool is_optimal() const; + expr_ref mk_block(); + + expr_ref mk_optimal_block(svector const& ws, rational const& weight); + private: + + void block(); + void normalize(); + + class compare_cost { + theory_wmaxsat& m_th; + public: + compare_cost(theory_wmaxsat& t):m_th(t) {} + bool operator() (theory_var v, theory_var w) const { + return m_th.m_mpz.gt(m_th.m_zweights[v], m_th.m_zweights[w]); + } + }; + + + }; +};