mirror of
https://github.com/Z3Prover/z3
synced 2025-04-23 17:15:31 +00:00
integrate v2 of lns
This commit is contained in:
Nikolaj Bjorner
parent
dfb7c87448
commit
0ec567fe15
18 changed files with 254 additions and 105 deletions
|
|
@ -83,6 +83,18 @@ private:
|
|||
memset(this, 0, sizeof(*this));
|
||||
}
|
||||
};
|
||||
|
||||
struct lns_maxres : public lns_context {
|
||||
maxres& i;
|
||||
lns_maxres(maxres& i) :i(i) {}
|
||||
~lns_maxres() override {}
|
||||
void update_model(model_ref& mdl) override { i.update_assignment(mdl); }
|
||||
void relax_cores(vector<expr_ref_vector> const& cores) override { i.relax_cores(cores); }
|
||||
rational cost(model& mdl) override { return i.cost(mdl); }
|
||||
rational weight(expr* e) override { return i.m_asm2weight[e]; }
|
||||
expr_ref_vector const& soft() override { return i.m_asms; }
|
||||
};
|
||||
|
||||
unsigned m_index;
|
||||
stats m_stats;
|
||||
expr_ref_vector m_B;
|
||||
|
|
@ -95,6 +107,8 @@ private:
|
|||
strategy_t m_st;
|
||||
rational m_max_upper;
|
||||
model_ref m_csmodel;
|
||||
lns_maxres m_lnsctx;
|
||||
lns m_lns;
|
||||
unsigned m_correction_set_size;
|
||||
bool m_found_feasible_optimum;
|
||||
bool m_hill_climb; // prefer large weight soft clauses for cores
|
||||
|
|
@ -125,6 +139,8 @@ public:
|
|||
m_mus(c.get_solver()),
|
||||
m_trail(m),
|
||||
m_st(st),
|
||||
m_lnsctx(*this),
|
||||
m_lns(s(), m_lnsctx),
|
||||
m_correction_set_size(0),
|
||||
m_found_feasible_optimum(false),
|
||||
m_hill_climb(true),
|
||||
|
|
@ -507,9 +523,10 @@ public:
|
|||
|
||||
void update_model(expr* def, expr* value) {
|
||||
SASSERT(is_uninterp_const(def));
|
||||
if (m_csmodel) {
|
||||
m_csmodel->register_decl(to_app(def)->get_decl(), (*m_csmodel)(value));
|
||||
}
|
||||
if (m_csmodel)
|
||||
m_csmodel->register_decl(to_app(def)->get_decl(), (*m_csmodel)(value));
|
||||
if (m_model)
|
||||
m_model->register_decl(to_app(def)->get_decl(), (*m_model)(value));
|
||||
}
|
||||
|
||||
void process_unsat(exprs const& core, rational w) {
|
||||
|
|
@ -729,7 +746,7 @@ public:
|
|||
fml = m.mk_and(b_i1, cls);
|
||||
update_model(asum, fml);
|
||||
}
|
||||
fml = m.mk_or(cs.size(), cs.c_ptr());
|
||||
fml = m.mk_or(cs);
|
||||
add(fml);
|
||||
}
|
||||
|
||||
|
|
@ -742,21 +759,13 @@ public:
|
|||
update_assignment(mdl);
|
||||
}
|
||||
|
||||
|
||||
|
||||
void improve_model(model_ref& mdl) {
|
||||
if (!m_enable_lns)
|
||||
return;
|
||||
flet<bool> _disable_lns(m_enable_lns, false);
|
||||
std::function<void(model_ref&)> update_model = [&](model_ref& mdl) {
|
||||
update_assignment(mdl);
|
||||
};
|
||||
std::function<void(vector<expr_ref_vector> const&)> _relax_cores = [&](vector<expr_ref_vector> const& cores) {
|
||||
relax_cores(cores);
|
||||
};
|
||||
|
||||
lns lns(s(), update_model);
|
||||
lns.set_conflicts(m_lns_conflicts);
|
||||
lns.set_relax(_relax_cores);
|
||||
lns.climb(mdl, m_asms);
|
||||
m_lns.climb(mdl);
|
||||
}
|
||||
|
||||
void relax_cores(vector<expr_ref_vector> const& cores) {
|
||||
|
|
@ -770,6 +779,13 @@ public:
|
|||
process_unsat(wcores);
|
||||
}
|
||||
|
||||
rational cost(model& mdl) {
|
||||
rational upper(0);
|
||||
for (soft& s : m_soft)
|
||||
if (!mdl.is_true(s.s))
|
||||
upper += s.weight;
|
||||
return upper;
|
||||
}
|
||||
|
||||
void update_assignment(model_ref & mdl) {
|
||||
improve_model(mdl);
|
||||
|
|
@ -787,14 +803,7 @@ public:
|
|||
|
||||
TRACE("opt_verbose", tout << *mdl;);
|
||||
|
||||
rational upper(0);
|
||||
|
||||
for (soft& s : m_soft) {
|
||||
TRACE("opt", tout << s.s << ": " << (*mdl)(s.s) << " " << s.weight << "\n";);
|
||||
if (!mdl->is_true(s.s)) {
|
||||
upper += s.weight;
|
||||
}
|
||||
}
|
||||
rational upper = cost(*mdl);
|
||||
|
||||
if (upper > m_upper) {
|
||||
TRACE("opt", tout << "new upper: " << upper << " vs existing upper: " << m_upper << "\n";);
|
||||
|
|
|
|||
|
|
@ -25,12 +25,12 @@ Author:
|
|||
|
||||
namespace opt {
|
||||
|
||||
lns::lns(solver& s, std::function<void(model_ref& mdl)>& update_model)
|
||||
lns::lns(solver& s, lns_context& ctx)
|
||||
: m(s.get_manager()),
|
||||
s(s),
|
||||
ctx(ctx),
|
||||
m_hardened(m),
|
||||
m_soft(m),
|
||||
m_update_model(update_model)
|
||||
m_unprocessed(m)
|
||||
{}
|
||||
|
||||
void lns::set_lns_params() {
|
||||
|
|
@ -39,7 +39,7 @@ namespace opt {
|
|||
p.set_uint("restart.initial", 1000000);
|
||||
p.set_uint("max_conflicts", m_max_conflicts);
|
||||
p.set_uint("simplify.delay", 1000000);
|
||||
// p.set_bool("gc.burst", true);
|
||||
// p.set_bool("gc.burst", true);
|
||||
s.updt_params(p);
|
||||
}
|
||||
|
||||
|
|
@ -52,17 +52,99 @@ namespace opt {
|
|||
p.set_uint("gc.burst", sp.gc_burst());
|
||||
}
|
||||
|
||||
unsigned lns::climb(model_ref& mdl, expr_ref_vector const& asms) {
|
||||
unsigned lns::climb(model_ref& mdl) {
|
||||
IF_VERBOSE(1, verbose_stream() << "(opt.lns :climb)\n");
|
||||
m_num_improves = 0;
|
||||
params_ref old_p(s.get_params());
|
||||
save_defaults(old_p);
|
||||
set_lns_params();
|
||||
setup_assumptions(mdl, asms);
|
||||
unsigned num_improved = improve_linear(mdl);
|
||||
// num_improved += improve_rotate(mdl, asms);
|
||||
update_best_model(mdl);
|
||||
for (unsigned i = 0; i < 2; ++i)
|
||||
improve_bs();
|
||||
IF_VERBOSE(1, verbose_stream() << "(opt.lns :relax-cores " << m_cores.size() << ")\n");
|
||||
relax_cores();
|
||||
s.updt_params(old_p);
|
||||
IF_VERBOSE(1, verbose_stream() << "(opt.lns :num-improves " << m_num_improves << " :remaining-soft " << m_soft.size() << ")\n");
|
||||
return num_improved;
|
||||
IF_VERBOSE(1, verbose_stream() << "(opt.lns :num-improves " << m_num_improves << ")\n");
|
||||
return m_num_improves;
|
||||
}
|
||||
|
||||
void lns::update_best_model(model_ref& mdl) {
|
||||
rational cost = ctx.cost(*mdl);
|
||||
if (m_best_cost.is_zero() || m_best_cost >= cost) {
|
||||
m_best_cost = cost;
|
||||
m_best_model = mdl;
|
||||
m_best_phase = s.get_phase();
|
||||
m_best_bound = 0;
|
||||
for (expr* e : ctx.soft())
|
||||
if (!mdl->is_true(e))
|
||||
m_best_bound += 1;
|
||||
}
|
||||
}
|
||||
|
||||
void lns::apply_best_model() {
|
||||
s.set_phase(m_best_phase.get());
|
||||
for (expr* e : m_unprocessed) {
|
||||
s.move_to_front(e);
|
||||
s.set_phase(e);
|
||||
}
|
||||
}
|
||||
|
||||
void lns::improve_bs() {
|
||||
m_unprocessed.reset();
|
||||
m_unprocessed.append(ctx.soft());
|
||||
|
||||
m_hardened.reset();
|
||||
for (expr* a : ctx.soft())
|
||||
m_is_assumption.mark(a);
|
||||
shuffle(m_unprocessed.size(), m_unprocessed.c_ptr(), m_rand);
|
||||
|
||||
model_ref mdl = m_best_model->copy();
|
||||
unsigned j = 0;
|
||||
for (unsigned i = 0; i < m_unprocessed.size(); ++i) {
|
||||
if (mdl->is_false(unprocessed(i))) {
|
||||
expr_ref tmp(m_unprocessed.get(j), m);
|
||||
m_unprocessed[j++] = m_unprocessed[i];
|
||||
m_unprocessed[i] = tmp;
|
||||
break;
|
||||
}
|
||||
}
|
||||
for (unsigned i = j; i < m_unprocessed.size(); ++i) {
|
||||
if (mdl->is_true(unprocessed(i))) {
|
||||
expr_ref tmp(m_unprocessed.get(j), m);
|
||||
m_unprocessed[j++] = m_unprocessed[i];
|
||||
m_unprocessed[i] = tmp;
|
||||
}
|
||||
}
|
||||
for (unsigned i = 0; i < 3 && !m_unprocessed.empty(); ++i)
|
||||
improve_bs1();
|
||||
}
|
||||
|
||||
void lns::improve_bs1() {
|
||||
model_ref mdl = m_best_model->copy();
|
||||
unsigned j = 0;
|
||||
for (expr* e : m_unprocessed) {
|
||||
if (!m.inc())
|
||||
return;
|
||||
if (mdl->is_true(e))
|
||||
m_hardened.push_back(e);
|
||||
else {
|
||||
apply_best_model();
|
||||
switch (improve_step(mdl, e)) {
|
||||
case l_true:
|
||||
m_hardened.push_back(e);
|
||||
ctx.update_model(mdl);
|
||||
update_best_model(mdl);
|
||||
break;
|
||||
case l_false:
|
||||
m_hardened.push_back(m.mk_not(e));
|
||||
break;
|
||||
case l_undef:
|
||||
m_unprocessed[j++] = e;
|
||||
break;
|
||||
}
|
||||
}
|
||||
}
|
||||
m_unprocessed.shrink(j);
|
||||
}
|
||||
|
||||
struct lns::scoped_bounding {
|
||||
|
|
@ -72,12 +154,13 @@ namespace opt {
|
|||
scoped_bounding(lns& l):m_lns(l) {
|
||||
if (!m_lns.m_enable_scoped_bounding)
|
||||
return;
|
||||
if (m_lns.m_best_bound == 0)
|
||||
return;
|
||||
m_cores_are_valid = m_lns.m_cores_are_valid;
|
||||
m_lns.m_cores_are_valid = false;
|
||||
m_lns.s.push();
|
||||
pb_util pb(m_lns.m);
|
||||
// TBD: bound should to be adjusted for current best solution, not number of soft constraints left.
|
||||
expr_ref bound(pb.mk_at_most_k(m_lns.m_soft, m_lns.m_soft.size() - 1), m_lns.m);
|
||||
expr_ref bound(pb.mk_at_most_k(m_lns.ctx.soft(), m_lns.m_best_bound - 1), m_lns.m);
|
||||
m_lns.s.assert_expr(bound);
|
||||
}
|
||||
~scoped_bounding() {
|
||||
|
|
@ -89,7 +172,7 @@ namespace opt {
|
|||
};
|
||||
|
||||
void lns::relax_cores() {
|
||||
if (!m_cores.empty() && m_relax_cores && m_cores_are_valid) {
|
||||
if (!m_cores.empty() && m_cores_are_valid) {
|
||||
std::sort(m_cores.begin(), m_cores.end(), [&](expr_ref_vector const& a, expr_ref_vector const& b) { return a.size() < b.size(); });
|
||||
unsigned num_disjoint = 0;
|
||||
vector<expr_ref_vector> new_cores;
|
||||
|
|
@ -104,43 +187,14 @@ namespace opt {
|
|||
new_cores.push_back(c);
|
||||
++num_disjoint;
|
||||
}
|
||||
m_relax_cores(new_cores);
|
||||
IF_VERBOSE(2, verbose_stream() << "num cores: " << m_cores.size() << " new cores: " << new_cores.size() << "\n");
|
||||
ctx.relax_cores(new_cores);
|
||||
}
|
||||
m_in_core.reset();
|
||||
m_is_assumption.reset();
|
||||
m_cores.reset();
|
||||
}
|
||||
|
||||
void lns::setup_assumptions(model_ref& mdl, expr_ref_vector const& asms) {
|
||||
m_hardened.reset();
|
||||
m_soft.reset();
|
||||
for (expr* a : asms) {
|
||||
m_is_assumption.mark(a);
|
||||
if (mdl->is_true(a))
|
||||
m_hardened.push_back(a);
|
||||
else
|
||||
m_soft.push_back(a);
|
||||
}
|
||||
}
|
||||
|
||||
unsigned lns::improve_rotate(model_ref& mdl, expr_ref_vector const& asms) {
|
||||
unsigned num_improved = 0;
|
||||
repeat:
|
||||
setup_assumptions(mdl, asms);
|
||||
unsigned sz = m_hardened.size();
|
||||
for (unsigned i = 0; i < sz; ++i) {
|
||||
expr_ref tmp(m_hardened.get(i), m);
|
||||
m_hardened[i] = m.mk_not(tmp);
|
||||
unsigned reward = improve_linear(mdl);
|
||||
if (reward > 1) {
|
||||
num_improved += (reward - 1);
|
||||
goto repeat;
|
||||
}
|
||||
setup_assumptions(mdl, asms);
|
||||
}
|
||||
return num_improved;
|
||||
}
|
||||
|
||||
unsigned lns::improve_linear(model_ref& mdl) {
|
||||
scoped_bounding _scoped_bouding(*this);
|
||||
unsigned num_improved = 0;
|
||||
|
|
@ -156,43 +210,42 @@ namespace opt {
|
|||
set_lns_params();
|
||||
}
|
||||
m_max_conflicts = max_conflicts;
|
||||
relax_cores();
|
||||
return num_improved;
|
||||
}
|
||||
|
||||
unsigned lns::improve_step(model_ref& mdl) {
|
||||
unsigned num_improved = 0;
|
||||
for (unsigned i = 0; m.inc() && i < m_soft.size(); ++i) {
|
||||
switch (improve_step(mdl, soft(i))) {
|
||||
for (unsigned i = 0; m.inc() && i < m_unprocessed.size(); ++i) {
|
||||
switch (improve_step(mdl, unprocessed(i))) {
|
||||
case l_undef:
|
||||
break;
|
||||
case l_false:
|
||||
TRACE("opt", tout << "pruned " << mk_bounded_pp(soft(i), m) << "\n";);
|
||||
m_hardened.push_back(m.mk_not(soft(i)));
|
||||
for (unsigned k = i; k + 1 < m_soft.size(); ++k)
|
||||
m_soft[k] = soft(k + 1);
|
||||
m_soft.pop_back();
|
||||
TRACE("opt", tout << "pruned " << mk_bounded_pp(unprocessed(i), m) << "\n";);
|
||||
m_hardened.push_back(m.mk_not(unprocessed(i)));
|
||||
for (unsigned k = i; k + 1 < m_unprocessed.size(); ++k)
|
||||
m_unprocessed[k] = unprocessed(k + 1);
|
||||
m_unprocessed.pop_back();
|
||||
--i;
|
||||
break;
|
||||
case l_true: {
|
||||
unsigned k = 0, offset = 0;
|
||||
for (unsigned j = 0; j < m_soft.size(); ++j) {
|
||||
if (mdl->is_true(soft(j))) {
|
||||
for (unsigned j = 0; j < m_unprocessed.size(); ++j) {
|
||||
if (mdl->is_true(unprocessed(j))) {
|
||||
if (j <= i)
|
||||
++offset;
|
||||
++m_num_improves;
|
||||
TRACE("opt", tout << "improved " << mk_bounded_pp(soft(j), m) << "\n";);
|
||||
m_hardened.push_back(soft(j));
|
||||
TRACE("opt", tout << "improved " << mk_bounded_pp(unprocessed(j), m) << "\n";);
|
||||
m_hardened.push_back(unprocessed(j));
|
||||
++num_improved;
|
||||
}
|
||||
else {
|
||||
m_soft[k++] = soft(j);
|
||||
m_unprocessed[k++] = unprocessed(j);
|
||||
}
|
||||
}
|
||||
m_soft.shrink(k);
|
||||
m_unprocessed.shrink(k);
|
||||
i -= offset;
|
||||
IF_VERBOSE(1, verbose_stream() << "(opt.lns :num-improves " << m_num_improves << " :remaining-soft " << m_soft.size() << ")\n");
|
||||
m_update_model(mdl);
|
||||
IF_VERBOSE(1, verbose_stream() << "(opt.lns :num-improves " << m_num_improves << " :remaining-soft " << m_unprocessed.size() << ")\n");
|
||||
ctx.update_model(mdl);
|
||||
break;
|
||||
}
|
||||
}
|
||||
|
|
@ -209,12 +262,12 @@ namespace opt {
|
|||
if (r == l_false) {
|
||||
expr_ref_vector core(m);
|
||||
s.get_unsat_core(core);
|
||||
bool all_assumed = true;
|
||||
bool all_assumed = true;
|
||||
for (expr* c : core)
|
||||
all_assumed &= m_is_assumption.is_marked(c);
|
||||
if (all_assumed) {
|
||||
m_cores.push_back(core);
|
||||
}
|
||||
IF_VERBOSE(2, verbose_stream() << "core " << all_assumed << " - " << core.size() << "\n");
|
||||
if (all_assumed)
|
||||
m_cores.push_back(core);
|
||||
}
|
||||
return r;
|
||||
}
|
||||
|
|
|
|||
|
|
@ -26,39 +26,55 @@ Author:
|
|||
|
||||
namespace opt {
|
||||
|
||||
class lns_context {
|
||||
public:
|
||||
virtual ~lns_context() {}
|
||||
virtual void update_model(model_ref& mdl) = 0;
|
||||
virtual void relax_cores(vector<expr_ref_vector> const& cores) = 0;
|
||||
virtual rational cost(model& mdl) = 0;
|
||||
virtual rational weight(expr* e) = 0;
|
||||
virtual expr_ref_vector const& soft() = 0;
|
||||
};
|
||||
|
||||
class lns {
|
||||
ast_manager& m;
|
||||
solver& s;
|
||||
lns_context& ctx;
|
||||
random_gen m_rand;
|
||||
expr_ref_vector m_hardened;
|
||||
expr_ref_vector m_soft;
|
||||
unsigned m_max_conflicts { 1000 };
|
||||
expr_ref_vector m_unprocessed;
|
||||
unsigned m_max_conflicts { 10000 };
|
||||
unsigned m_num_improves { 0 };
|
||||
bool m_cores_are_valid { true };
|
||||
bool m_enable_scoped_bounding { false };
|
||||
unsigned m_best_bound { 0 };
|
||||
|
||||
rational m_best_cost;
|
||||
model_ref m_best_model;
|
||||
scoped_ptr<solver::phase> m_best_phase;
|
||||
|
||||
vector<expr_ref_vector> m_cores;
|
||||
expr_mark m_in_core;
|
||||
expr_mark m_is_assumption;
|
||||
|
||||
struct scoped_bounding;
|
||||
|
||||
std::function<void(model_ref& m)> m_update_model;
|
||||
std::function<void(vector<expr_ref_vector> const&)> m_relax_cores;
|
||||
void update_best_model(model_ref& mdl);
|
||||
void improve_bs();
|
||||
void improve_bs1();
|
||||
void apply_best_model();
|
||||
|
||||
expr* soft(unsigned i) const { return m_soft[i]; }
|
||||
expr* unprocessed(unsigned i) const { return m_unprocessed[i]; }
|
||||
void set_lns_params();
|
||||
void save_defaults(params_ref& p);
|
||||
unsigned improve_step(model_ref& mdl);
|
||||
lbool improve_step(model_ref& mdl, expr* e);
|
||||
void relax_cores();
|
||||
unsigned improve_linear(model_ref& mdl);
|
||||
unsigned improve_rotate(model_ref& mdl, expr_ref_vector const& asms);
|
||||
void setup_assumptions(model_ref& mdl, expr_ref_vector const& asms);
|
||||
|
||||
public:
|
||||
lns(solver& s, std::function<void(model_ref&)>& update_model);
|
||||
void set_relax(std::function<void(vector<expr_ref_vector> const&)>& rc) { m_relax_cores = rc; }
|
||||
lns(solver& s, lns_context& ctx);
|
||||
void set_conflicts(unsigned c) { m_max_conflicts = c; }
|
||||
unsigned climb(model_ref& mdl, expr_ref_vector const& asms);
|
||||
unsigned climb(model_ref& mdl);
|
||||
};
|
||||
};
|
||||
|
|
|
|||
|
|
@ -110,7 +110,10 @@ namespace opt {
|
|||
void get_levels(ptr_vector<expr> const& vars, unsigned_vector& depth) override;
|
||||
expr_ref_vector get_trail() override { return m_context.get_trail(); }
|
||||
expr_ref_vector cube(expr_ref_vector&, unsigned) override { return expr_ref_vector(m); }
|
||||
void set_phase(expr* e) override { NOT_IMPLEMENTED_YET(); }
|
||||
void set_phase(expr* e) override { m_context.set_phase(e); }
|
||||
phase* get_phase() override { return m_context.get_phase(); }
|
||||
void set_phase(phase* p) override { m_context.set_phase(p); }
|
||||
void move_to_front(expr* e) override { m_context.move_to_front(e); }
|
||||
|
||||
void set_logic(symbol const& logic);
|
||||
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue