From ac893e907f918bb52ab554538fe09826c3426e5e Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 14 Dec 2013 16:06:03 +0200 Subject: [PATCH] fixes to maxsmt Signed-off-by: Nikolaj Bjorner --- src/opt/core_maxsat.cpp | 50 +++++++++++---------- src/opt/core_maxsat.h | 6 +-- src/opt/fu_malik.cpp | 87 ++++++++++++++++++------------------- src/opt/fu_malik.h | 3 +- src/opt/maxsmt.cpp | 41 ++++++++++------- src/opt/maxsmt.h | 5 +-- src/opt/opt_context.cpp | 10 ++++- src/opt/optsmt.cpp | 7 +-- src/opt/optsmt.h | 1 - src/opt/weighted_maxsat.cpp | 24 +++++----- src/opt/weighted_maxsat.h | 3 +- 11 files changed, 124 insertions(+), 113 deletions(-) diff --git a/src/opt/core_maxsat.cpp b/src/opt/core_maxsat.cpp index 1019465cd..9b4f284a5 100644 --- a/src/opt/core_maxsat.cpp +++ b/src/opt/core_maxsat.cpp @@ -21,11 +21,10 @@ Notes: #include "ast_pp.h" namespace opt { - core_maxsat::core_maxsat(ast_manager& m, solver& s, expr_ref_vector& soft_constraints): - m(m), s(s), m_soft(soft_constraints), m_answer(m) { - m_upper = m_soft.size(); + m(m), s(s), m_lower(0), m_upper(soft_constraints.size()), m_soft(soft_constraints) { + m_answer.resize(m_soft.size(), false); } core_maxsat::~core_maxsat() {} @@ -41,7 +40,7 @@ namespace opt { s.assert_expr(m.mk_or(a, m_soft[i].get())); block_vars.insert(aux.back()); } - while (m_answer.size() < m_upper) { + while (m_lower < m_upper) { ptr_vector vars; set2vector(block_vars, vars); lbool is_sat = s.check_sat(vars.size(), vars.c_ptr()); @@ -51,31 +50,31 @@ namespace opt { return l_undef; case l_true: { model_ref mdl; - expr_ref_vector ans(m); + svector ans; + unsigned new_lower = 0; s.get_model(mdl); - for (unsigned i = 0; i < aux.size(); ++i) { expr_ref val(m); VERIFY(mdl->eval(m_soft[i].get(), val)); - if (m.is_true(val)) { - ans.push_back(m_soft[i].get()); - } + ans.push_back(m.is_true(val)); + if (ans.back()) ++new_lower; } TRACE("opt", tout << "sat\n"; for (unsigned i = 0; i < ans.size(); ++i) { - tout << mk_pp(ans[i].get(), m) << "\n"; + tout << mk_pp(m_soft[i].get(), m) << " |-> " << ans[i] << "\n"; }); - IF_VERBOSE(1, verbose_stream() << "(maxsat.core sat with lower bound: " << ans.size() << "\n";); - if (ans.size() > m_answer.size()) { + IF_VERBOSE(1, verbose_stream() << "(maxsat.core sat with lower bound: " << new_lower << "\n";); + if (new_lower > m_lower) { m_answer.reset(); m_answer.append(ans); m_model = mdl.get(); + m_lower = new_lower; } - if (m_answer.size() == m_upper) { + if (m_lower == m_upper) { return l_true; } - SASSERT(m_soft.size() >= m_answer.size()+1); - unsigned k = m_soft.size()-m_answer.size()-1; + SASSERT(m_soft.size() >= new_lower+1); + unsigned k = m_soft.size()-new_lower-1; expr_ref fml = mk_at_most(core_vars, k); TRACE("opt", tout << "add: " << fml << "\n";); s.assert_expr(fml); @@ -95,7 +94,7 @@ namespace opt { } IF_VERBOSE(1, verbose_stream() << "(maxsat.core unsat (core size = " << core.size() << ")\n";); if (core.empty()) { - m_upper = m_answer.size(); + m_upper = m_lower; return l_true; } else { @@ -134,16 +133,13 @@ namespace opt { } rational core_maxsat::get_lower() const { - return rational(m_answer.size()); + return rational(m_soft.size()-m_upper); } rational core_maxsat::get_upper() const { - return rational(m_upper); + return rational(m_soft.size()-m_lower); } - rational core_maxsat::get_value() const { - return get_lower(); - } - expr_ref_vector core_maxsat::get_assignment() const { - return m_answer; + bool core_maxsat::get_assignment(unsigned idx) const { + return m_answer[idx]; } void core_maxsat::set_cancel(bool f) { @@ -153,6 +149,14 @@ namespace opt { } void core_maxsat::get_model(model_ref& mdl) { mdl = m_model.get(); + if (!mdl) { + SASSERT(m_upper == 0); + lbool is_sat = s.check_sat(0, 0); + if (is_sat == l_true) { + s.get_model(m_model); + } + mdl = m_model; + } } diff --git a/src/opt/core_maxsat.h b/src/opt/core_maxsat.h index cf4ce8d48..623868dc7 100644 --- a/src/opt/core_maxsat.h +++ b/src/opt/core_maxsat.h @@ -29,8 +29,9 @@ namespace opt { ast_manager& m; solver& s; expr_ref_vector m_soft; - expr_ref_vector m_answer; + svector m_answer; unsigned m_upper; + unsigned m_lower; model_ref m_model; public: core_maxsat(ast_manager& m, solver& s, expr_ref_vector& soft_constraints); @@ -38,8 +39,7 @@ namespace opt { virtual lbool operator()(); virtual rational get_lower() const; virtual rational get_upper() const; - virtual rational get_value() const; - virtual expr_ref_vector get_assignment() const; + virtual bool get_assignment(unsigned idx) const; virtual void set_cancel(bool f); virtual void collect_statistics(statistics& st) const; virtual void get_model(model_ref& mdl); diff --git a/src/opt/fu_malik.cpp b/src/opt/fu_malik.cpp index 4c15aedf0..4114ac080 100644 --- a/src/opt/fu_malik.cpp +++ b/src/opt/fu_malik.cpp @@ -49,7 +49,7 @@ namespace opt { expr_ref_vector m_soft; expr_ref_vector m_orig_soft; expr_ref_vector m_aux; - expr_ref_vector m_assignment; + svector m_assignment; unsigned m_upper; unsigned m_lower; model_ref m_model; @@ -63,12 +63,12 @@ namespace opt { m_soft(soft), m_orig_soft(soft), m_aux(m), - m_assignment(m), m_upper(0), m_lower(0), m_use_new_bv_solver(false) { m_upper = m_soft.size() + 1; + m_assignment.resize(m_soft.size(), false); } solver& s() { return *m_s; } @@ -286,44 +286,44 @@ namespace opt { // TBD: bug when cancel flag is set, fu_malik returns is_sat == l_true instead of l_undef lbool operator()() { + lbool is_sat = l_true; + if (m_soft.empty()) { + return is_sat; + } set_solver(); - lbool is_sat = s().check_sat(0,0); - if (!m_soft.empty() && is_sat == l_true) { - solver::scoped_push _sp(s()); - expr_ref tmp(m); - TRACE("opt", - tout << "soft constraints:\n"; - for (unsigned i = 0; i < m_soft.size(); ++i) { - tout << mk_pp(m_soft[i].get(), m) << "\n"; - }); - for (unsigned i = 0; i < m_soft.size(); ++i) { - m_aux.push_back(m.mk_fresh_const("p", m.mk_bool_sort())); - m_opt_solver.mc().insert(to_app(m_aux.back())->get_decl()); - tmp = m.mk_or(m_soft[i].get(), m_aux[i].get()); - s().assert_expr(tmp); - } - - lbool is_sat = l_true; - do { - is_sat = step(); - --m_upper; - } - while (is_sat == l_false); - - if (is_sat == l_true) { - // Get a list satisfying m_soft - s().get_model(m_model); - m_lower = m_upper; - m_assignment.reset(); - for (unsigned i = 0; i < m_orig_soft.size(); ++i) { - expr_ref val(m); - VERIFY(m_model->eval(m_orig_soft[i].get(), val)); - if (m.is_true(val)) { - m_assignment.push_back(m_orig_soft[i].get()); - } - } - TRACE("opt", tout << "maxsat cost: " << m_upper << "\n";); + solver::scoped_push _sp(s()); + expr_ref tmp(m); + + TRACE("opt", + tout << "soft constraints:\n"; + for (unsigned i = 0; i < m_soft.size(); ++i) { + tout << mk_pp(m_soft[i].get(), m) << "\n"; + }); + + for (unsigned i = 0; i < m_soft.size(); ++i) { + m_aux.push_back(m.mk_fresh_const("p", m.mk_bool_sort())); + m_opt_solver.mc().insert(to_app(m_aux.back())->get_decl()); + tmp = m.mk_or(m_soft[i].get(), m_aux[i].get()); + s().assert_expr(tmp); + } + + do { + is_sat = step(); + --m_upper; + } + while (is_sat == l_false); + + if (is_sat == l_true) { + // Get a list satisfying m_soft + s().get_model(m_model); + m_lower = m_upper; + m_assignment.reset(); + for (unsigned i = 0; i < m_orig_soft.size(); ++i) { + expr_ref val(m); + VERIFY(m_model->eval(m_orig_soft[i].get(), val)); + m_assignment.push_back(m.is_true(val)); } + TRACE("opt", tout << "maxsat cost: " << m_upper << "\n";); } // We are done and soft_constraints has // been updated with the max-sat assignment. @@ -347,16 +347,13 @@ namespace opt { return (*m_imp)(); } rational fu_malik::get_lower() const { - return rational(m_imp->m_lower); + return rational(m_imp->m_soft.size()-m_imp->m_upper); } rational fu_malik::get_upper() const { - return rational(m_imp->m_upper); + return rational(m_imp->m_soft.size()-m_imp->m_lower); } - rational fu_malik::get_value() const { - return rational(m_imp->m_assignment.size()); - } - expr_ref_vector fu_malik::get_assignment() const { - return m_imp->m_assignment; + bool fu_malik::get_assignment(unsigned idx) const { + return m_imp->m_assignment[idx]; } void fu_malik::set_cancel(bool f) { // no-op diff --git a/src/opt/fu_malik.h b/src/opt/fu_malik.h index df6c14a55..5dd0cbf50 100644 --- a/src/opt/fu_malik.h +++ b/src/opt/fu_malik.h @@ -38,8 +38,7 @@ namespace opt { virtual lbool operator()(); virtual rational get_lower() const; virtual rational get_upper() const; - virtual rational get_value() const; - virtual expr_ref_vector get_assignment() const; + virtual bool get_assignment(unsigned idx) const; virtual void set_cancel(bool f); virtual void collect_statistics(statistics& st) const; virtual void get_model(model_ref& m); diff --git a/src/opt/maxsmt.cpp b/src/opt/maxsmt.cpp index 369b26782..0d459c44d 100644 --- a/src/opt/maxsmt.cpp +++ b/src/opt/maxsmt.cpp @@ -28,14 +28,12 @@ namespace opt { lbool maxsmt::operator()(opt_solver& s) { lbool is_sat; - m_answer.reset(); m_msolver = 0; m_s = &s; if (m_soft_constraints.empty()) { TRACE("opt", tout << "no constraints\n";); m_msolver = 0; is_sat = s.check_sat(0, 0); - m_answer.reset(); } else if (is_maxsat_problem(m_weights)) { if (m_maxsat_engine == symbol("core_maxsat")) { @@ -51,7 +49,6 @@ namespace opt { if (m_msolver) { is_sat = (*m_msolver)(); - m_answer.append(m_msolver->get_assignment()); if (is_sat == l_true) { m_msolver->get_model(m_model); } @@ -75,16 +72,14 @@ namespace opt { return is_sat; } - expr_ref_vector maxsmt::get_assignment() const { - return m_answer; - } - - rational maxsmt::get_value() const { + bool maxsmt::get_assignment(unsigned idx) const { if (m_msolver) { - return m_msolver->get_value(); + return m_msolver->get_assignment(idx); } - return m_upper; - } + else { + return true; + } + } rational maxsmt::get_lower() const { rational r = m_lower; @@ -114,15 +109,29 @@ namespace opt { void maxsmt::commit_assignment() { SASSERT(m_s); - for (unsigned i = 0; i < m_answer.size(); ++i) { - m_s->assert_expr(m_answer[i].get()); + for (unsigned i = 0; i < m_soft_constraints.size(); ++i) { + expr_ref tmp(m); + tmp = m_soft_constraints[i].get(); + if (get_assignment(i)) { + m_s->assert_expr(tmp); + } + else { + tmp = m.mk_not(tmp); + m_s->assert_expr(tmp); + } } } void maxsmt::display_answer(std::ostream& out) const { - for (unsigned i = 0; i < m_answer.size(); ++i) { - out << mk_pp(m_answer[i], m) << "\n"; - } + for (unsigned i = 0; i < m_soft_constraints.size(); ++i) { + out << mk_pp(m_soft_constraints[i], m); + if (get_assignment(i)) { + out << " |-> true\n"; + } + else { + out << " |-> false\n"; + } + } } void maxsmt::set_cancel(bool f) { diff --git a/src/opt/maxsmt.h b/src/opt/maxsmt.h index b6d27f379..4a2822367 100644 --- a/src/opt/maxsmt.h +++ b/src/opt/maxsmt.h @@ -30,8 +30,7 @@ namespace opt { virtual lbool operator()() = 0; virtual rational get_lower() const = 0; virtual rational get_upper() const = 0; - virtual rational get_value() const = 0; - virtual expr_ref_vector get_assignment() const = 0; + virtual bool get_assignment(unsigned index) const = 0; virtual void set_cancel(bool f) = 0; virtual void collect_statistics(statistics& st) const = 0; virtual void get_model(model_ref& mdl) = 0; @@ -80,7 +79,7 @@ namespace opt { rational get_upper() const; void update_lower(rational const& r); void get_model(model_ref& mdl); - expr_ref_vector get_assignment() const; + bool get_assignment(unsigned index) const; void display_answer(std::ostream& out) const; void collect_statistics(statistics& st) const; diff --git a/src/opt/opt_context.cpp b/src/opt/opt_context.cpp index ce9fedf96..749fa071d 100644 --- a/src/opt/opt_context.cpp +++ b/src/opt/opt_context.cpp @@ -54,6 +54,7 @@ namespace opt { maxsmt* ms; if (!m_maxsmts.find(id, ms)) { ms = alloc(maxsmt, m); + ms->updt_params(m_params); m_maxsmts.insert(id, ms); m_objectives.push_back(objective(m, id)); m_indices.insert(id, m_objectives.size() - 1); @@ -352,6 +353,7 @@ namespace opt { obj.m_weights.append(weights); SASSERT(!m_maxsmts.contains(id)); maxsmt* ms = alloc(maxsmt, m); + ms->updt_params(m_params); m_maxsmts.insert(id, ms); m_indices.insert(id, index); } @@ -730,8 +732,14 @@ namespace opt { } break; } - case O_MAXSMT: + case O_MAXSMT: { + maxsmt& ms = *m_maxsmts.find(obj.m_id); + for (unsigned i = 0; i < obj.m_terms.size(); ++i) { + VERIFY(m_model->eval(obj.m_terms[i], val)); + SASSERT(ms.get_assignment(i) == (m.mk_true() == val)); + } break; + } } } } diff --git a/src/opt/optsmt.cpp b/src/opt/optsmt.cpp index 66d46f17c..97aec1e8c 100644 --- a/src/opt/optsmt.cpp +++ b/src/opt/optsmt.cpp @@ -296,9 +296,6 @@ namespace opt { return is_sat; } - inf_eps optsmt::get_value(unsigned i) const { - return get_lower(i); - } inf_eps optsmt::get_lower(unsigned i) const { return m_is_max[i]?m_lower[i]:-m_lower[i]; @@ -325,7 +322,7 @@ namespace opt { std::ostream& optsmt::display_objective(std::ostream& out, unsigned i) const { bool is_max = m_is_max[i]; - inf_eps val = get_value(i); + inf_eps val = get_lower(i); expr_ref obj(m_objs[i], m); if (!is_max) { arith_util a(m); @@ -344,7 +341,7 @@ namespace opt { << ":" << get_upper(i) << "]" << std::endl; } else { - display_objective(out, i) << " |-> " << get_value(i) << std::endl; + display_objective(out, i) << " |-> " << get_lower(i) << std::endl; } } } diff --git a/src/opt/optsmt.h b/src/opt/optsmt.h index 0de1e0319..1864e2a06 100644 --- a/src/opt/optsmt.h +++ b/src/opt/optsmt.h @@ -58,7 +58,6 @@ namespace opt { unsigned get_num_objectives() const { return m_objs.size(); } void commit_assignment(unsigned index); - inf_eps get_value(unsigned index) const; inf_eps get_lower(unsigned index) const; inf_eps get_upper(unsigned index) const; void get_model(model_ref& mdl); diff --git a/src/opt/weighted_maxsat.cpp b/src/opt/weighted_maxsat.cpp index 787625136..99d9287a5 100644 --- a/src/opt/weighted_maxsat.cpp +++ b/src/opt/weighted_maxsat.cpp @@ -46,15 +46,16 @@ namespace smt { /** \brief return the complement of variables that are currently assigned. */ - void get_assignment(expr_ref_vector& result) { + void get_assignment(svector& result) { result.reset(); std::sort(m_cost_save.begin(), m_cost_save.end()); for (unsigned i = 0, j = 0; i < m_vars.size(); ++i) { if (j < m_cost_save.size() && m_cost_save[j] == i) { + result.push_back(false); ++j; } else { - result.push_back(m_fmls[i].get()); + result.push_back(true); } } } @@ -282,15 +283,17 @@ namespace opt { ast_manager& m; opt_solver& s; expr_ref_vector m_soft; - expr_ref_vector m_assignment; + svector m_assignment; vector m_weights; rational m_upper; rational m_lower; model_ref m_model; imp(ast_manager& m, opt_solver& s, expr_ref_vector& soft_constraints, vector const& weights): - m(m), s(s), m_soft(soft_constraints), m_assignment(m), m_weights(weights) - {} + m(m), s(s), m_soft(soft_constraints), m_weights(weights) + { + m_assignment.resize(m_soft.size(), false); + } ~imp() {} smt::theory_weighted_maxsat* get_theory() const { @@ -333,9 +336,9 @@ namespace opt { wth.assert_weighted(m_soft[i].get(), m_weights[i]); } result = s.check_sat_core(0,0); - + SASSERT(result != l_true); wth.get_assignment(m_assignment); - if (!m_assignment.empty() && result == l_false) { + if (result == l_false) { result = l_true; } } @@ -382,11 +385,8 @@ namespace opt { rational wmaxsmt::get_upper() const { return m_imp->get_upper(); } - rational wmaxsmt::get_value() const { - return m_imp->get_upper(); - } - expr_ref_vector wmaxsmt::get_assignment() const { - return m_imp->m_assignment; + bool wmaxsmt::get_assignment(unsigned idx) const { + return m_imp->m_assignment[idx]; } void wmaxsmt::set_cancel(bool f) { // no-op diff --git a/src/opt/weighted_maxsat.h b/src/opt/weighted_maxsat.h index 01793b949..deae79893 100644 --- a/src/opt/weighted_maxsat.h +++ b/src/opt/weighted_maxsat.h @@ -36,8 +36,7 @@ namespace opt { virtual lbool operator()(); virtual rational get_lower() const; virtual rational get_upper() const; - virtual rational get_value() const; - virtual expr_ref_vector get_assignment() const; + virtual bool get_assignment(unsigned idx) const; virtual void set_cancel(bool f); virtual void collect_statistics(statistics& st) const; virtual void get_model(model_ref& mdl);