From 5e9bf2ef532fc42fbbf3382d8f21f5fac8ebe7ec Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 22 Jul 2014 15:42:08 +0200 Subject: [PATCH] maxres revised to handle weighted constraints Signed-off-by: Nikolaj Bjorner --- src/opt/maxres.cpp | 186 +++++++++++++++++++++++++++++++-------------- src/opt/maxres.h | 2 +- src/opt/maxsmt.cpp | 8 +- src/opt/mus.cpp | 60 ++++++++++----- src/opt/mus.h | 4 + 5 files changed, 177 insertions(+), 83 deletions(-) diff --git a/src/opt/maxres.cpp b/src/opt/maxres.cpp index 579a7c6e9..11d87a98e 100644 --- a/src/opt/maxres.cpp +++ b/src/opt/maxres.cpp @@ -12,62 +12,79 @@ using namespace opt; struct maxres::imp { - ast_manager& m; - solver& s; - expr_ref_vector m_B; - expr_ref_vector m_D; - expr_ref_vector m_asms; - app_ref_vector m_clss; - model_ref m_model; - expr_ref_vector m_soft_constraints; - volatile bool m_cancel; - rational m_lower; - rational m_upper; - obj_map m_asm2cls; + struct info { + app* m_cls; + rational m_weight; + info(app* cls, rational const& w): + m_cls(cls), m_weight(w) {} + info(): m_cls(0) {} + }; + ast_manager& m; + solver& s; + expr_ref_vector m_B; + expr_ref_vector m_D; + expr_ref_vector m_asms; + model_ref m_model; + expr_ref_vector m_soft_constraints; + volatile bool m_cancel; + rational m_lower; + rational m_upper; + obj_map m_asm2info; + ptr_vector m_new_core; + mus m_mus; + expr_ref_vector m_trail; - imp(ast_manager& m, solver& s, expr_ref_vector& soft_constraints): - m(m), s(s), m_B(m), m_D(m), m_asms(m), m_clss(m), m_soft_constraints(soft_constraints), - m_cancel(false) + imp(ast_manager& m, solver& s, expr_ref_vector& soft_constraints, vector const& weights): + m(m), s(s), m_B(m), m_D(m), m_asms(m), m_soft_constraints(m), + m_cancel(false), + m_mus(s, m), + m_trail(m) { + // TBD: this introduces an assertion to solver. + init_soft(weights, soft_constraints); } bool is_literal(expr* l) { return is_uninterp_const(l) || - m.is_not(l, l) && is_uninterp_const(l); + (m.is_not(l, l) && is_uninterp_const(l)); } - void add_soft(expr* e) { + void add_soft(expr* e, rational const& w) { TRACE("opt", tout << mk_pp(e, m) << "\n";); expr_ref asum(m), fml(m); app_ref cls(m); cls = mk_cls(e); - m_clss.push_back(cls); + m_trail.push_back(cls); if (is_literal(e)) { - m_asms.push_back(e); + asum = e; } else { asum = m.mk_fresh_const("soft", m.mk_bool_sort()); fml = m.mk_iff(asum, e); s.assert_expr(fml); - m_asms.push_back(asum); } - m_asm2cls.insert(m_asms.back(), cls.get()); + new_assumption(asum, cls, w); + m_upper += w; + } + + void new_assumption(expr* e, app* cls, rational const& w) { + info inf(cls, w); + m_asm2info.insert(e, inf); + m_asms.push_back(e); + m_trail.push_back(e); } lbool operator()() { expr_ref fml(m); - ptr_vector core, new_core; + ptr_vector core; solver::scoped_push _sc(s); - for (unsigned i = 0; i < m_soft_constraints.size(); ++i) { - add_soft(m_soft_constraints[i].get()); - } - m_upper = rational(m_soft_constraints.size()); while (true) { TRACE("opt", display_vec(tout, m_asms.size(), m_asms.c_ptr()); s.display(tout); tout << "\n"; + display(tout); ); lbool is_sat = s.check_sat(m_asms.size(), m_asms.c_ptr()); if (m_cancel) { @@ -85,37 +102,21 @@ struct maxres::imp { s.get_unsat_core(core); TRACE("opt", display_vec(tout << "core: ", core.size(), core.c_ptr());); SASSERT(!core.empty()); + is_sat = minimize_core(core); + SASSERT(!core.empty()); if (core.empty()) { return l_false; } -#if 1 - // minimize core: - mus ms(s, m); - for (unsigned i = 0; i < core.size(); ++i) { - app* cls = 0; - VERIFY(m_asm2cls.find(core[i], cls)); - SASSERT(cls); - SASSERT(m.is_or(cls)); - ms.add_soft(core[i], cls->get_num_args(), cls->get_args()); - } - unsigned_vector mus_idx; - is_sat = ms.get_mus(mus_idx); if (is_sat != l_true) { return is_sat; } - new_core.reset(); - for (unsigned i = 0; i < mus_idx.size(); ++i) { - new_core.push_back(core[mus_idx[i]]); - } - core.reset(); - core.append(new_core); - -#endif + remove_core(core); + rational w = split_core(core); TRACE("opt", display_vec(tout << "minimized core: ", core.size(), core.c_ptr());); - max_resolve(core); + max_resolve(core, w); fml = m.mk_not(m.mk_and(m_B.size(), m_B.c_ptr())); s.assert_expr(fml); - m_lower += rational::one(); + m_lower += w; break; } IF_VERBOSE(1, verbose_stream() << "(opt.max_res lower: " << m_lower << ")\n";); @@ -123,6 +124,57 @@ struct maxres::imp { return l_true; } + lbool minimize_core(ptr_vector& core) { + m_mus.reset(); + for (unsigned i = 0; i < core.size(); ++i) { + app* cls = get_clause(core[i]); + SASSERT(cls); + SASSERT(m.is_or(cls)); + m_mus.add_soft(core[i], cls->get_num_args(), cls->get_args()); + } + 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_asm2info.find(e).m_weight; + } + + app* get_clause(expr* e) { + return m_asm2info.find(e).m_cls; + } + + rational split_core(ptr_vector const& core) { + + // find the minimal weight: + SASSERT(!core.empty()); + rational w = get_weight(core[0]); + for (unsigned i = 1; i < core.size(); ++i) { + rational w2 = get_weight(core[i]); + if (w2 < w) { + w = w2; + } + } + // add fresh soft clauses for weights that are above w. + for (unsigned i = 0; i < core.size(); ++i) { + rational w2 = get_weight(core[i]); + if (w2 > w) { + new_assumption(core[i], get_clause(core[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) << " "; @@ -130,7 +182,14 @@ struct maxres::imp { out << "\n"; } - void max_resolve(ptr_vector& core) { + 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); @@ -144,7 +203,6 @@ struct maxres::imp { // d_i := (!core_{i+1} or d_{i+1}) for i = 0...sz-2 // soft (!d_i or core_i) // - remove_core(core); for (unsigned i = core.size()-1; i > 0; ) { --i; expr* d_i1 = m_D[i+1].get(); @@ -155,11 +213,10 @@ struct maxres::imp { asum = m.mk_fresh_const("a", m.mk_bool_sort()); cls = m.mk_implies(d_i, b_i); fml = m.mk_iff(asum, cls); - s.assert_expr(fml); - m_asms.push_back(asum); cls = mk_cls(cls); - m_clss.push_back(cls); - m_asm2cls.insert(asum, cls); + m_trail.push_back(cls); + new_assumption(asum, cls, w); + s.assert_expr(fml); } } @@ -199,9 +256,7 @@ struct maxres::imp { for (unsigned i = 0; i < m_asms.size(); ++i) { if (core.contains(m_asms[i].get())) { m_asms[i] = m_asms.back(); - m_clss[i] = m_clss.back(); m_asms.pop_back(); - m_clss.pop_back(); --i; } } @@ -217,11 +272,12 @@ struct maxres::imp { bool get_assignment(unsigned index) const { expr_ref tmp(m); - m_model->eval(m_soft_constraints[index], tmp); + VERIFY(m_model->eval(m_soft_constraints[index], tmp)); return m.is_true(tmp); } void set_cancel(bool f) { m_cancel = f; + m_mus.set_cancel(f); } void collect_statistics(statistics& st) const { } @@ -232,10 +288,22 @@ struct maxres::imp { ; } + void init_soft(vector const& weights, expr_ref_vector const& soft) { + m_soft_constraints.reset(); + m_upper.reset(); + m_lower.reset(); + m_asm2info.reset(); + m_trail.reset(); + m_soft_constraints.append(soft); + for (unsigned i = 0; i < m_soft_constraints.size(); ++i) { + add_soft(m_soft_constraints[i].get(), weights[i]); + } + } + }; -maxres::maxres(ast_manager& m, solver& s, expr_ref_vector& soft_constraints) { - m_imp = alloc(imp, m, s, soft_constraints); +maxres::maxres(ast_manager& m, solver& s, expr_ref_vector& soft_constraints, vector const& weights) { + m_imp = alloc(imp, m, s, soft_constraints, weights); } maxres::~maxres() { diff --git a/src/opt/maxres.h b/src/opt/maxres.h index 8b90158fb..41b57456f 100644 --- a/src/opt/maxres.h +++ b/src/opt/maxres.h @@ -4,7 +4,7 @@ namespace opt { struct imp; imp* m_imp; public: - maxres(ast_manager& m, solver& s, expr_ref_vector& soft_constraints); + maxres(ast_manager& m, solver& s, expr_ref_vector& soft_constraints, vectorconst& weights); ~maxres(); virtual lbool operator()(); virtual rational get_lower() const; diff --git a/src/opt/maxsmt.cpp b/src/opt/maxsmt.cpp index 2eb6e426b..1cc98d328 100644 --- a/src/opt/maxsmt.cpp +++ b/src/opt/maxsmt.cpp @@ -39,16 +39,16 @@ namespace opt { m_msolver = 0; is_sat = m_s->check_sat(0, 0); } + else if (m_maxsat_engine == symbol("maxres")) { + m_msolver = alloc(maxres, m, *m_s, m_soft_constraints, m_weights); + } else if (is_maxsat_problem(m_weights)) { if (m_maxsat_engine == symbol("core_maxsat")) { m_msolver = alloc(core_maxsat, m, *m_s, m_soft_constraints); } else if (m_maxsat_engine == symbol("weighted_maxsat")) { m_msolver = alloc(wmaxsmt, m, m_s.get(), m_soft_constraints, m_weights); - } - else if (m_maxsat_engine == symbol("maxres")) { - m_msolver = alloc(maxres, m, *m_s, m_soft_constraints); - } + } else { m_msolver = alloc(fu_malik, m, *m_s, m_soft_constraints); } diff --git a/src/opt/mus.cpp b/src/opt/mus.cpp index 1bed42f7d..9d9278a27 100644 --- a/src/opt/mus.cpp +++ b/src/opt/mus.cpp @@ -16,9 +16,21 @@ struct mus::imp { vector m_cls2lits; expr_ref_vector m_vars; obj_map m_var2idx; + volatile bool m_cancel; -public: - imp(solver& s, ast_manager& m): s(s), m(m), m_cls2expr(m), m_vars(m) {} + imp(solver& s, ast_manager& m): s(s), m(m), m_cls2expr(m), m_vars(m), m_cancel(false) {} + + void reset() { + m_cls2expr.reset(); + m_expr2cls.reset(); + m_cls2lits.reset(); + m_vars.reset(); + m_var2idx.reset(); + } + + void set_cancel(bool f) { + m_cancel = f; + } unsigned add_var(expr* v) { unsigned idx = m_vars.size(); @@ -47,10 +59,16 @@ public: m_cls2lits.push_back(lits); return idx; } + + expr* mk_not(expr* e) { + if (m.is_not(e, e)) { + return e; + } + return m.mk_not(e); + } lbool get_mus(unsigned_vector& mus) { TRACE("opt", tout << "\n";); - solver::scoped_push _sc(s); unsigned_vector core; for (unsigned i = 0; i < m_cls2expr.size(); ++i) { core.push_back(i); @@ -61,12 +79,17 @@ public: ptr_vector core_exprs; model.resize(m_vars.size()); while (!core.empty()) { - IF_VERBOSE(0, display_vec(tout << "core: ", core);); + TRACE("opt", + display_vec(tout << "core: ", core); + display_vec(tout << "mus: ", mus); + display_vec(tout << "model: ", model); + ); + IF_VERBOSE(1, verbose_stream() << "(opt.mus reducing core: " << core.size() << " new core: " << mus.size() << ")\n";); unsigned cls_id = core.back(); core.pop_back(); expr* cls = m_cls2expr[cls_id].get(); expr_ref not_cls(m); - not_cls = m.mk_not(cls); + not_cls = mk_not(cls); unsigned sz = assumptions.size(); assumptions.push_back(not_cls); add_core(core, assumptions); @@ -113,7 +136,7 @@ public: template void display_vec(std::ostream& out, T const& v) const { for (unsigned i = 0; i < v.size(); ++i) { - out << mk_pp(v[i], m) << " "; + out << v[i] << " "; } out << "\n"; } @@ -133,19 +156,18 @@ public: */ void rmr(unsigned_vector& M, unsigned_vector& mus, svector& model) { TRACE("opt", - display_vec(tout << "M:", M); - display_vec(tout << "mus:", mus); - display_vec(tout << "model:", model);); + display_vec(tout << "core: ", M); + display_vec(tout << "mus: ", mus); + display_vec(tout << "model: ", model);); unsigned cls_id = mus.back(); smt::literal_vector const& cls = m_cls2lits[cls_id]; - unsigned cls_id_new; for (unsigned i = 0; i < cls.size(); ++i) { smt::literal lit = cls[i]; SASSERT(model[lit.var()] == lit.sign()); // literal evaluates to false. model[lit.var()] = !model[lit.var()]; // swap assignment - if (has_single_unsat(model, cls_id_new)) { - mus.push_back(cls_id_new); + if (!mus.contains(cls_id) && has_single_unsat(model, cls_id)) { + mus.push_back(cls_id); rmr(M, mus, model); } model[lit.var()] = !model[lit.var()]; // swap assignment back @@ -176,13 +198,6 @@ public: return false; } - template - void display_vec(std::ostream& out, T const& v) { - for (unsigned i = 0; i < v.size(); ++i) { - out << v[i] << " "; - } - out << "\n"; - } }; mus::mus(solver& s, ast_manager& m) { @@ -201,3 +216,10 @@ lbool mus::get_mus(unsigned_vector& mus) { return m_imp->get_mus(mus); } +void mus::set_cancel(bool f) { + m_imp->set_cancel(f); +} + +void mus::reset() { + m_imp->reset(); +} diff --git a/src/opt/mus.h b/src/opt/mus.h index a2ba36f14..e3cb4c963 100644 --- a/src/opt/mus.h +++ b/src/opt/mus.h @@ -16,6 +16,10 @@ namespace opt { unsigned add_soft(expr* cls, unsigned sz, expr* const* args); lbool get_mus(unsigned_vector& mus); + + void reset(); + + void set_cancel(bool f); }; };