From 3da47a280e419547ea7d5324102a6b2c0d47e123 Mon Sep 17 00:00:00 2001
From: Anh-Dung Phan <phananhdung309@yahoo.com>
Date: Wed, 16 Oct 2013 17:55:53 -0700
Subject: [PATCH] Complete Fu & Malik MAXSAT implementation

Mistakes:
(1) ast_manager shouldn't be replicated.
(2) assumptions should be used to compare with unsat cores
---
 src/opt/fu_malik.cpp | 65 ++++++++++++++++++++++++++------------------
 src/opt/fu_malik.h   |  4 +--
 2 files changed, 41 insertions(+), 28 deletions(-)

diff --git a/src/opt/fu_malik.cpp b/src/opt/fu_malik.cpp
index 92b26ad0b..07d256d9e 100644
--- a/src/opt/fu_malik.cpp
+++ b/src/opt/fu_malik.cpp
@@ -6,8 +6,8 @@ Module Name:
     fu_malik.cpp
 
 Abstract:
-    Fu&Malik built-in optimization method.
-    Adapted from sample code.
+    Fu & Malik built-in optimization method.
+    Adapted from sample code in C.
 
 Author:
 
@@ -40,16 +40,18 @@ namespace opt {
         solver& s;
         expr_ref_vector m_soft;
         expr_ref_vector m_aux;
+
     public:
+
         fu_malik(ast_manager& m, solver& s, expr_ref_vector const& soft):
             m(m),
             s(s),
             m_soft(soft),
             m_aux(m)
         {
-            for (unsigned i = 0; i < m_soft.size(); i++) {
+            for (unsigned i = 0; i < m_soft.size(); ++i) {
                 m_aux.push_back(m.mk_fresh_const("p", m.mk_bool_sort()));
-                s.assert_expr(m.mk_or(soft[i], m_aux[i].get()));
+                s.assert_expr(m.mk_or(m_soft[i].get(), m_aux[i].get()));
             }
         }
 
@@ -82,12 +84,12 @@ namespace opt {
             ptr_vector<expr> core;
             s.get_unsat_core(core);
 
-            // update soft-constraints and aux_vars
-            for (unsigned i = 0; i < m_soft.size(); i++) {
+            // Update soft-constraints and aux_vars
+            for (unsigned i = 0; i < m_soft.size(); ++i) {
                 
                 bool found = false;
                 for (unsigned j = 0; !found && j < core.size(); ++j) {
-                    found = m_soft[i].get() == core[j];
+                    found = assumptions[i].get() == core[j];
                 }
                 if (!found) {
                     continue;
@@ -106,46 +108,57 @@ 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);
+            expr_ref has_one(m), has_zero(m), at_most_one(m);
+            mk_at_most_one(block_vars.size(), block_vars.c_ptr(), has_one, has_zero);
+            at_most_one = m.mk_or(has_one, has_zero);
             s.assert_expr(at_most_one);
         }
 
-        void mk_at_most_one(unsigned n, expr* const * vars, expr_ref& has_one, expr_ref& no_one) {
+        void mk_at_most_one(unsigned n, expr* const * vars, expr_ref& has_one, expr_ref& has_zero) {
+            SASSERT(n != 0);
             if (n == 1) {
                 has_one = vars[0];
-                no_one = m.mk_not(vars[0]);
+                has_zero = 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);
+                expr_ref has_one1(m), has_one2(m), has_zero1(m), has_zero2(m);
+                mk_at_most_one(mid,   vars,     has_one1, has_zero1);
+                mk_at_most_one(n-mid, vars+mid, has_one2, has_zero2);
+                has_one = m.mk_or(m.mk_and(has_one1, has_zero2), m.mk_and(has_one2, has_zero1));
+                has_zero  = m.mk_and(has_zero1, has_zero2);
             }
         }
 
     };
-
-    // 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();
+        ast_manager& m = soft_constraints.get_manager();
         lbool is_sat = s.check_sat(0,0);
         if (!soft_constraints.empty() && is_sat == l_true) {
             s.push();
+
             fu_malik fm(m, s, soft_constraints);
             while (!fm.step());
+
+            // Get a list of satisfying soft_constraints
+            model_ref model;
+            s.get_model(model);
+
+            expr_ref_vector result(m);
+            for (unsigned i = 0; i < soft_constraints.size(); ++i) {
+                expr_ref val(m);
+                VERIFY(model->eval(soft_constraints[i].get(), val));
+                if (!m.is_false(val)) {
+                    result.push_back(soft_constraints[i].get());
+                }
+            }
+            soft_constraints.reset();
+            soft_constraints.append(result);
+
             s.pop(1);
         }
-        // we are done and soft_constraints has 
+        // We are done and soft_constraints has 
         // been updated with the max-sat assignment.
 
         return is_sat;
diff --git a/src/opt/fu_malik.h b/src/opt/fu_malik.h
index 7f3bb7eb0..6bfe37f63 100644
--- a/src/opt/fu_malik.h
+++ b/src/opt/fu_malik.h
@@ -7,7 +7,7 @@ Module Name:
 
 Abstract:
     Fu&Malik built-in optimization method.
-    Adapted from sample code.
+    Adapted from sample code in C.
 
 Author:
 
@@ -23,7 +23,7 @@ Notes:
 
 namespace opt {
     /**
-       takes solver with hard constraints added.
+       Takes solver with hard constraints added.
        Returns a maximal satisfying subset of soft_constraints
        that are still consistent with the solver state.
     */