diff --git a/src/opt/mss_solver.cpp b/src/opt/mss_solver.cpp
index d27b6300c..1ac351855 100755
--- a/src/opt/mss_solver.cpp
+++ b/src/opt/mss_solver.cpp
@@ -11,45 +11,85 @@ class mss_solver: public maxsmt_solver_base {
private:
typedef ptr_vector<expr> exprs;
+ typedef obj_hashtable<expr> expr_set;
mss m_mss;
unsigned m_index;
- expr_ref_vector m_asms;
+ exprs m_asms;
+ unsigned m_mss_found;
+ vector<exprs> m_cores;
+ unsigned m_core_idx;
+ model_ref m_last_model;
+ exprs m_mss_trail;
+ exprs m_mcs_trail;
+ unsigned_vector m_mss_trail_lim;
+ unsigned_vector m_mcs_trail_lim;
unsigned m_max_mss;
+ bool m_disjoint_cores;
public:
mss_solver(maxsat_context& c, unsigned id, weights_t& ws, expr_ref_vector const& soft):
maxsmt_solver_base(c, ws, soft),
m_mss(c.get_solver(), m),
m_index(id),
- m_asms(m),
- m_max_mss(UINT_MAX) {
+ m_mss_found(0),
+ m_core_idx(0),
+ m_max_mss(UINT_MAX),
+ m_disjoint_cores(false) {
}
virtual ~mss_solver() {}
virtual lbool operator()() {
if (!init()) return l_undef;
- init_asms();
- lbool is_sat = check_sat(m_asms);
- if (is_sat == l_undef) return l_undef;
- if (is_sat == l_true) {
- IF_VERBOSE(2, verbose_stream() << "(opt.mss-solver :mss " << m_asms.size() << " :mcs " << 0 << ")\n";);
- model_ref mdl;
- s().get_model(mdl);
- update_assignment(mdl.get());
- return l_true;
+ init_local();
+ lbool is_sat = disjoint_cores();
+ if (is_sat != l_true) return is_sat;
+ if (m_cores.size() == 0) return l_true;
+ update_model();
+ exprs asms;
+ while (true) {
+ exprs mss, mcs;
+ mss.append(m_cores[m_core_idx]);
+ is_sat = cld(m_last_model, mss, mcs);
+ if (is_sat == l_undef || m.canceled()) return l_undef;
+ SASSERT(is_sat == l_true);
+ update_trails(mss, mcs);
+ if (m_core_idx < m_cores.size()-1) {
+ m_core_idx++;
+ }
+ else {
+ IF_VERBOSE(2, verbose_stream() << "(opt.mss-solver :mss " << m_mss_trail.size() + m_asms.size() << " :mcs " << m_mcs_trail.size() << ")\n";);
+ if (++m_mss_found >= m_max_mss) return l_true;
+ asms.push_back(relax_and_assert(m.mk_or(m_mcs_trail.size(), m_mcs_trail.c_ptr())));
+ is_sat = backtrack(asms);
+ if (is_sat == l_false) {
+ SASSERT(m_core_idx == 0);
+ is_sat = disjoint_cores(asms);
+ }
+ if (is_sat == l_undef) return l_undef;
+ if (is_sat == l_false) return l_true;
+ }
}
- return enumerate_mss();
+ return l_true;
}
virtual void updt_params(params_ref& p) {
maxsmt_solver_base::updt_params(p);
opt_params _p(p);
m_max_mss = _p.mss_max();
+ m_disjoint_cores = _p.mss_disjoint_cores();
}
private:
- void init_asms() {
+ void init_local() {
+ m_cores.reset();
+ m_core_idx = 0;
+ m_mss_found = 0;
+ m_last_model.reset();
+ m_mss_trail.reset();
+ m_mcs_trail.reset();
+ m_mss_trail_lim.reset();
+ m_mcs_trail_lim.reset();
m_asms.reset();
for (unsigned i = 0; i < m_soft.size(); ++i) {
expr* e = m_soft[i];
@@ -74,42 +114,84 @@ private:
return is_uninterp_const(l) || (m.is_not(l, l) && is_uninterp_const(l));
}
- lbool enumerate_mss() {
- expr_ref_vector asms(m);
- for (unsigned i = 0; i < m_max_mss; ++i) {
- exprs mss, mcs;
- lbool is_sat = next_mss(asms, mss, mcs);
- if (is_sat == l_false && i == 0) return l_false;
- if (is_sat == l_undef && i == 0) return l_undef;
- if (is_sat == l_false || is_sat == l_undef) return l_true;
- asms.push_back(relax_and_assert(m.mk_or(mcs.size(), mcs.c_ptr())));
+ lbool disjoint_cores(exprs const& asms) {
+ expr_set asm_lits, core_lits;
+ for (unsigned i = 0; i < asms.size(); ++i) {
+ asm_lits.insert(asms[i]);
}
- return l_true;
+ lbool is_sat = l_false;
+ exprs core;
+ while (is_sat == l_false) {
+ exprs tmp_asms;
+ tmp_asms.append(asms);
+ tmp_asms.append(m_asms);
+ is_sat = check_sat(tmp_asms);
+ if (is_sat == l_true) {
+ update_model();
+ }
+ else if (is_sat == l_false) {
+ core.reset();
+ s().get_unsat_core(core);
+ for (unsigned i = 0; i < core.size();) {
+ if (asm_lits.contains(core[i])) {
+ core[i] = core.back();
+ core.pop_back();
+ }
+ else {
+ core_lits.insert(core[i]);
+ ++i;
+ }
+ }
+ if (core.empty()) {
+ IF_VERBOSE(2, verbose_stream() << "(opt.mss-solver empty core)\n";);
+ return l_false;
+ }
+ if (m_disjoint_cores) {
+ m_cores.push_back(core);
+ IF_VERBOSE(2, verbose_stream() << "(opt.mss-solver :core-size " << core.size() << " :num-cores " << m_cores.size() << ")\n";);
+ for (unsigned i = 0; i < m_asms.size();) {
+ if (core_lits.contains(m_asms[i]) || !m_disjoint_cores) {
+ m_asms[i] = m_asms.back();
+ m_asms.pop_back();
+ }
+ else {
+ ++i;
+ }
+ }
+ }
+ else {
+ m_cores.push_back(m_asms);
+ m_asms.reset();
+ }
+ }
+ }
+ IF_VERBOSE(2, verbose_stream() << "(opt.mss-solver :num-cores " << m_cores.size() << ")\n";);
+ // TODO: update m_lower?
+ return is_sat;
}
- lbool next_mss(expr_ref_vector const& asms, exprs& mss, exprs& mcs) {
- mss.reset();
- mcs.reset();
- lbool is_sat = check_sat(asms);
- if (is_sat != l_true) return is_sat;
- model_ref mdl;
- s().get_model(mdl);
- update_assignment(mdl.get());
- vector<exprs> dummy;
- push_exprs(mss, m_asms);
- push_exprs(mss, asms);
- is_sat = cld(mdl.get(), mss, mcs);
- if (is_sat == l_true) {
- IF_VERBOSE(2, verbose_stream() << "(opt.mss-solver :mss " << mss.size() - asms.size() << " :mcs " << mcs.size() << ")\n";);
+ lbool disjoint_cores() {
+ return disjoint_cores(exprs());
+ }
+
+ lbool backtrack(exprs& asms) {
+ SASSERT(m_mss_trail_lim.size() == m_mcs_trail_lim.size());
+ lbool is_sat = l_false;
+ while (is_sat == l_false && m_core_idx > 0) {
+ m_core_idx--;
+ m_mss_trail.resize(m_mss_trail_lim.back());
+ m_mss_trail_lim.pop_back();
+ m_mcs_trail.resize(m_mcs_trail_lim.back());
+ m_mcs_trail_lim.pop_back();
+ exprs tmp_asms;
+ tmp_asms.append(asms);
+ get_trail_asms(tmp_asms);
+ is_sat = check_sat(tmp_asms);
+ if (is_sat == l_true) {
+ update_model();
+ }
}
- /*is_sat = m_mss(mdl.get(), dummy, mss, mcs);
- SASSERT(is_sat != l_false);
- if (is_sat == l_true) {
- mdl.reset();
- m_mss.get_model(mdl);
- update_assignment(mdl.get());
- IF_VERBOSE(2, verbose_stream() << "(opt.mss-solver :mss " << mss.size() - asms.size() << " :mcs " << mcs.size() << ")\n";);
- }*/
+ IF_VERBOSE(2, verbose_stream() << "(opt.mss-solver :backtrack-lvl " << m_core_idx << ")\n";);
return is_sat;
}
@@ -118,19 +200,19 @@ private:
undef.append(mss);
update_sat(initial_model, sat, undef);
lbool is_sat = l_true;
- while (is_sat == l_true) {
+ while (is_sat == l_true && !undef.empty()) {
expr_ref asum = relax_and_assert(m.mk_or(undef.size(), undef.c_ptr()));
- sat.push_back(asum);
- is_sat = check_sat(sat);
- sat.pop_back();
+ exprs asms;
+ asms.append(sat);
+ get_trail_asms(asms);
+ asms.push_back(asum);
+ is_sat = check_sat(asms);
if (is_sat == l_true) {
- model_ref mdl;
- s().get_model(mdl);
- update_sat(mdl, sat, undef);
- update_assignment(mdl.get());
+ update_model();
+ update_sat(m_last_model, sat, undef);
}
}
- if (is_sat == l_false) {
+ if (is_sat == l_false || undef.empty()) {
mss.reset();
mcs.reset();
mss.append(sat);
@@ -140,6 +222,26 @@ private:
return is_sat;
}
+ void get_trail_asms(exprs& asms) {
+ asms.append(m_mss_trail);
+ for (unsigned i = 0; i < m_mcs_trail.size(); ++i) {
+ asms.push_back(m.mk_not(m_mcs_trail[i]));
+ }
+ }
+
+ void update_trails(exprs const& mss, exprs const& mcs) {
+ m_mss_trail_lim.push_back(m_mss_trail.size());
+ m_mcs_trail_lim.push_back(m_mcs_trail.size());
+ m_mss_trail.append(mss);
+ m_mcs_trail.append(mcs);
+ }
+
+ void update_model() {
+ m_last_model.reset();
+ s().get_model(m_last_model);
+ update_assignment(m_last_model.get());
+ }
+
void update_sat(model_ref mdl, exprs& sat, exprs& undef) {
for (unsigned i = 0; i < undef.size();) {
if (is_true(mdl.get(), undef[i])) {
@@ -160,12 +262,7 @@ private:
}
lbool check_sat() {
- expr_ref_vector dummy(m);
- return check_sat(dummy);
- }
-
- lbool check_sat(expr_ref_vector const& asms) {
- return s().check_sat(asms);
+ return check_sat(exprs());
}
lbool check_sat(exprs const& asms) {
@@ -186,7 +283,7 @@ private:
for (unsigned i = 0; i < m_soft.size(); ++i) {
m_assignment[i] = is_true(m_soft[i]);
}
- // TODO: DEBUG verify assignment
+ // TODO: DEBUG verify assignment?
m_upper = upper;
trace_bounds("mss-solver");
}
diff --git a/src/opt/opt_params.pyg b/src/opt/opt_params.pyg
index 4cb22389d..41548452a 100644
--- a/src/opt/opt_params.pyg
+++ b/src/opt/opt_params.pyg
@@ -21,7 +21,8 @@ def_module_params('opt',
('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.pivot_on_correction_set', BOOL, True, 'reduce soft constraints if the current correction set is smaller than current core'),
- ('mss.max', UINT, UINT_MAX, 'maximum number of MSS to enumerate')
+ ('mss.max', UINT, UINT_MAX, 'maximum number of MSS to enumerate'),
+ ('mss.disjoint_cores', BOOL, True, 'partition soft based on disjoint cores')
))