From 13f05ae9dc93ea77c6d46a71806f80a7dd0b8744 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 28 Feb 2021 09:59:36 -0800 Subject: [PATCH] enable wcnf output for weighted maxsat problems --- src/ast/display_dimacs.cpp | 132 ++++++++++++++++++++++++------------- src/ast/display_dimacs.h | 2 +- src/opt/opt_context.cpp | 18 ++++- src/opt/opt_context.h | 11 ++-- src/opt/opt_params.pyg | 1 + src/sat/sat_solver.cpp | 11 ++-- 6 files changed, 115 insertions(+), 60 deletions(-) diff --git a/src/ast/display_dimacs.cpp b/src/ast/display_dimacs.cpp index 50a1ff6d0..6b2ef6658 100644 --- a/src/ast/display_dimacs.cpp +++ b/src/ast/display_dimacs.cpp @@ -20,14 +20,21 @@ Revision History: #include "ast.h" #include "display_dimacs.h" -std::ostream& display_dimacs(std::ostream& out, expr_ref_vector const& fmls, bool include_names) { - ast_manager& m = fmls.m(); +struct dimacs_pp { + ast_manager& m; unsigned_vector expr2var; ptr_vector exprs; - unsigned num_vars = 0; - unsigned num_cls = fmls.size(); - bool is_from_dimacs = true; - for (expr * f : fmls) { + unsigned num_vars { 0 }; + + dimacs_pp(ast_manager& m): m(m) {} + + void reset() { + num_vars = 0; + expr2var.reset(); + exprs.reset(); + } + + bool init_from_dimacs(expr* f) { unsigned num_lits; expr * const * lits; if (m.is_or(f)) { @@ -42,10 +49,8 @@ std::ostream& display_dimacs(std::ostream& out, expr_ref_vector const& fmls, boo expr * l = lits[j]; if (m.is_not(l)) l = to_app(l)->get_arg(0); - if (!is_uninterp_const(l)) { - is_from_dimacs = false; - break; - } + if (!is_uninterp_const(l)) + return false; symbol const& s = to_app(l)->get_decl()->get_name(); if (s.is_numerical() && s.get_num() > 0) { if (expr2var.get(l->get_id(), UINT_MAX) == UINT_MAX) { @@ -55,43 +60,35 @@ std::ostream& display_dimacs(std::ostream& out, expr_ref_vector const& fmls, boo } continue; } - is_from_dimacs = false; - break; + return false; } - if (!is_from_dimacs) { - num_vars = 0; - expr2var.reset(); - exprs.reset(); - break; + return true; + } + + void init_formula(expr* f) { + unsigned num_lits; + expr * const * lits; + if (m.is_or(f)) { + num_lits = to_app(f)->get_num_args(); + lits = to_app(f)->get_args(); } - } - - if (!is_from_dimacs) { - for (expr * f : fmls) { - unsigned num_lits; - expr * const * lits; - if (m.is_or(f)) { - num_lits = to_app(f)->get_num_args(); - lits = to_app(f)->get_args(); - } - else { - num_lits = 1; - lits = &f; - } - for (unsigned j = 0; j < num_lits; j++) { - expr * l = lits[j]; - if (m.is_not(l)) - l = to_app(l)->get_arg(0); - if (expr2var.get(l->get_id(), UINT_MAX) == UINT_MAX) { - num_vars++; - expr2var.setx(l->get_id(), num_vars, UINT_MAX); - exprs.setx(l->get_id(), l, nullptr); - } + else { + num_lits = 1; + lits = &f; + } + for (unsigned j = 0; j < num_lits; j++) { + expr * l = lits[j]; + if (m.is_not(l)) + l = to_app(l)->get_arg(0); + if (expr2var.get(l->get_id(), UINT_MAX) == UINT_MAX) { + num_vars++; + expr2var.setx(l->get_id(), num_vars, UINT_MAX); + exprs.setx(l->get_id(), l, nullptr); } } } - out << "p cnf " << num_vars << " " << num_cls << "\n"; - for (expr* f : fmls) { + + void pp_formula(std::ostream& out, expr* f) { unsigned num_lits; expr * const * lits; if (m.is_or(f)) { @@ -113,18 +110,61 @@ std::ostream& display_dimacs(std::ostream& out, expr_ref_vector const& fmls, boo } out << "0\n"; } - if (include_names && !is_from_dimacs) { - for (expr* e : exprs) { + + void pp_defs(std::ostream& out) { + for (expr* e : exprs) if (e && is_app(e)) { symbol const& n = to_app(e)->get_decl()->get_name(); out << "c " << expr2var[e->get_id()] << " " << n << "\n"; } + } + +}; + +std::ostream& display_dimacs(std::ostream& out, expr_ref_vector const& fmls, bool include_names) { + ast_manager& m = fmls.m(); + dimacs_pp pp(m); + unsigned num_cls = fmls.size(); + bool is_from_dimacs = true; + for (expr * f : fmls) { + is_from_dimacs = pp.init_from_dimacs(f); + if (!is_from_dimacs) + break; + } + + if (!is_from_dimacs) { + pp.reset(); + for (expr * f : fmls) { + pp.init_formula(f); } } + out << "p cnf " << pp.num_vars << " " << num_cls << "\n"; + for (expr* f : fmls) + pp.pp_formula(out, f); + if (include_names && !is_from_dimacs) + pp.pp_defs(out); return out; } -std::ostream& display_wcnf(std::ostream& out, expr_ref_vector const& fmls, vector> const& soft, bool include_names) { - NOT_IMPLEMENTED_YET(); +std::ostream& display_wcnf(std::ostream& out, expr_ref_vector const& fmls, svector> const& soft) { + ast_manager& m = fmls.m(); + dimacs_pp pp(m); + for (expr* f : fmls) + pp.init_formula(f); + for (auto s : soft) + pp.init_formula(s.first); + out << "p wcnf " << pp.num_vars << " " << fmls.size() + soft.size() << "\n"; + unsigned sum_soft = 1; + for (auto s : soft) + sum_soft += s.second; + for (expr* f : fmls) { + out << sum_soft << " "; + pp.pp_formula(out, f); + } + for (auto s : soft) { + out << s.second << " "; + pp.pp_formula(out, s.first); + } + pp.pp_defs(out); return out; } diff --git a/src/ast/display_dimacs.h b/src/ast/display_dimacs.h index a50684682..0af4dc4a0 100644 --- a/src/ast/display_dimacs.h +++ b/src/ast/display_dimacs.h @@ -22,5 +22,5 @@ Revision History: std::ostream& display_dimacs(std::ostream& out, expr_ref_vector const& fmls, bool include_names); -std::ostream& display_wcnf(std::ostream& out, expr_ref_vector const& fmls, vector> const& soft, bool include_names); +std::ostream& display_wcnf(std::ostream& out, expr_ref_vector const& fmls, svector> const& soft); diff --git a/src/opt/opt_context.cpp b/src/opt/opt_context.cpp index 2307c2488..429b537b9 100644 --- a/src/opt/opt_context.cpp +++ b/src/opt/opt_context.cpp @@ -24,6 +24,7 @@ Notes: #include "ast/pb_decl_plugin.h" #include "ast/ast_smt_pp.h" #include "ast/ast_pp_util.h" +#include "ast/display_dimacs.h" #include "model/model_smt2_pp.h" #include "tactic/goal.h" #include "tactic/tactic.h" @@ -1540,9 +1541,12 @@ namespace opt { m_enable_sls = _p.enable_sls(); m_maxsat_engine = _p.maxsat_engine(); m_pp_neat = _p.pp_neat(); + m_pp_wcnf = _p.pp_wcnf(); } - std::string context::to_string() const { + std::string context::to_string() { + if (m_pp_wcnf) + return to_wcnf(); return to_string(false, m_scoped_state.m_hard, m_scoped_state.m_objectives); } @@ -1557,6 +1561,9 @@ namespace opt { auto const& objectives = m_objectives; if (objectives.size() > 1) throw default_exception("only single objective weighted MaxSAT wcnf output is supported"); + ptr_vector soft_f; + vector soft_w; + svector> soft; if (objectives.size() == 1) { auto const& obj = objectives[0]; if (obj.m_type != O_MAXSMT) @@ -1565,10 +1572,15 @@ namespace opt { rational w = obj.m_weights[j]; if (!w.is_unsigned()) throw default_exception("only single objective weighted MaxSAT wcnf output is supported"); + soft_f.push_back(obj.m_terms[j]); + soft_w.push_back(w); } } - NOT_IMPLEMENTED_YET(); - return std::string(""); + std::ostringstream strm; + m_sat_solver = mk_inc_sat_solver(m, m_params); + m_sat_solver->assert_expr(m_hard_constraints); + inc_sat_display(strm, *m_sat_solver.get(), soft_f.size(), soft_f.c_ptr(), soft_w.c_ptr()); + return strm.str(); } std::string context::to_string(bool is_internal, expr_ref_vector const& hard, vector const& objectives) const { diff --git a/src/opt/opt_context.h b/src/opt/opt_context.h index 8a6df7129..28cff40d3 100644 --- a/src/opt/opt_context.h +++ b/src/opt/opt_context.h @@ -179,10 +179,11 @@ namespace opt { func_decl_ref_vector m_objective_refs; expr_ref_vector m_core; tactic_ref m_simplify; - bool m_enable_sat; - bool m_enable_sls; - bool m_is_clausal; - bool m_pp_neat; + bool m_enable_sat { true } ; + bool m_enable_sls { false }; + bool m_is_clausal { false }; + bool m_pp_neat { true }; + bool m_pp_wcnf { false }; symbol m_maxsat_engine; symbol m_logic; svector m_labels; @@ -232,7 +233,7 @@ namespace opt { void get_lower(unsigned idx, expr_ref_vector& es) { to_exprs(get_lower_as_num(idx), es); } void get_upper(unsigned idx, expr_ref_vector& es) { to_exprs(get_upper_as_num(idx), es); } - std::string to_string() const; + std::string to_string(); unsigned num_objectives() override { return m_scoped_state.m_objectives.size(); } diff --git a/src/opt/opt_params.pyg b/src/opt/opt_params.pyg index 2192ed9ce..5106c5492 100644 --- a/src/opt/opt_params.pyg +++ b/src/opt/opt_params.pyg @@ -16,6 +16,7 @@ def_module_params('opt', ('elim_01', BOOL, True, 'eliminate 01 variables'), ('pp.neat', BOOL, True, 'use neat (as opposed to less readable, but faster) pretty printer when displaying context'), ('pb.compile_equality', BOOL, False, 'compile arithmetical equalities into pseudo-Boolean equality (instead of two inequalites)'), + ('pp.wcnf', BOOL, False, 'print maxsat benchmark into wcnf format'), ('maxlex.enable', BOOL, True, 'enable maxlex heuristic for lexicographic MaxSAT problems'), ('maxres.hill_climb', BOOL, True, 'give preference for large weight cores'), ('maxres.add_upper_bound_block', BOOL, False, 'restict upper bound with constraint'), diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp index b156e6694..301140eb1 100644 --- a/src/sat/sat_solver.cpp +++ b/src/sat/sat_solver.cpp @@ -4002,17 +4002,18 @@ namespace sat { void solver::display_wcnf(std::ostream & out, unsigned sz, literal const* lits, unsigned const* weights) const { unsigned max_weight = 0; - for (unsigned i = 0; i < sz; ++i) { - max_weight = std::max(max_weight, weights[i]); - } + for (unsigned i = 0; i < sz; ++i) + max_weight += weights[i]; ++max_weight; + if (m_ext) + throw default_exception("wcnf is only supported for pure CNF problems"); + out << "p wcnf " << num_vars() << " " << num_clauses() + sz << " " << max_weight << "\n"; out << "c soft " << sz << "\n"; - for (literal lit : m_trail) { + for (literal lit : m_trail) out << max_weight << " " << dimacs_lit(lit) << " 0\n"; - } unsigned l_idx = 0; for (watch_list const& wlist : m_watches) { literal l = ~to_literal(l_idx);