adding core-based max-sat

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

src/opt/core_maxsat.cpp

@@ -0,0 +1,127 @@
+/*++
+Copyright (c) 2013 Microsoft Corporation
+
+Module Name:
+
+    core_maxsat.h
+
+Abstract:
+
+    Core and SAT guided MaxSAT with cardinality constraints.
+
+Author:
+
+    Nikolaj Bjorner (nbjorner) 2013-11-9
+
+Notes:
+
+--*/
+#include "core_maxsat.h"
+#include "card_decl_plugin.h"
+
+namespace opt {
+
+        
+    core_maxsat::core_maxsat(ast_manager& m, solver& s, expr_ref_vector& soft_constraints):
+        m(m), s(s), m_soft(soft_constraints), m_answer(m) {
+        m_upper = m_soft.size();
+    }
+    
+    core_maxsat::~core_maxsat() {}
+    
+    lbool core_maxsat::operator()() {
+        expr_ref_vector aux(m);         // auxiliary variables to track soft constraints
+        expr_set core_vars;             // variables used so far in some core
+        expr_set block_vars;            // variables that should be blocked.
+        solver::scoped_push _sp(s);
+        for (unsigned i = 0; i < m_soft.size(); ++i) {
+            expr* a = m.mk_fresh_const("p", m.mk_bool_sort());
+            aux.push_back(a);
+            s.assert_expr(m.mk_implies(a, m_soft[i].get()));
+            block_vars.insert(a);
+        }            
+        while (m_answer.size() < m_upper) {
+            ptr_vector<expr> vars;
+            set2vector(block_vars, vars);
+            lbool is_sat = s.check_sat(vars.size(), vars.c_ptr());
+            
+            switch(is_sat) {
+            case l_undef: 
+                return l_undef;
+            case l_true: {
+                model_ref model;
+                expr_ref_vector ans(m);
+                s.get_model(model);
+                
+                for (unsigned i = 0; i < aux.size(); ++i) {
+                    expr_ref val(m);
+                    VERIFY(model->eval(m_soft[i].get(), val));
+                    if (m.is_true(val)) {
+                        ans.push_back(m_soft[i].get());
+                    }
+                }
+                if (ans.size() > m_answer.size()) {
+                    m_answer.reset();
+                    m_answer.append(ans);
+                }
+                unsigned k = m_soft.size()-m_answer.size()-1; // TBD: fix this
+                expr_ref fml = mk_at_most(core_vars, k);
+                s.assert_expr(fml);
+                break;                    
+            }
+            case l_false: {
+                ptr_vector<expr> core;
+                s.get_unsat_core(core);
+                for (unsigned i = 0; i < core.size(); ++i) {
+                    core_vars.insert(core[i]);
+                    block_vars.remove(core[i]);
+                }
+                if (core.empty()) {
+                    m_upper = m_answer.size();
+                    return l_true;
+                }
+                else {
+                    // at least one core variable is True
+                    expr_ref fml = mk_at_most(core_vars, 0);
+                    fml = m.mk_not(fml);
+                    s.assert_expr(fml);
+                }
+                --m_upper;
+            }
+            }            
+        }
+        return l_true;
+    }
+    
+    void core_maxsat::set2vector(expr_set const& set, ptr_vector<expr>& es) const {
+        es.reset();
+        expr_set::iterator it = set.begin(), end = set.end();
+        for (; it != end; ++it) {
+            es.push_back(*it);
+        }
+    }
+
+    expr_ref core_maxsat::mk_at_most(expr_set const& set, unsigned k) {
+        card_util card(m);
+        ptr_vector<expr> es;
+        set2vector(set, es);
+        return expr_ref(card.mk_at_most_k(es.size(), es.c_ptr(), k), m);
+    }
+    
+    rational core_maxsat::get_lower() const {
+        return rational(m_answer.size());
+    }
+    rational core_maxsat::get_upper() const {
+        return rational(m_upper);
+    }
+    rational core_maxsat::get_value() const {
+        return get_lower();
+    }
+    expr_ref_vector core_maxsat::get_assignment() const {
+        return m_answer;
+    }
+    void core_maxsat::set_cancel(bool f) {
+        
+    }
+    
+};

src/opt/core_maxsat.h

@@ -0,0 +1,51 @@
+/*++
+Copyright (c) 2013 Microsoft Corporation
+
+Module Name:
+
+    core_maxsat.h
+
+Abstract:
+    Core and SAT guided MaxSAT with cardinality constraints.
+
+Author:
+
+    Nikolaj Bjorner (nbjorner) 2013-11-9
+
+Notes:
+
+--*/
+#ifndef _OPT_CORE_MAXSAT_H_
+#define _OPT_CORE_MAXSAT_H_
+
+#include "solver.h"
+#include "maxsmt.h"
+
+namespace opt {
+
+    class core_maxsat : public maxsmt_solver {
+        typedef obj_hashtable<expr> expr_set;
+
+        ast_manager&    m;
+        solver&         s;
+        expr_ref_vector m_soft;
+        expr_ref_vector m_answer;
+        unsigned        m_upper;
+    public:
+        core_maxsat(ast_manager& m, solver& s, expr_ref_vector& soft_constraints);
+        virtual ~core_maxsat();
+        virtual lbool operator()();
+        virtual rational get_lower() const;
+        virtual rational get_upper() const;
+        virtual rational get_value() const;
+        virtual expr_ref_vector get_assignment() const;
+        virtual void set_cancel(bool f);
+
+    private:
+        void set2vector(expr_set const& set, ptr_vector<expr>& es) const;
+        expr_ref mk_at_most(expr_set const& set, unsigned k);
+    };
+    
+};
+
+#endif

src/opt/fu_malik.cpp

@@ -53,10 +53,6 @@ namespace opt {
             m_aux(m),
             m_assignment(m)
         {
-            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(m_soft[i].get(), m_aux[i].get()));
-            }
             m_upper_size = m_soft.size() + 1;
         }
 
@@ -139,6 +135,10 @@ namespace opt {
             lbool is_sat = s.check_sat(0,0);
             if (!m_soft.empty() && is_sat == l_true) {
                 solver::scoped_push _sp(s);
+                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(m_soft[i].get(), m_aux[i].get()));
+                }
                 
                 lbool is_sat = l_true;                
                 do {