From 78975827b2ba6d9a29bb6abc9312ce1bc7c90851 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 18 Mar 2014 21:30:45 -0700 Subject: [PATCH] add sls test to wmax Signed-off-by: Nikolaj Bjorner --- src/opt/pb_sls.cpp | 94 ++++++++++++++++++++++++++++--------- src/opt/pb_sls.h | 2 +- src/opt/weighted_maxsat.cpp | 11 +++++ 3 files changed, 83 insertions(+), 24 deletions(-) diff --git a/src/opt/pb_sls.cpp b/src/opt/pb_sls.cpp index 57b919d96..ad1c06b3e 100644 --- a/src/opt/pb_sls.cpp +++ b/src/opt/pb_sls.cpp @@ -61,19 +61,25 @@ namespace smt { vector m_soft; // soft constraints vector m_weights; // weights of soft constraints rational m_penalty; // current penalty of soft constraints + rational m_best_penalty; vector m_hard_occ, m_soft_occ; // variable occurrence svector m_assignment; // current assignment. + 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. - unsigned m_max_flips; + uint_set m_hard_false; // list of hard clauses that are false. + uint_set m_soft_false; // list of soft clauses that are false. + unsigned m_max_flips; // maximal number of flips + unsigned m_non_greedy_perc; // percent of moves to do non-greedy style + random_gen m_rng; + imp(ast_manager& m): m(m), pb(m), m_cancel(false) { m_max_flips = 100; + m_non_greedy_perc = 30; } ~imp() { @@ -97,10 +103,16 @@ namespace smt { } } - void set_value(func_decl* f, bool b) { - literal lit = mk_literal(f); - SASSERT(!lit.sign()); - m_assignment[lit.var()] = b; + void set_model(model const& mdl) { + unsigned sz = mdl.get_num_constants(); + for (unsigned i = 0; i < sz; ++i) { + func_decl* f = mdl.get_constant(i); + if (m.is_bool(f->get_range())) { + literal lit = mk_literal(f); + SASSERT(!lit.sign()); + m_assignment[lit.var()] = m.is_true(mdl.get_const_interp(f)); + } + } } lbool operator()() { @@ -110,8 +122,14 @@ namespace smt { if (m_cancel) { return l_undef; } + IF_VERBOSE(3, verbose_stream() + << "(pb.sls violated: " << m_hard_false.num_elems() + << " penalty: " << m_penalty << ")\n";); + if (m_best_penalty.is_zero()) { + return l_true; + } } - return l_undef; + return m_best_assignment.empty()?l_false:l_true; } bool get_value(literal l) { @@ -120,11 +138,16 @@ namespace smt { void set_cancel(bool f) { m_cancel = f; } + void get_model(model_ref& mdl) { + mdl = alloc(model, m); + for (unsigned i = 0; i < m_var2decl.size(); ++i) { + mdl->register_decl(m_var2decl[i], m_best_assignment[i]?m.mk_true():m.mk_false()); + } + } + void collect_statistics(statistics& st) const { } - void get_model(model_ref& mdl) { - NOT_IMPLEMENTED_YET(); - } + void updt_params(params_ref& p) { } @@ -155,22 +178,31 @@ namespace smt { } void init() { + m_best_assignment.reset(); + m_best_penalty.reset(); + m_hard_false.reset(); + m_hard_occ.reset(); + m_soft_false.reset(); + m_soft_occ.reset(); + m_penalty.reset(); + // initialize the occurs vectors. init_occ(m_clauses, m_hard_occ); init_occ(m_soft, m_soft_occ); + // add clauses that are false. for (unsigned i = 0; i < m_clauses.size(); ++i) { if (!eval(m_clauses[i])) { m_hard_false.insert(i); } } - m_penalty.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_best_penalty = m_penalty; } void flip() { @@ -200,8 +232,12 @@ namespace smt { } VERIFY(-break_count == flip(~lit)); } - // just do a greedy move: - flip(cls.m_lits[min_bc_index]); + if (m_rng(100) <= m_non_greedy_perc) { + flip(cls.m_lits[m_rng(cls.m_lits.size())]); + } + else { + flip(cls.m_lits[min_bc_index]); + } } void flip_soft() { @@ -216,19 +252,30 @@ namespace smt { break_count = flip(lit); SASSERT(break_count >= 0); if (break_count == 0 && penalty > m_penalty) { - // TODO: save into best so far if this qualifies. + if (m_best_penalty > m_penalty) { + IF_VERBOSE(1, verbose_stream() << "(pb.sls improved bound " + << m_penalty << ")\n";); + m_best_assignment.reset(); + m_best_assignment.append(m_assignment); + m_best_penalty = m_penalty; + } return; } if ((break_count < min_bc) || (break_count == min_bc && m_penalty < min_penalty)) { min_bc = break_count; min_bc_index = i; - min_penality = m_penalty; + min_penalty = m_penalty; } VERIFY(-break_count == flip(~lit)); } - // just do a greedy move: - flip(cls.m_lits[min_bc_index]); + if (m_rng(100) <= m_non_greedy_perc) { + flip(cls.m_lits[m_rng(cls.m_lits.size())]); + } + else { + // just do a greedy move: + flip(cls.m_lits[min_bc_index]); + } } // @@ -310,13 +357,14 @@ namespace smt { literal mk_literal(func_decl* f) { SASSERT(f->get_family_id() == null_family_id); unsigned var; - if (!m_expr2var.find(f, var)) { + if (!m_decl2var.find(f, var)) { var = m_hard_occ.size(); - SASSERT(m_expr2var.size() == var); + SASSERT(m_var2decl.size() == var); + SASSERT(m_soft_occ.size() == var); m_hard_occ.push_back(unsigned_vector()); m_soft_occ.push_back(unsigned_vector()); m_assignment.push_back(false); - m_expr2var.insert(f, var); + m_decl2var.insert(f, var); m_var2decl.push_back(f); } return literal(var); @@ -412,8 +460,8 @@ namespace smt { void pb_sls::add(expr* f, rational const& w) { m_imp->add(f, w); } - void pb_sls::set_value(func_decl* f, bool b) { - m_imp->set_value(f, b); + void pb_sls::set_model(model const& mdl) { + m_imp->set_model(mdl); } lbool pb_sls::operator()() { return (*m_imp)(); diff --git a/src/opt/pb_sls.h b/src/opt/pb_sls.h index 05c7becaa..2d01e9043 100644 --- a/src/opt/pb_sls.h +++ b/src/opt/pb_sls.h @@ -35,7 +35,7 @@ namespace smt { ~pb_sls(); void add(expr* f); void add(expr* f, rational const& w); - void set_value(func_decl* f, bool b); + void set_model(model const& mdl); lbool operator()(); void set_cancel(bool f); void collect_statistics(statistics& st) const; diff --git a/src/opt/weighted_maxsat.cpp b/src/opt/weighted_maxsat.cpp index 89e0a5813..1fdb35256 100644 --- a/src/opt/weighted_maxsat.cpp +++ b/src/opt/weighted_maxsat.cpp @@ -28,6 +28,7 @@ Notes: #include "tactical.h" #include "tactic.h" #include "model_smt2_pp.h" +#include "pb_sls.h" namespace smt { @@ -521,6 +522,10 @@ namespace opt { lbool incremental_solve() { IF_VERBOSE(3, verbose_stream() << "(incremental solve)\n";); + smt::pb_sls sls(m); + for (unsigned i = 0; i < s.get_num_assertions(); ++i) { + sls.add(s.get_assertion(i)); + } TRACE("opt", tout << "weighted maxsat\n";); scoped_ensure_theory wth(*this); solver::scoped_push _s(s); @@ -528,6 +533,7 @@ namespace opt { bool was_sat = false; for (unsigned i = 0; i < m_soft.size(); ++i) { wth().assert_weighted(m_soft[i].get(), m_weights[i]); + sls.add(m_soft[i].get(), m_weights[i]); } solver::scoped_push __s(s); while (l_true == is_sat) { @@ -543,6 +549,11 @@ namespace opt { model_ref mdl; s.get_model(mdl); model_smt2_pp(std::cout, m, *(mdl.get()), 0); + + sls.set_model(*(mdl.get())); + lbool found = sls(); + std::cout << found << "\n"; + } expr_ref fml = wth().mk_block(); s.assert_expr(fml);