MSS based MaxSMT solver

src/opt/maxsmt.cpp

@@ -21,6 +21,7 @@ Notes:
 #include "opt/maxsmt.h"
 #include "opt/maxres.h"
 #include "opt/wmax.h"
+#include "opt/mss_solver.h"
 #include "ast/ast_pp.h"
 #include "util/uint_set.h"
 #include "opt/opt_context.h"
@@ -240,6 +241,9 @@ namespace opt {
         else if (maxsat_engine == symbol("pd-maxres")) {            
             m_msolver = mk_primal_dual_maxres(m_c, m_index, m_weights, m_soft_constraints);
         }
+        else if (maxsat_engine == symbol("mss")) {
+            m_msolver = mk_mss_solver(m_c, m_index, m_weights, m_soft_constraints);
+        }
         else if (maxsat_engine == symbol("wmax")) {
             m_msolver = mk_wmax(m_c, m_weights, m_soft_constraints);
         }

src/opt/mss_solver.cpp

@@ -0,0 +1,156 @@
+#include "solver/solver.h"
+#include "opt/maxsmt.h"
+#include "opt/mss_solver.h"
+#include "opt/mss.h"
+#include "opt/opt_context.h"
+#include "opt/opt_params.hpp"
+
+using namespace opt;
+
+class mss_solver: public maxsmt_solver_base {
+
+private:
+    typedef ptr_vector<expr> exprs;
+    mss                 m_mss;
+    unsigned            m_index;
+    expr_ref_vector     m_asms;
+    unsigned            m_max_mss;
+
+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) {
+    }
+
+    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;
+        }
+        return enumerate_mss();
+    }
+
+    virtual void updt_params(params_ref& p) {
+        maxsmt_solver_base::updt_params(p);
+        opt_params _p(p);
+        m_max_mss = _p.mss_max();
+    }
+
+private:
+    void init_asms() {
+        m_asms.reset();
+        for (unsigned i = 0; i < m_soft.size(); ++i) {
+            expr* e = m_soft[i];
+            m_asms.push_back(relax_and_assert(e));
+        }
+    }
+
+    expr_ref relax_and_assert(expr* e) {
+        expr_ref asum(m);
+        if (is_literal(e)) {
+            asum = e;
+        }
+        else {
+            asum = mk_fresh_bool("r");
+            e = m.mk_iff(asum, e);
+            s().assert_expr(e);
+        }
+        return asum;
+    }
+
+    bool is_literal(expr* l) {
+        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())));
+        }
+        return l_true;
+    }
+
+    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 = m_mss(mdl.get(), dummy, mss, mcs);
+        SASSERT(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";);
+        return is_sat;
+    }
+
+    void push_exprs(exprs& dst, expr_ref_vector const& src) {
+        for (unsigned i = 0; i < src.size(); ++i) {
+            dst.push_back(src[i]);
+        }
+    }
+
+    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);
+    }
+
+    void update_assignment(model* mdl) {
+        rational upper(0);
+        for (unsigned i = 0; i < m_soft.size(); ++i) {
+            if (!is_true(mdl, m_soft[i])) {
+                upper += m_weights[i];
+            }
+        }
+        if (upper > m_upper) return;
+        if (!m_c.verify_model(m_index, mdl, upper)) return;
+        m_model = mdl;
+        m_c.model_updated(mdl);
+        for (unsigned i = 0; i < m_soft.size(); ++i) {
+            m_assignment[i] = is_true(m_soft[i]);
+        }
+        // TODO: DEBUG verify assignment
+        m_upper = upper;
+        trace_bounds("mss-solver");
+    }
+
+    bool is_true(model* mdl, expr* e) {
+        expr_ref tmp(m);
+        return mdl->eval(e, tmp, true) && m.is_true(tmp);
+    }
+
+    bool is_true(expr* e) {
+        return is_true(m_model.get(), e);
+    }
+};
+
+maxsmt_solver_base* opt::mk_mss_solver(maxsat_context& c, unsigned id, weights_t& ws, expr_ref_vector const& soft) {
+    return alloc(mss_solver, c, id, ws, soft);
+}

src/opt/mss_solver.h

@@ -0,0 +1,12 @@
+#ifndef MSS_SOLVER_H_
+#define MSS_SOLVER_H_
+
+#include "opt/maxsmt.h"
+
+namespace opt {
+
+    maxsmt_solver_base* mk_mss_solver(maxsat_context& c, unsigned id, weights_t& ws, expr_ref_vector const& soft);
+
+}
+
+#endif

src/opt/opt_params.pyg

@@ -2,13 +2,13 @@ def_module_params('opt',
                   description='optimization parameters',
                   export=True,
                   params=(('optsmt_engine', SYMBOL, 'basic', "select optimization engine: 'basic', 'farkas', 'symba'"),
-                          ('maxsat_engine', SYMBOL, 'maxres', "select engine for maxsat: 'core_maxsat', 'wmax', 'maxres', 'pd-maxres'"),
+                          ('maxsat_engine', SYMBOL, 'maxres', "select engine for maxsat: 'core_maxsat', 'wmax', 'maxres', 'pd-maxres', 'mss'"),
                           ('priority', SYMBOL, 'lex', "select how to priortize objectives: 'lex' (lexicographic), 'pareto', or 'box'"),
                           ('dump_benchmarks', BOOL, False, 'dump benchmarks for profiling'),
                           ('solution_prefix', SYMBOL, '', "path prefix to dump intermediary, but non-optimal, solutions"),
                           ('timeout', UINT, UINT_MAX, 'timeout (in milliseconds) (UINT_MAX and 0 mean no timeout)'),
                           ('rlimit', UINT, 0, 'resource limit (0 means no limit)'),
-                          ('enable_sls', BOOL, False, 'enable SLS tuning during weighted maxsast'),
+                          ('enable_sls', BOOL, False, 'enable SLS tuning during weighted maxsat'),
                           ('enable_sat', BOOL, True, 'enable the new SAT core for propositional constraints'),
                           ('elim_01', BOOL, True, 'eliminate 01 variables'),
                           ('pp.neat', BOOL, True, 'use neat (as opposed to less readable, but faster) pretty printer when displaying context'),
@@ -20,8 +20,8 @@ def_module_params('opt',
                           ('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.pivot_on_correction_set', BOOL, True, 'reduce soft constraints if the current correction set is smaller than current core')
+                          ('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')
                           ))