From bf35a62da7d4a8efd4025a35d2e572f62f1ad06f Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 21 Jul 2014 23:28:19 +0200 Subject: [PATCH] adding mus extraction Signed-off-by: Nikolaj Bjorner --- src/opt/maxres.cpp | 88 ++++++++++++++++++-- src/opt/mus.cpp | 203 +++++++++++++++++++++++++++++++++++++++++++++ src/opt/mus.h | 21 +++++ 3 files changed, 306 insertions(+), 6 deletions(-) create mode 100644 src/opt/mus.cpp create mode 100644 src/opt/mus.h diff --git a/src/opt/maxres.cpp b/src/opt/maxres.cpp index b9c09350c..579a7c6e9 100644 --- a/src/opt/maxres.cpp +++ b/src/opt/maxres.cpp @@ -1,8 +1,13 @@ +/** + MaxRes (weighted) max-sat algorithm by Nina and Bacchus, AAAI 2014. + +*/ + #include "solver.h" #include "maxsmt.h" #include "maxres.h" #include "ast_pp.h" - +#include "mus.h" using namespace opt; @@ -12,14 +17,16 @@ struct maxres::imp { 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; 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_soft_constraints(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) { } @@ -32,20 +39,25 @@ struct maxres::imp { void add_soft(expr* e) { 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); if (is_literal(e)) { m_asms.push_back(e); } else { - expr_ref asum(m), fml(m); asum = m.mk_fresh_const("soft", m.mk_bool_sort()); - fml = m.mk_implies(asum, e); + fml = m.mk_iff(asum, e); s.assert_expr(fml); m_asms.push_back(asum); } + m_asm2cls.insert(m_asms.back(), cls.get()); } lbool operator()() { expr_ref fml(m); + ptr_vector core, new_core; solver::scoped_push _sc(s); for (unsigned i = 0; i < m_soft_constraints.size(); ++i) { add_soft(m_soft_constraints[i].get()); @@ -69,12 +81,37 @@ struct maxres::imp { case l_undef: return l_undef; default: - ptr_vector core; + core.reset(); s.get_unsat_core(core); TRACE("opt", display_vec(tout << "core: ", core.size(), core.c_ptr());); + 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 + TRACE("opt", display_vec(tout << "minimized core: ", core.size(), core.c_ptr());); max_resolve(core); fml = m.mk_not(m.mk_and(m_B.size(), m_B.c_ptr())); s.assert_expr(fml); @@ -96,6 +133,7 @@ struct maxres::imp { void max_resolve(ptr_vector& core) { SASSERT(!core.empty()); expr_ref fml(m), asum(m); + app_ref cls(m); m_B.reset(); m_D.reset(); m_D.resize(core.size()); @@ -115,17 +153,55 @@ struct maxres::imp { m_D[i] = m.mk_implies(b_i1, d_i1); expr* d_i = m_D[i].get(); asum = m.mk_fresh_const("a", m.mk_bool_sort()); - fml = m.mk_implies(asum, m.mk_implies(d_i, b_i)); + 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); } } + app_ref mk_cls(expr* e) { + expr_ref_vector disj(m), todo(m); + expr_ref f(m); + app_ref result(m); + expr* e1, *e2; + todo.push_back(e); + while (!todo.empty()) { + f = todo.back(); + todo.pop_back(); + if (m.is_implies(f, e1, e2)) { + todo.push_back(m.mk_not(e1)); + todo.push_back(e2); + } + else if (m.is_not(f, e1) && m.is_not(e1, e2)) { + todo.push_back(e2); + } + else if (m.is_or(f)) { + todo.append(to_app(f)->get_num_args(), to_app(f)->get_args()); + } + else if (m.is_not(f, e1) && m.is_and(e1)) { + for (unsigned i = 0; i < to_app(e1)->get_num_args(); ++i) { + todo.push_back(m.mk_not(to_app(e1)->get_arg(i))); + } + } + else { + disj.push_back(f); + } + } + result = m.mk_or(disj.size(), disj.c_ptr()); + return result; + } + void remove_core(ptr_vector const& core) { 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; } } diff --git a/src/opt/mus.cpp b/src/opt/mus.cpp new file mode 100644 index 000000000..1bed42f7d --- /dev/null +++ b/src/opt/mus.cpp @@ -0,0 +1,203 @@ +#include "solver.h" +#include "smt_literal.h" +#include "mus.h" +#include "ast_pp.h" + +using namespace opt; + +// Faster MUS extraction based on Belov et.al. HYB (Algorithm 3, 4) + + +struct mus::imp { + solver& s; + ast_manager& m; + expr_ref_vector m_cls2expr; + obj_map m_expr2cls; + vector m_cls2lits; + expr_ref_vector m_vars; + obj_map m_var2idx; + +public: + imp(solver& s, ast_manager& m): s(s), m(m), m_cls2expr(m), m_vars(m) {} + + unsigned add_var(expr* v) { + unsigned idx = m_vars.size(); + if (!m_var2idx.find(v, idx)) { + m_var2idx.insert(v, idx); + m_vars.push_back(v); + } + return idx; + } + + unsigned add_soft(expr* cls, unsigned sz, expr* const* args) { + TRACE("opt", tout << sz << ": " << mk_pp(cls, m) << "\n";); + smt::literal_vector lits; + expr* arg; + for (unsigned i = 0; i < sz; ++i) { + if (m.is_not(args[i], arg)) { + lits.push_back(smt::literal(add_var(arg), true)); + } + else { + lits.push_back(smt::literal(add_var(args[i]), false)); + } + } + unsigned idx = m_cls2lits.size(); + m_expr2cls.insert(cls, idx); + m_cls2expr.push_back(cls); + m_cls2lits.push_back(lits); + return idx; + } + + 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); + } + mus.reset(); + expr_ref_vector assumptions(m); + svector model; + ptr_vector core_exprs; + model.resize(m_vars.size()); + while (!core.empty()) { + IF_VERBOSE(0, display_vec(tout << "core: ", core);); + 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); + unsigned sz = assumptions.size(); + assumptions.push_back(not_cls); + add_core(core, assumptions); + lbool is_sat = s.check_sat(assumptions.size(), assumptions.c_ptr()); + assumptions.resize(sz); + switch(is_sat) { + case l_undef: + return is_sat; + case l_true: + assumptions.push_back(cls); + mus.push_back(cls_id); + extract_model(s, model); + sz = core.size(); + core.append(mus); + rmr(core, mus, model); + core.resize(sz); + break; + default: + core_exprs.reset(); + s.get_unsat_core(core_exprs); + if (!core_exprs.contains(not_cls)) { + // core := core_exprs \ mus + core.reset(); + for (unsigned i = 0; i < core_exprs.size(); ++i) { + cls = core_exprs[i]; + cls_id = m_expr2cls.find(cls); + if (!mus.contains(cls_id)) { + core.push_back(cls_id); + } + } + } + break; + } + } + return l_true; + } + + void add_core(unsigned_vector const& core, expr_ref_vector& assumptions) { + for (unsigned i = 0; i < core.size(); ++i) { + assumptions.push_back(m_cls2expr[core[i]].get()); + } + } + + 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 << "\n"; + } + + void extract_model(solver& s, svector& model) { + model_ref mdl; + s.get_model(mdl); + for (unsigned i = 0; i < m_vars.size(); ++i) { + expr_ref tmp(m); + mdl->eval(m_vars[i].get(), tmp); + model[i] = m.is_true(tmp); + } + } + + /** + Recursive model rotation. + */ + 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);); + + 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); + rmr(M, mus, model); + } + model[lit.var()] = !model[lit.var()]; // swap assignment back + } + } + + bool has_single_unsat(svector const& model, unsigned& cls_id) const { + cls_id = UINT_MAX; + for (unsigned i = 0; i < m_cls2lits.size(); ++i) { + if (!eval(model, m_cls2lits[i])) { + if (cls_id == UINT_MAX) { + cls_id = i; + } + else { + return false; + } + } + } + return cls_id != UINT_MAX; + } + + bool eval(svector const& model, smt::literal_vector const& cls) const { + for (unsigned i = 0; i < cls.size(); ++i) { + if (model[cls[i].var()] != cls[i].sign()) { + return true; + } + } + 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) { + m_imp = alloc(imp, s, m); +} + +mus::~mus() { + dealloc(m_imp); +} + +unsigned mus::add_soft(expr* cls, unsigned sz, expr* const* args) { + return m_imp->add_soft(cls, sz, args); +} + +lbool mus::get_mus(unsigned_vector& mus) { + return m_imp->get_mus(mus); +} + diff --git a/src/opt/mus.h b/src/opt/mus.h new file mode 100644 index 000000000..a2ba36f14 --- /dev/null +++ b/src/opt/mus.h @@ -0,0 +1,21 @@ + +namespace opt { + class mus { + struct imp; + imp * m_imp; + public: + mus(solver& s, ast_manager& m); + ~mus(); + /** + Add soft constraint. + + Assume that the solver context enforces that + cls is equivalent to a disjunction of args. + Assume also that cls is a literal. + */ + unsigned add_soft(expr* cls, unsigned sz, expr* const* args); + + lbool get_mus(unsigned_vector& mus); + }; + +};