fill in details on max sat

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

src/opt/fu_malik.cpp

@@ -38,26 +38,24 @@ namespace opt {
     class fu_malik {
         ast_manager& m;
         solver& s;
-        expr_ref_vector& m_soft;
+        expr_ref_vector m_soft;
         expr_ref_vector m_aux;
     public:
-        fu_malik(ast_manager& m, solver& s, expr_ref_vector& soft):
+        fu_malik(ast_manager& m, solver& s, expr_ref_vector const& soft):
             m(m),
             s(s),
             m_soft(soft),
-            m_aux_vars(m)
+            m_aux(m)
         {
-            m_aux.reset();
             for (unsigned i = 0; i < m_soft.size(); i++) {
-                m_aux.push_back(m.mk_fresh_const("p",m.mk_bool()));
+                m_aux.push_back(m.mk_fresh_const("p", m.mk_bool_sort()));
-                s.assert_expr(m.mk_or(m_soft[i].get(), m_aux[i].get()));
+                s.assert_expr(m.mk_or(soft[i], m_aux[i].get()));
             }
         }
 
 
         /**
-           \brief Implement one step of the Fu&Malik algorithm.
+           \brief One step of the Fu&Malik algorithm.
-           See fu_malik_maxsat function for more details.
            
            Input:    soft constraints + aux-vars (aka answer literals) 
            Output:   done/not-done  when not done return updated set of soft-constraints and aux-vars. 
@@ -85,7 +83,7 @@ namespace opt {
             s.get_unsat_core(core);
 
             // update soft-constraints and aux_vars
-            for (i = 0; i < m_soft.size(); i++) {
+            for (unsigned i = 0; i < m_soft.size(); i++) {
                 
                 bool found = false;
                 for (unsigned j = 0; !found && j < core.size(); ++j) {
@@ -108,36 +106,49 @@ namespace opt {
     private:
 
         void assert_at_most_one(expr_ref_vector const& block_vars) {
-            
+            expr_ref has_one(m), no_one(m), at_most_one(m);
+            mk_at_most_one(block_vars.size(), block_vars.c_ptr(), has_one, no_one);
+            at_most_one = m.mk_or(has_one, no_one);
+            s.assert_expr(at_most_one);
         }
 
-#if 0
+        void mk_at_most_one(unsigned n, expr* const * vars, expr_ref& has_one, expr_ref& no_one) {
-        expr_ref mk_at_most_one(unsigned n, expr* const * vars) {
+            if (n == 1) {
-            if (n <= 1) {
+                has_one = vars[0];
-                return expr_ref(m.mk_true(), m);
+                no_one = m.mk_not(vars[0]);
             }
+            else {
                 unsigned mid = n/2;
-            
+                expr_ref has_one1(m), has_one2(m), no_one1(m), no_one2(m);
+                mk_at_most_one(mid,   vars,     has_one1, no_one1);
+                mk_at_most_one(n-mid, vars+mid, has_one2, no_one2);
+                has_one = m.mk_or(m.mk_and(has_one1, no_one2), m.mk_and(has_one2, no_one1));
+                no_one  = m.mk_and(no_one1, no_one2);
+            }
         }
-#endif
 
     };
 
+    // TBD: the vector of soft constraints gets updated
+    // but we really want to return the maximal set of
+    // original soft constraints that are satisfied.
+    // so we need to read out of the model what soft constraints
+    // were satisfied. 
+
     
     lbool fu_malik_maxsat(solver& s, expr_ref_vector& soft_constraints) {
         ast_manager m = soft_constraints.get_manager();
-        lbool is_sat = s.check();
+        lbool is_sat = s.check_sat(0,0);
-        if (is_sat != l_true) {
+        if (!soft_constraints.empty() && is_sat == l_true) {
-            return is_sat;
-        }
-        if (soft_constraints.empty()) {
-            return is_sat;
-        }
             s.push();
             fu_malik fm(m, s, soft_constraints);
             while (!fm.step());
-        s.pop();
+            s.pop(1);
-        // we are done and soft_constraints has been updated with the max-sat assignment.
+        }
+        // we are done and soft_constraints has 
+        // been updated with the max-sat assignment.
+
+        return is_sat;
     }
 };
 

src/opt/opt_cmds.cpp

@@ -18,6 +18,8 @@ Notes:
 #include "opt_cmds.h"
 #include "cmd_context.h"
 #include "ast_pp.h"
+#include "smt_solver.h"
+#include "fu_malik.h"
 
 class opt_context {
     ast_manager& m;
@@ -93,7 +95,6 @@ public:
     }
 
     virtual void execute(cmd_context & ctx) {
-        std::cout << "TODO: " << mk_pp(m_formula, ctx.m()) << " " << m_weight << "\n";
         m_opt_ctx->add_formula(m_formula, m_weight);
         reset(ctx);
     }
@@ -141,22 +142,51 @@ public:
     }
 
     virtual void execute(cmd_context & ctx) {
+        ast_manager& m = m_term.get_manager();
         std::cout << "TODO: " << mk_pp(m_term, ctx.m()) << "\n";
         // Here is how to retrieve the soft constraints
-        m_opt_ctx->formulas();
+        expr_ref_vector const& fmls = m_opt_ctx->formulas();
-        m_opt_ctx->weights();
+        vector<rational> const& ws  = m_opt_ctx->weights();
-        get_background(ctx);
+
-        // reset m_opt_ctx?
+        // TODO: move most functionaltiy to separate module, because it is going to grow..
-    }
+        ref<solver> s;
+        symbol logic;
+        params_ref p;
+        p.set_bool("model", true);
+        p.set_bool("unsat_core", true);        
+        s = mk_smt_solver(m, p, logic);
 
-private:
-    void get_background(cmd_context& ctx) {
         ptr_vector<expr>::const_iterator it  = ctx.begin_assertions();
         ptr_vector<expr>::const_iterator end = ctx.end_assertions();
         for (; it != end; ++it) {
-            // Need a solver object that supports soft constraints
+            s->assert_expr(*it);
-            // m_solver.assert_expr(*it);
         }
+        expr_ref_vector fmls_copy(fmls);
+        if (is_maxsat_problem(ws)) {
+            lbool is_sat = opt::fu_malik_maxsat(*s, fmls_copy);
+            std::cout << "is-sat: " << is_sat << "\n";
+            if (is_sat == l_true) {
+                for (unsigned i = 0; i < fmls_copy.size(); ++i) {
+                    std::cout << mk_pp(fmls_copy[i].get(), m) << "\n";
+                }
+            }
+        }
+        else {
+            NOT_IMPLEMENTED_YET();
+        }
+
+        // handle optimization criterion.        
+    }
+
+private:
+
+    bool is_maxsat_problem(vector<rational> const& ws) const {
+        for (unsigned i = 0; i < ws.size(); ++i) {
+            if (!ws[i].is_one()) {
+                return false;
+            }
+        }
+        return true;
     }
 
 };