From 293a97bdfc962345112065465217a3799bdcc8db Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 9 Nov 2013 15:54:38 -0800 Subject: [PATCH] working on core-maxsat Signed-off-by: Nikolaj Bjorner --- src/opt/core_maxsat.cpp | 30 ++++++++++++++++++++++++------ src/opt/core_maxsat.h | 1 + src/opt/fu_malik.h | 10 +++++----- src/opt/maxsmt.cpp | 13 +++++++++++-- src/opt/maxsmt.h | 3 ++- src/opt/opt_params.pyg | 1 + src/smt/theory_card.cpp | 16 ++++++++-------- 7 files changed, 52 insertions(+), 22 deletions(-) diff --git a/src/opt/core_maxsat.cpp b/src/opt/core_maxsat.cpp index b0234c6cf..0ea239854 100644 --- a/src/opt/core_maxsat.cpp +++ b/src/opt/core_maxsat.cpp @@ -18,6 +18,7 @@ Notes: --*/ #include "core_maxsat.h" #include "card_decl_plugin.h" +#include "ast_pp.h" namespace opt { @@ -36,9 +37,9 @@ namespace opt { solver::scoped_push _sp(s); for (unsigned i = 0; i < m_soft.size(); ++i) { expr* a = m.mk_fresh_const("p", m.mk_bool_sort()); - aux.push_back(a); - s.assert_expr(m.mk_implies(a, m_soft[i].get())); - block_vars.insert(a); + aux.push_back(m.mk_not(a)); + s.assert_expr(m.mk_or(a, m_soft[i].get())); + block_vars.insert(aux.back()); } while (m_answer.size() < m_upper) { ptr_vector vars; @@ -60,20 +61,30 @@ namespace opt { ans.push_back(m_soft[i].get()); } } + TRACE("opt", tout << "sat\n"; + for (unsigned i = 0; i < ans.size(); ++i) { + tout << mk_pp(ans[i].get(), m) << "\n"; + }); if (ans.size() > m_answer.size()) { m_answer.reset(); m_answer.append(ans); } - unsigned k = m_soft.size()-m_answer.size()-1; // TBD: fix this + unsigned k = m_soft.size()-m_answer.size()-1; expr_ref fml = mk_at_most(core_vars, k); + TRACE("opt", tout << "add: " << fml << "\n";); s.assert_expr(fml); break; } case l_false: { ptr_vector core; s.get_unsat_core(core); + TRACE("opt", tout << "core"; + for (unsigned i = 0; i < core.size(); ++i) { + tout << mk_pp(core[i], m) << " "; + } + tout << "\n";); for (unsigned i = 0; i < core.size(); ++i) { - core_vars.insert(core[i]); + core_vars.insert(get_not(core[i])); block_vars.remove(core[i]); } if (core.empty()) { @@ -84,9 +95,10 @@ namespace opt { // at least one core variable is True expr_ref fml = mk_at_most(core_vars, 0); fml = m.mk_not(fml); + TRACE("opt", tout << "add: " << fml << "\n";); s.assert_expr(fml); } - --m_upper; + --m_upper; } } } @@ -107,6 +119,12 @@ namespace opt { set2vector(set, es); return expr_ref(card.mk_at_most_k(es.size(), es.c_ptr(), k), m); } + + expr* core_maxsat::get_not(expr* e) const { + expr* result = 0; + VERIFY(m.is_not(e, result)); + return result; + } rational core_maxsat::get_lower() const { return rational(m_answer.size()); diff --git a/src/opt/core_maxsat.h b/src/opt/core_maxsat.h index eebcf1d91..b5ee6e422 100644 --- a/src/opt/core_maxsat.h +++ b/src/opt/core_maxsat.h @@ -44,6 +44,7 @@ namespace opt { private: void set2vector(expr_set const& set, ptr_vector& es) const; expr_ref mk_at_most(expr_set const& set, unsigned k); + expr* get_not(expr* e) const; }; }; diff --git a/src/opt/fu_malik.h b/src/opt/fu_malik.h index 48be07316..9375e29c2 100644 --- a/src/opt/fu_malik.h +++ b/src/opt/fu_malik.h @@ -6,6 +6,7 @@ Module Name: fu_malik.h Abstract: + Fu&Malik built-in optimization method. Adapted from sample code in C. @@ -15,6 +16,10 @@ Author: Notes: + Takes solver with hard constraints added. + Returns a maximal satisfying subset of soft_constraints + that are still consistent with the solver state. + --*/ #ifndef _OPT_FU_MALIK_H_ #define _OPT_FU_MALIK_H_ @@ -23,11 +28,6 @@ Notes: #include "maxsmt.h" namespace opt { - /** - Takes solver with hard constraints added. - Returns a maximal satisfying subset of soft_constraints - that are still consistent with the solver state. - */ class fu_malik : public maxsmt_solver { struct imp; diff --git a/src/opt/maxsmt.cpp b/src/opt/maxsmt.cpp index 9603286d1..b2f09f3c1 100644 --- a/src/opt/maxsmt.cpp +++ b/src/opt/maxsmt.cpp @@ -3,7 +3,7 @@ Copyright (c) 2013 Microsoft Corporation Module Name: - opt_maxsmt.cpp + maxsmt.cpp Abstract: @@ -19,8 +19,10 @@ Notes: #include "maxsmt.h" #include "fu_malik.h" +#include "core_maxsat.h" #include "weighted_maxsat.h" #include "ast_pp.h" +#include "opt_params.hpp" namespace opt { @@ -35,7 +37,12 @@ namespace opt { m_answer.append(m_soft_constraints); } else if (is_maxsat_problem(m_weights)) { - m_msolver = alloc(fu_malik, m, s, m_soft_constraints); + if (m_maxsat_engine == symbol("core_maxsat")) { + m_msolver = alloc(core_maxsat, m, s, m_soft_constraints); + } + else { + m_msolver = alloc(fu_malik, m, s, m_soft_constraints); + } } else { m_msolver = alloc(wmaxsmt, m, opt_solver::to_opt(s), m_soft_constraints, m_weights); @@ -110,6 +117,8 @@ namespace opt { } void maxsmt::updt_params(params_ref& p) { + opt_params _p(p); + m_maxsat_engine = _p.maxsat_engine(); } diff --git a/src/opt/maxsmt.h b/src/opt/maxsmt.h index e3105847d..b6bb15e52 100644 --- a/src/opt/maxsmt.h +++ b/src/opt/maxsmt.h @@ -3,7 +3,7 @@ Copyright (c) 2013 Microsoft Corporation Module Name: - opt_maxsmt.h + maxsmt.h Abstract: @@ -47,6 +47,7 @@ namespace opt { expr_ref_vector m_answer; vector m_weights; scoped_ptr m_msolver; + symbol m_maxsat_engine; public: maxsmt(ast_manager& m): m(m), m_s(0), m_cancel(false), m_soft_constraints(m), m_answer(m) {} diff --git a/src/opt/opt_params.pyg b/src/opt/opt_params.pyg index 3c2381040..983c3ed73 100644 --- a/src/opt/opt_params.pyg +++ b/src/opt/opt_params.pyg @@ -3,6 +3,7 @@ def_module_params('opt', export=True, params=(('timeout', UINT, UINT_MAX, 'set timeout'), ('engine', SYMBOL, 'basic', "select optimization engine: 'basic', 'farkas', 'symba'"), + ('maxsat_engine', SYMBOL, 'fu_malik', "select engine for non-weighted maxsat: 'fu_malik', 'core_maxsat'"), ('pareto', BOOL, False, 'return a Pareto front (as opposed to a bounding box)'), )) diff --git a/src/smt/theory_card.cpp b/src/smt/theory_card.cpp index 4cd23d225..af8c2cdff 100644 --- a/src/smt/theory_card.cpp +++ b/src/smt/theory_card.cpp @@ -453,19 +453,19 @@ namespace smt { void theory_card::pop_scope_eh(unsigned num_scopes) { unsigned sz = m_watch_lim[m_watch_lim.size()-num_scopes]; - for (unsigned i = m_watch_trail.size(); i > sz; ) { - --i; + while (m_watch_trail.size() > sz) { ptr_vector* cards = 0; - VERIFY(m_watch.find(m_watch_trail[i], cards)); + VERIFY(m_watch.find(m_watch_trail.back(), cards)); SASSERT(cards && !cards->empty()); cards->pop_back(); + m_watch_trail.pop_back(); } m_watch_lim.resize(m_watch_lim.size()-num_scopes); sz = m_cards_lim[m_cards_lim.size()-num_scopes]; - for (unsigned i = m_cards_trail.size(); i > sz; ) { - --i; - SASSERT(m_cards.contains(m_cards_trail[i])); - m_cards.remove(m_cards_trail[i]); + while (m_cards_trail.size() > sz) { + SASSERT(m_cards.contains(m_cards_trail.back())); + m_cards.remove(m_cards_trail.back()); + m_cards_trail.pop_back(); } m_cards_lim.resize(m_cards_lim.size()-num_scopes); } @@ -482,7 +482,7 @@ namespace smt { TRACE("card", ctx.display_literals_verbose(tout, lits.size(), lits.c_ptr()); tout << "\n";); justification* js = 0; ctx.mk_clause(lits.size(), lits.c_ptr(), js, CLS_AUX_LEMMA, 0); - IF_VERBOSE(0, + IF_VERBOSE(1, for (unsigned i = 0; i < lits.size(); ++i) { verbose_stream() << lits[i] << " "; }