add option to "rotate" cores during core finding

enable to find multiple cores in a round and at the same time facilitate rotation around satisfiable subsets to explore neighborhoods for improved assignments.

src/opt/CMakeLists.txt

@@ -5,6 +5,7 @@ z3_add_component(opt
     maxsmt.cpp
     opt_cmds.cpp
     opt_context.cpp
+    opt_cores.cpp
     opt_lns.cpp
     opt_pareto.cpp
     opt_parse.cpp

src/opt/maxcore.cpp

@@ -11,8 +11,8 @@ Abstract:
 
     - mu:        max-sat algorithm by Nina and Bacchus, AAAI 2014.
     - mus-mss:   based on dual refinement of bounds.
-    - binary
+    - binary:    binary versino of maxres
-    - binary-delay
+    - rc2:       implementaion of rc2 heuristic using cardinality constraints
 
 
     MaxRes is a core-guided approach to maxsat.
@@ -66,6 +66,7 @@ Notes:
 #include "opt/opt_context.h"
 #include "opt/opt_params.hpp"
 #include "opt/opt_lns.h"
+#include "opt/opt_cores.h"
 #include "opt/maxsmt.h"
 #include "opt/maxcore.h"
 
@@ -119,7 +120,6 @@ private:
     bool             m_hill_climb;             // prefer large weight soft clauses for cores
     unsigned         m_last_index;             // last index used during hill-climbing
     bool             m_add_upper_bound_block;  // restrict upper bound with constraint
-    unsigned         m_max_num_cores;          // max number of cores per round.
     unsigned         m_max_core_size;          // max core size per round.
     bool             m_maximize_assignment;    // maximize assignment to find MCS
     unsigned         m_max_correction_set_size;// maximal set of correction set that is tolerated.
@@ -127,9 +127,9 @@ private:
                                                // this option is disabled if SAT core is used.
     bool             m_pivot_on_cs;            // prefer smaller correction set to core.
     bool             m_dump_benchmarks;        // display benchmarks (into wcnf format)
-    bool             m_enable_lns { false };   // enable LNS improvements
+    bool             m_enable_lns = false;     // enable LNS improvements
-    unsigned         m_lns_conflicts { 1000 }; // number of conflicts used for LNS improvement
+    unsigned         m_lns_conflicts = 1000;   // number of conflicts used for LNS improvement
-    
+    bool             m_enable_core_rotate = false; 
     std::string      m_trace_id;
     typedef ptr_vector<expr> exprs;
 
@@ -148,7 +148,6 @@ public:
         m_correction_set_size(0),
         m_found_feasible_optimum(false),
         m_hill_climb(true),
-        m_last_index(0),
         m_add_upper_bound_block(false),
         m_max_num_cores(UINT_MAX),
         m_max_core_size(3),
@@ -323,17 +322,15 @@ public:
                Give preference to cores that have large minimal values.
             */
             sort_assumptions(asms);              
-            m_last_index = 0;
+            unsigned last_index = 0;
             unsigned index = 0;
-            bool first = index > 0;
             SASSERT(index < asms.size() || asms.empty());
             IF_VERBOSE(10, verbose_stream() << "start hill climb " << index << " asms: " << asms.size() << "\n";);
             while (index < asms.size() && is_sat == l_true) {
-                while (!first && asms.size() > 20*(index - m_last_index) && index < asms.size()) {
+                while (asms.size() > 20*(index - last_index) && index < asms.size()) {
                     index = next_index(asms, index);
                 }
-                first = false;
+                last_index = index;
-                m_last_index = index;
                 is_sat = check_sat(index, asms.data());
             }            
         }
@@ -390,13 +387,6 @@ public:
         st.update("maxsat-correction-sets", m_stats.m_num_cs);
     }
 
-    struct weighted_core {
-        exprs    m_core;
-        rational m_weight;
-        weighted_core(exprs const& c, rational const& w):
-            m_core(c), m_weight(w) {}
-    };
-
     lbool get_cores(vector<weighted_core>& cores) {
         // assume m_s is unsat.
         lbool is_sat = l_false;
@@ -434,8 +424,8 @@ public:
             remove_soft(core, m_asms);
             split_core(core);  
 
-            if (core.size()  >= m_max_core_size) break;
+            if (core.size() >= m_max_core_size)
-            if (cores.size() >= m_max_num_cores) break;
+                break;
 
             is_sat = check_sat_hill_climb(m_asms);            
         }
@@ -511,6 +501,9 @@ public:
     }
 
     lbool process_unsat() {
+        if (m_enable_core_rotate) 
+            return core_rotate();
+
         vector<weighted_core> cores;
         lbool is_sat = get_cores(cores);
         if (is_sat != l_true) {
@@ -525,6 +518,21 @@ public:
         }
     }
 
+    lbool core_rotate() {
+        cores find_cores(s(), m_lnsctx);
+        find_cores.updt_params(m_params);
+        vector<weighted_core> const& cores = find_cores();
+        for (auto const & [core, w] : cores) {
+            if (core.empty())
+                return l_false;
+            remove_soft(core, m_asms);
+            split_core(core);
+            process_unsat(core, w);
+        }
+        return l_true;
+    }
+
+    
     unsigned max_core_size(vector<exprs> const& cores) {
         unsigned result = 0;
         for (auto const& c : cores) {
@@ -980,7 +988,6 @@ public:
         opt_params p(_p);
         m_hill_climb =              p.maxres_hill_climb();
         m_add_upper_bound_block =   p.maxres_add_upper_bound_block();
-        m_max_num_cores =           p.maxres_max_num_cores();
         m_max_core_size =           p.maxres_max_core_size();
         m_maximize_assignment =     p.maxres_maximize_assignment();
         m_max_correction_set_size = p.maxres_max_correction_set_size();
@@ -988,6 +995,7 @@ public:
         m_wmax =                    p.maxres_wmax();
         m_dump_benchmarks =         p.dump_benchmarks();
         m_enable_lns =              p.enable_lns(); 
+        m_enable_core_rotate =      p.enable_core_rotate(); 
         m_lns_conflicts =           p.lns_conflicts();
 	if (m_c.num_objectives() > 1)
 	  m_add_upper_bound_block = false;
@@ -1000,7 +1008,6 @@ public:
             add_soft(e, w);
         m_max_upper = m_upper;
         m_found_feasible_optimum = false;
-        m_last_index = 0;
         add_upper_bound_block();
         m_csmodel = nullptr;
         m_correction_set_size = 0;

src/opt/maxsmt.h

@@ -31,6 +31,13 @@ namespace opt {
 
     typedef vector<rational> const weights_t;
 
+    struct weighted_core {
+        ptr_vector<expr>  m_core;
+        rational          m_weight;
+        weighted_core(ptr_vector<expr> const& c, rational const& w):
+            m_core(c), m_weight(w) {}
+    };
+
     class maxsat_context;
 
     class maxsmt_solver {

src/opt/opt_cores.cpp

@@ -0,0 +1,398 @@
+/*++
+Copyright (c) 2022 Microsoft Corporation
+
+Module Name:
+
+    opt_cores.cpp
+
+Abstract:
+   
+    "walk" subsets of soft constraints to extract multiple cores and satisfying assignments.
+
+    core rotation starts with an initial unsat core, which is a subset of soft constraints.
+    Then it removes one element from the core from the soft constraints and finds remaining cores.
+    At every stage it operates over a set of detected cores, and a subset of soft constraints have
+    a hitting set from the cores removed.
+    When enough constraints are removed, the remaining soft constraints become satisfiable.
+    It then attempts extend the satisfying assignment by adding soft constraints removed in 
+    the hitting set. In this process it detects new cores and may find assignments that improve
+    the current feasible bound. As a final effort, it takes a maximal satisfying assignment and
+    rotates out elements that belong to cores to explore a neighborhood for satisfying assignments
+    that may potentially satisfy other soft constraints and potentially more of them.
+
+Author:
+
+    Nikolaj Bjorner (nbjorner) 2022-04-27
+
+--*/
+
+#include "solver/solver.h"
+#include "opt/maxsmt.h"
+#include "opt/opt_cores.h"
+#include "opt/opt_params.hpp"
+
+namespace opt {
+
+    cores::cores(solver& s, lns_context& ctx):
+        m(s.get_manager()), s(s), ctx(ctx) {}
+
+    void cores::hitting_set(obj_hashtable<expr>& set) {
+        for (auto const& [core, w] : m_cores) {
+            bool seen = false;
+            for (auto * c : core)
+                seen |= set.contains(c);
+            if (seen)
+                continue;
+            set.insert(core[m_rand(core.size())]);
+        }
+    }
+
+    bool cores::improve() {
+        model_ref mdl;
+        s.get_model(mdl);
+        rational cost = ctx.cost(*mdl);
+        IF_VERBOSE(3, verbose_stream() << "(opt.maxcore new model cost " << cost << ")\n");
+        if (m_best_cost < 0 || cost < m_best_cost) {            
+            m_best_cost = cost;
+            ctx.update_model(mdl);
+            return true;
+        }
+        return false;
+    }
+
+    /**
+     * retrieve cores that are disjoint modulo weights.
+     * weighted soft constraints are treated as multi-sets.
+     */
+    vector<weighted_core> const& cores::disjoint_cores() {
+        std::sort(m_cores.begin(), m_cores.end(), [&](weighted_core const& c1, weighted_core const& c2) { return c1.m_core.size() < c2.m_core.size(); });
+        vector<weighted_core> result;
+        for (auto const& [core, w] : m_cores) {
+            rational weight = core_weight(core);
+            if (weight == 0 && !core.empty())
+                continue;
+            for (auto *c : core) 
+                m_weight[c] -= weight;
+            result.push_back(weighted_core(core, weight));
+        }
+        IF_VERBOSE(3, verbose_stream() << "(opt.cores :cores-found " << m_cores.size() << " :disjoint-cores " << result.size() << ")\n");
+        m_cores.reset();
+        m_cores.append(result);
+        return m_cores;
+    }
+
+    void cores::rotate_rec(obj_hashtable<expr> const& _mss, obj_map<expr, ptr_vector<expr>>& backbone2core, unsigned depth) {
+        obj_map<expr, unsigned> counts;
+        obj_hashtable<expr> mss(_mss);
+        for (auto* f : mss)
+            counts.insert(f, 0);
+        for (auto const& [k, core] : backbone2core) 
+            for (auto* c : core) 
+                counts[c] += 1;
+                    
+        unsigned plateaus = 0;
+        for (auto const& [c, count] : counts)
+            if (count <= 1)
+                ++plateaus;
+        IF_VERBOSE(3, verbose_stream() << "(opt.maxcore :num-plateaus " << plateaus << "\n");
+
+        for (auto const& [c, count] : counts) {
+            if (count <= 1)
+                continue;
+            mss.remove(c);
+            bool rotated = rotate(mss, c, depth + 1);
+            mss.insert(c);
+            if (rotated)
+                break;
+        }
+    }
+
+    /**
+     * collect soft constraints that are not in the satisfying assignment mss into the set ps.
+     * Try to add elements from ps in some order.
+     * If an element can be added, (mss + p is sat), then mss is extended.
+     * If mss + p is unsat, then extract core that includes p and a subset of mss
+     * Then Not(p) is a backbone, and we maintain a map from Not(p) to the subset of mss used
+     * in the core. Backbone literals are used in the satisfiability check.
+     * For backbone literals that are used in other cores, resolve away Not(p) by the subset
+     * of mss that comprised the core for p + mss.
+     * The set qs accumulates don't knows. If a satisfiable assignment is found that satisfies
+     * elements from qs, they are added to mss.
+     */
+    bool cores::rotate(obj_hashtable<expr> const& _mss, expr* excl, unsigned depth) {
+        obj_hashtable<expr> ps, qs, mss(_mss);
+        expr_ref_vector backbones(m);
+        obj_map<expr, ptr_vector<expr>> backbone2core;
+        bool improved = false;
+        for (expr* f : ctx.soft())
+            if (!mss.contains(f) && f != excl)
+                ps.insert(f);
+        while (!ps.empty() && m.inc() && m_cores.size() < m_max_num_cores) {
+            expr* p = *ps.begin();
+            ps.remove(p);
+            expr_ref_vector asms(backbones);
+            asms.push_back(p);
+            for (expr* f : mss)
+                asms.push_back(f);
+            lbool is_sat = s.check_sat(asms);
+            switch (is_sat) {
+            case l_true: {
+                model_ref mdl;
+                s.get_model(mdl);
+                ptr_vector<expr> moved;
+                moved.push_back(p);
+                for (auto* q : qs) 
+                    if (mdl->is_true(q))
+                        moved.push_back(q);
+
+                for (auto* q : ps) 
+                    if (mdl->is_true(q)) 
+                        moved.push_back(q);
+
+                for (auto* q : moved) {
+                    mss.insert(q);
+                    qs.remove(q);
+                    ps.remove(q);
+                }
+                
+                if (improve())
+                    improved = true;
+                break;
+            }
+            case l_false: {
+                obj_hashtable<expr> core;
+                for (auto* f : unsat_core()) {
+                    ptr_vector<expr> core1;
+                    if (backbone2core.find(f, core1))
+                        for (expr* c : core1)
+                            core.insert(c);
+                    else
+                        core.insert(f);
+                }
+                expr_ref_vector core1(m);
+                for (expr* c : core)
+                    core1.push_back(c);
+                saturate_core(core1);
+                add_core(core1);
+                expr_ref not_p(m.mk_not(p), m);
+                backbones.push_back(not_p);
+                ptr_vector<expr> core2(core1.size(), core1.data());
+                core2.erase(p);
+                backbone2core.insert(not_p, core2);
+                break;
+            }                
+            default:
+                qs.insert(p);
+                break;
+            }
+        }
+        if (improved)
+            rotate_rec(mss, backbone2core, depth);
+        return improved;
+    }
+
+    struct cores::scoped_update {
+        cores& c;
+        char const* par;
+        bool     is_uint = true;
+        unsigned old_uval;
+        bool     old_bval;
+    public:
+        scoped_update(cores& c, char const* par, unsigned old_val, unsigned new_val):
+            c(c), par(par), old_uval(old_val) {
+            params_ref p;        
+            p.set_uint(par, new_val);
+            c.s.updt_params(p);
+        }
+
+        scoped_update(cores& c, char const* par, bool old_val, bool new_val):
+            c(c), par(par), old_bval(old_val) {
+            is_uint = false;
+            params_ref p;        
+            p.set_bool(par, new_val);
+            c.s.updt_params(p);
+        }
+
+        ~scoped_update() {            
+            params_ref p;
+            if (is_uint)
+                p.set_uint(par, old_uval);
+            else
+                p.set_bool(par, old_bval);
+            c.s.updt_params(p);
+        }
+    };
+
+    void cores::saturate_core(expr_ref_vector& core) {
+        scoped_update _upd(*this, "max_conflicts", m_max_conflicts, m_max_saturate_conflicts);
+        shuffle(core.size(), core.data(), m_rand);
+        while (l_false == s.check_sat(core) && unsat_core().size() < core.size()) {
+            core.reset();
+            core.append(unsat_core());
+            shuffle(core.size(), core.data(), m_rand);
+        }
+    }
+
+    void cores::local_mss() {
+        obj_hashtable<expr> mss;
+        model_ref mdl;
+        s.get_model(mdl);
+        for (expr* f : ctx.soft()) 
+            if (mdl->is_true(f))
+                mss.insert(f);
+        rotate(mss, nullptr, 0);
+    }
+
+    expr_ref_vector cores::unsat_core() {
+        expr_ref_vector core(m);
+        s.get_unsat_core(core);
+        return core;
+    }
+
+    /**
+     * The solver state is unsatisfiable when this function is called.
+     * Erase one element from each code that is found
+     */
+    void cores::rotate_cores() {
+        expr_ref_vector soft(m);
+        soft.append(ctx.soft());
+        unsigned num_sat = 0, num_unsat = 0, num_undef = 0;        
+        lbool is_sat = l_false;
+        while (m.inc() && m_cores.size() < m_max_num_cores) {
+            switch (is_sat) {
+            case l_false: {
+                ++num_unsat;
+                auto core = unsat_core();
+                add_core(core);
+                if (core.empty())
+                    return;
+                soft.erase(core.get(m_rand(core.size())));
+                num_sat = 0;
+                break;                
+            }
+            case l_true: {
+                ++num_sat;
+                improve();
+                local_mss();
+                if (num_sat > 1) 
+                    return;
+                soft.reset();
+                obj_hashtable<expr> hs;
+                hitting_set(hs);
+                for (auto s : ctx.soft())
+                    if (!hs.contains(s))
+                        soft.push_back(s);
+                break;
+            }
+            case l_undef:
+                ++num_undef;
+                if (num_undef > 2)
+                    return;
+            }
+            is_sat = s.check_sat(soft);
+        }        
+    }
+
+    rational cores::core_weight(unsigned sz, expr* const* core) {
+        if (sz == 0)
+            return rational(0);
+        rational min_weight = m_weight[core[0]];
+        for (unsigned i = 1; i < sz; ++i) {
+            auto* c = core[i];
+            if (m_weight[c] < min_weight)
+                min_weight = m_weight[c];
+        }
+        return min_weight;
+    }
+
+
+    vector<weighted_core> const& cores::weighted_disjoint_cores() {
+        lbool is_sat = l_false;
+        expr_ref_vector soft = ctx.soft();
+        
+        while (is_sat == l_false && m.inc()) {
+            auto core = unsat_core();
+            saturate_core(core);
+            rational weight = core_weight(core);
+            add_core(core);
+            if (core.empty()) {
+                IF_VERBOSE(100, verbose_stream() << "(opt.maxres :empty-core)\n";);
+                TRACE("opt", tout << "empty core\n";);
+                break;
+            }
+
+            for (auto *c : core) {
+                m_weight[c] -= weight;
+                if (m_weight[c] == 0)
+                    soft.erase(c);
+            }
+
+            if (core.size()  >= m_max_core_size)
+                break;
+            
+            if (m_cores.size() >= m_max_num_cores)
+                break;
+
+            if (m_hill_climb)
+                is_sat = check_sat_hill_climb(soft);
+            else
+                is_sat = s.check_sat(soft);
+        }
+        return m_cores;
+    }
+
+    /**
+     * Give preference to cores that have large minimal values.
+     * Explore largest values, and grow the set of explored values by at least 5% 
+     * of all soft constraints in iterations (capping maximal iterations at 20).
+     */
+    lbool cores::check_sat_hill_climb(expr_ref_vector const& _soft) {
+        expr_ref_vector soft(_soft);
+        lbool is_sat = l_true;
+        std::sort(soft.data(), soft.data() + soft.size(), [&](expr* a, expr* b) { return m_weight[a] > m_weight[b]; });
+        unsigned index = 0, last_index = 0;
+        SASSERT(index < soft.size() || soft.empty());
+        IF_VERBOSE(10, verbose_stream() << "start hill climb " << index << " soft: " << soft.size() << "\n";);
+        while (index < soft.size() && is_sat == l_true) {
+            while (soft.size() > 20*(index - last_index) && index < soft.size()) {
+                rational w = m_weight[_soft[index]];
+                for (++index; index < soft.size() && w == m_weight[_soft[index]]; ++index); 
+            }
+            last_index = index;
+            is_sat = s.check_sat(index, soft.data());
+        }            
+        return is_sat;
+    }
+
+    void cores::add_core(expr_ref_vector const& core) {
+        IF_VERBOSE(3, verbose_stream() << "(opt.maxcore :core-size " << core.size() << ")\n");
+        m_cores.push_back(weighted_core(ptr_vector<expr>(core.size(), core.data()), core_weight(core)));
+    }
+
+    void cores::updt_params(params_ref& _p) {
+        std::cout << _p << "\n";
+        opt_params p(_p);
+        m_hill_climb =         p.maxres_hill_climb();
+        m_max_num_cores =      p.maxres_max_num_cores();
+        m_max_core_size =      p.maxres_max_core_size();
+        m_enable_core_rotate = p.enable_core_rotate();        
+    }
+    
+    vector<weighted_core> const& cores::operator()() {
+        scoped_update _upd1(*this, "max_conflicts", UINT_MAX, m_max_conflicts);
+        m_cores.reset();
+        m_weight.reset();
+        for (expr* s : ctx.soft())
+            m_weight.insert(s, ctx.weight(s));
+
+        if (m_enable_core_rotate) {
+            scoped_update _upd2(*this, "minimize_core", false, false);
+            rotate_cores();
+            return disjoint_cores();
+        }
+        else {
+            return weighted_disjoint_cores();
+        }
+    }
+
+};

src/opt/opt_cores.h

@@ -0,0 +1,71 @@
+/*++
+Copyright (c) 2022 Microsoft Corporation
+
+Module Name:
+
+    opt_cores.h
+
+Abstract:
+   
+    "walk" subsets of soft constraints to extract multiple cores and satisfying assignments.
+
+Author:
+
+    Nikolaj Bjorner (nbjorner) 2022-04-27
+
+--*/
+
+#pragma once
+#include "opt/opt_lns.h"
+
+namespace opt {
+
+
+    class cores {
+        ast_manager&     m;
+        solver&          s;
+        lns_context&     ctx;
+
+        random_gen               m_rand;
+        rational                 m_best_cost = rational::minus_one();
+        vector<weighted_core>    m_cores;
+        obj_map<expr, rational>  m_weight;
+
+        unsigned m_max_saturate_conflicts = 500;
+        unsigned m_max_conflicts          = 1000;
+        bool     m_hill_climb             = true;
+        unsigned m_max_num_cores          = UINT_MAX;
+        unsigned m_max_core_size          = 4;
+        bool     m_enable_core_rotate     = false;
+
+        struct scoped_update;
+
+        bool improve();
+        void rotate_rec(obj_hashtable<expr> const& mss, obj_map<expr, ptr_vector<expr>>& backbone2core, unsigned depth);
+        bool rotate(obj_hashtable<expr> const& mss, expr* excl, unsigned depth);
+        void saturate_core(expr_ref_vector& core);
+        void local_mss();
+        void hitting_set(obj_hashtable<expr>& hs);
+        rational core_weight(expr_ref_vector const& core) { return core_weight(core.size(), core.data()); }
+        rational core_weight(ptr_vector<expr> const& core) { return core_weight(core.size(), core.data()); }
+        rational core_weight(unsigned sz, expr* const* core);
+        lbool check_sat_hill_climb(expr_ref_vector const& _soft);
+
+        void add_core(expr_ref_vector const& core);
+
+        vector<weighted_core> const& disjoint_cores();
+
+        void rotate_cores();
+
+        vector<weighted_core> const& weighted_disjoint_cores();
+
+        expr_ref_vector unsat_core();
+
+    public:
+        cores(solver& s, lns_context& ctx);
+        
+        vector<weighted_core> const& operator()();
+
+        void updt_params(params_ref& p);
+    };
+};

src/opt/opt_params.pyg

@@ -10,8 +10,9 @@ def_module_params('opt',
                           ('timeout', UINT, UINT_MAX, 'timeout (in milliseconds) (UINT_MAX and 0 mean no timeout)'),
                           ('rlimit', UINT, 0, 'resource limit (0 means no limit)'),
                           ('enable_sls', BOOL, False, 'enable SLS tuning during weighted maxsat'),
-                          ('enable_lns', BOOL, False, 'enable LNS during weighted maxsat'),
+                          ('enable_lns', BOOL, False, 'enable LNS during weighted maxsat'),			  
                           ('lns_conflicts', UINT, 1000, 'initial conflict count for LNS search'),
+                          ('enable_core_rotate', BOOL, False, 'enable core rotation to both sample cores and correction sets'),
                           ('enable_sat', BOOL, True, 'enable the new SAT core for propositional constraints'),
                           ('elim_01', BOOL, True, 'eliminate 01 variables'),
                           ('pp.neat', BOOL, True, 'use neat (as opposed to less readable, but faster) pretty printer when displaying context'),
@@ -20,7 +21,7 @@ def_module_params('opt',
                           ('maxlex.enable', BOOL, True, 'enable maxlex heuristic for lexicographic MaxSAT problems'),
                           ('maxres.hill_climb', BOOL, True, 'give preference for large weight cores'),
                           ('maxres.add_upper_bound_block', BOOL, False, 'restict upper bound with constraint'),
-                          ('maxres.max_num_cores', UINT, UINT_MAX, 'maximal number of cores per round'),
+                          ('maxres.max_num_cores', UINT, 200, 'maximal number of cores per round'),
                           ('maxres.max_core_size', UINT, 3, 'break batch of generated cores if size reaches this number'),
                           ('maxres.maximize_assignment', BOOL, False, 'find an MSS/MCS to improve current assignment'), 
                           ('maxres.max_correction_set_size', UINT, 3, 'allow generating correction set constraints up to maximal size'),