From 39ac22c37e5e54bed8fca354e62dd6043b8081db Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 20 Mar 2014 17:34:01 -0700 Subject: [PATCH] sls testing Signed-off-by: Nikolaj Bjorner --- src/opt/pb_sls.cpp | 118 ++++++++++++++++++++++++------------ src/opt/weighted_maxsat.cpp | 85 ++++++++++++-------------- tests/sls1.smt2 | 2 + 3 files changed, 121 insertions(+), 84 deletions(-) diff --git a/src/opt/pb_sls.cpp b/src/opt/pb_sls.cpp index 002170924..dde0f67d1 100644 --- a/src/opt/pb_sls.cpp +++ b/src/opt/pb_sls.cpp @@ -19,12 +19,50 @@ Notes: #include "pb_sls.h" #include "smt_literal.h" #include "ast_pp.h" -#include "uint_set.h" #include "th_rewriter.h" namespace smt { struct pb_sls::imp { + struct index_set { + unsigned_vector m_elems; + unsigned_vector m_index; + + unsigned num_elems() const { return m_elems.size(); } + + void reset() { m_elems.reset(); m_index.reset(); } + + bool empty() const { return m_elems.empty(); } + + bool contains(unsigned idx) const { + return + (idx < m_index.size()) && + (m_index[idx] < m_elems.size()) && + (m_elems[m_index[idx]] == idx); + } + + void insert(unsigned idx) { + m_index.reserve(idx+1); + if (!contains(idx)) { + m_index[idx] = m_elems.size(); + m_elems.push_back(idx); + } + } + + void remove(unsigned idx) { + if (!contains(idx)) return; + unsigned pos = m_index[idx]; + m_elems[pos] = m_elems.back(); + m_index[m_elems[pos]] = pos; + m_elems.pop_back(); + } + + unsigned choose(random_gen& rnd) const { + SASSERT(!empty()); + return m_elems[rnd(num_elems())]; + } + }; + struct clause { literal_vector m_lits; scoped_mpz_vector m_weights; @@ -71,8 +109,8 @@ namespace smt { svector m_best_assignment; obj_map m_decl2var; // map declarations to Boolean variables. ptr_vector m_var2decl; // reverse map - uint_set m_hard_false; // list of hard clauses that are false. - uint_set m_soft_false; // list of soft clauses that are false. + index_set m_hard_false; // list of hard clauses that are false. + index_set m_soft_false; // list of soft clauses that are false. unsigned m_max_flips; // maximal number of flips unsigned m_non_greedy_percent; // percent of moves to do non-greedy style random_gen m_rng; @@ -133,29 +171,46 @@ namespace smt { IF_VERBOSE(1, verbose_stream() << "(pb.sls initial penalty: " << m_best_penalty << ")\n"; verbose_stream() << "(pb.sls violated: " << m_hard_false.num_elems() << " penalty: " << m_penalty << ")\n";); - init_max_flips(); - while (m_max_flips > 0) { - --m_max_flips; - literal lit = flip(); - if (m_cancel) { - return l_undef; + svector assignment(m_assignment); + for (unsigned i = 0; i < 20; ++i) { + init_max_flips(); + while (m_max_flips > 0) { + --m_max_flips; + literal lit = flip(); + if (m_cancel) { + return l_undef; + } + IF_VERBOSE(1, verbose_stream() + << "(pb.sls violated: " << m_hard_false.num_elems() + << " penalty: " << m_penalty << " " << lit << ")\n";); + if (m_hard_false.empty() && m_best_penalty.is_zero()) { + break; + } } - IF_VERBOSE(1, verbose_stream() - << "(pb.sls violated: " << m_hard_false.num_elems() - << " penalty: " << m_penalty << " " << lit << ")\n";); - if (m_hard_false.num_elems() == 0 && m_best_penalty.is_zero()) { - return l_true; + if (m_hard_false.empty() && m_best_penalty.is_zero()) { + break; + } + IF_VERBOSE(1, verbose_stream() << "(pb.sls best penalty " << m_best_penalty << ")\n";); + if (!m_best_assignment.empty()) { + assignment.reset(); + assignment.append(m_best_assignment); } - } - IF_VERBOSE(1, verbose_stream() << "(pb.sls best penalty " << m_best_penalty << ")\n";); - if (m_best_assignment.empty()) { - return l_false; - } - else { m_assignment.reset(); - m_assignment.append(m_best_assignment); - return l_true; + m_assignment.append(assignment); + m_penalty = m_best_penalty; + m_best_assignment.reset(); + m_soft_false.reset(); + for (unsigned i = 0; i < m_soft.size(); ++i) { + if (!eval(m_soft[i])) { + m_soft_false.insert(i); + m_penalty += m_weights[i]; + } + } } + m_assignment.reset(); + m_assignment.append(assignment); + m_penalty = m_best_penalty; + return l_true; } bool get_value(literal l) { @@ -362,27 +417,12 @@ namespace smt { // crude selection strategy. clause const& pick_hard_clause() { SASSERT(!m_hard_false.empty()); - uint_set::iterator it = m_hard_false.begin(); - uint_set::iterator end = m_hard_false.end(); - SASSERT(it != end); - return m_clauses[*it]; + return m_clauses[m_hard_false.choose(m_rng)]; } clause const& pick_soft_clause() { SASSERT(!m_soft_false.empty()); - uint_set::iterator it = m_soft_false.begin(); - uint_set::iterator end = m_soft_false.end(); - SASSERT(it != end); - unsigned index = *it; - rational penalty = m_weights[index]; - ++it; - for (; it != end; ++it) { - if (m_weights[*it] > penalty) { - index = *it; - penalty = m_weights[*it]; - } - } - return m_soft[index]; + return m_soft[m_soft_false.choose(m_rng)]; } int flip(literal l) { diff --git a/src/opt/weighted_maxsat.cpp b/src/opt/weighted_maxsat.cpp index b3628f10b..5d42bb63a 100644 --- a/src/opt/weighted_maxsat.cpp +++ b/src/opt/weighted_maxsat.cpp @@ -448,10 +448,12 @@ namespace opt { params_ref m_params; opt_solver m_solver; scoped_ptr m_imp; + smt::pb_sls m_sls; imp(ast_manager& m, opt_solver& s, expr_ref_vector const& soft_constraints, vector const& weights): m(m), s(s), m_soft(soft_constraints), m_weights(weights), m_print_all_models(false), m_cancel(false), - m_solver(m, m_params, symbol("bound")) + m_solver(m, m_params, symbol("bound")), + m_sls(m) { m_assignment.resize(m_soft.size(), false); } @@ -585,71 +587,63 @@ namespace opt { } lbool sls_solve() { - IF_VERBOSE(3, verbose_stream() << "(incremental solve)\n";); - smt::pb_sls sls(m); - svector ws; + IF_VERBOSE(1, verbose_stream() << "(sls solve)\n";); for (unsigned i = 0; i < s.get_num_assertions(); ++i) { - sls.add(s.get_assertion(i)); + m_sls.add(s.get_assertion(i)); + } + pb_util u(m); + expr_ref fml(m), val(m); + app_ref b(m); + expr_ref_vector nsoft(m); + m_lower = m_upper = rational::zero(); + solver::scoped_push __s(s); + for (unsigned i = 0; i < m_soft.size(); ++i) { + m_upper += m_weights[i]; + b = m.mk_fresh_const("b", m.mk_bool_sort()); + s.mc().insert(b->get_decl()); + fml = m.mk_or(m_soft[i].get(), b); + s.assert_expr(fml); + nsoft.push_back(b); + m_sls.add(m_soft[i].get(), m_weights[i]); } - TRACE("opt", tout << "weighted maxsat\n";); - scoped_ensure_theory wth(*this); - solver::scoped_push _s(s); lbool is_sat = l_true; bool was_sat = false; - for (unsigned i = 0; i < m_soft.size(); ++i) { - ws.push_back(wth().assert_weighted(m_soft[i].get(), m_weights[i])); - sls.add(m_soft[i].get(), m_weights[i]); - } - - expr_ref fml(m); - solver::scoped_push __s(s); while (l_true == is_sat) { is_sat = s.check_sat_core(0,0); if (m_cancel) { is_sat = l_undef; } if (is_sat == l_true) { - if (wth().is_optimal()) { - m_upper = wth().get_min_cost(); - updt_model(s); - sls.set_model(m_model); - if (l_true == sls()) { - sls.get_model(m_model); - svector wsf; - rational weight(0); - for (unsigned i = 0; i < ws.size(); ++i) { - if (!sls.soft_holds(i)) { - wsf.push_back(ws[i]); - weight += m_weights[i]; - } - } - fml = wth().mk_optimal_block(wsf, weight); - m_upper = weight; - s.assert_expr(fml); - } - else { - fml = wth().mk_block(); + updt_model(s); + m_sls.set_model(m_model); + m_upper = rational::zero(); + if (l_true == m_sls()) { + m_sls.get_model(m_model); + for (unsigned i = 0; i < m_soft.size(); ++i) { + m_assignment[i] = m_sls.soft_holds(i); } } else { - fml = wth().mk_block(); + for (unsigned i = 0; i < m_soft.size(); ++i) { + VERIFY(m_model->eval(nsoft[i].get(), val)); + m_assignment[i] = !m.is_true(val); + } + } + for (unsigned i = 0; i < m_soft.size(); ++i) { + if (!m_assignment[i]) { + m_upper += m_weights[i]; + } } + IF_VERBOSE(1, verbose_stream() << "(sls.pb with upper bound: " << m_upper << ")\n";); + fml = m.mk_not(u.mk_ge(nsoft.size(), m_weights.c_ptr(), nsoft.c_ptr(), m_upper)); s.assert_expr(fml); was_sat = true; } - IF_VERBOSE(3, verbose_stream() << "(incremental bound)\n";); - } - if (was_sat) { - wth().get_assignment(m_assignment); - } + } if (is_sat == l_false && was_sat) { is_sat = l_true; - } - m_upper = wth().get_min_cost(); - if (is_sat == l_true) { m_lower = m_upper; } - TRACE("opt", tout << "min cost: " << m_upper << "\n";); return is_sat; } @@ -1288,6 +1282,7 @@ namespace opt { return m_imp->m_assignment[idx]; } void wmaxsmt::set_cancel(bool f) { + m_imp->m_sls.set_cancel(f); m_imp->m_cancel = f; m_imp->m_solver.set_cancel(f); m_imp->m_imp->m_cancel = f; diff --git a/tests/sls1.smt2 b/tests/sls1.smt2 index b0daf5451..2218993a2 100644 --- a/tests/sls1.smt2 +++ b/tests/sls1.smt2 @@ -1,3 +1,5 @@ +(set-option :smt.relevancy 0) +(set-option :smt.pb.conflict_frequency 10000) (declare-fun x_354 () Int) (declare-fun x_522 () Int) (declare-fun x_464 () Int)