From 00f45579cc222a06b3e4a8a94ef12e0ef9dfeb09 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 14 Apr 2014 16:24:23 -0700 Subject: [PATCH] refactor weighted maxsmt Signed-off-by: Nikolaj Bjorner --- src/opt/maxsmt.cpp | 14 +- src/opt/maxsmt.h | 4 +- src/opt/opt_context.cpp | 4 +- src/opt/weighted_maxsat.cpp | 1709 +++++++++++++++++++---------------- src/opt/weighted_maxsat.h | 5 +- 5 files changed, 940 insertions(+), 796 deletions(-) diff --git a/src/opt/maxsmt.cpp b/src/opt/maxsmt.cpp index cc926484c..d2f308488 100644 --- a/src/opt/maxsmt.cpp +++ b/src/opt/maxsmt.cpp @@ -27,29 +27,29 @@ Notes: namespace opt { - lbool maxsmt::operator()(opt_solver& s) { + lbool maxsmt::operator()(opt_solver* s) { lbool is_sat; m_msolver = 0; - m_s = &s; + m_s = s; IF_VERBOSE(1, verbose_stream() << "(maxsmt)\n";); if (m_soft_constraints.empty()) { TRACE("opt", tout << "no constraints\n";); m_msolver = 0; - is_sat = s.check_sat(0, 0); + is_sat = m_s->check_sat(0, 0); } else if (is_maxsat_problem(m_weights)) { if (m_maxsat_engine == symbol("core_maxsat")) { - m_msolver = alloc(core_maxsat, m, s, m_soft_constraints); + m_msolver = alloc(core_maxsat, m, *m_s, m_soft_constraints); } else if (m_maxsat_engine == symbol("weighted_maxsat")) { - m_msolver = alloc(wmaxsmt, m, opt_solver::to_opt(s), m_soft_constraints, m_weights); + m_msolver = alloc(wmaxsmt, m, m_s.get(), m_soft_constraints, m_weights); } else { - m_msolver = alloc(fu_malik, m, s, m_soft_constraints); + m_msolver = alloc(fu_malik, m, *m_s, m_soft_constraints); } } else { - m_msolver = alloc(wmaxsmt, m, opt_solver::to_opt(s), m_soft_constraints, m_weights); + m_msolver = alloc(wmaxsmt, m, m_s.get(), m_soft_constraints, m_weights); } if (m_msolver) { diff --git a/src/opt/maxsmt.h b/src/opt/maxsmt.h index 9eb1f66f5..ffcfcab63 100644 --- a/src/opt/maxsmt.h +++ b/src/opt/maxsmt.h @@ -44,7 +44,7 @@ namespace opt { class maxsmt { ast_manager& m; - opt_solver* m_s; + ref m_s; volatile bool m_cancel; expr_ref_vector m_soft_constraints; expr_ref_vector m_answer; @@ -58,7 +58,7 @@ namespace opt { public: maxsmt(ast_manager& m): m(m), m_s(0), m_cancel(false), m_soft_constraints(m), m_answer(m) {} - lbool operator()(opt_solver& s); + lbool operator()(opt_solver* s); void set_cancel(bool f); diff --git a/src/opt/opt_context.cpp b/src/opt/opt_context.cpp index 45b828b5f..36775aab3 100644 --- a/src/opt/opt_context.cpp +++ b/src/opt/opt_context.cpp @@ -194,7 +194,7 @@ namespace opt { lbool context::execute_maxsat(symbol const& id, bool committed) { model_ref tmp; maxsmt& ms = *m_maxsmts.find(id); - lbool result = ms(get_solver()); + lbool result = ms(m_solver.get()); if (result == l_true && committed) ms.commit_assignment(); if (result != l_false && (ms.get_model(tmp), tmp.get())) ms.get_model(m_model); return result; @@ -381,7 +381,7 @@ namespace opt { params_ref lia_p; lia_p.set_bool("compile_equality", optp.pb_compile_equality()); tac3->updt_params(lia_p); - m_simplify = and_then(tac0.get(), tac2.get(), tac3.get(), mk_nnf_tactic(m)); + m_simplify = and_then(tac0.get(), tac2.get(), tac3.get()); } else { m_simplify = tac0.get(); diff --git a/src/opt/weighted_maxsat.cpp b/src/opt/weighted_maxsat.cpp index 2d2d67320..2fe441f53 100644 --- a/src/opt/weighted_maxsat.cpp +++ b/src/opt/weighted_maxsat.cpp @@ -39,37 +39,48 @@ Notes: namespace opt { - struct wmaxsmt::imp { + + // --------------------------------------------- + // base class with common utilities used + // by maxsmt solvers + // + class maxsmt_solver_base : public maxsmt_solver { + protected: + ref m_s; ast_manager& m; - 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; - 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 - + expr_ref_vector m_soft; + vector m_weights; + rational m_lower; + rational m_upper; + model_ref m_model; + ref m_mc; // model converter to remove fresh variables + svector m_assignment; // truth assignment to soft constraints + params_ref m_params; // config + public: + maxsmt_solver_base(solver* s, ast_manager& m): + m_s(s), m(m), m_cancel(false), m_soft(m) {} - 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_solver(m, m_params, symbol("bound")), - m_sls(m), - m_bvsls(m, m_params) - { - m_assignment.resize(m_soft.size(), false); + virtual ~maxsmt_solver_base() {} + virtual rational get_lower() const { return m_lower; } + virtual rational get_upper() const { return m_upper; } + virtual bool get_assignment(unsigned index) const { return m_assignment[index]; } + virtual void set_cancel(bool f) { m_cancel = f; } + virtual void collect_statistics(statistics& st) const { } + virtual void get_model(model_ref& mdl) { mdl = m_model.get(); } + virtual void updt_params(params_ref& p) { + m_params = p; + s().updt_params(p); + } + void add_soft( + vector const& weights, + expr_ref_vector const& soft) { + m_weights.append(weights); + m_soft.append(soft); } - - ~imp() {} + void add_hard(expr* e){ s().assert_expr(e); } + solver& s() { return *m_s; } + void set_converter(filter_model_converter* mc) { m_mc = mc; } void re_init(expr_ref_vector const& soft, vector const& weights) { m_soft.reset(); @@ -81,474 +92,6 @@ namespace opt { m_lower.reset(); m_upper.reset(); } - - 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); - } - else { - return 0; - } - } - - smt::theory_wmaxsat* ensure_theory() { - smt::theory_wmaxsat* wth = get_theory(); - if (wth) { - wth->reset(); - } - else { - wth = alloc(smt::theory_wmaxsat, m, s.mc_ref()); - s.get_context().register_plugin(wth); - } - return wth; - } - - /** - Takes solver with hard constraints added. - Returns a maximal satisfying subset of weighted soft_constraints - that are still consistent with the solver state. - */ - - lbool operator()() { - if (m_engine == symbol("iwmax")) { - return iterative_solve(); - } - if (m_engine == symbol("pwmax")) { - return pb_solve(); - } - if (m_engine == symbol("bvmax")) { - return pb2sat_solve(); - } - if (m_engine == symbol("wpm2")) { - return wpm2_solve(); - } - if (m_engine == symbol("wpm2b")) { - return wpm2b_solve(); - } - if (m_engine == symbol("sls")) { - return sls_solve(); - } - if (m_engine == symbol("bvsls")) { - return bvsls_solve(); - } - if (m_engine == symbol::null || m_engine == symbol("wmax")) { - return incremental_solve(); - } - IF_VERBOSE(0, verbose_stream() << "(unknown engine " << m_engine << " using default 'wmax')\n";); - return incremental_solve(); - } - - rational get_lower() const { - return m_lower; - } - - rational get_upper() const { - return m_upper; - } - - void get_model(model_ref& mdl) { - mdl = m_model.get(); - } - - void set_cancel(bool f) { - if (m_sat_solver) { - 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; - m_imp->m_solver.set_cancel(f); - } - - void collect_statistics(statistics& st) const { - m_solver.collect_statistics(st); - if (m_sat_solver) { - m_sat_solver->collect_statistics(st); - } - } - - - class scoped_ensure_theory { - smt::theory_wmaxsat* m_wth; - public: - scoped_ensure_theory(imp& i) { - m_wth = i.ensure_theory(); - } - ~scoped_ensure_theory() { - m_wth->reset(); - } - smt::theory_wmaxsat& operator()() { return *m_wth; } - }; - - lbool incremental_solve() { - IF_VERBOSE(3, verbose_stream() << "(incremental 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; - 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) { - is_sat = s.check_sat_core(0,0); - if (m_cancel) { - is_sat = l_undef; - } - if (is_sat == l_true) { - if (wth().is_optimal()) { - m_upper = wth().get_min_cost(); - updt_model(s); - } - expr_ref fml = wth().mk_block(); - s.assert_expr(fml); - was_sat = true; - } - IF_VERBOSE(3, verbose_stream() << "(incremental bound)\n";); - } - 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; - } - - lbool sls_solve() { - IF_VERBOSE(1, verbose_stream() << "(sls solve)\n";); - for (unsigned i = 0; i < s.get_num_assertions(); ++i) { - m_sls.add(s.get_assertion(i)); - } - pb_util u(m); - expr_ref fml(m), val(m); - app_ref b(m); - expr_ref_vector nsoft(m); - m_lower = m_upper = rational::zero(); - solver::scoped_push __s(s); - for (unsigned i = 0; i < m_soft.size(); ++i) { - m_upper += m_weights[i]; - b = m.mk_fresh_const("b", m.mk_bool_sort()); - s.mc().insert(b->get_decl()); - fml = m.mk_or(m_soft[i].get(), b); - s.assert_expr(fml); - nsoft.push_back(b); - m_sls.add(m_soft[i].get(), m_weights[i]); - } - lbool is_sat = l_true; - bool was_sat = false; - while (l_true == is_sat) { - is_sat = s.check_sat_core(0,0); - if (m_cancel) { - is_sat = l_undef; - } - if (is_sat == l_true) { - updt_model(s); - m_sls.set_model(m_model); - m_upper = rational::zero(); - if (l_true == m_sls()) { - m_sls.get_model(m_model); - for (unsigned i = 0; i < m_soft.size(); ++i) { - m_assignment[i] = m_sls.soft_holds(i); - } - } - else { - for (unsigned i = 0; i < m_soft.size(); ++i) { - VERIFY(m_model->eval(nsoft[i].get(), val)); - m_assignment[i] = !m.is_true(val); - } - } - for (unsigned i = 0; i < m_soft.size(); ++i) { - if (!m_assignment[i]) { - m_upper += m_weights[i]; - } - } - IF_VERBOSE(1, verbose_stream() << "(sls.pb with upper bound: " << m_upper << ")\n";); - fml = m.mk_not(u.mk_ge(nsoft.size(), m_weights.c_ptr(), nsoft.c_ptr(), m_upper)); - s.assert_expr(fml); - was_sat = true; - } - } - if (is_sat == l_false && was_sat) { - is_sat = l_true; - m_lower = m_upper; - } - return is_sat; - } - - lbool bvsls_solve() { - IF_VERBOSE(1, verbose_stream() << "(bvsls solve)\n";); - - bv_util bv(m); - pb::card_pb_rewriter pb_rewriter(m); - expr_ref tmp(m), objective(m), zero(m); - expr_ref_vector es(m); - - goal_ref g(alloc(goal, m, true, false)); - for (unsigned i = 0; i < s.get_num_assertions(); ++i) { - pb_rewriter(s.get_assertion(i), tmp); - g->assert_expr(tmp); - } - tactic_ref simplify = mk_nnf_tactic(m); - proof_converter_ref pc; - expr_dependency_ref core(m); - goal_ref_buffer result; - model_converter_ref model_converter; - (*simplify)(g, result, model_converter, pc, core); - SASSERT(result.size() == 1); - goal* r = result[0]; - for (unsigned i = 0; i < r->size(); ++i) { - m_bvsls.assert_expr(r->form(i)); - } - - m_lower = m_upper = rational::zero(); - - for (unsigned i = 0; i < m_soft.size(); ++i) { - m_upper += m_weights[i]; - } - rational num = numerator(m_upper); - rational den = denominator(m_upper); - rational maxval = num*den; - unsigned bv_size = maxval.get_num_bits(); - zero = bv.mk_numeral(rational(0), bv_size); - for (unsigned i = 0; i < m_soft.size(); ++i) { - pb_rewriter(m_soft[i].get(), tmp); - es.push_back(m.mk_ite(tmp, bv.mk_numeral(den*m_weights[i], bv_size), zero)); - } - if (es.empty()) { - objective = bv.mk_numeral(0, bv_size); - } - else { - objective = es[0].get(); - for (unsigned i = 1; i < es.size(); ++i) { - objective = bv.mk_bv_add(objective, es[i].get()); - } - } - lbool is_sat = s.check_sat_core(0, 0); - if (is_sat == l_true) { - updt_model(s); - // TBD: can we set an initial model on m_bvsls? - // CMW: Yes, see next line. - bvsls_opt_engine::optimization_result res = m_bvsls.optimize(objective, m_model, true); - switch (res.is_sat) { - case l_true: { - unsigned bv_size = 0; - m_bvsls.get_model(m_model); - VERIFY(bv.is_numeral(res.optimum, m_lower, bv_size)); - break; - } - case l_false: - case l_undef: - break; - } - return res.is_sat; - } - else - return is_sat; - - } - - /** - Iteratively increase cost until there is an assignment during - final_check that satisfies min_cost. - - Takes: log (n / log(n)) iterations - */ - - lbool iterative_solve() { - scoped_ensure_theory wth(*this); - solver::scoped_push _s(s); - for (unsigned i = 0; i < m_soft.size(); ++i) { - wth().assert_weighted(m_soft[i].get(), m_weights[i]); - } - solver::scoped_push __s(s); - rational cost = wth().get_min_cost(); - rational log_cost(1), tmp(1); - while (tmp < cost) { - ++log_cost; - tmp *= rational(2); - } - expr_ref_vector bounds(m); - expr_ref bound(m); - lbool result = l_false; - unsigned nsc = 0; - m_upper = cost; - while (result == l_false) { - bound = wth().set_min_cost(log_cost); - s.push_core(); - ++nsc; - IF_VERBOSE(1, verbose_stream() << "(wmaxsat.iwmax min cost: " << log_cost << ")\n";); - TRACE("opt", tout << "cost: " << log_cost << " " << bound << "\n";); - bounds.push_back(bound); - result = conditional_solve(bound); - if (result == l_false) { - m_lower = log_cost; - } - if (log_cost > cost) { - break; - } - log_cost *= rational(2); - if (m_cancel) { - result = l_undef; - } - } - s.pop_core(nsc); - return result; - } - - lbool conditional_solve(expr* cond) { - IF_VERBOSE(1, verbose_stream() << "(wmaxsat.conditional solve)\n";); - smt::theory_wmaxsat& wth = *get_theory(); - bool was_sat = false; - lbool is_sat = l_true; - while (l_true == is_sat) { - is_sat = s.check_sat_core(1,&cond); - if (m_cancel) { - is_sat = l_undef; - } - if (is_sat == l_true) { - if (wth.is_optimal()) { - s.get_model(m_model); - was_sat = true; - } - expr_ref fml = wth.mk_block(); - s.assert_expr(fml); - } - } - if (was_sat) { - wth.get_assignment(m_assignment); - } - if (is_sat == l_false && was_sat) { - is_sat = l_true; - } - if (is_sat == l_true) { - m_lower = m_upper = wth.get_min_cost(); - } - TRACE("opt", tout << "min cost: " << m_upper << "\n";); - return is_sat; - } - - - // convert bounds constraint into pseudo-Boolean - lbool pb_solve() { - pb_util u(m); - expr_ref fml(m), val(m); - app_ref b(m); - expr_ref_vector nsoft(m); - m_lower = m_upper = rational::zero(); - solver::scoped_push __s(s); - for (unsigned i = 0; i < m_soft.size(); ++i) { - m_upper += m_weights[i]; - b = m.mk_fresh_const("b", m.mk_bool_sort()); - s.mc().insert(b->get_decl()); - fml = m.mk_or(m_soft[i].get(), b); - s.assert_expr(fml); - nsoft.push_back(b); - } - lbool is_sat = l_true; - bool was_sat = false; - fml = m.mk_true(); - while (l_true == is_sat) { - solver::scoped_push _s(s); - s.assert_expr(fml); - is_sat = s.check_sat_core(0,0); - if (m_cancel) { - is_sat = l_undef; - } - if (is_sat == l_true) { - s.get_model(m_model); - m_upper = rational::zero(); - 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() << "(wmaxsat.pb with upper bound: " << m_upper << ")\n";); - fml = m.mk_not(u.mk_ge(nsoft.size(), m_weights.c_ptr(), nsoft.c_ptr(), m_upper)); - was_sat = true; - } - } - if (is_sat == l_false && was_sat) { - is_sat = l_true; - m_lower = m_upper; - } - return is_sat; - } - - // - // convert bounds constraint into pseudo-Boolean, - // then treat pseudo-Booleans as bit-vectors and - // sorting circuits. - // - lbool pb2sat_solve() { - IF_VERBOSE(1, verbose_stream() << "(wmaxsat.bv solve)\n";); - pb_util u(m); - expr_ref fml(m), val(m); - app_ref b(m); - expr_ref_vector nsoft(m); - m_lower = m_upper = rational::zero(); - tactic_ref pb2bv = mk_card2bv_tactic(m, m_params); - tactic_ref bv2sat = mk_qfbv_tactic(m, m_params); - tactic_ref tac = and_then(pb2bv.get(), bv2sat.get()); - m_sat_solver = mk_tactic2solver(m, tac.get(), m_params); - unsigned sz = s.get_num_assertions(); - for (unsigned i = 0; i < sz; ++i) { - m_sat_solver->assert_expr(s.get_assertion(i)); - } - for (unsigned i = 0; i < m_soft.size(); ++i) { - m_upper += m_weights[i]; - b = m.mk_fresh_const("b", m.mk_bool_sort()); - // TODO: s.mc().insert(b->get_decl()); - fml = m.mk_or(m_soft[i].get(), b); - m_sat_solver->assert_expr(fml); - nsoft.push_back(b); - } - lbool is_sat = l_true; - bool was_sat = false; - fml = m.mk_true(); - while (l_true == is_sat) { - solver::scoped_push __s(*(m_sat_solver)); - m_sat_solver->assert_expr(fml); - is_sat = m_sat_solver->check_sat(0,0); - if (m_cancel) { - is_sat = l_undef; - } - if (is_sat == l_true) { - m_sat_solver->get_model(m_model); - m_upper = rational::zero(); - 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() << "(wmaxsat.bv with upper bound: " << m_upper << ")\n";); - fml = m.mk_not(u.mk_ge(nsoft.size(), m_weights.c_ptr(), nsoft.c_ptr(), m_upper)); - was_sat = true; - } - } - if (is_sat == l_false && was_sat) { - is_sat = l_true; - m_lower = m_upper; - } - return is_sat; - } - expr* mk_not(expr* e) { if (m.is_not(e, e)) { return e; @@ -557,9 +100,206 @@ namespace opt { return m.mk_not(e); } } + }; - lbool pb_simplify_solve() { - TRACE("opt", s.display(tout); tout << "\n"; + // ------------------------------------------------------ + // Morgado, Heras, Marques-Silva 2013 + // (initial version without model-based optimizations) + // + class bcd2 : public maxsmt_solver_base { + struct wcore { + unsigned_vector m_R; + rational m_lower; + rational m_mid; + rational m_upper; + }; + public: + bcd2(solver* s, ast_manager& m): + maxsmt_solver_base(s, m) {} + + virtual ~bcd2() {} + + + virtual lbool operator()() { + expr_ref fml(m), val(m); + app_ref r(m); + vector cores; + obj_map ans2core; // answer literal to core index + lbool is_sat = l_undef; + expr_ref_vector rs(m), asms(m); + m_lower = m_upper = rational::zero(); // current upper and lower bounds + vector sigmas; // sigma_j := w_j if soft clause has not been satisfied + bool first = true; + for (unsigned i = 0; i < m_soft.size(); ++i) { + m_upper += m_weights[i]; + r = m.mk_fresh_const("r", m.mk_bool_sort()); + if (m_mc) { + m_mc->insert(r->get_decl()); + } + fml = m.mk_or(m_soft[i].get(), r); + s().assert_expr(fml); // does not get asserted in model-based mode. + rs.push_back(r); + asms.push_back(m.mk_not(r)); + sigmas.push_back(m_weights[i]); + m_assignment.push_back(false); + } + m_upper += rational(1); + solver::scoped_push _s(s()); + while (m_lower < m_upper) { + solver::scoped_push __s(s()); + if (m_cancel) { + return l_undef; + } + for (unsigned i = 0; i < cores.size(); ++i) { + assert_core(cores[i]); + NOT_IMPLEMENTED_YET(); + // need assumptions here as well. + } + is_sat = s().check_sat(asms.size(), asms.c_ptr()); + switch(is_sat) { + case l_undef: + return l_undef; + case l_true: { + s().get_model(m_model); + m_upper.reset(); + for (unsigned i = 0; i < m_soft.size(); ++i) { + VERIFY(m_model->eval(m_soft[i].get(), val)); + m_assignment[i] = m.is_true(val); + } + for (unsigned i = 0; i < cores.size(); ++i) { + wcore& c_i = cores[i]; + unsigned_vector const& R = c_i.m_R; + c_i.m_upper.reset(); + for (unsigned j = 0; j core; + uint_set subC, soft; + rational delta(0), lower(0); + wcore c_s; + s().get_unsat_core(core); + core2indices(core, ans2core, subC, soft); + for (uint_set::iterator it = subC.begin(); it != subC.end(); ++it) { + unsigned j = *it; + c_s.m_R.push_back(j); + lower += cores[j].m_lower; + rational new_delta = rational(1) + cores[j].m_upper - cores[j].m_mid; + SASSERT(new_delta.is_pos()); + if (delta.is_zero() || delta > new_delta) { + delta = new_delta; + } + } + if (soft.num_elems() == 0 && subC.num_elems() == 1) { + SASSERT(core.size() == 1); + unsigned s = *subC.begin(); + wcore& c_s = cores[s]; + c_s.m_lower = refine(c_s.m_R, c_s.m_mid); + } + else { + 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(first?0:1); + for (unsigned i = 0; i < c_s.m_R.size(); ++i) { + c_s.m_upper += sigmas[c_s.m_R[i]]; + } + c_s.m_mid = div(c_s.m_lower + c_s.m_upper, rational(2)); + subtract(cores, subC); + cores.push_back(c_s); + } + break; + } + } + m_lower = compute_lower(cores); + } + return is_sat; + } + + + private: + rational compute_lower(vector const& cores) { + rational result(0); + for (unsigned i = 0; i < cores.size(); ++i) { + result += 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)) { + if (j != i) { + cores[j] = cores[i]; + } + ++j; + } + } + cores.resize(j); + } + + void core2indices( + ptr_vector const& core, + obj_map const& ans2core, + uint_set& subC, + uint_set& soft) + { + for (unsigned i = 0; i < core.size(); ++i) { + unsigned j; + if (ans2core.find(core[i], j)) { + subC.insert(j); + } + else { + soft.insert(i); + } + } + } + + 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) { + NOT_IMPLEMENTED_YET(); + } + + void assert_core(wcore const& core) { + expr_ref fml(m); + vector ws; + ptr_vector rs; + for (unsigned j = 0; j < core.m_R.size(); ++j) { + unsigned idx = core.m_R[j]; + ws.push_back(m_weights[idx]); + rs.push_back(m_soft[idx].get()); // TBD: check + } + // TBD: fml = pb.mk_le(ws.size(), ws.c_ptr(), rs.c_ptr(), core.m_mid); + NOT_IMPLEMENTED_YET(); + s().assert_expr(fml); + } + }; + + class pb_simplify_solve : public maxsmt_solver_base { + public: + pb_simplify_solve(solver* s, ast_manager& m): + maxsmt_solver_base(s, m) {} + + virtual ~pb_simplify_solve() {} + + lbool operator()() { + 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"; } @@ -572,14 +312,14 @@ namespace opt { m_upper += m_weights[i]; nsoft.push_back(mk_not(m_soft[i].get())); } - solver::scoped_push _s1(s); + solver::scoped_push _s1(s()); lbool is_sat = l_true; bool was_sat = false; fml = m.mk_true(); while (l_true == is_sat) { - TRACE("opt", s.display(tout<<"looping\n");); - solver::scoped_push _s2(s); - s.assert_expr(fml); + TRACE("opt", s().display(tout<<"looping\n");); + solver::scoped_push _s2(s()); + s().assert_expr(fml); is_sat = simplify_and_check_sat(0,0); if (m_cancel) { is_sat = l_undef; @@ -608,132 +348,64 @@ namespace opt { return is_sat; } - // ------------------------------------------------------ - // Morgado, Heras, Marques-Silva 2013 - - struct wcore { - unsigned_vector m_R; - rational m_lower; - rational m_mid; - rational m_upper; - }; - - lbool bcd2_solve() { - return l_undef; -#if 0 - expr_ref fml(m), val(m); - app_ref r(m); - vector cores; - obj_map ans2core; // answer literal to core index - lbool is_sat = l_undef; - expr_ref_vector soft(m), rs(m); - m_lower = m_upper = rational::zero(); - bool first = true; - for (unsigned i = 0; i < m_soft.size(); ++i) { - m_upper += m_weights[i]; - r = m.mk_fresh_const("r", m.mk_bool_sort()); - s.mc().insert(r->get_decl()); - fml = m.mk_or(m_soft[i].get(), r); - s.assert_expr(fml); - rs.push_back(r); - asms.push_back(m.mk_not(r)); + private: + lbool simplify_and_check_sat(unsigned n, expr* const* assumptions) { + lbool is_sat = l_true; + tactic_ref tac1 = mk_simplify_tactic(m); + // tactic_ref tac2 = mk_pb_preprocess_tactic(m); + tactic_ref tac = tac1; // and_then(tac1.get(), tac2.get()); // TBD: make attribute for cancelation. + proof_converter_ref pc; + expr_dependency_ref core(m); + model_converter_ref mc; + goal_ref_buffer result; + goal_ref g(alloc(goal, m, true, false)); + for (unsigned i = 0; i < s().get_num_assertions(); ++i) { + g->assert_expr(s().get_assertion(i)); } - m_upper += rational(1); - solver::scoped_push _s(s); - while (m_lower < m_upper) { - solver::scoped_push _s(s); - if (m_cancel) { - return l_undef; - } - for (unsigned i = 0; i < cores.size(); ++i) { - assert_core(cores[i]); - // need assumptions here as well. - } - is_sat = check_sat(asms.size(), asms.c_ptr()); - switch(is_sat) { - case l_undef: - return l_undef; - case l_true: { - updt_model(s); - m_upper.reset(); - for (unsigned i = 0; i < cores.size(); ++i) { - wcore& c_i = 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]; - VERIFY(m_model->eval(m_soft[r_j].get(), val)); - if (m.is_false(val)) { - c_i.m_upper += m_weights[r_j]; - } - } - c_i.m_mid = div(c_i.m_lower + c_i.m_upper, rational(2)); - m_upper += c_i.m_upper; - } - first = false; - break; - } - case l_false: { - ptr_vector core; - s.get_unsat_core(core); - uint_set subC; - unsigned_vector soft; - rational delta(0); - for (unsigned i = 0; i < core.size(); ++i) { - unsigned j; - if (ans2core.find(core[i], j)) { - subC.insert(j); - rational new_delta = rational(1) + cores[j].m_upper - cores[j].m_mid; - SASSERT(new_delta.is_pos()); - if (delta.is_zero() || delta > new_delta) { - delta = new_delta; - } - } - else { - soft.push_back(i); - } - } - if (soft.empty() && subC.num_elems() == 1) { - SASSERT(core.size() == 1); - unsigned s = *subS.begin(); - wcore& c_s = cores[s]; - m_lower -= c_s.m_lower; - c_s.m_lower = refine(c_s, c_s.m_mid); - m_lower += c_s.m_lower; - } - else { - wcore c_s; - relax(subC, soft, c_s.m_R); - for (unsigned i = 0; i < subC.size(); ++i) { - - } - } - break; + for (unsigned i = 0; i < n; ++i) { + NOT_IMPLEMENTED_YET(); + // add assumption in a wrapper. + } + (*tac)(g, result, mc, pc, core); + if (result.empty()) { + is_sat = l_false; + } + else { + SASSERT(result.size() == 1); + goal_ref r = result[0]; + solver::scoped_push _s(s()); + // TBD ptr_vector asms; + for (unsigned i = 0; i < r->size(); ++i) { + // TBD collect assumptions from r + s().assert_expr(r->form(i)); } + is_sat = s().check_sat(0, 0); + if (l_true == is_sat && !m_cancel) { + s().get_model(m_model); + if (mc && m_model) (*mc)(m_model, 0); + IF_VERBOSE(2, + g->display(verbose_stream() << "goal:\n"); + r->display(verbose_stream() << "reduced:\n"); + model_smt2_pp(verbose_stream(), m, *m_model, 0);); } } return is_sat; -#endif } + }; - void assert_core(wcore const& core) { - expr_ref fml(m); - vector ws; - ptr_vector rs; - for (unsigned j = 0; j < core.m_R.size(); ++j) { - unsigned idx = core.m_R[j]; - ws.push_back(m_weights[idx]); - rs.push_back(m_soft[idx].get()); // TBD: check - } - // TBD: fml = pb.mk_le(ws.size(), ws.c_ptr(), rs.c_ptr(), core.m_mid); - s.assert_expr(fml); - } + // ------------------------------------------------------ + // AAAI 2010 + class wpm2 : public maxsmt_solver_base { + scoped_ptr maxs; + public: + wpm2(solver* s, ast_manager& m, maxsmt_solver_base* maxs): + maxsmt_solver_base(s, m), maxs(maxs) {} - // ------------------------------------------------------ - // AAAI 2010 - lbool wpm2_solve() { + virtual ~wpm2() {} + + lbool operator()() { IF_VERBOSE(1, verbose_stream() << "(wmaxsat.wpm2 solve)\n";); - solver::scoped_push _s(s); + solver::scoped_push _s(s()); pb_util u(m); app_ref fml(m), a(m), b(m), c(m); expr_ref val(m); @@ -748,21 +420,21 @@ namespace opt { m_upper += w; b = m.mk_fresh_const("b", m.mk_bool_sort()); - s.mc().insert(b->get_decl()); + m_mc->insert(b->get_decl()); block.push_back(b); expr* bb = b; a = m.mk_fresh_const("a", m.mk_bool_sort()); - s.mc().insert(a->get_decl()); + m_mc->insert(a->get_decl()); 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); + s().assert_expr(fml); c = m.mk_fresh_const("c", m.mk_bool_sort()); - s.mc().insert(c->get_decl()); + m_mc->insert(c->get_decl()); fml = m.mk_implies(c, u.mk_le(1,&w,&bb,rational(0))); - s.assert_expr(fml); + s().assert_expr(fml); sc.push_back(uint_set()); sc.back().insert(i); @@ -775,7 +447,7 @@ namespace opt { ptr_vector core; asms.append(ans); asms.append(am); - lbool is_sat = s.check_sat(asms.size(), asms.c_ptr()); + lbool is_sat = s().check_sat(asms.size(), asms.c_ptr()); TRACE("opt", tout << "\nassumptions: "; for (unsigned i = 0; i < asms.size(); ++i) { @@ -786,7 +458,7 @@ namespace opt { tout << "lower: " << m_lower << "\n"; if (is_sat == l_true) { model_ref mdl; - s.get_model(mdl); + s().get_model(mdl); model_smt2_pp(tout, m, *(mdl.get()), 0); }); @@ -795,7 +467,7 @@ namespace opt { } if (is_sat == l_true) { m_upper = m_lower; - updt_model(s); + 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";); @@ -805,7 +477,7 @@ namespace opt { if (is_sat != l_false) { return is_sat; } - s.get_unsat_core(core); + s().get_unsat_core(core); if (core.empty()) { return l_false; } @@ -863,21 +535,643 @@ namespace opt { 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); + s().assert_expr(B_ge_k); al.push_back(B_ge_k); IF_VERBOSE(1, verbose_stream() << "(wmaxsat.wpm2 lower bound: " << m_lower << ")\n";); IF_VERBOSE(2, verbose_stream() << "New lower bound: " << B_ge_k << "\n";); c = m.mk_fresh_const("c", m.mk_bool_sort()); - s.mc().insert(c->get_decl()); + m_mc->insert(c->get_decl()); fml = m.mk_implies(c, B_le_k); - s.assert_expr(fml); + s().assert_expr(fml); sc.push_back(B); am.push_back(c); amk.push_back(k); } } + 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->re_init(nbs, ws); + lbool is_sat = (*maxs)(); + SASSERT(maxs->get_lower() > k); + k = maxs->get_lower(); + return is_sat; + } + }; + + class sls : public maxsmt_solver_base { + smt::pb_sls m_sls; // used for sls improvement of assignment + public: + sls(solver* s, ast_manager& m): maxsmt_solver_base(s, m), m_sls(m) {} + virtual ~sls() {} + lbool operator()() { + IF_VERBOSE(1, verbose_stream() << "(sls solve)\n";); + for (unsigned i = 0; i < s().get_num_assertions(); ++i) { + m_sls.add(s().get_assertion(i)); + } + pb_util u(m); + expr_ref fml(m), val(m); + app_ref b(m); + expr_ref_vector nsoft(m); + m_lower = m_upper = rational::zero(); + solver::scoped_push __s(s()); + for (unsigned i = 0; i < m_soft.size(); ++i) { + m_upper += m_weights[i]; + b = m.mk_fresh_const("b", m.mk_bool_sort()); + m_mc->insert(b->get_decl()); + fml = m.mk_or(m_soft[i].get(), b); + s().assert_expr(fml); + nsoft.push_back(b); + m_sls.add(m_soft[i].get(), m_weights[i]); + } + lbool is_sat = l_true; + bool was_sat = false; + while (l_true == is_sat) { + is_sat = s().check_sat(0,0); + if (m_cancel) { + is_sat = l_undef; + } + if (is_sat == l_true) { + s().get_model(m_model); + m_sls.set_model(m_model); + m_upper = rational::zero(); + if (l_true == m_sls()) { + m_sls.get_model(m_model); + for (unsigned i = 0; i < m_soft.size(); ++i) { + m_assignment[i] = m_sls.soft_holds(i); + } + } + else { + for (unsigned i = 0; i < m_soft.size(); ++i) { + VERIFY(m_model->eval(nsoft[i].get(), val)); + m_assignment[i] = !m.is_true(val); + } + } + for (unsigned i = 0; i < m_soft.size(); ++i) { + if (!m_assignment[i]) { + m_upper += m_weights[i]; + } + } + IF_VERBOSE(1, verbose_stream() << "(sls.pb with upper bound: " << m_upper << ")\n";); + fml = m.mk_not(u.mk_ge(nsoft.size(), m_weights.c_ptr(), nsoft.c_ptr(), m_upper)); + s().assert_expr(fml); + was_sat = true; + } + } + if (is_sat == l_false && was_sat) { + is_sat = l_true; + m_lower = m_upper; + } + return is_sat; + } + + virtual void set_cancel(bool f) { + m_sls.set_cancel(f); + } + }; + + class bvsls : public maxsmt_solver_base { + bvsls_opt_engine m_bvsls; // used for bvsls improvements of assignment + public: + bvsls(solver* s, ast_manager& m): + maxsmt_solver_base(s, m), + m_bvsls(m, m_params) {} + virtual ~bvsls() {} + lbool operator()() { + IF_VERBOSE(1, verbose_stream() << "(bvsls solve)\n";); + + bv_util bv(m); + pb::card_pb_rewriter pb_rewriter(m); + expr_ref tmp(m), objective(m), zero(m); + expr_ref_vector es(m); + + goal_ref g(alloc(goal, m, true, false)); + for (unsigned i = 0; i < s().get_num_assertions(); ++i) { + pb_rewriter(s().get_assertion(i), tmp); + g->assert_expr(tmp); + } + tactic_ref simplify = mk_nnf_tactic(m); + proof_converter_ref pc; + expr_dependency_ref core(m); + goal_ref_buffer result; + model_converter_ref model_converter; + (*simplify)(g, result, model_converter, pc, core); + SASSERT(result.size() == 1); + goal* r = result[0]; + for (unsigned i = 0; i < r->size(); ++i) { + m_bvsls.assert_expr(r->form(i)); + } + + m_lower = m_upper = rational::zero(); + + for (unsigned i = 0; i < m_soft.size(); ++i) { + m_upper += m_weights[i]; + } + rational num = numerator(m_upper); + rational den = denominator(m_upper); + rational maxval = num*den; + unsigned bv_size = maxval.get_num_bits(); + zero = bv.mk_numeral(rational(0), bv_size); + for (unsigned i = 0; i < m_soft.size(); ++i) { + pb_rewriter(m_soft[i].get(), tmp); + es.push_back(m.mk_ite(tmp, bv.mk_numeral(den*m_weights[i], bv_size), zero)); + } + if (es.empty()) { + objective = bv.mk_numeral(0, bv_size); + } + else { + objective = es[0].get(); + for (unsigned i = 1; i < es.size(); ++i) { + objective = bv.mk_bv_add(objective, es[i].get()); + } + } + lbool is_sat = s().check_sat(0, 0); + if (is_sat == l_true) { + s().get_model(m_model); + bvsls_opt_engine::optimization_result res = m_bvsls.optimize(objective, m_model, true); + switch (res.is_sat) { + case l_true: { + unsigned bv_size = 0; + m_bvsls.get_model(m_model); + VERIFY(bv.is_numeral(res.optimum, m_lower, bv_size)); + break; + } + case l_false: + case l_undef: + break; + } + return res.is_sat; + } + else { + return is_sat; + } + } + virtual void set_cancel(bool f) { + m_bvsls.set_cancel(f); + } + + }; + + + class maxsmt_solver_wbase : public maxsmt_solver_base { + smt::context& ctx; + public: + maxsmt_solver_wbase(solver* s, ast_manager& m, smt::context& ctx): + maxsmt_solver_base(s, m), 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; + } + } + }; + /** + Iteratively increase cost until there is an assignment during + final_check that satisfies min_cost. + + Takes: log (n / log(n)) iterations + */ + + class iwmax : public maxsmt_solver_wbase { + public: + + iwmax(solver* s, ast_manager& m, smt::context& ctx): maxsmt_solver_wbase(s, m, ctx) {} + virtual ~iwmax() {} + + lbool operator()() { + scoped_ensure_theory wth(*this); + solver::scoped_push _s(s()); + for (unsigned i = 0; i < m_soft.size(); ++i) { + wth().assert_weighted(m_soft[i].get(), m_weights[i]); + } + solver::scoped_push __s(s()); + rational cost = wth().get_min_cost(); + rational log_cost(1), tmp(1); + while (tmp < cost) { + ++log_cost; + tmp *= rational(2); + } + expr_ref_vector bounds(m); + expr_ref bound(m); + lbool result = l_false; + unsigned nsc = 0; + m_upper = cost; + while (result == l_false) { + bound = wth().set_min_cost(log_cost); + s().push(); + ++nsc; + IF_VERBOSE(1, verbose_stream() << "(wmaxsat.iwmax min cost: " << log_cost << ")\n";); + TRACE("opt", tout << "cost: " << log_cost << " " << bound << "\n";); + bounds.push_back(bound); + result = conditional_solve(bound); + if (result == l_false) { + m_lower = log_cost; + } + if (log_cost > cost) { + break; + } + log_cost *= rational(2); + if (m_cancel) { + result = l_undef; + } + } + s().pop(nsc); + return result; + } + private: + lbool conditional_solve(expr* cond) { + IF_VERBOSE(1, verbose_stream() << "(wmaxsat.conditional solve)\n";); + smt::theory_wmaxsat& wth = *get_theory(); + bool was_sat = false; + lbool is_sat = l_true; + while (l_true == is_sat) { + is_sat = s().check_sat(1,&cond); + if (m_cancel) { + is_sat = l_undef; + } + if (is_sat == l_true) { + if (wth.is_optimal()) { + s().get_model(m_model); + was_sat = true; + } + expr_ref fml = wth.mk_block(); + s().assert_expr(fml); + } + } + if (was_sat) { + wth.get_assignment(m_assignment); + } + if (is_sat == l_false && was_sat) { + is_sat = l_true; + } + if (is_sat == l_true) { + m_lower = m_upper = wth.get_min_cost(); + } + TRACE("opt", tout << "min cost: " << m_upper << "\n";); + return is_sat; + } + + }; + + class wmax : public maxsmt_solver_wbase { + public: + wmax(solver* s, ast_manager& m, smt::context& ctx): maxsmt_solver_wbase(s, m, ctx) {} + virtual ~wmax() {} + + lbool operator()() { + IF_VERBOSE(3, verbose_stream() << "(incremental 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; + 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) { + 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_VERBOSE(3, verbose_stream() << "(incremental bound)\n";); + } + 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; + } + }; + + class bvmax : public maxsmt_solver_base { + solver* mk_sat_solver(solver* s) { + tactic_ref pb2bv = mk_card2bv_tactic(m, m_params); + tactic_ref bv2sat = mk_qfbv_tactic(m, m_params); + tactic_ref tac = and_then(pb2bv.get(), bv2sat.get()); + solver* sat_solver = mk_tactic2solver(m, tac.get(), m_params); + unsigned sz = s->get_num_assertions(); + for (unsigned i = 0; i < sz; ++i) { + sat_solver->assert_expr(s->get_assertion(i)); + } + return sat_solver; + } + public: + bvmax(solver* s, ast_manager& m): maxsmt_solver_base(mk_sat_solver(s), m) {} + virtual ~bvmax() {} + + // + // convert bounds constraint into pseudo-Boolean, + // then treat pseudo-Booleans as bit-vectors and + // sorting circuits. + // + lbool operator()() { + IF_VERBOSE(1, verbose_stream() << "(wmaxsat.bv solve)\n";); + pb_util u(m); + expr_ref fml(m), val(m); + app_ref b(m); + expr_ref_vector nsoft(m); + m_lower = m_upper = rational::zero(); + for (unsigned i = 0; i < m_soft.size(); ++i) { + m_upper += m_weights[i]; + b = m.mk_fresh_const("b", m.mk_bool_sort()); + m_mc->insert(b->get_decl()); + fml = m.mk_or(m_soft[i].get(), b); + s().assert_expr(fml); + nsoft.push_back(b); + } + lbool is_sat = l_true; + bool was_sat = false; + fml = m.mk_true(); + while (l_true == is_sat) { + solver::scoped_push __s(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); + m_upper = rational::zero(); + 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() << "(wmaxsat.bv with upper bound: " << m_upper << ")\n";); + fml = m.mk_not(u.mk_ge(nsoft.size(), m_weights.c_ptr(), nsoft.c_ptr(), m_upper)); + was_sat = true; + } + } + if (is_sat == l_false && was_sat) { + is_sat = l_true; + m_lower = m_upper; + } + return is_sat; + } + + }; + + class pwmax : public maxsmt_solver_base { + public: + pwmax(solver* s, ast_manager& m): maxsmt_solver_base(s, m) {} + virtual ~pwmax() {} + lbool operator()() { + pb_util u(m); + expr_ref fml(m), val(m); + app_ref b(m); + expr_ref_vector nsoft(m); + m_lower = m_upper = rational::zero(); + solver::scoped_push __s(s()); + for (unsigned i = 0; i < m_soft.size(); ++i) { + m_upper += m_weights[i]; + b = m.mk_fresh_const("b", m.mk_bool_sort()); + m_mc->insert(b->get_decl()); + fml = m.mk_or(m_soft[i].get(), b); + s().assert_expr(fml); + nsoft.push_back(b); + } + lbool is_sat = l_true; + bool was_sat = false; + fml = m.mk_true(); + while (l_true == is_sat) { + solver::scoped_push _s(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); + m_upper = rational::zero(); + 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() << "(wmaxsat.pb with upper bound: " << m_upper << ")\n";); + fml = m.mk_not(u.mk_ge(nsoft.size(), m_weights.c_ptr(), nsoft.c_ptr(), m_upper)); + was_sat = true; + } + } + if (is_sat == l_false && was_sat) { + is_sat = l_true; + m_lower = m_upper; + } + return is_sat; + } + + }; + + struct wmaxsmt::imp { + ast_manager& m; + ref s; // solver state that contains hard constraints + expr_ref_vector m_soft; // set of soft constraints + vector m_weights; // their weights + symbol m_engine; // config + mutable params_ref m_params; // config + mutable scoped_ptr m_maxsmt; // underlying maxsmt solver + + 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) + { + } + + maxsmt_solver_base& maxsmt() const { + if (m_maxsmt) { + return *m_maxsmt; + } + if (m_engine == symbol("iwmax")) { + m_maxsmt = alloc(iwmax, s.get(), m, s->get_context()); + } + else if (m_engine == symbol("pwmax")) { + m_maxsmt = alloc(pwmax, s.get(), m); + } + else if (m_engine == symbol("bvmax")) { + m_maxsmt = alloc(bvmax, s.get(), m); + } + else if (m_engine == symbol("wpm2")) { + maxsmt_solver_base* s2 = alloc(pb_simplify_solve, s.get(), m); + m_maxsmt = alloc(wpm2, s.get(), m, s2); + } + else if (m_engine == symbol("bvsls")) { + m_maxsmt = alloc(bvsls, s.get(), m); + } + else if (m_engine == symbol::null || m_engine == symbol("wmax")) { + m_maxsmt = alloc(wmax, s.get(), m, s->get_context()); + } + else { + IF_VERBOSE(0, verbose_stream() << "(unknown engine " << m_engine << " using default 'wmax')\n";); + m_maxsmt = alloc(wmax, s.get(), m, s->get_context()); + } + m_maxsmt->updt_params(m_params); + m_maxsmt->add_soft(m_weights, m_soft); + m_maxsmt->set_converter(s->mc_ref().get()); + return *m_maxsmt; + } + + ~imp() {} + + /** + Takes solver with hard constraints added. + Returns a maximal satisfying subset of weighted soft_constraints + that are still consistent with the solver state. + */ + lbool operator()() { + return maxsmt()(); + } + rational get_lower() const { + return maxsmt().get_lower(); + } + rational get_upper() const { + return maxsmt().get_upper(); + } + void get_model(model_ref& mdl) { + if (m_maxsmt) m_maxsmt->get_model(mdl); + } + void set_cancel(bool f) { + if (m_maxsmt) m_maxsmt->set_cancel(f); + } + bool get_assignment(unsigned index) const { + return maxsmt().get_assignment(index); + } + void collect_statistics(statistics& st) const { + if (m_maxsmt) m_maxsmt->collect_statistics(st); + } + void updt_params(params_ref& p) { + opt_params _p(p); + m_engine = _p.wmaxsat_engine(); + m_maxsmt = 0; + } + }; + + wmaxsmt::wmaxsmt(ast_manager& m, + opt_solver* s, + expr_ref_vector& soft_constraints, + vector const& weights) { + m_imp = alloc(imp, m, s, soft_constraints, weights); + } + wmaxsmt::~wmaxsmt() { + dealloc(m_imp); + } + lbool wmaxsmt::operator()() { + return (*m_imp)(); + } + rational wmaxsmt::get_lower() const { + return m_imp->get_lower(); + } + rational wmaxsmt::get_upper() const { + return m_imp->get_upper(); + } + bool wmaxsmt::get_assignment(unsigned idx) const { + return m_imp->get_assignment(idx); + } + void wmaxsmt::set_cancel(bool f) { + m_imp->set_cancel(f); + } + void wmaxsmt::collect_statistics(statistics& st) const { + m_imp->collect_statistics(st); + } + void wmaxsmt::get_model(model_ref& mdl) { + m_imp->get_model(mdl); + } + void wmaxsmt::updt_params(params_ref& p) { + m_imp->updt_params(p); + } +}; + + +#if 0 // ------------------------------------------------------ // Version from CP'13 lbool wpm2b_solve() { @@ -929,7 +1223,7 @@ namespace opt { expr_ref_vector asms(m); asms.append(ans); asms.append(am); - lbool is_sat = s.check_sat(asms.size(), asms.c_ptr()); + lbool is_sat = s().check_sat(asms.size(), asms.c_ptr()); if (m_cancel && is_sat != l_false) { is_sat = l_undef; } @@ -1052,159 +1346,6 @@ namespace opt { } } - 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(m_solver); - for (unsigned i = 0; i < al.size(); ++i) { - m_solver.assert_expr(al[i]); - } - for (unsigned i = 0; i < bs.size(); ++i) { - nbs.push_back(mk_not(bs[i])); - } - TRACE("opt", - m_solver.display(tout); - tout << "\n"; - for (unsigned i = 0; i < bs.size(); ++i) { - tout << mk_pp(bs[i], m) << " " << ws[i] << "\n"; - }); - m_imp->re_init(nbs, ws); - lbool is_sat = m_imp->pb_simplify_solve(); - SASSERT(m_imp->m_lower > k); - k = m_imp->m_lower; - return is_sat; - } - void updt_params(params_ref& p) { - opt_params _p(p); - m_engine = _p.wmaxsat_engine(); - m_print_all_models = _p.print_all_models(); - m_solver.updt_params(p); - if (m_imp) { - m_imp->updt_params(p); - } - } - - void updt_model(solver& s) { - s.get_model(m_model); - if (m_print_all_models) { - std::cout << "[" << m_lower << ":" << m_upper << "]\n"; - std::cout << "(model " << std::endl; - model_smt2_pp(std::cout, m, *(m_model.get()), 2); - std::cout << ")" << std::endl; - } - } - - lbool simplify_and_check_sat(unsigned n, expr* const* assumptions) { - lbool is_sat = l_true; - tactic_ref tac1 = mk_simplify_tactic(m); - // tactic_ref tac2 = mk_pb_preprocess_tactic(m); - tactic_ref tac = tac1; // and_then(tac1.get(), tac2.get()); // TBD: make attribute for cancelation. - proof_converter_ref pc; - expr_dependency_ref core(m); - model_converter_ref mc; - goal_ref_buffer result; - goal_ref g(alloc(goal, m, true, false)); - for (unsigned i = 0; i < s.get_num_assertions(); ++i) { - g->assert_expr(s.get_assertion(i)); - } - for (unsigned i = 0; i < n; ++i) { - NOT_IMPLEMENTED_YET(); - // add assumption in a wrapper. - } - (*tac)(g, result, mc, pc, core); - if (result.empty()) { - is_sat = l_false; - } - else { - SASSERT(result.size() == 1); - goal_ref r = result[0]; - solver::scoped_push _s(m_solver); - // TBD ptr_vector asms; - for (unsigned i = 0; i < r->size(); ++i) { - // TBD collect assumptions from r - m_solver.assert_expr(r->form(i)); - } - is_sat = m_solver.check_sat_core(0, 0); - if (l_true == is_sat && !m_cancel) { - updt_model(m_solver); - if (mc && m_model) (*mc)(m_model, 0); - IF_VERBOSE(2, - g->display(verbose_stream() << "goal:\n"); - r->display(verbose_stream() << "reduced:\n"); - model_smt2_pp(verbose_stream(), m, *m_model, 0);); - } - } - return is_sat; - } - - }; - - wmaxsmt::wmaxsmt(ast_manager& m, opt_solver& s, expr_ref_vector& soft_constraints, vector const& weights) { - m_imp = alloc(imp, m, s, soft_constraints, weights); - m_imp->m_imp = alloc(imp, m, m_imp->m_solver, soft_constraints, weights); - } - - wmaxsmt::~wmaxsmt() { - dealloc(m_imp); - } - - lbool wmaxsmt::operator()() { - return (*m_imp)(); - } - rational wmaxsmt::get_lower() const { - return m_imp->get_lower(); - } - rational wmaxsmt::get_upper() const { - return m_imp->get_upper(); - } - bool wmaxsmt::get_assignment(unsigned idx) const { - return m_imp->m_assignment[idx]; - } - void wmaxsmt::set_cancel(bool f) { - m_imp->set_cancel(f); - } - void wmaxsmt::collect_statistics(statistics& st) const { - m_imp->collect_statistics(st); - } - void wmaxsmt::get_model(model_ref& mdl) { - m_imp->get_model(mdl); - } - - void wmaxsmt::updt_params(params_ref& p) { - m_imp->updt_params(p); - } - -}; - -#if 0 - 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/opt/weighted_maxsat.h b/src/opt/weighted_maxsat.h index 9a407ba56..c3b75cd32 100644 --- a/src/opt/weighted_maxsat.h +++ b/src/opt/weighted_maxsat.h @@ -31,7 +31,10 @@ namespace opt { struct imp; imp* m_imp; public: - wmaxsmt(ast_manager& m, opt_solver& s, expr_ref_vector& soft_constraints, vector const& weights); + wmaxsmt(ast_manager& m, + opt_solver* s, + expr_ref_vector& soft_constraints, + vector const& weights); ~wmaxsmt(); virtual lbool operator()(); virtual rational get_lower() const;