diff --git a/src/opt/opt_params.pyg b/src/opt/opt_params.pyg index dd9e26aae..e93a8b973 100644 --- a/src/opt/opt_params.pyg +++ b/src/opt/opt_params.pyg @@ -1,7 +1,7 @@ def_module_params('opt', description='optimization parameters', export=True, - params=(('optsmt_engine', SYMBOL, 'basic', "select optimization engine: 'basic', 'farkas', 'symba'"), + params=(('optsmt_engine', SYMBOL, 'basic', "select optimization engine: 'basic', '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'"), ('dump_benchmarks', BOOL, False, 'dump benchmarks for profiling'), diff --git a/src/opt/optsmt.cpp b/src/opt/optsmt.cpp index 723ee17cf..25022d78e 100644 --- a/src/opt/optsmt.cpp +++ b/src/opt/optsmt.cpp @@ -107,7 +107,7 @@ namespace opt { unsigned steps = 0; unsigned step_incs = 0; rational delta_per_step(1); - unsigned num_scopes = 0; + unsigned num_scopes = 1; unsigned delta_index = 0; // index of objective to speed up. while (!m.canceled()) { @@ -116,8 +116,8 @@ namespace opt { is_sat = m_s->check_sat(0, nullptr); if (is_sat == l_true) { bound = update_lower(); - if (!get_max_delta(lower, delta_index)) { - delta_per_step = rational::one(); + if (!can_increment_delta(lower, delta_index)) { + delta_per_step = 1; } else if (steps > step_incs) { delta_per_step *= rational(2); @@ -133,31 +133,43 @@ namespace opt { // only try to improve delta_index. bound = m_s->mk_ge(delta_index, m_lower[delta_index] + inf_eps(delta_per_step)); } - TRACE("opt", tout << delta_per_step << " " << bound << "\n";); - m_s->assert_expr(bound); + TRACE("opt", tout << "index: " << delta_index << " delta: " << delta_per_step << " : " << bound << "\n";); + m_s->assert_expr(bound); } else if (is_sat == l_false && delta_per_step > rational::one()) { steps = 0; step_incs = 0; - delta_per_step = rational::one(); + delta_per_step = 1; SASSERT(num_scopes > 0); --num_scopes; m_s->pop(1); } + else if (is_sat == l_false) { + // we are done with this delta_index. + m_upper[delta_index] = m_lower[delta_index]; + if (num_scopes > 0) m_s->pop(num_scopes); + num_scopes = 0; + bool all_tight = true; + for (unsigned i = 0; i < m_lower.size(); ++i) { + all_tight &= m_lower[i] == m_upper[i]; + } + if (all_tight) + break; + delta_per_step = 1; + steps = 0; + step_incs = 0; + ++delta_index; + } else { + if (num_scopes > 0) m_s->pop(num_scopes); + num_scopes = 0; break; } } - m_s->pop(num_scopes); if (m.canceled() || is_sat == l_undef) { return l_undef; } - - // set the solution tight. - for (unsigned i = 0; i < m_lower.size(); ++i) { - m_upper[i] = m_lower[i]; - } return l_true; } @@ -256,46 +268,16 @@ namespace opt { return l_true; } - bool optsmt::get_max_delta(vector const& lower, unsigned& idx) { + bool optsmt::can_increment_delta(vector const& lower, unsigned i) { arith_util arith(m); inf_eps max_delta; - for (unsigned i = 0; i < m_lower.size(); ++i) { - if (arith.is_int(m_objs[i].get())) { - inf_eps delta = m_lower[i] - lower[i]; - if (m_lower[i].is_finite() && delta > max_delta) { - max_delta = delta; - } + if (m_lower[i] < m_upper[i] && arith.is_int(m_objs[i].get())) { + inf_eps delta = m_lower[i] - lower[i]; + if (m_lower[i].is_finite() && delta > max_delta) { + return true; } } - return max_delta.is_pos(); - } - - /* - Enumerate locally optimal assignments until fixedpoint. - */ - lbool optsmt::farkas_opt() { - smt::theory_opt& opt = m_s->get_optimizer(); - - if (typeid(smt::theory_inf_arith) != typeid(opt)) { - return l_undef; - } - - lbool is_sat = l_true; - - while (is_sat == l_true && !m.canceled()) { - is_sat = update_upper(); - } - - if (m.canceled() || is_sat == l_undef) { - return l_undef; - } - - // set the solution tight. - for (unsigned i = 0; i < m_lower.size(); ++i) { - m_upper[i] = m_lower[i]; - } - - return l_true; + return false; } lbool optsmt::symba_opt() { @@ -303,6 +285,7 @@ namespace opt { smt::theory_opt& opt = m_s->get_optimizer(); if (typeid(smt::theory_inf_arith) != typeid(opt)) { + m_s->set_reason_unknown("symba optimization requires theory_inf_arith"); return l_undef; } @@ -503,10 +486,7 @@ namespace opt { m_context.get_base_model(m_best_model); solver::scoped_push _push(*m_s); SASSERT(obj_index < m_vars.size()); - if (is_maximize && m_optsmt_engine == symbol("farkas")) { - return farkas_opt(); - } - else if (is_maximize && m_optsmt_engine == symbol("symba")) { + if (is_maximize && m_optsmt_engine == symbol("symba")) { return symba_opt(); } else { @@ -514,45 +494,6 @@ namespace opt { } } - // deprecated - lbool optsmt::basic_lex(unsigned obj_index, bool is_maximize) { - lbool is_sat = l_true; - expr_ref bound(m); - - for (unsigned i = 0; i < obj_index; ++i) { - commit_assignment(i); - } - while (is_sat == l_true && !m.canceled()) { - is_sat = m_s->check_sat(0, nullptr); - if (is_sat != l_true) break; - - m_s->maximize_objective(obj_index, bound); - m_s->get_model(m_model); - inf_eps obj = m_s->saved_objective_value(obj_index); - update_lower_lex(obj_index, obj, is_maximize); - TRACE("opt", tout << "strengthen bound: " << bound << "\n";); - m_s->assert_expr(bound); - - // TBD: only works for simplex - // blocking formula should be extracted based - // on current state. - } - - if (m.canceled() || is_sat == l_undef) { - TRACE("opt", tout << "undef: " << m.canceled() << " " << is_sat << "\n";); - return l_undef; - } - - // set the solution tight. - m_upper[obj_index] = m_lower[obj_index]; - for (unsigned i = obj_index+1; i < m_lower.size(); ++i) { - m_lower[i] = inf_eps(rational(-1), inf_rational(0)); - } - return l_true; - } - - - /** Takes solver with hard constraints added. Returns an optimal assignment to objective functions. @@ -564,10 +505,7 @@ namespace opt { } // assertions added during search are temporary. solver::scoped_push _push(*m_s); - if (m_optsmt_engine == symbol("farkas")) { - is_sat = farkas_opt(); - } - else if (m_optsmt_engine == symbol("symba")) { + if (m_optsmt_engine == symbol("symba")) { is_sat = symba_opt(); } else { diff --git a/src/opt/optsmt.h b/src/opt/optsmt.h index f8e86d43f..df8760e3c 100644 --- a/src/opt/optsmt.h +++ b/src/opt/optsmt.h @@ -72,33 +72,27 @@ namespace opt { void update_upper(unsigned idx, inf_eps const& r); void reset(); - - private: - bool get_max_delta(vector const& lower, unsigned& idx); - lbool basic_opt(); + + bool can_increment_delta(vector const& lower, unsigned i); + + private: lbool geometric_opt(); lbool symba_opt(); - lbool basic_lex(unsigned idx, bool is_maximize); - lbool geometric_lex(unsigned idx, bool is_maximize); - lbool farkas_opt(); - void set_max(vector& dst, vector const& src, expr_ref_vector& fmls); expr_ref update_lower(); void update_lower_lex(unsigned idx, inf_eps const& r, bool is_maximize); - lbool update_upper(); - }; };