first implementation of maxres

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

src/opt/hitting_sets.cpp

@@ -40,11 +40,12 @@ namespace opt {
         public:
             explicit justification(kind_t k):m_kind(k), m_value(0), m_pos(false) {}
             explicit justification(unsigned v, bool pos):m_kind(CLAUSE), m_value(v), m_pos(pos) {}
-            justification(justification const& other): m_kind(other.m_kind), m_value(other.m_value), m_pos(other.m_pos) {}
+            justification(justification const& other): 
+                m_kind(other.m_kind), m_value(other.m_value), m_pos(other.m_pos) {}
             justification& operator=(justification const& other) {
-                m_kind = other.m_kind;
+                m_kind  = other.m_kind;
                 m_value = other.m_value;
-                m_pos = other.m_pos;
+                m_pos   = other.m_pos;
                 return *this;
             }
             unsigned clause() const { return m_value; }
@@ -147,6 +148,7 @@ namespace opt {
             m_cancel(false), 
             m_max_weight(0), 
             m_denominator(1),
+            m_alloc("hitting-sets"),
             m_weights_var(0),
             m_qhead(0),
             m_scope_lvl(0),
@@ -157,7 +159,14 @@ namespace opt {
             m_enable_simplex = true;
 
         }
-        ~imp() {}
+        ~imp() {
+            for (unsigned i = 0; i < m_T.size(); ++i) {
+                m_alloc.deallocate(m_T[i]->alloc_size(), m_T[i]);
+            }
+            for (unsigned i = 0; i < m_F.size(); ++i) {
+                m_alloc.deallocate(m_F[i]->alloc_size(), m_F[i]);
+            }
+        }
 
         void add_weight(rational const& w) {
             SASSERT(w.is_pos());
@@ -198,9 +207,7 @@ namespace opt {
             ptr_vector<set>& Sets = sign?m_F:m_T;
             vector<unsigned_vector>& watch = sign?m_fwatch:m_twatch;
             init_weights();            
-            if (sz == 0) {                
+            if (sz == 0) { 
-                // TBD
-                IF_VERBOSE(0, verbose_stream() << "empty clause\n";);
                 set_conflict(0, justification(justification::AXIOM));
             }
             else if (sz == 1) {                
@@ -375,7 +382,8 @@ namespace opt {
             }
             out << "trail\n";
             for (unsigned i = 0; i < m_trail.size(); ++i) {
-                out << m_trail[i] << " ";
+                unsigned idx = m_trail[i];
+                out << (m_justification[idx].is_decision()?"d":"") << idx << " ";
             }
             out << "\n";
         }
@@ -406,6 +414,14 @@ namespace opt {
             }
         }
 
+        void display_lemma(std::ostream& out) {
+            out << "lemma: ";
+            for (unsigned i = 0; i < m_lemma.size(); ++i) {
+                out << m_lemma[i] << " ";
+            }
+            out << "\n";
+        }
+
         struct scoped_push {
             imp& s;
             scoped_push(imp& s):s(s) { s.push(); }
@@ -850,11 +866,7 @@ namespace opt {
             }
             while (num_marks > 0);
             m_lemma[0] = conflict_l;
-            TRACE("opt",
+            TRACE("opt", display_lemma(tout););
-                  for (unsigned i = 0; i < m_lemma.size(); ++i) {
-                      tout << m_lemma[i] << " ";
-                  }
-                  tout << "\n";);
             SASSERT(value(conflict_l) == l_true);
             unsigned new_scope_lvl = 0;
             for (unsigned i = 1; i < m_lemma.size(); ++i) {
@@ -1046,15 +1058,21 @@ namespace opt {
                 }                    
             }
             // undo the lower bounds.
+            TRACE("opt",
+                  tout << "prune branch: " << m_weight << " ";
+                  display_lemma(tout);
+                  display(tout);
+                  );
             justification j = add_exists_false(m_lemma.size(), m_lemma.c_ptr());
-            TRACE("opt", display(tout, j););
+            unsigned idx = m_lemma.empty()?0:m_lemma[0];
-            set_conflict(m_lemma[0], j);                
+            set_conflict(idx, j);                            
         }
 
         // TBD: derive strong inequalities and add them to Simplex.
-        // x_i1 + .. + x_ik >= k-1 for each subset k from set n:  x_1 + .. + x_n >= k 
+        // x_i1 + .. + x_ik >= k-1 for each subset k from set n:  x_1 + .. + x_n >= k         
-        
     };
+
+
     hitting_sets::hitting_sets() { m_imp = alloc(imp); }
     hitting_sets::~hitting_sets() { dealloc(m_imp); }
     void hitting_sets::add_weight(rational const& w) { m_imp->add_weight(w); }

src/opt/maxres.cpp

@@ -0,0 +1,194 @@
+#include "solver.h"
+#include "maxsmt.h"
+#include "maxres.h"
+#include "ast_pp.h"
+
+
+using namespace opt;
+
+struct maxres::imp {
+    ast_manager&    m;
+    solver&         s;
+    expr_ref_vector m_B;
+    expr_ref_vector m_D;
+    expr_ref_vector m_asms;    
+    model_ref       m_model;
+    expr_ref_vector m_soft_constraints;
+    volatile bool   m_cancel;
+    rational        m_lower;
+    rational        m_upper;
+
+    imp(ast_manager& m, solver& s, expr_ref_vector& soft_constraints):
+        m(m), s(s), m_B(m), m_D(m), m_asms(m), m_soft_constraints(soft_constraints),
+        m_cancel(false)
+    {
+    }
+
+    bool is_literal(expr* l) {
+        return 
+            is_uninterp_const(l) ||
+            m.is_not(l, l) && is_uninterp_const(l);
+    }
+
+    void add_soft(expr* e) {
+        TRACE("opt", tout << mk_pp(e, m) << "\n";);
+        if (is_literal(e)) {
+            m_asms.push_back(e);
+        }
+        else {
+            expr_ref asum(m), fml(m);
+            asum = m.mk_fresh_const("soft", m.mk_bool_sort());
+            fml = m.mk_implies(asum, e);
+            s.assert_expr(fml);
+            m_asms.push_back(asum);
+        }
+    }
+
+    lbool operator()() {
+        expr_ref fml(m);
+        solver::scoped_push _sc(s);
+        for (unsigned i = 0; i < m_soft_constraints.size(); ++i) {
+            add_soft(m_soft_constraints[i].get());
+        }
+        m_upper = rational(m_soft_constraints.size());
+        while (true) {
+            TRACE("opt", 
+                  display_vec(tout, m_asms.size(), m_asms.c_ptr());
+                  s.display(tout);
+                  tout << "\n";
+                  );
+            lbool is_sat = s.check_sat(m_asms.size(), m_asms.c_ptr());
+            if (m_cancel) {
+                return l_undef;
+            }
+            switch (is_sat) {
+            case l_true: 
+                s.get_model(m_model);
+                m_upper = m_lower;
+                return l_true;
+            case l_undef:
+                return l_undef;
+            default:
+                ptr_vector<expr> core;
+                s.get_unsat_core(core);
+                TRACE("opt", display_vec(tout << "core: ", core.size(), core.c_ptr()););
+                if (core.empty()) {
+                    return l_false;
+                }
+                max_resolve(core);
+                fml = m.mk_not(m.mk_and(m_B.size(), m_B.c_ptr()));
+                s.assert_expr(fml);
+                m_lower += rational::one();
+                break;
+            }
+            IF_VERBOSE(1, verbose_stream() << "(opt.max_res lower: " << m_lower << ")\n";);
+        }
+        return l_true;
+    }
+
+    void display_vec(std::ostream& out, unsigned sz, expr* const* args) {
+        for (unsigned i = 0; i < sz; ++i) {
+            out << mk_pp(args[i], m) << " ";
+        }
+        out << "\n";
+    }
+
+    void max_resolve(ptr_vector<expr>& core) {
+        SASSERT(!core.empty());
+        expr_ref fml(m), asum(m);
+        m_B.reset();
+        m_D.reset();
+        m_D.resize(core.size());
+        m_B.append(core.size(), core.c_ptr());
+        m_D[core.size()-1] = m.mk_false();
+        //
+        // d_{sz-1} := false
+        // d_i := (!core_{i+1} or d_{i+1})    for i = 0...sz-2
+        // soft (!d_i or core_i) 
+        //
+        remove_core(core);
+        for (unsigned i = core.size()-1; i > 0; ) {
+            --i;
+            expr* d_i1 = m_D[i+1].get();
+            expr* b_i = m_B[i].get();
+            expr* b_i1 = m_B[i+1].get();
+            m_D[i] = m.mk_implies(b_i1, d_i1);
+            expr* d_i = m_D[i].get();
+            asum = m.mk_fresh_const("a", m.mk_bool_sort());
+            fml = m.mk_implies(asum, m.mk_implies(d_i, b_i));
+            s.assert_expr(fml);
+            m_asms.push_back(asum);
+        }
+    }
+
+    void remove_core(ptr_vector<expr> const& core) {
+        for (unsigned i = 0; i < m_asms.size(); ++i) {
+            if (core.contains(m_asms[i].get())) {
+                m_asms[i] = m_asms.back();
+                m_asms.pop_back();
+                --i;
+            }
+        }
+    }
+
+    rational get_lower() const {
+        return m_lower;
+    }
+
+    rational get_upper() const {        
+        return m_upper;
+    }
+
+    bool get_assignment(unsigned index) const {
+        expr_ref tmp(m);
+        m_model->eval(m_soft_constraints[index], tmp);
+        return m.is_true(tmp);
+    }
+    void set_cancel(bool f) {
+        m_cancel = f;
+    }
+    void collect_statistics(statistics& st) const {
+    }
+    void get_model(model_ref& mdl) {
+        mdl = m_model;
+    }
+    void updt_params(params_ref& p) {
+        ;
+    }
+
+};
+
+maxres::maxres(ast_manager& m, solver& s, expr_ref_vector& soft_constraints) {
+    m_imp = alloc(imp, m, s, soft_constraints);
+}
+
+maxres::~maxres() {
+    dealloc(m_imp);
+}
+
+
+lbool maxres::operator()() {
+    return (*m_imp)();
+}
+
+rational maxres::get_lower() const {
+    return m_imp->get_lower();
+}
+rational maxres::get_upper() const {
+    return m_imp->get_upper();
+}
+bool maxres::get_assignment(unsigned index) const {
+    return m_imp->get_assignment(index);
+}
+void maxres::set_cancel(bool f) {
+    m_imp->set_cancel(f);
+}
+void maxres::collect_statistics(statistics& st) const {
+    m_imp->collect_statistics(st);
+}
+void maxres::get_model(model_ref& mdl) {
+    m_imp->get_model(mdl);
+}
+void maxres::updt_params(params_ref& p) {
+    m_imp->updt_params(p);
+}

src/opt/maxres.h

@@ -0,0 +1,18 @@
+
+namespace opt {
+    class maxres : public maxsmt_solver {
+        struct imp;
+        imp* m_imp;
+    public:
+        maxres(ast_manager& m, solver& s, expr_ref_vector& soft_constraints);
+        ~maxres();
+        virtual lbool operator()();
+        virtual rational get_lower() const;
+        virtual rational get_upper() const;
+        virtual bool get_assignment(unsigned index) const;
+        virtual void set_cancel(bool f);
+        virtual void collect_statistics(statistics& st) const;
+        virtual void get_model(model_ref& mdl);
+        virtual void updt_params(params_ref& p);
+    };
+};

src/opt/maxsmt.cpp

@@ -21,6 +21,7 @@ Notes:
 #include "maxsmt.h"
 #include "fu_malik.h"
 #include "core_maxsat.h"
+#include "maxres.h"
 #include "weighted_maxsat.h"
 #include "ast_pp.h"
 #include "opt_params.hpp"
@@ -45,6 +46,9 @@ namespace opt {
             else if (m_maxsat_engine == symbol("weighted_maxsat")) {
                 m_msolver = alloc(wmaxsmt, m, m_s.get(), m_soft_constraints, m_weights);
             }
+            else if (m_maxsat_engine == symbol("maxres")) {
+                m_msolver = alloc(maxres, m, *m_s, m_soft_constraints);
+            }
             else {
                 m_msolver = alloc(fu_malik, m, *m_s, m_soft_constraints);
             }