From 6aa00869690d7c9234f11236419624d5b7223f69 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 20 Dec 2013 16:46:23 -0800 Subject: [PATCH] adding wpm2 algorithm Signed-off-by: Nikolaj Bjorner --- src/opt/weighted_maxsat.cpp | 197 ++++++++++++++++++++++++++++++++++-- src/smt/smt_context.cpp | 6 +- src/smt/theory_pb.cpp | 3 + 3 files changed, 197 insertions(+), 9 deletions(-) diff --git a/src/opt/weighted_maxsat.cpp b/src/opt/weighted_maxsat.cpp index 1b25ba688..0619953b9 100644 --- a/src/opt/weighted_maxsat.cpp +++ b/src/opt/weighted_maxsat.cpp @@ -22,6 +22,7 @@ Notes: #include "ast_pp.h" #include "opt_params.hpp" #include "pb_decl_plugin.h" +#include "uint_set.h" namespace smt { @@ -85,7 +86,7 @@ namespace smt { for (unsigned i = 0; i < m_vars.size(); ++i) { tout << mk_pp(m_vars[i].get(), get_manager()) << " "; } - tout << "\nassignment"; + tout << "\nassignment: "; for (unsigned i = 0; i < result.size(); ++i) { tout << result[i] << " "; } @@ -350,12 +351,17 @@ namespace opt { model_ref m_model; symbol m_engine; volatile bool m_cancel; + params_ref m_params; + opt_solver m_solver; + scoped_ptr m_imp; - imp(ast_manager& m, opt_solver& s, expr_ref_vector& soft_constraints, vector const& weights): - m(m), s(s), m_soft(soft_constraints), m_weights(weights), m_cancel(false) + 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_cancel(false), + m_solver(m, m_params, symbol("bound")) { m_assignment.resize(m_soft.size(), false); } + ~imp() {} smt::theory_weighted_maxsat* get_theory() const { @@ -398,6 +404,9 @@ namespace opt { if (m_engine == symbol("pwmax")) { return pb_solve(); } + if (m_engine == symbol("wpm2")) { + return wpm2_solve(); + } return incremental_solve(); } @@ -606,8 +615,7 @@ namespace opt { if (!m_assignment[i]) { m_upper += m_weights[i]; } - } - + } IF_VERBOSE(1, verbose_stream() << "(wmaxsat.pb with upper bound: " << m_upper << ")\n";); fml = u.mk_le(nsoft.size(), m_weights.c_ptr(), nsoft.c_ptr(), m_upper - minw); s.assert_expr(fml); @@ -621,6 +629,178 @@ namespace opt { return is_sat; } + lbool wpm2_solve() { + 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); + m_lower = m_upper = rational::zero(); + obj_map ans_index; + vector amk; + vector sc; + for (unsigned i = 0; i < m_soft.size(); ++i) { + rational w = m_weights[i]; + m_upper += w; + + b = m.mk_fresh_const("b", m.mk_bool_sort()); + s.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()); + 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 = m.mk_fresh_const("c", m.mk_bool_sort()); + s.mc().insert(c->get_decl()); + 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()); + if (m_cancel && is_sat != l_false) { + is_sat = l_undef; + } + if (is_sat == l_true) { + s.get_model(m_model); + m_upper = m_lower; + for (unsigned i = 0; i < block.size(); ++i) { + VERIFY(m_model->eval(block[i].get(), val)); + m_assignment[i] = m.is_false(val); + } + } + if (is_sat != l_false) { + return is_sat; + } + s.get_unsat_core(core); + if (core.empty()) { + return l_false; + } + 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; + for (unsigned i = 0; i < sc.size(); ++i) { + uint_set t(sc[i]); + t &= A; + if (!t.empty()) { + B |= sc[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()); + } + } + rational k; + is_sat = new_bound(al, ws, bs, k); + if (is_sat != l_true) { + return is_sat; + } + m_lower += k; + 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() << "(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()); + fml = m.mk_implies(c, B_le_k); + s.assert_expr(fml); + sc.push_back(B); + am.push_back(c); + amk.push_back(k); + } + } + + lbool new_bound(expr_ref_vector const& al, + vector const& ws, + expr_ref_vector const& bs, + rational& k) { + pb_util u(m); + lbool is_sat = bound(al, ws, bs, k); + if (is_sat != l_true) return is_sat; +#if 1 + rational mininc(0); + for (unsigned i = 0; i < ws.size(); ++i) { + if (mininc.is_zero() || mininc > ws[i]) { + mininc = ws[i]; + } + } + k += mininc; +#else + expr_ref_vector al2(m); + al2.append(al); + // w_j*b_j > k + rational k0 = k; + al2.push_back(m.mk_not(u.mk_le(ws.size(), ws.c_ptr(), bs.c_ptr(), k))); + is_sat = bound(al2, ws, bs, k); + if (is_sat == l_true) { + SASSERT(k > k0); + } +#endif + return is_sat; + } + + // + // 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); + m_solver.push_core(); + 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(m.mk_not(bs[i])); + } + m_imp = alloc(imp, m, m_solver, nbs, ws); // race condition. + lbool is_sat = m_imp->pb_solve(); + k = m_imp->m_lower; + m_solver.pop_core(1); + return is_sat; + } + void updt_params(params_ref& p) { opt_params _p(p); m_engine = _p.wmaxsat_engine(); @@ -650,9 +830,14 @@ namespace opt { } void wmaxsmt::set_cancel(bool f) { m_imp->m_cancel = f; + m_imp->m_solver.set_cancel(f); + // TBD race + if (m_imp->m_imp) { + m_imp->m_imp->m_cancel = f; + } } void wmaxsmt::collect_statistics(statistics& st) const { - // no-op + m_imp->m_solver.collect_statistics(st); } void wmaxsmt::get_model(model_ref& mdl) { m_imp->get_model(mdl); diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp index 84d26e40b..2cce3931e 100644 --- a/src/smt/smt_context.cpp +++ b/src/smt/smt_context.cpp @@ -199,6 +199,9 @@ namespace smt { bool context::bcp() { SASSERT(!inconsistent()); while (m_qhead < m_assigned_literals.size()) { + if (m_cancel_flag) { + return true; + } literal l = m_assigned_literals[m_qhead]; SASSERT(get_assignment(l) == l_true); m_qhead++; @@ -225,9 +228,6 @@ namespace smt { case l_true: break; } - if (m_cancel_flag) { - return true; - } } } diff --git a/src/smt/theory_pb.cpp b/src/smt/theory_pb.cpp index 0777edf10..755bc4c2c 100644 --- a/src/smt/theory_pb.cpp +++ b/src/smt/theory_pb.cpp @@ -35,6 +35,7 @@ namespace smt { sum += coeff(i); } m_k = sum - m_k + numeral::one(); + VERIFY(l_undef == normalize()); SASSERT(well_formed()); } @@ -381,9 +382,11 @@ namespace smt { else { SASSERT(m_util.is_at_least_k(atom) || m_util.is_ge(atom)); } + TRACE("pb", display(tout, *c);); c->unique(); lbool is_true = c->normalize(); c->prune(); + TRACE("pb", display(tout, *c);); literal lit(abv);