From 582dbe509cd2a1f6eb8b83c04a2376ca4ad199ec Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 21 Jul 2014 22:24:34 +0200 Subject: [PATCH] first implementation of maxres Signed-off-by: Nikolaj Bjorner --- src/opt/hitting_sets.cpp | 52 +++++++---- src/opt/maxres.cpp | 194 +++++++++++++++++++++++++++++++++++++++ src/opt/maxres.h | 18 ++++ src/opt/maxsmt.cpp | 4 + 4 files changed, 251 insertions(+), 17 deletions(-) create mode 100644 src/opt/maxres.cpp create mode 100644 src/opt/maxres.h diff --git a/src/opt/hitting_sets.cpp b/src/opt/hitting_sets.cpp index d85e6b3f4..fb9d2d009 100644 --- a/src/opt/hitting_sets.cpp +++ b/src/opt/hitting_sets.cpp @@ -40,11 +40,12 @@ namespace opt { public: explicit justification(kind_t k):m_kind(k), m_value(0), m_pos(false) {} explicit justification(unsigned v, bool pos):m_kind(CLAUSE), m_value(v), m_pos(pos) {} - justification(justification const& other): m_kind(other.m_kind), m_value(other.m_value), m_pos(other.m_pos) {} + justification(justification const& other): + m_kind(other.m_kind), m_value(other.m_value), m_pos(other.m_pos) {} justification& operator=(justification const& other) { - m_kind = other.m_kind; + m_kind = other.m_kind; m_value = other.m_value; - m_pos = other.m_pos; + m_pos = other.m_pos; return *this; } unsigned clause() const { return m_value; } @@ -147,6 +148,7 @@ namespace opt { m_cancel(false), m_max_weight(0), m_denominator(1), + m_alloc("hitting-sets"), m_weights_var(0), m_qhead(0), m_scope_lvl(0), @@ -157,7 +159,14 @@ namespace opt { m_enable_simplex = true; } - ~imp() {} + ~imp() { + for (unsigned i = 0; i < m_T.size(); ++i) { + m_alloc.deallocate(m_T[i]->alloc_size(), m_T[i]); + } + for (unsigned i = 0; i < m_F.size(); ++i) { + m_alloc.deallocate(m_F[i]->alloc_size(), m_F[i]); + } + } void add_weight(rational const& w) { SASSERT(w.is_pos()); @@ -198,9 +207,7 @@ namespace opt { ptr_vector& Sets = sign?m_F:m_T; vector& watch = sign?m_fwatch:m_twatch; init_weights(); - if (sz == 0) { - // TBD - IF_VERBOSE(0, verbose_stream() << "empty clause\n";); + if (sz == 0) { set_conflict(0, justification(justification::AXIOM)); } else if (sz == 1) { @@ -375,7 +382,8 @@ namespace opt { } out << "trail\n"; for (unsigned i = 0; i < m_trail.size(); ++i) { - out << m_trail[i] << " "; + unsigned idx = m_trail[i]; + out << (m_justification[idx].is_decision()?"d":"") << idx << " "; } out << "\n"; } @@ -406,6 +414,14 @@ namespace opt { } } + void display_lemma(std::ostream& out) { + out << "lemma: "; + for (unsigned i = 0; i < m_lemma.size(); ++i) { + out << m_lemma[i] << " "; + } + out << "\n"; + } + struct scoped_push { imp& s; scoped_push(imp& s):s(s) { s.push(); } @@ -850,11 +866,7 @@ namespace opt { } while (num_marks > 0); m_lemma[0] = conflict_l; - TRACE("opt", - for (unsigned i = 0; i < m_lemma.size(); ++i) { - tout << m_lemma[i] << " "; - } - tout << "\n";); + TRACE("opt", display_lemma(tout);); SASSERT(value(conflict_l) == l_true); unsigned new_scope_lvl = 0; for (unsigned i = 1; i < m_lemma.size(); ++i) { @@ -1046,15 +1058,21 @@ namespace opt { } } // undo the lower bounds. + TRACE("opt", + tout << "prune branch: " << m_weight << " "; + display_lemma(tout); + display(tout); + ); justification j = add_exists_false(m_lemma.size(), m_lemma.c_ptr()); - TRACE("opt", display(tout, j);); - set_conflict(m_lemma[0], j); + unsigned idx = m_lemma.empty()?0:m_lemma[0]; + set_conflict(idx, j); } // TBD: derive strong inequalities and add them to Simplex. - // x_i1 + .. + x_ik >= k-1 for each subset k from set n: x_1 + .. + x_n >= k - + // x_i1 + .. + x_ik >= k-1 for each subset k from set n: x_1 + .. + x_n >= k }; + + hitting_sets::hitting_sets() { m_imp = alloc(imp); } hitting_sets::~hitting_sets() { dealloc(m_imp); } void hitting_sets::add_weight(rational const& w) { m_imp->add_weight(w); } diff --git a/src/opt/maxres.cpp b/src/opt/maxres.cpp new file mode 100644 index 000000000..b9c09350c --- /dev/null +++ b/src/opt/maxres.cpp @@ -0,0 +1,194 @@ +#include "solver.h" +#include "maxsmt.h" +#include "maxres.h" +#include "ast_pp.h" + + +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; + model_ref m_model; + expr_ref_vector m_soft_constraints; + volatile bool m_cancel; + rational m_lower; + rational m_upper; + + 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_cancel(false) + { + } + + bool is_literal(expr* l) { + return + is_uninterp_const(l) || + m.is_not(l, l) && is_uninterp_const(l); + } + + void add_soft(expr* e) { + TRACE("opt", tout << mk_pp(e, m) << "\n";); + 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); + s.assert_expr(fml); + m_asms.push_back(asum); + } + } + + lbool operator()() { + expr_ref fml(m); + 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"; + ); + lbool is_sat = s.check_sat(m_asms.size(), m_asms.c_ptr()); + if (m_cancel) { + return l_undef; + } + switch (is_sat) { + case l_true: + s.get_model(m_model); + m_upper = m_lower; + return l_true; + case l_undef: + return l_undef; + default: + ptr_vector core; + s.get_unsat_core(core); + TRACE("opt", display_vec(tout << "core: ", core.size(), core.c_ptr());); + if (core.empty()) { + return l_false; + } + max_resolve(core); + fml = m.mk_not(m.mk_and(m_B.size(), m_B.c_ptr())); + s.assert_expr(fml); + m_lower += rational::one(); + break; + } + IF_VERBOSE(1, verbose_stream() << "(opt.max_res lower: " << m_lower << ")\n";); + } + return l_true; + } + + void display_vec(std::ostream& out, unsigned sz, expr* const* args) { + for (unsigned i = 0; i < sz; ++i) { + out << mk_pp(args[i], m) << " "; + } + out << "\n"; + } + + void max_resolve(ptr_vector& core) { + SASSERT(!core.empty()); + expr_ref fml(m), asum(m); + m_B.reset(); + m_D.reset(); + m_D.resize(core.size()); + m_B.append(core.size(), core.c_ptr()); + m_D[core.size()-1] = m.mk_false(); + // + // d_{sz-1} := false + // 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(); + expr* b_i = m_B[i].get(); + expr* b_i1 = m_B[i+1].get(); + 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)); + s.assert_expr(fml); + m_asms.push_back(asum); + } + } + + 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_asms.pop_back(); + --i; + } + } + } + + rational get_lower() const { + return m_lower; + } + + rational get_upper() const { + return m_upper; + } + + bool get_assignment(unsigned index) const { + expr_ref tmp(m); + m_model->eval(m_soft_constraints[index], tmp); + return m.is_true(tmp); + } + void set_cancel(bool f) { + m_cancel = f; + } + void collect_statistics(statistics& st) const { + } + void get_model(model_ref& mdl) { + mdl = m_model; + } + void updt_params(params_ref& p) { + ; + } + +}; + +maxres::maxres(ast_manager& m, solver& s, expr_ref_vector& soft_constraints) { + m_imp = alloc(imp, m, s, soft_constraints); +} + +maxres::~maxres() { + dealloc(m_imp); +} + + +lbool maxres::operator()() { + return (*m_imp)(); +} + +rational maxres::get_lower() const { + return m_imp->get_lower(); +} +rational maxres::get_upper() const { + return m_imp->get_upper(); +} +bool maxres::get_assignment(unsigned index) const { + return m_imp->get_assignment(index); +} +void maxres::set_cancel(bool f) { + m_imp->set_cancel(f); +} +void maxres::collect_statistics(statistics& st) const { + m_imp->collect_statistics(st); +} +void maxres::get_model(model_ref& mdl) { + m_imp->get_model(mdl); +} +void maxres::updt_params(params_ref& p) { + m_imp->updt_params(p); +} diff --git a/src/opt/maxres.h b/src/opt/maxres.h new file mode 100644 index 000000000..8b90158fb --- /dev/null +++ b/src/opt/maxres.h @@ -0,0 +1,18 @@ + +namespace opt { + class maxres : public maxsmt_solver { + struct imp; + imp* m_imp; + public: + maxres(ast_manager& m, solver& s, expr_ref_vector& soft_constraints); + ~maxres(); + virtual lbool operator()(); + virtual rational get_lower() const; + virtual rational get_upper() const; + virtual bool get_assignment(unsigned index) const; + virtual void set_cancel(bool f); + virtual void collect_statistics(statistics& st) const; + virtual void get_model(model_ref& mdl); + virtual void updt_params(params_ref& p); + }; +}; diff --git a/src/opt/maxsmt.cpp b/src/opt/maxsmt.cpp index 9da9f9f2e..2eb6e426b 100644 --- a/src/opt/maxsmt.cpp +++ b/src/opt/maxsmt.cpp @@ -21,6 +21,7 @@ Notes: #include "maxsmt.h" #include "fu_malik.h" #include "core_maxsat.h" +#include "maxres.h" #include "weighted_maxsat.h" #include "ast_pp.h" #include "opt_params.hpp" @@ -45,6 +46,9 @@ namespace opt { 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); }