mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 02:15:19 +00:00
add option for using corr set and use partial cores
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
7f219e84de
commit
0ed38ed59b
|
@ -93,6 +93,8 @@ private:
|
|||
expr_ref_vector m_trail;
|
||||
strategy_t m_st;
|
||||
rational m_max_upper;
|
||||
model_ref m_csmodel;
|
||||
unsigned m_correction_set_size;
|
||||
bool m_found_feasible_optimum;
|
||||
bool m_hill_climb; // prefer large weight soft clauses for cores
|
||||
unsigned m_last_index; // last index used during hill-climbing
|
||||
|
@ -103,6 +105,7 @@ private:
|
|||
unsigned m_max_correction_set_size;// maximal set of correction set that is tolerated.
|
||||
bool m_wmax; // Block upper bound using wmax
|
||||
// this option is disabled if SAT core is used.
|
||||
bool m_pivot_on_cs; // prefer smaller correction set to core.
|
||||
bool m_dump_benchmarks; // display benchmarks (into wcnf format)
|
||||
|
||||
std::string m_trace_id;
|
||||
|
@ -118,6 +121,7 @@ public:
|
|||
m_mss(c.get_solver(), m),
|
||||
m_trail(m),
|
||||
m_st(st),
|
||||
m_correction_set_size(0),
|
||||
m_found_feasible_optimum(false),
|
||||
m_hill_climb(true),
|
||||
m_last_index(0),
|
||||
|
@ -125,7 +129,8 @@ public:
|
|||
m_max_num_cores(UINT_MAX),
|
||||
m_max_core_size(3),
|
||||
m_maximize_assignment(false),
|
||||
m_max_correction_set_size(3)
|
||||
m_max_correction_set_size(3),
|
||||
m_pivot_on_cs(true)
|
||||
{
|
||||
switch(st) {
|
||||
case s_primal:
|
||||
|
@ -203,7 +208,12 @@ public:
|
|||
return l_true;
|
||||
case l_false:
|
||||
is_sat = process_unsat();
|
||||
if (is_sat != l_true) return is_sat;
|
||||
if (is_sat == l_false) {
|
||||
m_lower = m_upper;
|
||||
}
|
||||
if (is_sat == l_undef) {
|
||||
return is_sat;
|
||||
}
|
||||
break;
|
||||
case l_undef:
|
||||
return l_undef;
|
||||
|
@ -386,7 +396,6 @@ public:
|
|||
}
|
||||
|
||||
void get_current_correction_set(model* mdl, exprs& cs) {
|
||||
++m_stats.m_num_cs;
|
||||
cs.reset();
|
||||
if (!mdl) return;
|
||||
for (unsigned i = 0; i < m_asms.size(); ++i) {
|
||||
|
@ -428,12 +437,15 @@ public:
|
|||
}
|
||||
|
||||
void process_sat(exprs const& corr_set) {
|
||||
++m_stats.m_num_cs;
|
||||
expr_ref fml(m), tmp(m);
|
||||
TRACE("opt", display_vec(tout << "corr_set: ", corr_set););
|
||||
remove_core(corr_set);
|
||||
rational w = split_core(corr_set);
|
||||
cs_max_resolve(corr_set, w);
|
||||
IF_VERBOSE(2, verbose_stream() << "(opt.maxres.correction-set " << corr_set.size() << ")\n";);
|
||||
m_csmodel = 0;
|
||||
m_correction_set_size = 0;
|
||||
}
|
||||
|
||||
lbool process_unsat() {
|
||||
|
@ -464,8 +476,19 @@ public:
|
|||
process_unsat(cores[i]);
|
||||
}
|
||||
}
|
||||
|
||||
void update_model(expr* def, expr* value) {
|
||||
SASSERT(is_uninterp_const(def));
|
||||
if (m_csmodel) {
|
||||
expr_ref val(m);
|
||||
SASSERT(m_csmodel.get());
|
||||
VERIFY(m_csmodel->eval(value, val));
|
||||
m_csmodel->register_decl(to_app(def)->get_decl(), val);
|
||||
}
|
||||
}
|
||||
|
||||
void process_unsat(exprs const& core) {
|
||||
IF_VERBOSE(3, verbose_stream() << "(maxres cs model valid: " << (m_csmodel.get() != 0) << " cs size:" << m_correction_set_size << " core: " << core.size() << ")\n";);
|
||||
expr_ref fml(m);
|
||||
remove_core(core);
|
||||
SASSERT(!core.empty());
|
||||
|
@ -479,7 +502,20 @@ public:
|
|||
if (m_st == s_primal_dual) {
|
||||
m_lower = std::min(m_lower, m_upper);
|
||||
}
|
||||
if (m_csmodel.get() && m_correction_set_size > 0) {
|
||||
// this estimate can overshoot for weighted soft constraints.
|
||||
--m_correction_set_size;
|
||||
}
|
||||
trace();
|
||||
if (m_pivot_on_cs && m_csmodel.get() && m_correction_set_size < core.size()) {
|
||||
exprs cs;
|
||||
get_current_correction_set(m_csmodel.get(), cs);
|
||||
m_correction_set_size = cs.size();
|
||||
if (m_correction_set_size < core.size()) {
|
||||
process_sat(cs);
|
||||
return;
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
bool get_mus_model(model_ref& mdl) {
|
||||
|
@ -601,11 +637,14 @@ public:
|
|||
fml = m.mk_implies(dd, b_i);
|
||||
s().assert_expr(fml);
|
||||
m_defs.push_back(fml);
|
||||
fml = m.mk_and(d, b_i);
|
||||
update_model(dd, fml);
|
||||
d = dd;
|
||||
}
|
||||
asum = mk_fresh_bool("a");
|
||||
cls = m.mk_or(b_i1, d);
|
||||
fml = m.mk_implies(asum, cls);
|
||||
update_model(asum, cls);
|
||||
new_assumption(asum, w);
|
||||
s().assert_expr(fml);
|
||||
m_defs.push_back(fml);
|
||||
|
@ -638,8 +677,10 @@ public:
|
|||
if (i > 2) {
|
||||
d = mk_fresh_bool("d");
|
||||
fml = m.mk_implies(d, cls);
|
||||
update_model(d, cls);
|
||||
s().assert_expr(fml);
|
||||
m_defs.push_back(fml);
|
||||
|
||||
}
|
||||
else {
|
||||
d = cls;
|
||||
|
@ -652,12 +693,25 @@ public:
|
|||
s().assert_expr(fml);
|
||||
m_defs.push_back(fml);
|
||||
new_assumption(asum, w);
|
||||
fml = m.mk_and(b_i1, cls);
|
||||
update_model(asum, fml);
|
||||
}
|
||||
fml = m.mk_or(m_B.size(), m_B.c_ptr());
|
||||
s().assert_expr(fml);
|
||||
}
|
||||
|
||||
void update_assignment(model* mdl) {
|
||||
unsigned correction_set_size = 0;
|
||||
for (unsigned i = 0; i < m_asms.size(); ++i) {
|
||||
if (is_false(mdl, m_asms[i].get())) {
|
||||
++correction_set_size;
|
||||
}
|
||||
}
|
||||
if (!m_csmodel.get() || correction_set_size < m_correction_set_size) {
|
||||
m_csmodel = mdl;
|
||||
m_correction_set_size = correction_set_size;
|
||||
}
|
||||
|
||||
rational upper(0);
|
||||
expr_ref tmp(m);
|
||||
for (unsigned i = 0; i < m_soft.size(); ++i) {
|
||||
|
@ -665,16 +719,18 @@ public:
|
|||
upper += m_weights[i];
|
||||
}
|
||||
}
|
||||
|
||||
if (upper >= m_upper) {
|
||||
return;
|
||||
}
|
||||
m_model = mdl;
|
||||
|
||||
|
||||
for (unsigned i = 0; i < m_soft.size(); ++i) {
|
||||
m_assignment[i] = is_true(m_soft[i]);
|
||||
}
|
||||
m_upper = upper;
|
||||
DEBUG_CODE(verify_assignment(););
|
||||
|
||||
m_upper = upper;
|
||||
trace();
|
||||
|
||||
add_upper_bound_block();
|
||||
|
@ -744,6 +800,7 @@ public:
|
|||
m_max_core_size = _p.maxres_max_core_size();
|
||||
m_maximize_assignment = _p.maxres_maximize_assignment();
|
||||
m_max_correction_set_size = _p.maxres_max_correction_set_size();
|
||||
m_pivot_on_cs = _p.maxres_pivot_on_correction_set();
|
||||
m_wmax = _p.maxres_wmax();
|
||||
m_dump_benchmarks = _p.dump_benchmarks();
|
||||
}
|
||||
|
@ -759,6 +816,8 @@ public:
|
|||
m_found_feasible_optimum = false;
|
||||
m_last_index = 0;
|
||||
add_upper_bound_block();
|
||||
m_csmodel = 0;
|
||||
m_correction_set_size = 0;
|
||||
}
|
||||
|
||||
virtual void commit_assignment() {
|
||||
|
|
|
@ -94,6 +94,7 @@ namespace opt {
|
|||
void maxsmt_solver_base::set_mus(bool f) {
|
||||
params_ref p;
|
||||
p.set_bool("minimize_core", f);
|
||||
// p.set_bool("minimize_core_partial", f);
|
||||
s().updt_params(p);
|
||||
}
|
||||
|
||||
|
|
|
@ -18,7 +18,8 @@ def_module_params('opt',
|
|||
('maxres.max_core_size', UINT, 3, 'break batch of generated cores if size reaches this number'),
|
||||
('maxres.maximize_assignment', BOOL, False, 'find an MSS/MCS to improve current assignment'),
|
||||
('maxres.max_correction_set_size', UINT, 3, 'allow generating correction set constraints up to maximal size'),
|
||||
('maxres.wmax', BOOL, False, 'use weighted theory solver to constrain upper bounds')
|
||||
('maxres.wmax', BOOL, False, 'use weighted theory solver to constrain upper bounds'),
|
||||
('maxres.pivot_on_correction_set', BOOL, True, 'prefer reducing soft constraints if the current correction set is smaller than current core')
|
||||
|
||||
))
|
||||
|
||||
|
|
|
@ -33,7 +33,7 @@ namespace sat {
|
|||
m_mus.reset();
|
||||
m_model.reset();
|
||||
m_best_value = 0;
|
||||
m_max_restarts = 10;
|
||||
m_max_restarts = (s.m_stats.m_restart - m_restart) + 10;
|
||||
m_restart = s.m_stats.m_restart;
|
||||
}
|
||||
|
||||
|
@ -59,12 +59,13 @@ namespace sat {
|
|||
|
||||
lbool mus::operator()() {
|
||||
flet<bool> _disable_min(s.m_config.m_minimize_core, false);
|
||||
flet<bool> _disable_min_partial(s.m_config.m_minimize_core_partial, false);
|
||||
flet<bool> _disable_opt(s.m_config.m_optimize_model, false);
|
||||
flet<bool> _is_active(m_is_active, true);
|
||||
IF_VERBOSE(3, verbose_stream() << "(sat.mus " << s.get_core() << ")\n";);
|
||||
reset();
|
||||
return mus1();
|
||||
lbool r = mus1();
|
||||
m_restart = s.m_stats.m_restart;
|
||||
return r;
|
||||
}
|
||||
|
||||
lbool mus::mus1() {
|
||||
|
@ -95,6 +96,11 @@ namespace sat {
|
|||
// IF_VERBOSE(0, verbose_stream() << "num literals: " << core << " " << mus << "\n";);
|
||||
break;
|
||||
}
|
||||
if (s.m_config.m_minimize_core_partial && s.m_stats.m_restart - m_restart > m_max_restarts) {
|
||||
IF_VERBOSE(1, verbose_stream() << "restart budget exceeded\n";);
|
||||
set_core();
|
||||
return l_true;
|
||||
}
|
||||
|
||||
literal lit = core.back();
|
||||
core.pop_back();
|
||||
|
@ -166,7 +172,7 @@ namespace sat {
|
|||
|
||||
lbool mus::qx(literal_set& assignment, literal_set& support, bool has_support) {
|
||||
lbool is_sat = l_true;
|
||||
if (s.m_stats.m_restart - m_restart > m_max_restarts) {
|
||||
if (s.m_config.m_minimize_core_partial && s.m_stats.m_restart - m_restart > m_max_restarts) {
|
||||
IF_VERBOSE(1, verbose_stream() << "restart budget exceeded\n";);
|
||||
return l_true;
|
||||
}
|
||||
|
|
|
@ -940,7 +940,6 @@ namespace sat {
|
|||
|
||||
bool solver::init_weighted_assumptions(unsigned num_lits, literal const* lits, double const* weights, double max_weight) {
|
||||
flet<bool> _min1(m_config.m_minimize_core, false);
|
||||
flet<bool> _min2(m_config.m_minimize_core_partial, false);
|
||||
m_weight = 0;
|
||||
m_blocker.reset();
|
||||
svector<lbool> values;
|
||||
|
@ -2017,7 +2016,7 @@ namespace sat {
|
|||
idx--;
|
||||
}
|
||||
reset_unmark(old_size);
|
||||
if (m_config.m_minimize_core || m_config.m_minimize_core_partial) {
|
||||
if (m_config.m_minimize_core) {
|
||||
if (m_min_core_valid && m_min_core.size() < m_core.size()) {
|
||||
IF_VERBOSE(1, verbose_stream() << "(sat.updating core " << m_min_core.size() << " " << m_core.size() << ")\n";);
|
||||
m_core.reset();
|
||||
|
|
|
@ -1592,11 +1592,11 @@ namespace smt {
|
|||
}
|
||||
|
||||
TRACE("opt", tout << "after traversing row:\nx_i: v" << x_i << ", x_j: v" << x_j << ", gain: " << max_gain << "\n";
|
||||
tout << "best efforts: " << best_efforts << "\n";
|
||||
display(tout););
|
||||
tout << "best efforts: " << best_efforts << "\n";);
|
||||
|
||||
if (x_j == null_theory_var) {
|
||||
TRACE("opt", tout << "row is " << (max ? "maximized" : "minimized") << "\n";);
|
||||
TRACE("opt", tout << "row is " << (max ? "maximized" : "minimized") << "\n";
|
||||
display_row(tout, r, true););
|
||||
SASSERT(!maintain_integrality || valid_assignment());
|
||||
SASSERT(satisfy_bounds());
|
||||
result = OPTIMIZED;
|
||||
|
@ -1772,7 +1772,7 @@ namespace smt {
|
|||
SASSERT(satisfy_bounds());
|
||||
SASSERT(!is_quasi_base(v));
|
||||
if ((max && at_upper(v)) || (!max && at_lower(v))) {
|
||||
TRACE("opt", tout << "At bound: " << mk_pp(e, get_manager()) << "...\n";);
|
||||
TRACE("opt", display_var(tout << "At " << (max?"max: ":"min: ") << mk_pp(e, get_manager()) << " \n", v););
|
||||
return AT_BOUND; // nothing to be done...
|
||||
}
|
||||
m_tmp_row.reset();
|
||||
|
@ -1796,10 +1796,10 @@ namespace smt {
|
|||
mk_bound_from_row(v, get_value(v), max ? B_UPPER : B_LOWER, m_tmp_row);
|
||||
}
|
||||
else if (r == UNBOUNDED) {
|
||||
TRACE("opt", tout << "unbounded: " << mk_pp(e, get_manager()) << "...\n";);
|
||||
TRACE("opt", display_var(tout << "unbounded: " << mk_pp(e, get_manager()) << "\n", v););
|
||||
}
|
||||
else {
|
||||
TRACE("opt", tout << "not optimized: " << mk_pp(e, get_manager()) << "...\n";);
|
||||
TRACE("opt", display_var(tout << "not optimized: " << mk_pp(e, get_manager()) << "\n", v););
|
||||
}
|
||||
return r;
|
||||
}
|
||||
|
|
Loading…
Reference in a new issue