From 71af72eed45bd7770578fd8aa1dcaee84b7f9993 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Mon, 14 Apr 2014 15:24:47 +0100 Subject: [PATCH 1/2] bugfix for bvsls_opt_engine Signed-off-by: Christoph M. Wintersteiger --- src/opt/weighted_maxsat.cpp | 5 +++++ src/tactic/sls/bvsls_opt_engine.cpp | 5 ++++- 2 files changed, 9 insertions(+), 1 deletion(-) diff --git a/src/opt/weighted_maxsat.cpp b/src/opt/weighted_maxsat.cpp index 2d2d67320..b7b906ca6 100644 --- a/src/opt/weighted_maxsat.cpp +++ b/src/opt/weighted_maxsat.cpp @@ -347,6 +347,11 @@ namespace opt { unsigned bv_size = 0; m_bvsls.get_model(m_model); VERIFY(bv.is_numeral(res.optimum, m_lower, bv_size)); + for (unsigned i = 0; i < m_soft.size(); ++i) { + expr_ref tmp(m); + m_model->eval(m_soft[i].get(), tmp, true); + m_assignment[i] = m.is_true(tmp); + } break; } case l_false: diff --git a/src/tactic/sls/bvsls_opt_engine.cpp b/src/tactic/sls/bvsls_opt_engine.cpp index 37587428c..ff17ced2b 100644 --- a/src/tactic/sls/bvsls_opt_engine.cpp +++ b/src/tactic/sls/bvsls_opt_engine.cpp @@ -100,6 +100,8 @@ expr_ref bvsls_opt_engine::maximize(expr_ref const & objective) m_mpz_manager.set(score, top_score()); m_mpz_manager.set(max_score, m_powers(obj_bv_sz)); m_mpz_manager.dec(max_score); + IF_IVERBOSE(10, verbose_stream() << "Initial score: " << m_mpz_manager.to_string(score) << std::endl;); + save_model(score); while (check_restart((unsigned)m_stats.m_stopwatch.get_current_seconds()) && @@ -126,7 +128,8 @@ expr_ref bvsls_opt_engine::maximize(expr_ref const & objective) m_mpz_manager.set(score, top_score()); } else { - TRACE("sls_opt", tout << "New best: " << m_mpz_manager.to_string(score) << std::endl;); + TRACE("sls_opt", tout << "New optimum: " << m_mpz_manager.to_string(score) << std::endl;); + IF_IVERBOSE(10, verbose_stream() << "New optimum: " << m_mpz_manager.to_string(score) << std::endl;); func_decl * fd = consts[new_const]; incremental_score(fd, new_value); m_obj_evaluator.update(fd, new_value); From 64106af5ec8107d659a73f9ef4d36697e826d65a Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Mon, 14 Apr 2014 17:48:09 +0100 Subject: [PATCH 2/2] bvsls_opt_engine fixes Signed-off-by: Christoph M. Wintersteiger --- src/opt/weighted_maxsat.cpp | 5 +- src/tactic/sls/bvsls_opt_engine.cpp | 121 +++++++++++++--------- src/tactic/sls/bvsls_opt_engine.h | 8 +- src/tactic/sls/sls_compilation_settings.h | 2 +- 4 files changed, 82 insertions(+), 54 deletions(-) diff --git a/src/opt/weighted_maxsat.cpp b/src/opt/weighted_maxsat.cpp index b7b906ca6..2e7e2f4aa 100644 --- a/src/opt/weighted_maxsat.cpp +++ b/src/opt/weighted_maxsat.cpp @@ -339,8 +339,11 @@ namespace opt { lbool is_sat = s.check_sat_core(0, 0); if (is_sat == l_true) { updt_model(s); + params_ref p; + p.set_uint("restarts", 20); + m_bvsls.updt_params(p); // TBD: can we set an initial model on m_bvsls? - // CMW: Yes, see next line. + // CMW: Yes, see next line. bvsls_opt_engine::optimization_result res = m_bvsls.optimize(objective, m_model, true); switch (res.is_sat) { case l_true: { diff --git a/src/tactic/sls/bvsls_opt_engine.cpp b/src/tactic/sls/bvsls_opt_engine.cpp index ff17ced2b..12a0cf631 100644 --- a/src/tactic/sls/bvsls_opt_engine.cpp +++ b/src/tactic/sls/bvsls_opt_engine.cpp @@ -16,6 +16,7 @@ Author: Notes: --*/ +#include "sls_compilation_settings.h" #include "nnf.h" #include "bvsls_opt_engine.h" @@ -41,7 +42,8 @@ bvsls_opt_engine::optimization_result bvsls_opt_engine::optimize( TRACE("sls_opt", tout << "objective: " << (_maximize?"maximize":"minimize") << " " << mk_ismt2_pp(objective, m()) << std::endl;); m_hard_tracker.initialize(m_assertions); - m_restart_limit = _RESTART_LIMIT_; + m_restart_limit = _RESTART_LIMIT_; + setup_opt_tracker(objective, _maximize); if (initial_model.get() != 0) { TRACE("sls_opt", tout << "Initial model provided: " << std::endl; @@ -51,62 +53,88 @@ bvsls_opt_engine::optimization_result bvsls_opt_engine::optimize( tout << fd->get_name() << " := " << mk_ismt2_pp(val, m()) << std::endl; }); m_hard_tracker.set_model(initial_model); - } - - optimization_result res(m_manager); - - res.is_sat = m_hard_tracker.is_sat() ? l_true : l_undef; - - if (!res.is_sat) { - do { - checkpoint(); - - IF_VERBOSE(1, verbose_stream() << "Satisfying... restarts left:" << (m_max_restarts - m_stats.m_restarts) << std::endl;); - res.is_sat = search(); - - if (res.is_sat == l_undef) - m_hard_tracker.randomize(m_assertions); - } while (m_stats.m_stopwatch.get_current_seconds() < _TIMELIMIT_ && - res.is_sat != l_true && m_stats.m_restarts++ < m_max_restarts); } + + optimization_result res(m_manager); + lbool is_sat = m_hard_tracker.is_sat() ? l_true : l_undef; - if (res.is_sat) - res.optimum = _maximize ? maximize(objective) : minimize(objective); + for (m_stats.m_restarts = 0; + m_stats.m_restarts < m_max_restarts; + m_stats.m_restarts++) + { + mpz old_best; + m_mpz_manager.set(old_best, m_best_model_score); + + if (!is_sat) { + do { + checkpoint(); + + IF_VERBOSE(1, verbose_stream() << "Satisfying... restarts left:" << (m_max_restarts - m_stats.m_restarts) << std::endl;); + is_sat = search(); + + if (is_sat == l_undef) + m_hard_tracker.randomize(m_assertions); + } + while (is_sat != l_true && + m_stats.m_restarts++ < m_max_restarts); + } + + if (is_sat == l_true) { + IF_VERBOSE(1, verbose_stream() << "Optimizing... restarts left:" << (m_max_restarts - m_stats.m_restarts) << std::endl;); + res.is_sat = l_true; + m_obj_tracker.set_model(m_hard_tracker.get_model()); + m_obj_evaluator.update_all(); + expr_ref local_best = maximize(); + if ((_maximize && m_mpz_manager.gt(m_best_model_score, old_best)) || + (!_maximize && m_mpz_manager.lt(m_best_model_score, old_best))) + { + res.optimum = local_best; + } + } + + m_hard_tracker.randomize(m_assertions); + m_evaluator.update_all(); + is_sat = m_hard_tracker.is_sat() ? l_true : l_undef; + } TRACE("sls_opt", tout << "sat: " << res.is_sat << "; optimum: " << mk_ismt2_pp(res.optimum, m()) << std::endl;); return res; } -expr_ref bvsls_opt_engine::maximize(expr_ref const & objective) +void bvsls_opt_engine::setup_opt_tracker(expr_ref const & objective, bool _max) +{ + expr_ref obj(m_manager); + obj = objective; + if (!_max) + obj = m_bv_util.mk_bv_neg(objective); + + m_obj_e = obj.get(); + m_obj_bv_sz = m_bv_util.get_bv_size(m_obj_e); + ptr_vector objs; + objs.push_back(m_obj_e); + m_obj_tracker.initialize(objs); +} + +expr_ref bvsls_opt_engine::maximize() { SASSERT(m_hard_tracker.is_sat()); - expr * obj_e = objective.get(); - unsigned obj_bv_sz = m_bv_util.get_bv_size(obj_e); - ptr_vector objs; - objs.push_back(obj_e); - m_obj_tracker.initialize(objs); - m_obj_tracker.set_model(m_hard_tracker.get_model()); - m_obj_evaluator.update_all(); - - TRACE("sls_opt", tout << "Initial opt model:" << std::endl; m_obj_tracker.show_model(tout);); - IF_VERBOSE(1, verbose_stream() << "Maximizing... restarts left:" << (m_max_restarts - m_stats.m_restarts) << std::endl;); + TRACE("sls_opt", tout << "Initial opt model:" << std::endl; m_obj_tracker.show_model(tout);); mpz score, old_score, max_score, new_value; unsigned new_const = (unsigned)-1, new_bit = 0; ptr_vector consts = m_obj_tracker.get_constants(); move_type move; m_mpz_manager.set(score, top_score()); - m_mpz_manager.set(max_score, m_powers(obj_bv_sz)); m_mpz_manager.dec(max_score); + m_mpz_manager.set(max_score, m_powers(m_obj_bv_sz)); m_mpz_manager.dec(max_score); - IF_IVERBOSE(10, verbose_stream() << "Initial score: " << m_mpz_manager.to_string(score) << std::endl;); + IF_VERBOSE(10, verbose_stream() << "Initial score: " << m_mpz_manager.to_string(score) << std::endl;); save_model(score); - while (check_restart((unsigned)m_stats.m_stopwatch.get_current_seconds()) && - m_stats.m_stopwatch.get_current_seconds() < _TIMELIMIT_ && - m_mpz_manager.lt(score, max_score)) { + while (m_mpz_manager.lt(score, max_score) && check_restart(m_stats.m_moves)) + { checkpoint(); m_stats.m_moves++; m_mpz_manager.set(old_score, score); @@ -114,22 +142,24 @@ expr_ref bvsls_opt_engine::maximize(expr_ref const & objective) mpz score(0); m_mpz_manager.set(score, - find_best_move(consts, score, new_const, new_value, new_bit, move, max_score, obj_e)); + find_best_move(consts, score, new_const, new_value, new_bit, move, max_score, m_obj_e)); if (new_const == static_cast(-1)) { m_mpz_manager.set(score, old_score); if (m_mpz_manager.gt(score, m_best_model_score)) - save_model(score); + save_model(score); if (!randomize_wrt_hard()) { // Can't improve and can't randomize; can't do anything other than bail out. TRACE("sls_opt", tout << "Got stuck; bailing out." << std::endl;); + IF_VERBOSE(10, verbose_stream() << "No local improvements possible." << std::endl;); goto bailout; - } - m_mpz_manager.set(score, top_score()); + } + m_mpz_manager.set(score, top_score()); } else { + m_stats.m_moves++; TRACE("sls_opt", tout << "New optimum: " << m_mpz_manager.to_string(score) << std::endl;); - IF_IVERBOSE(10, verbose_stream() << "New optimum: " << m_mpz_manager.to_string(score) << std::endl;); + IF_VERBOSE(10, verbose_stream() << "New optimum: " << m_mpz_manager.to_string(score) << std::endl;); func_decl * fd = consts[new_const]; incremental_score(fd, new_value); m_obj_evaluator.update(fd, new_value); @@ -141,17 +171,10 @@ bailout: m_mpz_manager.del(new_value); expr_ref res(m_manager); - res = m_bv_util.mk_numeral(m_best_model_score, obj_bv_sz); + res = m_bv_util.mk_numeral(m_best_model_score, m_obj_bv_sz); return res; } -expr_ref bvsls_opt_engine::minimize(expr_ref const & objective) -{ - expr_ref n_obj(m_manager); - n_obj = m_bv_util.mk_bv_neg(objective); - return maximize(n_obj); -} - void bvsls_opt_engine::save_model(mpz const & score) { model_ref mdl = m_hard_tracker.get_model(); model_ref obj_mdl = m_obj_tracker.get_model(); diff --git a/src/tactic/sls/bvsls_opt_engine.h b/src/tactic/sls/bvsls_opt_engine.h index befd00353..75216c49e 100644 --- a/src/tactic/sls/bvsls_opt_engine.h +++ b/src/tactic/sls/bvsls_opt_engine.h @@ -27,7 +27,9 @@ class bvsls_opt_engine : public sls_engine { sls_evaluator m_obj_evaluator; model_ref m_best_model; mpz m_best_model_score; - + unsigned m_obj_bv_sz; + expr * m_obj_e; + public: bvsls_opt_engine(ast_manager & m, params_ref const & p); ~bvsls_opt_engine(); @@ -44,8 +46,8 @@ public: void get_model(model_ref & result) { result = m_best_model; } protected: - expr_ref maximize(expr_ref const & objective); - expr_ref minimize(expr_ref const & objective); + void setup_opt_tracker(expr_ref const & objective, bool _max); + expr_ref maximize(); bool what_if(func_decl * fd, const unsigned & fd_inx, const mpz & temp, mpz & best_score, unsigned & best_const, mpz & best_value); diff --git a/src/tactic/sls/sls_compilation_settings.h b/src/tactic/sls/sls_compilation_settings.h index 4d8c83599..321320c39 100644 --- a/src/tactic/sls/sls_compilation_settings.h +++ b/src/tactic/sls/sls_compilation_settings.h @@ -38,7 +38,7 @@ Notes: // do we use restarts? // 0 = no, 1 = use #moves, 2 = use #plateaus, 3 = use time -#define _RESTARTS_ 3 +#define _RESTARTS_ 1 // limit of moves/plateaus/seconds until first restart occurs #define _RESTART_LIMIT_ 10 // 0 = initialize with all zero, 1 initialize with random value