From 489df0760f69dfed704e5fd035c2f89c6d0da094 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 2 Feb 2021 13:03:54 -0800 Subject: [PATCH] experiments with LNS --- src/ast/pb_decl_plugin.h | 2 ++ src/opt/maxres.cpp | 18 ++++++++++ src/opt/opt_lns.cpp | 72 +++++++++++++++++++++++++++++++--------- src/opt/opt_lns.h | 9 ++++- 4 files changed, 85 insertions(+), 16 deletions(-) diff --git a/src/ast/pb_decl_plugin.h b/src/ast/pb_decl_plugin.h index dafce43f2..33f2f11cc 100644 --- a/src/ast/pb_decl_plugin.h +++ b/src/ast/pb_decl_plugin.h @@ -90,6 +90,8 @@ public: family_id get_family_id() const { return m_fid; } app * mk_at_most_k(unsigned num_args, expr * const * args, unsigned k); app * mk_at_least_k(unsigned num_args, expr * const * args, unsigned k); + app * mk_at_most_k(expr_ref_vector const& args, unsigned k) { return mk_at_most_k(args.size(), args.c_ptr(), k); } + app * mk_at_least_k(expr_ref_vector const& args, unsigned k) { return mk_at_least_k(args.size(), args.c_ptr(), k); } app * mk_le(unsigned num_args, rational const * coeffs, expr * const * args, rational const& k); app * mk_ge(unsigned num_args, rational const * coeffs, expr * const * args, rational const& k); app * mk_eq(unsigned num_args, rational const * coeffs, expr * const * args, rational const& k); diff --git a/src/opt/maxres.cpp b/src/opt/maxres.cpp index 722bebc8c..139b22ca2 100644 --- a/src/opt/maxres.cpp +++ b/src/opt/maxres.cpp @@ -502,6 +502,7 @@ public: for (auto const & c : cores) { process_unsat(c.m_core, c.m_weight); } + improve_model(m_model); } void update_model(expr* def, expr* value) { @@ -748,11 +749,28 @@ public: std::function update_model = [&](model_ref& mdl) { update_assignment(mdl); }; + std::function const&)> _relax_cores = [&](vector const& cores) { + relax_cores(cores); + }; + lns lns(s(), update_model); lns.set_conflicts(m_lns_conflicts); + lns.set_relax(_relax_cores); lns.climb(mdl, m_asms); } + void relax_cores(vector const& cores) { + vector wcores; + for (auto & core : cores) { + exprs _core(core.size(), core.c_ptr()); + wcores.push_back(weighted_core(_core, core_weight(_core))); + remove_soft(_core, m_asms); + split_core(_core); + } + process_unsat(wcores); + } + + void update_assignment(model_ref & mdl) { improve_model(mdl); mdl->set_model_completion(true); diff --git a/src/opt/opt_lns.cpp b/src/opt/opt_lns.cpp index a9439cf22..21ba939e1 100644 --- a/src/opt/opt_lns.cpp +++ b/src/opt/opt_lns.cpp @@ -17,6 +17,7 @@ Author: #include "ast/ast_ll_pp.h" #include "ast/ast_pp.h" +#include "ast/pb_decl_plugin.h" #include "opt/maxsmt.h" #include "opt/opt_lns.h" #include "sat/sat_params.hpp" @@ -38,6 +39,7 @@ namespace opt { p.set_uint("restart.initial", 1000000); p.set_uint("max_conflicts", m_max_conflicts); p.set_uint("simplify.delay", 1000000); +// p.set_bool("gc.burst", true); s.updt_params(p); } @@ -47,6 +49,7 @@ namespace opt { p.set_uint("restart.initial", sp.restart_initial()); p.set_uint("max_conflicts", sp.max_conflicts()); p.set_uint("simplify.delay", sp.simplify_delay()); + p.set_uint("gc.burst", sp.gc_burst()); } unsigned lns::climb(model_ref& mdl, expr_ref_vector const& asms) { @@ -56,22 +59,63 @@ namespace opt { set_lns_params(); setup_assumptions(mdl, asms); unsigned num_improved = improve_linear(mdl); -// num_improved += improve_rotate(mdl, asms); + // num_improved += improve_rotate(mdl, asms); s.updt_params(old_p); IF_VERBOSE(1, verbose_stream() << "(opt.lns :num-improves " << m_num_improves << " :remaining-soft " << m_soft.size() << ")\n"); return num_improved; } + struct lns::scoped_bounding { + lns& m_lns; + bool m_cores_are_valid { true }; + + scoped_bounding(lns& l):m_lns(l) { + if (!m_lns.m_enable_scoped_bounding) + return; + m_cores_are_valid = m_lns.m_cores_are_valid; + m_lns.m_cores_are_valid = false; + m_lns.s.push(); + pb_util pb(m_lns.m); + // TBD: bound should to be adjusted for current best solution, not number of soft constraints left. + expr_ref bound(pb.mk_at_most_k(m_lns.m_soft, m_lns.m_soft.size() - 1), m_lns.m); + m_lns.s.assert_expr(bound); + } + ~scoped_bounding() { + if (!m_lns.m_enable_scoped_bounding) + return; + m_lns.m_cores_are_valid = m_cores_are_valid; + m_lns.s.pop(1); + } + }; + + void lns::relax_cores() { + if (!m_cores.empty() && m_relax_cores && m_cores_are_valid) { + std::sort(m_cores.begin(), m_cores.end(), [&](expr_ref_vector const& a, expr_ref_vector const& b) { return a.size() < b.size(); }); + unsigned num_disjoint = 0; + vector new_cores; + for (auto const& c : m_cores) { + bool in_core = false; + for (auto* e : c) + in_core |= m_in_core.is_marked(e); + if (in_core) + continue; + for (auto* e : c) + m_in_core.mark(e); + new_cores.push_back(c); + ++num_disjoint; + } + m_relax_cores(new_cores); + } + m_in_core.reset(); + m_is_assumption.reset(); + m_cores.reset(); + } + void lns::setup_assumptions(model_ref& mdl, expr_ref_vector const& asms) { m_hardened.reset(); m_soft.reset(); - std::cout << "disjoint cores: " << m_cores.size() << "\n"; - for (auto const& c : m_cores) - std::cout << c.size() << "\n"; - m_was_flipped.reset(); - m_in_core.reset(); - m_cores.reset(); for (expr* a : asms) { + m_is_assumption.mark(a); if (mdl->is_true(a)) m_hardened.push_back(a); else @@ -98,9 +142,11 @@ namespace opt { } unsigned lns::improve_linear(model_ref& mdl) { + scoped_bounding _scoped_bouding(*this); unsigned num_improved = 0; unsigned max_conflicts = m_max_conflicts; while (m.inc()) { + unsigned hard = m_hardened.size(); unsigned reward = improve_step(mdl); if (reward == 0) break; @@ -110,6 +156,7 @@ namespace opt { set_lns_params(); } m_max_conflicts = max_conflicts; + relax_cores(); return num_improved; } @@ -124,7 +171,6 @@ namespace opt { m_hardened.push_back(m.mk_not(soft(i))); for (unsigned k = i; k + 1 < m_soft.size(); ++k) m_soft[k] = soft(k + 1); - m_was_flipped.mark(m_hardened.back()); m_soft.pop_back(); --i; break; @@ -160,20 +206,16 @@ namespace opt { m_hardened.pop_back(); if (r == l_true) s.get_model(mdl); -#if 0 if (r == l_false) { expr_ref_vector core(m); s.get_unsat_core(core); - bool was_flipped = false; + bool all_assumed = true; for (expr* c : core) - was_flipped |= m_was_flipped.is_marked(c); - if (!was_flipped) { - for (expr* c : core) - m_in_core.mark(c, true); + all_assumed &= m_is_assumption.is_marked(c); + if (all_assumed) { m_cores.push_back(core); } } -#endif return r; } diff --git a/src/opt/opt_lns.h b/src/opt/opt_lns.h index 41e33ab81..26b4c6e4a 100644 --- a/src/opt/opt_lns.h +++ b/src/opt/opt_lns.h @@ -33,24 +33,31 @@ namespace opt { expr_ref_vector m_soft; unsigned m_max_conflicts { 1000 }; unsigned m_num_improves { 0 }; + bool m_cores_are_valid { true }; + bool m_enable_scoped_bounding { false }; vector m_cores; expr_mark m_in_core; - expr_mark m_was_flipped; + expr_mark m_is_assumption; + + struct scoped_bounding; std::function m_update_model; + std::function const&)> m_relax_cores; expr* soft(unsigned i) const { return m_soft[i]; } void set_lns_params(); void save_defaults(params_ref& p); unsigned improve_step(model_ref& mdl); lbool improve_step(model_ref& mdl, expr* e); + void relax_cores(); unsigned improve_linear(model_ref& mdl); unsigned improve_rotate(model_ref& mdl, expr_ref_vector const& asms); void setup_assumptions(model_ref& mdl, expr_ref_vector const& asms); public: lns(solver& s, std::function& update_model); + void set_relax(std::function const&)>& rc) { m_relax_cores = rc; } void set_conflicts(unsigned c) { m_max_conflicts = c; } unsigned climb(model_ref& mdl, expr_ref_vector const& asms); };