diff --git a/src/opt/CMakeLists.txt b/src/opt/CMakeLists.txt index 3f1d8253c..28a14be2e 100644 --- a/src/opt/CMakeLists.txt +++ b/src/opt/CMakeLists.txt @@ -5,7 +5,6 @@ z3_add_component(opt mss.cpp opt_cmds.cpp opt_context.cpp - opt_lns.cpp opt_pareto.cpp opt_parse.cpp optsmt.cpp diff --git a/src/opt/opt_context.cpp b/src/opt/opt_context.cpp index 33aaa0b27..0793e5c53 100644 --- a/src/opt/opt_context.cpp +++ b/src/opt/opt_context.cpp @@ -254,9 +254,6 @@ namespace opt { if (m_pareto) { return execute_pareto(); } - if (m_lns) { - return execute_lns(); - } if (m_box_index != UINT_MAX) { return execute_box(); } @@ -276,9 +273,6 @@ namespace opt { opt_params optp(m_params); symbol pri = optp.priority(); - if (pri == symbol("lns")) { - return execute_lns(); - } IF_VERBOSE(1, verbose_stream() << "(optimize:check-sat)\n"); lbool is_sat = s.check_sat(0,0); @@ -311,9 +305,6 @@ namespace opt { if (pri == symbol("pareto")) { is_sat = execute_pareto(); } - else if (pri == symbol("lns")) { - is_sat = execute_lns(); - } else if (pri == symbol("box")) { is_sat = execute_box(); } @@ -536,12 +527,8 @@ namespace opt { } void context::yield() { - if (m_pareto) { - m_pareto->get_model(m_model, m_labels); - } - else if (m_lns) { - m_lns->get_model(m_model, m_labels); - } + SASSERT (m_pareto); + m_pareto->get_model(m_model, m_labels); update_bound(true); update_bound(false); } @@ -560,19 +547,6 @@ namespace opt { return is_sat; } - lbool context::execute_lns() { - if (!m_lns) { - m_lns = alloc(lns, *this, m_solver.get()); - } - lbool is_sat = (*(m_lns.get()))(); - if (is_sat != l_true) { - m_lns = nullptr; - } - if (is_sat == l_true) { - yield(); - } - return l_undef; - } std::string context::reason_unknown() const { if (m.canceled()) { @@ -1020,23 +994,6 @@ namespace opt { } } - /** - \brief retrieve literals used by the neighborhood search feature. - */ - - void context::get_lns_literals(expr_ref_vector& lits) { - for (objective & obj : m_objectives) { - switch(obj.m_type) { - case O_MAXSMT: - for (expr* f : obj.m_terms) { - lits.push_back(f); - } - break; - default: - break; - } - } - } bool context::verify_model(unsigned index, model* md, rational const& _v) { rational r; @@ -1401,7 +1358,6 @@ namespace opt { void context::clear_state() { m_pareto = nullptr; - m_lns = nullptr; m_box_index = UINT_MAX; m_model.reset(); } diff --git a/src/opt/opt_context.h b/src/opt/opt_context.h index 9f55d5ca1..abc6268dd 100644 --- a/src/opt/opt_context.h +++ b/src/opt/opt_context.h @@ -27,7 +27,6 @@ Notes: #include "opt/opt_solver.h" #include "opt/opt_pareto.h" #include "opt/optsmt.h" -#include "opt/opt_lns.h" #include "opt/maxsmt.h" #include "cmd_context/cmd_context.h" @@ -147,7 +146,6 @@ namespace opt { ref m_solver; ref m_sat_solver; scoped_ptr m_pareto; - scoped_ptr m_lns; scoped_ptr m_qmax; sref_vector m_box_models; unsigned m_box_index; @@ -234,8 +232,6 @@ namespace opt { virtual bool verify_model(unsigned id, model* mdl, rational const& v); - void get_lns_literals(expr_ref_vector& lits); - private: lbool execute(objective const& obj, bool committed, bool scoped); lbool execute_min_max(unsigned index, bool committed, bool scoped, bool is_max); @@ -243,7 +239,6 @@ namespace opt { lbool execute_lex(); lbool execute_box(); lbool execute_pareto(); - lbool execute_lns(); lbool adjust_unknown(lbool r); bool scoped_lex(); expr_ref to_expr(inf_eps const& n); diff --git a/src/opt/opt_lns.cpp b/src/opt/opt_lns.cpp deleted file mode 100644 index 0cdcf19c4..000000000 --- a/src/opt/opt_lns.cpp +++ /dev/null @@ -1,145 +0,0 @@ -/*++ -Copyright (c) 2018 Microsoft Corporation - -Module Name: - - opt_lns.cpp - -Abstract: - - Large neighborhood search default implementation - based on phase saving and assumptions - -Author: - - Nikolaj Bjorner (nbjorner) 2018-3-13 - ---*/ - -#include "ast/ast_pp.h" -#include "opt/opt_lns.h" -#include "opt/opt_context.h" - -namespace opt { - - lns::lns(context& ctx, solver* s): - m(ctx.get_manager()), - m_ctx(ctx), - m_solver(s), - m_models_trail(m), - m_atoms(m) - {} - - lns::~lns() {} - - void lns::display(std::ostream & out) const { - for (auto const& q : m_queue) { - expr_ref tmp(mk_and(q.m_assignment)); - out << q.m_index << ": " << tmp << "\n"; - } - } - - lbool lns::operator()() { - if (m_queue.empty()) { - expr_ref_vector lits(m), atoms(m); - m_ctx.get_lns_literals(lits); - for (expr* l : lits) { - expr* nl = nullptr; - if (m.is_not(l, nl)) { - m_atoms.push_back(nl); - } - else { - atoms.push_back(l); - m_atoms.push_back(l); - } - } - m_queue.push_back(queue_elem(atoms)); - m_qhead = 0; - } - - params_ref p; - p.set_uint("inprocess.max", 3ul); - m_solver->updt_params(p); - - while (m_qhead < m_queue.size()) { - obj_hashtable atoms; - for (expr* f : m_queue[m_qhead].m_assignment) { - atoms.insert(f); - } - unsigned& index = m_queue[m_qhead].m_index; - expr* lit = nullptr; - for (; index < m_atoms.size(); ++index) { - lit = m_atoms[index].get(); - if (!atoms.contains(lit) && !m_failed.contains(lit)) break; - } - if (index == m_atoms.size()) { - m_qhead++; - continue; - } - - IF_VERBOSE(2, verbose_stream() << "(opt.lns :queue " << m_qhead << " :index " << index << ")\n"); - - p.set_uint("local_search_threads", 0); - p.set_uint("unit_walk_threads", 0); - m_solver->updt_params(p); - - // recalibrate state to an initial satisfying assignment - lbool is_sat = m_solver->check_sat(m_queue[m_qhead].m_assignment); - IF_VERBOSE(2, verbose_stream() << "(opt.lns :calibrate-status " << is_sat << ")\n"); - if (!m.limit().inc()) { - return l_undef; - } - - expr_ref_vector lits(m); - lits.push_back(lit); - ++index; - - // freeze phase in both SAT solver and local search to current assignment - p.set_uint("inprocess.max", 5); - p.set_bool("phase.sticky", true); - p.set_uint("local_search_threads", 1); - p.set_uint("max_conflicts", 100000); - //p.set_uint("unit_walk_threads", 1); - m_solver->updt_params(p); - - is_sat = m_solver->check_sat(lits); - IF_VERBOSE(2, verbose_stream() << "(opt.lns :lookahead-status " << is_sat << " " << mk_pp(lit, m) << ")\n"); - if (is_sat == l_true && add_assignment()) { - return l_true; - } - if (is_sat == l_false) { - m_failed.insert(lit); - expr_ref nlit(m.mk_not(lit), m); - m_solver->assert_expr(nlit); - } - if (!m.limit().inc()) { - return l_undef; - } - } - return l_false; - } - - bool lns::add_assignment() { - model_ref mdl; - m_solver->get_model(mdl); - m_ctx.fix_model(mdl); - expr_ref tmp(m); - expr_ref_vector fmls(m); - for (expr* f : m_atoms) { - mdl->eval(f, tmp); - if (m.is_true(tmp)) { - fmls.push_back(f); - } - } - tmp = mk_and(fmls); - if (m_models.contains(tmp)) { - return false; - } - else { - m_models.insert(tmp); - m_models_trail.push_back(tmp); - return true; - } - } -} - diff --git a/src/opt/opt_lns.h b/src/opt/opt_lns.h deleted file mode 100644 index 827df3081..000000000 --- a/src/opt/opt_lns.h +++ /dev/null @@ -1,68 +0,0 @@ -/*++ -Copyright (c) 2018 Microsoft Corporation - -Module Name: - - opt_lns.h - -Abstract: - - Large neighborhood seearch - -Author: - - Nikolaj Bjorner (nbjorner) 2018-3-13 - -Notes: - - ---*/ -#ifndef OPT_LNS_H_ -#define OPT_LNS_H_ - -#include "solver/solver.h" -#include "model/model.h" - -namespace opt { - - class context; - - class lns { - struct queue_elem { - expr_ref_vector m_assignment; - unsigned m_index; - queue_elem(expr_ref_vector& assign): - m_assignment(assign), - m_index(0) - {} - }; - ast_manager& m; - context& m_ctx; - ref m_solver; - model_ref m_model; - svector m_labels; - vector m_queue; - unsigned m_qhead; - expr_ref_vector m_models_trail; - expr_ref_vector m_atoms; - obj_hashtable m_models; - obj_hashtable m_failed; - - bool add_assignment(); - public: - lns(context& ctx, solver* s); - - ~lns(); - - void display(std::ostream & out) const; - - lbool operator()(); - - void get_model(model_ref& mdl, svector& labels) { - mdl = m_model; - labels = m_labels; - } - }; -} - -#endif diff --git a/src/opt/opt_params.pyg b/src/opt/opt_params.pyg index 21845d38a..911b0a694 100644 --- a/src/opt/opt_params.pyg +++ b/src/opt/opt_params.pyg @@ -3,7 +3,7 @@ def_module_params('opt', export=True, params=(('optsmt_engine', SYMBOL, 'basic', "select optimization engine: 'basic', 'farkas', 'symba'"), ('maxsat_engine', SYMBOL, 'maxres', "select engine for maxsat: 'core_maxsat', 'wmax', 'maxres', 'pd-maxres'"), - ('priority', SYMBOL, 'lex', "select how to priortize objectives: 'lex' (lexicographic), 'pareto', 'box', or 'lns' (large neighborhood search)"), + ('priority', SYMBOL, 'lex', "select how to priortize objectives: 'lex' (lexicographic), 'pareto', 'box'"), ('dump_benchmarks', BOOL, False, 'dump benchmarks for profiling'), ('timeout', UINT, UINT_MAX, 'timeout (in milliseconds) (UINT_MAX and 0 mean no timeout)'), ('rlimit', UINT, 0, 'resource limit (0 means no limit)'),