adding maxlex, throttle use of asymmetric literal addition

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

src/opt/CMakeLists.txt

@@ -1,5 +1,6 @@
 z3_add_component(opt
   SOURCES
+    maxlex.cpp
     maxres.cpp
     maxsmt.cpp
     opt_cmds.cpp

src/opt/maxlex.cpp

@@ -0,0 +1,185 @@
+/*++
+Copyright (c) 2019 Microsoft Corporation
+
+Module Name:
+
+    maxlex.cpp
+
+Abstract:
+   
+    MaxLex solves weighted max-sat problems where weights impose lexicographic order.
+    MaxSAT is particularly easy for this class:
+     In order of highest weight, check if soft constraint can be satisfied.
+     If so, assert it, otherwise assert the negation and record whether the soft 
+     constraint is true or false in the solution.
+
+Author:
+
+    Nikolaj Bjorner (nbjorner) 2019-25-1
+
+--*/
+
+#include "opt/opt_context.h"
+#include "opt/maxsmt.h"
+#include "opt/maxlex.h"
+
+namespace opt {
+
+    bool is_maxlex(weights_t & _ws) {
+        vector<rational> ws(_ws);
+        std::sort(ws.begin(), ws.end());
+        ws.reverse();
+        rational sum(0);
+        for (rational const& w : ws) {
+            sum += w;
+        }
+        for (rational const& w : ws) {
+            if (sum > w + w) return false;
+            sum -= w;
+        }
+        return true;
+    }
+
+    class maxlex : public maxsmt_solver_base {
+
+        struct cmp_soft {
+            bool operator()(soft const& s1, soft const& s2) const {
+                return s1.weight > s2.weight;
+            }
+        };
+
+        ast_manager&    m;
+        maxsat_context& m_c;
+        
+        void update_assignment() {
+            model_ref mdl;
+            s().get_model(mdl);
+            if (mdl) {
+                m_c.model_updated(mdl.get());
+                update_assignment(mdl);
+            }
+        }
+
+        void assert_value(soft& soft) {
+            switch (soft.value) {
+            case l_true:
+                s().assert_expr(soft.s);
+                break;
+            case l_false: 
+                s().assert_expr(expr_ref(m.mk_not(soft.s), m));
+                break;
+            default:
+                break;
+            }
+        }
+
+        void set_value(soft& soft, lbool v) {
+            soft.set_value(v);
+            assert_value(soft);
+        }
+
+        void update_assignment(model_ref & mdl) {
+            for (auto & soft : m_soft) {
+                switch (soft.value) {
+                case l_undef:
+                    if (mdl->is_true(soft.s)) {
+                        set_value(soft, l_true);
+                    }
+                    else {
+                        update_bounds();
+                        return;
+                    }
+                    break;
+                case l_true:
+                    break;
+                case l_false:
+                    break;
+                }
+            }
+            update_bounds();
+        }
+        
+        void update_bounds() {
+            m_lower.reset();
+            m_upper.reset();
+            bool prefix_defined = true;
+            for (auto & soft : m_soft) {
+                if (!prefix_defined) {
+                    m_upper += soft.weight;
+                    continue;
+                }
+                switch (soft.value) {
+                case l_undef:
+                    prefix_defined = false;
+                    m_upper += soft.weight;
+                    break;
+                case l_true:
+                    break;
+                case l_false:
+                    m_lower += soft.weight;
+                    m_upper += soft.weight;
+                    break;
+                }
+            }
+            trace_bounds("maxlex");
+        }
+
+        void init() {
+            model_ref mdl;
+            s().get_model(mdl);
+            update_assignment(mdl);
+        }
+
+    public:
+
+        maxlex(maxsat_context& c, unsigned id, weights_t & ws, expr_ref_vector const& s):
+            maxsmt_solver_base(c, ws, s),
+            m(c.get_manager()),
+            m_c(c) {
+            cmp_soft cmp;
+            std::sort(m_soft.begin(), m_soft.end(), cmp);
+        }
+            
+        
+        lbool operator()() override {
+            init();
+
+            for (auto & soft : m_soft) {
+                if (soft.value == l_true) {
+                    continue;
+                }
+                SASSERT(soft.value() == l_undef);
+                expr* a = soft.s;                
+                lbool is_sat = s().check_sat(1, &a);
+                switch (is_sat) {
+                case l_false: 
+                    set_value(soft, l_false);
+                    update_bounds();
+                    break;
+                case l_true:
+                    update_assignment();
+                    SASSERT(soft.value == l_true);
+                    break;
+                case l_undef:
+                    return l_undef;
+                }
+            }
+            return l_true;
+        }
+
+        void commit_assignment() override {
+            for (auto & soft : m_soft) {
+                if (soft.value == l_undef) {
+                    return;
+                }
+                assert_value(soft);
+            }
+        }
+
+    };
+
+    maxsmt_solver_base* mk_maxlex(maxsat_context& c, unsigned id, weights_t & ws, expr_ref_vector const& soft) {
+        return alloc(maxlex, c, id, ws, soft);
+    }
+
+}

src/opt/maxlex.h

@@ -0,0 +1,32 @@
+/*++
+Copyright (c) 2014 Microsoft Corporation
+
+Module Name:
+
+    maxlex.h
+
+Abstract:
+   
+    MaxLex solves weighted max-sat problems where weights impose lexicographic order.
+
+Author:
+
+    Nikolaj Bjorner (nbjorner) 2019-25-1
+
+Notes:
+
+--*/
+
+#ifndef MAXLEX_H_
+#define MAXLEX_H_
+
+namespace opt {
+
+    bool is_maxlex(weights_t & ws);
+
+    maxsmt_solver_base* mk_maxlex(maxsat_context& c, unsigned id, weights_t & ws, expr_ref_vector const& soft);
+
+
+};
+
+#endif

src/opt/maxres.cpp

@@ -329,8 +329,8 @@ public:
         verify_assumptions();
         m_lower.reset();
         for (soft& s : m_soft) {
-            s.is_true = m_model->is_true(s.s);
+            s.set_value(m_model->is_true(s.s));
-            if (!s.is_true) {
+            if (!s.is_true()) {
                 m_lower += s.weight;
             }
         }
@@ -764,7 +764,7 @@ public:
         TRACE("opt", tout << "updated upper: " << upper << "\nmodel\n" << *m_model;);
 
         for (soft& s : m_soft) {
-            s.is_true = m_model->is_true(s.s);
+            s.set_value(m_model->is_true(s.s));
         }
        
         verify_assignment();
@@ -878,7 +878,7 @@ public:
         expr_ref n(m);
         for (soft& s : m_soft) {
             n = s.s;
-            if (!s.is_true) {
+            if (!s.is_true()) {
                 n = mk_not(m, n);
             }
             _solver->assert_expr(n);

src/opt/maxsmt.cpp

@@ -18,17 +18,18 @@ Notes:
 --*/
 
 #include <typeinfo>
+#include "util/uint_set.h"
+#include "ast/ast_pp.h"
+#include "ast/ast_util.h"
+#include "ast/pb_decl_plugin.h"
 #include "opt/maxsmt.h"
 #include "opt/maxres.h"
+#include "opt/maxlex.h"
 #include "opt/wmax.h"
 #include "opt/opt_params.hpp"
-#include "ast/ast_pp.h"
-#include "util/uint_set.h"
 #include "opt/opt_context.h"
 #include "smt/theory_wmaxsat.h"
 #include "smt/theory_pb.h"
-#include "ast/ast_util.h"
-#include "ast/pb_decl_plugin.h"
 
 
 namespace opt {
@@ -61,7 +62,7 @@ namespace opt {
         rational k(0), cost(0);
         vector<rational> weights;
         for (soft const& s : m_soft) {
-            if (s.is_true) {
+            if (s.is_true()) {
                 k += s.weight;
             }
             else {
@@ -80,13 +81,13 @@ namespace opt {
         m_lower.reset();
         m_upper.reset();
         for (soft& s : m_soft) {
-            s.is_true = m.is_true(s.s);
+            s.set_value(m.is_true(s.s));
-            if (!s.is_true) m_upper += s.weight;
+            if (!s.is_true()) m_upper += s.weight;
         }
         
         TRACE("opt", 
               tout << "upper: " << m_upper << " assignments: ";
-              for (soft& s : m_soft) tout << (s.is_true?"T":"F");              
+              for (soft& s : m_soft) tout << (s.is_true()?"T":"F");              
               tout << "\n";);
         return true;
     }
@@ -234,7 +235,10 @@ namespace opt {
         symbol const& maxsat_engine = m_c.maxsat_engine();
         IF_VERBOSE(1, verbose_stream() << "(maxsmt)\n";);
         TRACE("opt_verbose", s().display(tout << "maxsmt\n") << "\n";);
-        if (m_soft_constraints.empty() || maxsat_engine == symbol("maxres") || maxsat_engine == symbol::null) {            
+        if (is_maxlex(m_weights)) {
+            m_msolver = mk_maxlex(m_c, m_index, m_weights, m_soft_constraints);
+        }
+        else if (m_soft_constraints.empty() || maxsat_engine == symbol("maxres") || maxsat_engine == symbol::null) {            
             m_msolver = mk_maxres(m_c, m_index, m_weights, m_soft_constraints);
         }
         else if (maxsat_engine == symbol("pd-maxres")) {            

src/opt/maxsmt.h

@@ -59,10 +59,13 @@ namespace opt {
         struct soft { 
             expr_ref  s; 
             rational  weight; 
-            bool      is_true;
+            lbool     value;
-            soft(expr_ref const& s, rational const& w, bool t): s(s), weight(w), is_true(t) {}
+            void set_value(bool t) { value = t?l_true:l_undef; }
-            soft(soft const& other):s(other.s), weight(other.weight), is_true(other.is_true) {}
+            void set_value(lbool t) { value = t; }
-            soft& operator=(soft const& other) { s = other.s; weight = other.weight; is_true = other.is_true; return *this; }            
+            bool is_true() const { return value == l_true; }
+            soft(expr_ref const& s, rational const& w, bool t): s(s), weight(w), value(t?l_true:l_undef) {}
+            soft(soft const& other):s(other.s), weight(other.weight), value(other.value) {}
+            soft& operator=(soft const& other) { s = other.s; weight = other.weight; value = other.value; return *this; }            
         };
         ast_manager&     m;
         maxsat_context&  m_c;        
@@ -84,7 +87,7 @@ namespace opt {
         ~maxsmt_solver_base() override {}
         rational get_lower() const override { return m_lower; }
         rational get_upper() const override { return m_upper; }
-        bool get_assignment(unsigned index) const override { return m_soft[index].is_true; }
+        bool get_assignment(unsigned index) const override { return m_soft[index].is_true(); }
         void collect_statistics(statistics& st) const override { }
         void get_model(model_ref& mdl, svector<symbol>& labels) override { mdl = m_model.get(); labels = m_labels;}
         virtual void commit_assignment();

src/opt/sortmax.cpp

@@ -114,7 +114,7 @@ namespace opt {
         }
 
         void update_assignment() {
-            for (soft& s : m_soft) s.is_true = is_true(s.s);
+            for (soft& s : m_soft) s.set_value(is_true(s.s));
         }
 
         bool is_true(expr* e) {

src/opt/wmax.cpp

@@ -122,7 +122,7 @@ namespace opt {
         }
 
         void update_assignment() {
-            for (soft& s : m_soft) s.is_true = is_true(s.s);
+            for (soft& s : m_soft) s.set_value(is_true(s.s));
         }
 
         struct compare_asm {

src/sat/sat_simplifier.cpp

@@ -1014,6 +1014,9 @@ namespace sat {
         svector<bool>  m_in_intersection;
         unsigned       m_ala_qhead;
         clause_wrapper m_clause;
+        unsigned       m_ala_cost;
+        unsigned       m_ala_benefit;
+        unsigned       m_ala_max_cost;
 
         blocked_clause_elim(simplifier & _s, unsigned limit, model_converter & _mc, use_list & l,
                             vector<watch_list> & wlist):
@@ -1021,8 +1024,11 @@ namespace sat {
             m_counter(limit),
             m_mc(_mc),
             m_queue(l, wlist),
-            m_clause(null_literal, null_literal) {
+            m_clause(null_literal, null_literal),
+            m_ala_cost(0),
+            m_ala_benefit(0) {
             m_in_intersection.resize(s.s.num_vars() * 2, false);
+            m_ala_max_cost = (s.s.m_clauses.size() * s.m_num_calls)/5;
         }
 
         void insert(literal l) {
@@ -1034,6 +1040,10 @@ namespace sat {
             return !s.s.is_assumption(v) && !s.was_eliminated(v) && !s.is_external(v) && s.value(v) == l_undef;
         }
 
+        bool reached_max_cost() {
+            return m_ala_benefit <= m_ala_cost * 100 && m_ala_cost > m_ala_max_cost;
+        }
+
         enum elim_type {
             bce_t,
             cce_t,
@@ -1296,13 +1306,15 @@ namespace sat {
          */
         bool add_ala() {
             unsigned init_size = m_covered_clause.size();
-            for (; m_ala_qhead < m_covered_clause.size() && m_ala_qhead < 5*init_size; ++m_ala_qhead) {
+            for (; m_ala_qhead < m_covered_clause.size() && m_ala_qhead < 5*init_size && !reached_max_cost(); ++m_ala_qhead) {
+                ++m_ala_cost;
                 literal l = m_covered_clause[m_ala_qhead];                
                 for (watched & w : s.get_wlist(~l)) {
                     if (w.is_binary_non_learned_clause()) {
                         literal lit = w.get_literal();
                         if (revisit_binary(l, lit)) continue;
                         if (s.is_marked(lit)) {
+                            ++m_ala_benefit;
                             return true;
                         }
                         if (!s.is_marked(~lit)) {
@@ -1333,6 +1345,7 @@ namespace sat {
                     }
                     if (!ok) continue;
                     if (lit1 == null_literal) {
+                        ++m_ala_benefit;
                         return true;
                     }
                     m_covered_clause.push_back(~lit1);
@@ -1504,7 +1517,9 @@ namespace sat {
 
         template<elim_type et>
         void cce_binary() {
-            while (!m_queue.empty() && m_counter >= 0) {
+            m_ala_cost = 0;
+            m_ala_benefit = 0;
+            while (!m_queue.empty() && m_counter >= 0 && !reached_max_cost()) {
                 s.checkpoint();
                 process_cce_binary<et>(m_queue.next());
             }
@@ -1516,7 +1531,7 @@ namespace sat {
             watch_list & wlist = s.get_wlist(~l);
             m_counter -= wlist.size();
             model_converter::kind k;
-            for (watched & w : wlist) {
+            for (watched& w : wlist) {
                 if (!w.is_binary_non_learned_clause()) continue;
                 if (!select_clause<et>(2)) continue;
                 literal l2 = w.get_literal();
@@ -1543,9 +1558,13 @@ namespace sat {
         template<elim_type et>
         void cce_clauses() {
             literal blocked;
+            m_ala_cost = 0;
+            m_ala_benefit = 0;
             model_converter::kind k;
-            for (clause* cp : s.s.m_clauses) {
+            unsigned start = s.s.m_rand(); 
-                clause& c = *cp;
+            unsigned sz = s.s.m_clauses.size();
+            for (unsigned i = 0; i < sz; ++i) {
+                clause& c = *s.s.m_clauses[(i + start) % sz];
                 if (c.was_removed() || c.is_learned()) continue;
                 if (!select_clause<et>(c.size())) continue;
                 elim_type r = cce<et>(c, blocked, k);
@@ -1563,7 +1582,10 @@ namespace sat {
                     break;
                 }
                 s.checkpoint();
-            }
+                if (reached_max_cost()) {
+                    break;
+                }
+            }            
         }
 
         void inc_bc(elim_type et) {