adding preferred sat, currently disabled, to wmax. Fixing issue #815

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

src/opt/opt_solver.cpp

@@ -198,6 +198,10 @@ namespace opt {
         return m_context.find_mutexes(vars, mutexes);
     }
 
+    lbool opt_solver::preferred_sat(expr_ref_vector const& asms, vector<expr_ref_vector>& cores) {
+        return m_context.preferred_sat(asms, cores);
+    }
+
 
 
     /**

src/opt/opt_solver.h

@@ -107,6 +107,7 @@ namespace opt {
         virtual std::ostream& display(std::ostream & out) const;
         virtual ast_manager& get_manager() const { return m; } 
         virtual lbool find_mutexes(expr_ref_vector const& vars, vector<expr_ref_vector>& mutexes);
+        virtual lbool preferred_sat(expr_ref_vector const& asms, vector<expr_ref_vector>& cores);
         void set_logic(symbol const& logic);
 
         smt::theory_var add_objective(app* term);

src/opt/wmax.cpp

@@ -32,64 +32,286 @@ namespace opt {
 
 
     class wmax : public maxsmt_solver_base {
+        obj_map<expr, rational>  m_weights;
+        obj_map<expr, expr*>     m_keys;
+        expr_ref_vector m_trail, m_defs;
+
+        void reset() {
+            m_weights.reset();
+            m_keys.reset();
+            m_trail.reset();
+            m_defs.reset();
+        }
+
     public:
         wmax(maxsat_context& c, weights_t& ws, expr_ref_vector const& soft): 
-            maxsmt_solver_base(c, ws, soft) {}
+            maxsmt_solver_base(c, ws, soft),
+            m_trail(m),
+            m_defs(m) {}
+
         virtual ~wmax() {}
 
         lbool operator()() {
             TRACE("opt", tout << "weighted maxsat\n";);
             scoped_ensure_theory wth(*this);
             obj_map<expr, rational> soft;            
+            reset();
             lbool is_sat = find_mutexes(soft);
             if (is_sat != l_true) {
                 return is_sat;
             }
-            rational offset = m_lower;
+            m_upper = m_lower;
-            m_upper = offset;
             bool was_sat = false;
-            expr_ref_vector disj(m);
+            expr_ref_vector disj(m), asms(m);
+            vector<expr_ref_vector> cores;
             obj_map<expr, rational>::iterator it = soft.begin(), end = soft.end();
             for (; it != end; ++it) {
-                expr_ref tmp(m);
+                expr* c = assert_weighted(wth(), it->m_key, it->m_value);
-                bool is_true = m_model->eval(it->m_key, tmp) && m.is_true(tmp);
+                if (!is_true(it->m_key)) {
-                expr* c = wth().assert_weighted(it->m_key, it->m_value, is_true);
+                    disj.push_back(m.mk_not(c));
-                if (!is_true) {
                     m_upper += it->m_value;
-                    disj.push_back(c);
                 }
             }
+            wth().init_min_cost(m_upper - m_lower);
             s().assert_expr(mk_or(disj));
             trace_bounds("wmax");
-            while (l_true == is_sat && m_lower < m_upper) {
+            
+            while (!m.canceled() && m_lower < m_upper) {
+                //mk_assumptions(asms);
+                //is_sat = s().preferred_sat(asms, cores);
                 is_sat = s().check_sat(0, 0);
                 if (m.canceled()) {
                     is_sat = l_undef;
                 }
+                if (is_sat == l_false) {
+                    break;
+                }
                 if (is_sat == l_true) {
                     if (wth().is_optimal()) {
-                        m_upper = offset + wth().get_min_cost();
+                        m_upper = m_lower + wth().get_cost();
                         s().get_model(m_model);
                     }
                     expr_ref fml = wth().mk_block();
+                    //DEBUG_CODE(verify_cores(cores););
                     s().assert_expr(fml);
                     was_sat = true;
                 }
+                else {
+                    //DEBUG_CODE(verify_cores(cores););
+                }
+                update_cores(wth(), cores);
+                wth().init_min_cost(m_upper - m_lower);
                 trace_bounds("wmax");
+                SASSERT(m_lower <= m_upper);
             }
-            if (was_sat) {
+
-                wth().get_assignment(m_assignment);
+            update_assignment();
-                m_upper = offset + wth().get_min_cost();
+            
-            }
+            if (!m.canceled() && is_sat == l_undef && m_lower == m_upper) {
-            if (is_sat == l_false && was_sat) {
                 is_sat = l_true;
             }
-            if (is_sat == l_true) {
+            if (is_sat == l_false) {
+                is_sat = l_true;
                 m_lower = m_upper;
             }
             TRACE("opt", tout << "min cost: " << m_upper << "\n";);
             return is_sat;
         }
+
+        bool is_true(expr* e) {
+            expr_ref tmp(m);
+            return m_model->eval(e, tmp) && m.is_true(tmp);
+        }
+
+        void update_assignment() {
+            m_assignment.reset();
+            for (unsigned i = 0; i < m_soft.size(); ++i) {
+                m_assignment.push_back(is_true(m_soft[i]));
+            }
+        }
+
+        struct compare_asm {
+            wmax& max;
+            compare_asm(wmax& max):max(max) {}
+            bool operator()(expr* a, expr* b) const {
+                return max.m_weights[a] > max.m_weights[b];
+            }
+        };
+
+        void mk_assumptions(expr_ref_vector& asms) {
+            ptr_vector<expr> _asms;
+            obj_map<expr, rational>::iterator it = m_weights.begin(), end = m_weights.end();
+            for (; it != end; ++it) {
+                _asms.push_back(it->m_key);
+            }
+            compare_asm comp(*this);
+            std::sort(_asms.begin(),_asms.end(), comp); 
+            asms.reset();
+            for (unsigned i = 0; i < _asms.size(); ++i) {
+                asms.push_back(m.mk_not(_asms[i]));
+            }
+        }
+
+        void verify_cores(vector<expr_ref_vector> const& cores) {
+            for (unsigned i = 0; i < cores.size(); ++i) {
+                verify_core(cores[i]);
+            }
+        }
+
+        void verify_core(expr_ref_vector const& core) {
+            s().push();
+            s().assert_expr(core);
+            VERIFY(l_false == s().check_sat(0, 0));          
+            s().pop(1);
+        }
+
+        void update_cores(smt::theory_wmaxsat& th, vector<expr_ref_vector> const& cores) {
+            obj_hashtable<expr> seen;
+            bool updated = false;
+            unsigned min_core_size = UINT_MAX;
+            for (unsigned i = 0; i < cores.size(); ++i) {
+                expr_ref_vector const& core = cores[i];
+                if (core.size() <= 20) {
+                    s().assert_expr(m.mk_not(mk_and(core)));
+                }
+                min_core_size = std::min(core.size(), min_core_size);
+                if (core.size() >= 11) {
+                    continue;
+                }
+                bool found = false;
+                for (unsigned j = 0; !found && j < core.size(); ++j) {
+                    found = seen.contains(core[j]);
+                }
+                if (found) {
+                    continue;
+                }
+                for (unsigned j = 0; j < core.size(); ++j) {
+                    seen.insert(core[j]);
+                }
+                update_core(th, core);
+                updated = true;
+            }
+            // if no core was selected, then take the smallest cores.
+            for (unsigned i = 0; !updated && i < cores.size(); ++i) {
+                expr_ref_vector const& core = cores[i];
+                if (core.size() > min_core_size + 2) {
+                    continue;
+                }
+                bool found = false;
+                for (unsigned j = 0; !found && j < core.size(); ++j) {
+                    found = seen.contains(core[j]);
+                }
+                if (found) {
+                    continue;
+                }
+                for (unsigned j = 0; j < core.size(); ++j) {
+                    seen.insert(core[j]);
+                }
+                update_core(th, core);                
+            }            
+        }
+
+
+        rational remove_negations(smt::theory_wmaxsat& th, expr_ref_vector const& core, ptr_vector<expr>& keys, vector<rational>& weights) {
+            rational min_weight(-1);
+            for (unsigned i = 0; i < core.size(); ++i) {
+                expr* e;
+                VERIFY(m.is_not(core[i], e));
+                keys.push_back(m_keys[e]);
+                rational weight = m_weights[e];
+                if (i == 0 || weight < min_weight) {
+                    min_weight = weight;
+                }
+                weights.push_back(weight);
+                m_weights.erase(e);
+                m_keys.erase(e);
+                th.disable_var(e);
+            }
+            for (unsigned i = 0; i < core.size(); ++i) {
+                rational weight = weights[i];
+                if (weight > min_weight) {
+                    weight -= min_weight;
+                    assert_weighted(th, keys[i], weight);
+                }
+            }
+            return min_weight;
+        }
+
+        // assert maxres clauses
+        // assert new core members with value of current model.
+        // update lower bound
+        // bounds get re-normalized when solver is invoked.
+        // each element of core is negated literal from theory_wmaxsat
+        // disable those literals from th
+
+        void update_core(smt::theory_wmaxsat& th, expr_ref_vector const& core) {
+            ptr_vector<expr> keys;
+            vector<rational> weights;
+            rational min_weight = remove_negations(th, core, keys, weights);            
+            max_resolve(th, keys, min_weight);            
+            m_lower += min_weight;
+            // std::cout << core << " " << min_weight << "\n";
+        }
+
+        void max_resolve(smt::theory_wmaxsat& th, ptr_vector<expr> const& core, rational const& w) {
+            SASSERT(!core.empty());
+            expr_ref fml(m), asum(m);
+            app_ref cls(m), d(m), dd(m);
+            //
+            // d_0 := true
+            // d_i := b_{i-1} and d_{i-1}    for i = 1...sz-1
+            // soft (b_i or !d_i) 
+            //   == (b_i or !(!b_{i-1} or d_{i-1}))
+            //   == (b_i or b_0 & b_1 & ... & b_{i-1})
+            // 
+            // Soft constraint is satisfied if previous soft constraint
+            // holds or if it is the first soft constraint to fail.
+            // 
+            // Soundness of this rule can be established using MaxRes
+            // 
+            for (unsigned i = 1; i < core.size(); ++i) {
+                expr* b_i = core[i-1];
+                expr* b_i1 = core[i];
+                if (i == 1) {
+                    d = to_app(b_i);
+                }
+                else if (i == 2) {
+                    d = m.mk_and(b_i, d);
+                    m_trail.push_back(d);
+                }
+                else {
+                    dd = mk_fresh_bool("d");
+                    fml = m.mk_implies(dd, d);
+                    s().assert_expr(fml);
+                    m_defs.push_back(fml);
+                    fml = m.mk_implies(dd, b_i);
+                    s().assert_expr(fml);
+                    m_defs.push_back(fml);
+                    fml = m.mk_and(d, b_i);
+                    update_model(dd, fml);
+                    d = dd;
+                }
+                cls = m.mk_or(b_i1, d);
+                m_trail.push_back(cls);
+                assert_weighted(th, cls, w);
+            }
+        }
+
+        expr* assert_weighted(smt::theory_wmaxsat& th, expr* key, rational const& w) {
+            expr* c = th.assert_weighted(key, w);
+            m_weights.insert(c, w);
+            m_keys.insert(c, key);
+            m_trail.push_back(c);
+            return c;
+        }
+
+        void update_model(expr* def, expr* value) {
+            expr_ref val(m);
+            if (m_model && m_model->eval(value, val, true)) {
+                m_model->register_decl(to_app(def)->get_decl(), val);
+            }
+        }
+                
     };
 
     maxsmt_solver_base* mk_wmax(maxsat_context& c, weights_t& ws, expr_ref_vector const& soft) {

src/smt/smt_consequences.cpp

@@ -56,36 +56,7 @@ namespace smt {
             s.insert(lit.var());
         }
         else {
-            b_justification js = get_justification(lit.var());
+            justify(lit, s);
-            switch (js.get_kind()) {
-            case b_justification::CLAUSE: {
-                clause * cls = js.get_clause();
-                if (!cls) break;
-                unsigned num_lits = cls->get_num_literals();
-                for (unsigned j = 0; j < num_lits; ++j) {
-                    literal lit2 = cls->get_literal(j);
-                    if (lit2.var() != lit.var()) {
-                        s |= m_antecedents.find(lit2.var());
-                    }
-                }
-                break;
-            }
-            case b_justification::BIN_CLAUSE: {
-                s |= m_antecedents.find(js.get_literal().var());
-                break;
-            }
-            case b_justification::AXIOM: {
-                break;
-            }
-            case b_justification::JUSTIFICATION: {
-                literal_vector literals;
-                m_conflict_resolution->justification2literals(js.get_justification(), literals);
-                for (unsigned j = 0; j < literals.size(); ++j) {
-                    s |= m_antecedents.find(literals[j].var());
-                }
-                break;
-            }
-            }
         }
         m_antecedents.insert(lit.var(), s);
         TRACE("context", display_literal_verbose(tout, lit); 
@@ -122,6 +93,39 @@ namespace smt {
         }
     }
 
+    void context::justify(literal lit, index_set& s) {
+        b_justification js = get_justification(lit.var());
+        switch (js.get_kind()) {
+        case b_justification::CLAUSE: {
+            clause * cls = js.get_clause();
+            if (!cls) break;
+            unsigned num_lits = cls->get_num_literals();
+            for (unsigned j = 0; j < num_lits; ++j) {
+                literal lit2 = cls->get_literal(j);
+                if (lit2.var() != lit.var()) {
+                    s |= m_antecedents.find(lit2.var());
+                }
+            }
+            break;
+        }
+        case b_justification::BIN_CLAUSE: {
+            s |= m_antecedents.find(js.get_literal().var());
+            break;
+            }
+        case b_justification::AXIOM: {
+            break;
+        }
+        case b_justification::JUSTIFICATION: {
+            literal_vector literals;
+            m_conflict_resolution->justification2literals(js.get_justification(), literals);
+            for (unsigned j = 0; j < literals.size(); ++j) {
+                s |= m_antecedents.find(literals[j].var());
+            }
+            break;
+        }
+        }        
+    }
+
     void context::extract_fixed_consequences(unsigned& start, obj_map<expr, expr*>& vars, index_set const& assumptions, expr_ref_vector& conseq) {
         pop_to_search_lvl();
         SASSERT(!inconsistent());
@@ -369,6 +373,142 @@ namespace smt {
              << ")\n";
     }  
 
+    void context::extract_cores(expr_ref_vector const& asms, vector<expr_ref_vector>& cores, unsigned& min_core_size) {
+        index_set _asms, _nasms;
+        u_map<expr*> var2expr;
+        for (unsigned i = 0; i < asms.size(); ++i) {
+            literal lit = get_literal(asms[i]);
+            _asms.insert(lit.index());
+            _nasms.insert((~lit).index());
+            var2expr.insert(lit.var(), asms[i]);
+        }
+
+        m_antecedents.reset();
+        literal_vector const& lits = assigned_literals();
+        for (unsigned i = 0; i < lits.size(); ++i) {
+            literal lit = lits[i];
+            index_set s;
+            if (_asms.contains(lit.index())) {
+                s.insert(lit.var());
+            }
+            else {
+                justify(lit, s);
+            }
+            m_antecedents.insert(lit.var(), s);
+            if (_nasms.contains(lit.index())) {
+                expr_ref_vector core(m_manager);
+                index_set::iterator it = s.begin(), end = s.end();
+                for (; it != end; ++it) {
+                    core.push_back(var2expr[*it]);
+                }
+                core.push_back(var2expr[lit.var()]);
+                cores.push_back(core);
+                min_core_size = std::min(min_core_size, core.size());
+            }
+        }
+    }
+
+    void context::preferred_sat(literal_vector& lits) {
+        bool retry = true;
+        while (retry) {
+            retry = false;
+            for (unsigned i = 0; i < lits.size(); ++i) {
+                literal lit = lits[i];
+                if (lit == null_literal || get_assignment(lit) != l_undef) {
+                    continue;
+                }
+                push_scope();
+                assign(lit, b_justification::mk_axiom(), true);
+                while (!propagate()) {
+                    lits[i] = null_literal;
+                    retry = true;
+                    if (!resolve_conflict() || inconsistent()) {
+                        SASSERT(inconsistent());
+                        return;
+                    }
+                }      
+            }
+        }
+    }
+
+    void context::display_partial_assignment(std::ostream& out, expr_ref_vector const& asms, unsigned min_core_size) {
+        unsigned num_true = 0, num_false = 0, num_undef = 0;
+        for (unsigned i = 0; i < asms.size(); ++i) {
+            literal lit = get_literal(asms[i]);
+            if (get_assignment(lit) == l_false) {
+                ++num_false;
+            }
+            if (get_assignment(lit) == l_true) {
+                ++num_true;
+            }
+            if (get_assignment(lit) == l_undef) {
+                ++num_undef;
+            }
+        }
+        out << "(smt.preferred-sat true: " << num_true << " false: " << num_false << " undef: " << num_undef << " min core: " << min_core_size << ")\n"; 
+    }
+
+    lbool context::preferred_sat(expr_ref_vector const& asms, vector<expr_ref_vector>& cores) {        
+        pop_to_base_lvl();
+        cores.reset();
+        setup_context(false);
+        internalize_assertions();
+        if (m_asserted_formulas.inconsistent() || inconsistent()) {
+            return l_false;
+        }
+        scoped_mk_model smk(*this);
+        init_search();
+        flet<bool> l(m_searching, true);
+        unsigned level = m_scope_lvl;
+        unsigned min_core_size = UINT_MAX;
+        lbool is_sat = l_true;
+        unsigned num_restarts = 0;
+
+        while (true) {
+            if (m_manager.canceled()) {
+                is_sat = l_undef;
+                break;
+            }
+            literal_vector lits;
+            for (unsigned i = 0; i < asms.size(); ++i) {
+                lits.push_back(get_literal(asms[i]));
+            }
+            preferred_sat(lits);
+            if (inconsistent()) {
+                SASSERT(m_scope_lvl == level);
+                is_sat = l_false;
+                break;
+            }
+            extract_cores(asms, cores, min_core_size); 
+            IF_VERBOSE(1, display_partial_assignment(verbose_stream(), asms, min_core_size););
+            
+            if (min_core_size <= 10) {
+                is_sat = l_undef;
+                break;
+            }
+            
+            is_sat = bounded_search();
+            if (!restart(is_sat, level)) {
+                break;
+            }
+            ++num_restarts;
+            if (num_restarts >= min_core_size) {
+                is_sat = l_undef;
+                while (num_restarts <= 10*min_core_size) {
+                    is_sat = bounded_search();
+                    if (!restart(is_sat, level)) {
+                        break;
+                    }
+                    ++num_restarts;
+                }
+                break;
+            }            
+        }
+        end_search();
+
+        return check_finalize(is_sat);
+    }
+
     struct neg_literal {
         unsigned negate(unsigned i) {
             return (~to_literal(i)).index();

src/smt/smt_context.cpp

@@ -1111,6 +1111,8 @@ namespace smt {
 
         if (r1 == r2) {
             TRACE("add_diseq_inconsistent", tout << "add_diseq #" << n1->get_owner_id() << " #" << n2->get_owner_id() << " inconsistency, scope_lvl: " << m_scope_lvl << "\n";);
+            //return false;
+
             theory_id  t1 = r1->m_th_var_list.get_th_id();
             if (t1 == null_theory_id) return false;
             return get_theory(t1)->use_diseqs();
@@ -3293,19 +3295,6 @@ namespace smt {
         m_num_conflicts_since_restart = 0;
     }
 
-    struct context::scoped_mk_model {
-        context & m_ctx;
-        scoped_mk_model(context & ctx):m_ctx(ctx) {
-            m_ctx.m_proto_model = 0;
-            m_ctx.m_model       = 0;
-        }
-        ~scoped_mk_model() {
-            if (m_ctx.m_proto_model.get() != 0) {
-                m_ctx.m_model = m_ctx.m_proto_model->mk_model();
-                m_ctx.m_proto_model = 0; // proto_model is not needed anymore.
-            }
-        }
-    };
 
     lbool context::search() {
 #ifndef _EXTERNAL_RELEASE 
@@ -3334,43 +3323,57 @@ namespace smt {
             TRACE("assigned_literals_per_lvl", display_num_assigned_literals_per_lvl(tout); 
                   tout << ", num_assigned: " << m_assigned_literals.size() << "\n";);
                                     
+            if (!restart(status, curr_lvl)) {
+                break;
+            }
+        }
+        
+        TRACE("search_lite", tout << "status: " << status << "\n";);
+        TRACE("guessed_literals", 
+              expr_ref_vector guessed_lits(m_manager);
+              get_guessed_literals(guessed_lits);
+              unsigned sz = guessed_lits.size();
+              for (unsigned i = 0; i < sz; i++) {
+                  tout << mk_pp(guessed_lits.get(i), m_manager) << "\n";
+              });
+        end_search();
+        return status;
+    }
+
+    bool context::restart(lbool& status, unsigned curr_lvl) {
+
         if (m_last_search_failure != OK) {
             if (status != l_false) {
                 // build candidate model before returning
                 mk_proto_model(status);
                 // status = l_undef;
             }
-                break;
+            return false;
         }
 
-            bool force_restart = false;
-            
         if (status == l_false) {
-                break;
+            return false;
         }
-            else if (status == l_true) {
+        if (status == l_true) {
             SASSERT(!inconsistent());
             mk_proto_model(l_true);
             // possible outcomes   DONE l_true, DONE l_undef, CONTINUE
             quantifier_manager::check_model_result cmr = m_qmanager->check_model(m_proto_model.get(), m_model_generator->get_root2value());
             if (cmr == quantifier_manager::SAT) {
                 // done 
-                    break; 
+                status = l_true;
+                return false;
             }
             if (cmr == quantifier_manager::UNKNOWN) {
                 IF_VERBOSE(1, verbose_stream() << "(smt.giveup quantifiers)\n";);
                 // giving up
                 m_last_search_failure = QUANTIFIERS;
                 status = l_undef;
-                    break;
+                return false;
             }
-                status        = l_undef;
-                force_restart = true;
         }
-            
-            SASSERT(status == l_undef);
         inc_limits();
-            if (force_restart || !m_fparams.m_restart_adaptive || m_agility < m_fparams.m_restart_agility_threshold) {
+        if (status == l_true || !m_fparams.m_restart_adaptive || m_agility < m_fparams.m_restart_agility_threshold) {
             SASSERT(!inconsistent());
             IF_VERBOSE(1, verbose_stream() << "(smt.restarting :propagations " << m_stats.m_num_propagations 
                        << " :decisions " << m_stats.m_num_decisions
@@ -3399,25 +3402,16 @@ namespace smt {
             if (inconsistent()) {
                 VERIFY(!resolve_conflict());
                 status = l_false;
-                    break;
+                return false;
             }
         }
         if (m_fparams.m_simplify_clauses)
             simplify_clauses();
         if (m_fparams.m_lemma_gc_strategy == LGC_AT_RESTART)
             del_inactive_lemmas();
-        }
 
-        TRACE("search_lite", tout << "status: " << status << "\n";);
+        status = l_undef;
-        TRACE("guessed_literals", 
+        return true;
-              expr_ref_vector guessed_lits(m_manager);
-              get_guessed_literals(guessed_lits);
-              unsigned sz = guessed_lits.size();
-              for (unsigned i = 0; i < sz; i++) {
-                  tout << mk_pp(guessed_lits.get(i), m_manager) << "\n";
-              });
-        end_search();
-        return status;
     }
     
     void context::tick(unsigned & counter) const {

src/smt/smt_context.h

@@ -200,7 +200,20 @@ namespace smt {
         model_ref                  m_model;
         std::string                m_unknown;
         void                       mk_proto_model(lbool r);
-        struct scoped_mk_model;
+        struct scoped_mk_model {
+            context & m_ctx;
+            scoped_mk_model(context & ctx):m_ctx(ctx) {
+                m_ctx.m_proto_model = 0;
+                m_ctx.m_model       = 0;
+            }
+            ~scoped_mk_model() {
+                if (m_ctx.m_proto_model.get() != 0) {
+                    m_ctx.m_model = m_ctx.m_proto_model->mk_model();
+                    m_ctx.m_proto_model = 0; // proto_model is not needed anymore.
+                }
+            }
+        };
+
 
         // -----------------------------------
         //
@@ -234,7 +247,6 @@ namespace smt {
             return m_params;
         }
 
-
         bool get_cancel_flag() { return !m_manager.limit().inc(); }
 
         region & get_region() {
@@ -1056,6 +1068,8 @@ namespace smt {
 
         void inc_limits();
 
+        bool restart(lbool& status, unsigned curr_lvl);
+
         void tick(unsigned & counter) const;
 
         lbool bounded_search();
@@ -1367,6 +1381,13 @@ namespace smt {
         void validate_consequences(expr_ref_vector const& assumptions, expr_ref_vector const& vars, 
                                    expr_ref_vector const& conseq, expr_ref_vector const& unfixed);
 
+        void justify(literal lit, index_set& s);
+
+        void extract_cores(expr_ref_vector const& asms, vector<expr_ref_vector>& cores, unsigned& min_core_size);
+
+        void preferred_sat(literal_vector& literals);
+
+        void display_partial_assignment(std::ostream& out, expr_ref_vector const& asms, unsigned min_core_size);
 
     public:
         context(ast_manager & m, smt_params & fp, params_ref const & p = params_ref());
@@ -1411,6 +1432,8 @@ namespace smt {
 
         lbool find_mutexes(expr_ref_vector const& vars, vector<expr_ref_vector>& mutexes);
 
+        lbool preferred_sat(expr_ref_vector const& asms, vector<expr_ref_vector>& cores);
+        
         lbool setup_and_check(bool reset_cancel = true);
         
         // return 'true' if assertions are inconsistent.

src/smt/smt_context_inv.cpp

@@ -322,6 +322,9 @@ namespace smt {
     bool context::check_th_diseq_propagation() const {
         TRACE("check_th_diseq_propagation", tout << "m_propagated_th_diseqs.size() " << m_propagated_th_diseqs.size() << "\n";);
         int num = get_num_bool_vars();
+        if (inconsistent()) {
+            return true;
+        }
         for (bool_var v = 0; v < num; v++) {
             if (has_enode(v)) {
                 enode * n = bool_var2enode(v);

src/smt/smt_kernel.cpp

@@ -115,6 +115,11 @@ namespace smt {
             return m_kernel.get_consequences(assumptions, vars, conseq, unfixed);
         }
 
+        lbool preferred_sat(expr_ref_vector const& asms, vector<expr_ref_vector>& cores) {
+            return m_kernel.preferred_sat(asms, cores);
+        }
+
+
         lbool find_mutexes(expr_ref_vector const& vars, vector<expr_ref_vector>& mutexes) {
             return m_kernel.find_mutexes(vars, mutexes);
         }
@@ -282,6 +287,10 @@ namespace smt {
         return m_imp->get_consequences(assumptions, vars, conseq, unfixed);
     }
 
+    lbool kernel::preferred_sat(expr_ref_vector const& asms, vector<expr_ref_vector>& cores) {
+        return m_imp->preferred_sat(asms, cores);
+    }
+
     lbool kernel::find_mutexes(expr_ref_vector const& vars, vector<expr_ref_vector>& mutexes) {
         return m_imp->find_mutexes(vars, mutexes);
     }

src/smt/smt_kernel.h

@@ -133,11 +133,16 @@ namespace smt {
         lbool get_consequences(expr_ref_vector const& assumptions, expr_ref_vector const& vars, 
                                expr_ref_vector& conseq, expr_ref_vector& unfixed);
 
-        /*
+        /**
           \brief find mutually exclusive variables.
          */
         lbool find_mutexes(expr_ref_vector const& vars, vector<expr_ref_vector>& mutexes);
 
+        /**
+           \brief Preferential SAT. 
+        */
+        lbool preferred_sat(expr_ref_vector const& asms, vector<expr_ref_vector>& cores);
+
         /**
            \brief Return the model associated with the last check command.
         */

src/smt/theory_wmaxsat.cpp

@@ -21,6 +21,7 @@ Notes:
 #include "smt_context.h"
 #include "ast_pp.h"
 #include "theory_wmaxsat.h"
+#include "smt_justification.h"
 
 namespace smt {
 
@@ -80,14 +81,13 @@ void theory_wmaxsat::get_assignment(svector<bool>& result) {
                   tout << result[i] << " ";
               }
               tout << "\n";);                          
-    
     }
     
     void theory_wmaxsat::init_search_eh() {
         m_propagate = true;
     }
     
-expr* theory_wmaxsat::assert_weighted(expr* fml, rational const& w, bool is_true) {
+    expr* theory_wmaxsat::assert_weighted(expr* fml, rational const& w) {
         context & ctx = get_context();
         ast_manager& m = get_manager();
         app_ref var(m), wfml(m);
@@ -99,11 +99,21 @@ expr* theory_wmaxsat::assert_weighted(expr* fml, rational const& w, bool is_true
         m_vars.push_back(var);
         m_fmls.push_back(fml);
         m_assigned.push_back(false);
-    if (!is_true) {
+        m_enabled.push_back(true);
-        m_rmin_cost += w;
-    }
         m_normalize = true;
-    return ctx.bool_var2expr(register_var(var, true));
+        bool_var bv = register_var(var, true);
+        TRACE("opt", tout << "enable: v" << m_bool2var[bv] << " b" << bv << " " << mk_pp(var, get_manager()) << "\n";
+              tout << wfml << "\n";);
+        return var;
+    }
+
+    void theory_wmaxsat::disable_var(expr* var) {
+        context& ctx = get_context();
+        SASSERT(ctx.b_internalized(var));
+        bool_var bv = ctx.get_bool_var(var);
+        theory_var tv = m_bool2var[bv];
+        m_enabled[tv] = false;
+        TRACE("opt", tout << "disable: v" << tv << " b" << bv << " " << mk_pp(var, get_manager()) << "\n";);
     }
     
     bool_var theory_wmaxsat::register_var(app* var, bool attach) {
@@ -130,37 +140,46 @@ bool_var theory_wmaxsat::register_var(app* var, bool attach) {
         return bv;
     }
     
-rational const& theory_wmaxsat::get_min_cost() { 
+    rational theory_wmaxsat::get_cost() { 
         unsynch_mpq_manager mgr;
         scoped_mpq q(mgr);
-    mgr.set(q, m_zmin_cost, m_den.to_mpq().numerator());
+        mgr.set(q, m_zcost, m_den.to_mpq().numerator());
-    m_rmin_cost = rational(q);
+        return rational(q);
-    return m_rmin_cost; 
     }
 
+    void theory_wmaxsat::init_min_cost(rational const& r) {
+        m_rmin_cost = r;
+        m_zmin_cost = (m_rmin_cost * m_den).to_mpq().numerator();
+    }
+
+
     void theory_wmaxsat::assign_eh(bool_var v, bool is_true) {
-    TRACE("opt", tout << "Assign " << mk_pp(m_vars[m_bool2var[v]].get(), get_manager()) << " " << is_true << "\n";);
         if (is_true) {
             if (m_normalize) normalize();
             context& ctx = get_context();
             theory_var tv = m_bool2var[v];
-        if (m_assigned[tv]) return;
+            if (m_assigned[tv] || !m_enabled[tv]) return;
             scoped_mpz w(m_mpz);
             w = m_zweights[tv];
             ctx.push_trail(numeral_trail(m_zcost, m_old_values));
             ctx.push_trail(push_back_vector<context, svector<theory_var> >(m_costs));
             ctx.push_trail(value_trail<context, bool>(m_assigned[tv]));
             m_zcost += w;
+            TRACE("opt", tout << "Assign v" << tv << " weight: " << w << " cost: " << m_zcost << " " << mk_pp(m_vars[m_bool2var[v]].get(), get_manager()) << "\n";);
             m_costs.push_back(tv);
             m_assigned[tv] = true;
-        if (m_zcost > m_zmin_cost) {
+            if (m_zcost >= m_zmin_cost) {
                 block();
             }            
+            else {
+                m_can_propagate = true;
+            }
         }
     }
 
     final_check_status theory_wmaxsat::final_check_eh() {
         if (m_normalize) normalize();
+        // std::cout << "cost: " << m_zcost << " min cost: " << m_zmin_cost << "\n";
         return FC_DONE;
     }
 
@@ -175,7 +194,6 @@ void theory_wmaxsat::reset_local() {
         m_fmls.reset();
         m_rweights.reset();
         m_rmin_cost.reset();
-    m_rcost.reset();
         m_zweights.reset();
         m_zcost.reset();
         m_zmin_cost.reset();
@@ -183,8 +201,10 @@ void theory_wmaxsat::reset_local() {
         m_bool2var.reset();
         m_var2bool.reset();
         m_propagate = false;
+        m_can_propagate = false;
         m_found_optimal = false;
         m_assigned.reset();
+        m_enabled.reset();
     }
 
 
@@ -198,6 +218,9 @@ void theory_wmaxsat::propagate() {
             }
         }
         m_propagate = false;
+        //while (m_found_optimal && max_unassigned_is_blocked() && !ctx.inconsistent()) { }
+
+        m_can_propagate = false;
     }       
     
     bool theory_wmaxsat::is_optimal() const {
@@ -214,15 +237,13 @@ expr_ref theory_wmaxsat::mk_block() {
         scoped_mpz weight(m_mpz);
         m_mpz.reset(weight);
         for (unsigned i = 0; i < costs.size() && m_mpz.lt(weight, m_zmin_cost); ++i) {
-        weight += m_zweights[costs[i]];
+            theory_var tv = costs[i];
-        disj.push_back(m.mk_not(m_vars[costs[i]].get()));
+            if (m_enabled[tv]) {
+                weight += m_zweights[tv];
+                disj.push_back(m.mk_not(m_vars[tv].get()));
+            }
         }
         if (is_optimal()) {
-        unsynch_mpq_manager mgr;
-        scoped_mpq q(mgr);
-        mgr.set(q, m_zmin_cost, m_den.to_mpq().numerator());
-        rational rw = rational(q);
-        m_zmin_cost = weight;
             m_found_optimal = true;
             m_cost_save.reset();
             m_cost_save.append(m_costs);
@@ -232,7 +253,7 @@ expr_ref theory_wmaxsat::mk_block() {
                       tout << mk_pp(get_enode(m_costs[i])->get_owner(), get_manager()) << " ";
                   }
                   tout << "\n";
-              get_context().display(tout);                      
+                  //get_context().display(tout);                      
                   );
         }
         expr_ref result(m.mk_or(disj.size(), disj.c_ptr()), m);
@@ -242,21 +263,7 @@ expr_ref theory_wmaxsat::mk_block() {
         return result;
     }
 
-expr_ref theory_wmaxsat::mk_optimal_block(svector<bool_var> const& ws, rational const& weight) {
+    void theory_wmaxsat::restart_eh() {}
-    ast_manager& m = get_manager();
-    expr_ref_vector disj(m);
-    rational new_w = weight*m_den;
-    m_zmin_cost = new_w.to_mpq().numerator();
-    m_cost_save.reset();
-    for (unsigned i = 0; i < ws.size(); ++i) {
-        bool_var bv = ws[i];
-        theory_var v = m_bool2var[bv];
-        m_cost_save.push_back(v);
-        disj.push_back(m.mk_not(m_vars[v].get()));
-    }
-    expr_ref result(m.mk_or(disj.size(), disj.c_ptr()), m);
-    return result;
-}
 
     void theory_wmaxsat::block() {
         if (m_vars.empty()) {
@@ -273,40 +280,90 @@ void theory_wmaxsat::block() {
         m_mpz.reset(weight);
         for (unsigned i = 0; i < costs.size() && weight < m_zmin_cost; ++i) {
             weight += m_zweights[costs[i]];
-        lits.push_back(~literal(m_var2bool[costs[i]]));
+            lits.push_back(literal(m_var2bool[costs[i]]));
+        }
+        TRACE("opt", ctx.display_literals_verbose(tout, lits); tout << "\n";);
+        
+        ctx.set_conflict(
+            ctx.mk_justification(
+                ext_theory_conflict_justification(get_id(), ctx.get_region(), lits.size(), lits.c_ptr(), 0, 0, 0, 0)));
+    }     
+
+    bool theory_wmaxsat::max_unassigned_is_blocked() {
+        context& ctx = get_context();
+        unsigned max_unassigned = m_max_unassigned_index;
+        if (max_unassigned < m_sorted_vars.size() && 
+            m_zcost + m_zweights[m_sorted_vars[max_unassigned]] < m_zmin_cost) {
+            return false;
+        }
+        // update value of max-unassigned
+        while (max_unassigned < m_sorted_vars.size() &&
+               ctx.get_assignment(m_var2bool[m_sorted_vars[max_unassigned]]) != l_undef) {
+            ++max_unassigned;
+        }
+        // 
+        if (max_unassigned > m_max_unassigned_index) {
+            ctx.push_trail(value_trail<context, unsigned>(m_max_unassigned_index));
+            m_max_unassigned_index = max_unassigned;
+        }
+        if (max_unassigned < m_sorted_vars.size() && 
+            m_zcost + m_zweights[m_sorted_vars[max_unassigned]] >= m_zmin_cost) {
+            theory_var tv = m_sorted_vars[max_unassigned];
+            propagate(m_var2bool[tv]);
+            m_max_unassigned_index++;
+            return true;
+        }
+
+        return false;
+    }
+    
+    void theory_wmaxsat::propagate(bool_var v) {
+        ++m_stats.m_num_propagations;
+        context& ctx = get_context();
+        literal_vector lits;
+        literal lit(v, true);
+        
+        SASSERT(ctx.get_assignment(lit) == l_undef);
+        
+        for (unsigned i = 0; i < m_costs.size(); ++i) {
+            bool_var w = m_var2bool[m_costs[i]];
+            lits.push_back(literal(w));        
         }
         TRACE("opt", 
-          ast_manager& m = get_manager();
+              ctx.display_literals_verbose(tout, lits.size(), lits.c_ptr()); 
-          tout << "block: ";
+              ctx.display_literal_verbose(tout << " --> ", lit););
-          for (unsigned i = 0; i < lits.size(); ++i) {
-              expr_ref tmp(m);
-              ctx.literal2expr(lits[i], tmp);
-              tout << tmp << " ";
-          }
-          tout << "\n";
-          );
         
-    ctx.mk_th_axiom(get_id(), lits.size(), lits.c_ptr());
+        region& r = ctx.get_region();
+        ctx.assign(lit, ctx.mk_justification(
+                       ext_theory_propagation_justification(
+                           get_id(), r, lits.size(), lits.c_ptr(), 0, 0, lit, 0, 0)));
     }                
 
 
     void theory_wmaxsat::normalize() {
         m_den = rational::one();
         for (unsigned i = 0; i < m_rweights.size(); ++i) {
+            if (m_enabled[i]) {
                 m_den = lcm(m_den, denominator(m_rweights[i]));
             }
+        }
         m_den = lcm(m_den, denominator(m_rmin_cost));
         SASSERT(!m_den.is_zero());
         m_zweights.reset();
+        m_sorted_vars.reset();
         for (unsigned i = 0; i < m_rweights.size(); ++i) {            
             rational r = m_rweights[i]*m_den;
             SASSERT(r.is_int());
             mpq const& q = r.to_mpq();
             m_zweights.push_back(q.numerator());
+            m_sorted_vars.push_back(i);
         }
-    rational r = m_rcost* m_den;
+        compare_cost compare_cost(*this);
-    m_zcost = r.to_mpq().numerator();
+        std::sort(m_sorted_vars.begin(), m_sorted_vars.end(), compare_cost);
-    r = m_rmin_cost * m_den;
+        m_max_unassigned_index = 0;
+        
+        m_zcost.reset();
+        rational r = m_rmin_cost * m_den;
         m_zmin_cost = r.to_mpq().numerator();
         m_normalize = false;
     }

src/smt/theory_wmaxsat.h

@@ -28,6 +28,7 @@ namespace smt {
     class theory_wmaxsat : public theory {
         struct stats {
             unsigned m_num_blocks;
+            unsigned m_num_propagations;
             void reset() { memset(this, 0, sizeof(*this)); }
             stats() { reset(); }
         };        
@@ -39,8 +40,9 @@ namespace smt {
         scoped_mpz_vector        m_zweights;
         scoped_mpz_vector        m_old_values;
         svector<theory_var>      m_costs;       // set of asserted theory variables
+        unsigned                 m_max_unassigned_index; // index of literal that is not yet assigned and has maximal weight.
+        svector<theory_var>      m_sorted_vars; // set of all theory variables, sorted by cost
         svector<theory_var>      m_cost_save;   // set of asserted theory variables
-        rational                 m_rcost;       // current sum of asserted costs
         rational                 m_rmin_cost;   // current maximal cost assignment.
         scoped_mpz               m_zcost;       // current sum of asserted costs
         scoped_mpz               m_zmin_cost;   // current maximal cost assignment.
@@ -48,18 +50,21 @@ namespace smt {
         u_map<theory_var>        m_bool2var;    // bool_var -> theory_var
         svector<bool_var>        m_var2bool;    // theory_var -> bool_var
         bool                     m_propagate;
+        bool                     m_can_propagate;
         bool                     m_normalize; 
         rational                 m_den;         // lcm of denominators for rational weights.
-        svector<bool>            m_assigned;
+        svector<bool>            m_assigned, m_enabled;
         stats                    m_stats;
     public:
         theory_wmaxsat(ast_manager& m, filter_model_converter& mc);
         virtual ~theory_wmaxsat();
         void get_assignment(svector<bool>& result);
-        virtual void init_search_eh();
+        expr* assert_weighted(expr* fml, rational const& w);
-        expr* assert_weighted(expr* fml, rational const& w, bool is_true);
+        void  disable_var(expr* var);
         bool_var register_var(app* var, bool attach);
-        rational const& get_min_cost();
+        rational get_cost();
+        void init_min_cost(rational const& r);
+
         class numeral_trail : public trail<context> {
             typedef scoped_mpz T;
             T & m_value;
@@ -79,6 +84,8 @@ namespace smt {
                 m_old_values.shrink(m_old_values.size() - 1);
             }
         };
+
+        virtual void init_search_eh();
         virtual void assign_eh(bool_var v, bool is_true);
         virtual final_check_status final_check_eh();
         virtual bool use_diseqs() const { 
@@ -95,24 +102,31 @@ namespace smt {
         virtual void new_eq_eh(theory_var v1, theory_var v2) { }
         virtual void new_diseq_eh(theory_var v1, theory_var v2) { }
         virtual void display(std::ostream& out) const {}
+        virtual void restart_eh();
 
         virtual void collect_statistics(::statistics & st) const {
             st.update("wmaxsat num blocks", m_stats.m_num_blocks);
+            st.update("wmaxsat num props", m_stats.m_num_propagations);
         }
         virtual bool can_propagate() {
-            return m_propagate;
+            return m_propagate || m_can_propagate;
         }
 
         virtual void propagate();
+
         bool is_optimal() const;
         expr_ref mk_block();
 
-        expr_ref mk_optimal_block(svector<bool_var> const& ws, rational const& weight);
+        
+
     private:
 
         void block();
+        void propagate(bool_var v);
         void normalize();
 
+        bool max_unassigned_is_blocked();
+       
         class compare_cost {
             theory_wmaxsat& m_th;
         public:

src/solver/solver.cpp

@@ -154,6 +154,10 @@ lbool solver::find_mutexes(expr_ref_vector const& vars, vector<expr_ref_vector>&
     return l_true;
 }
 
+lbool solver::preferred_sat(expr_ref_vector const& asms, vector<expr_ref_vector>& cores) {
+    return check_sat(0, 0);
+}
+
 bool solver::is_literal(ast_manager& m, expr* e) {
     return is_uninterp_const(e) || (m.is_not(e, e) && is_uninterp_const(e));
 }

src/solver/solver.h

@@ -166,6 +166,12 @@ public:
 
     virtual lbool find_mutexes(expr_ref_vector const& vars, vector<expr_ref_vector>& mutexes);
 
+    /**
+       \brief Preferential SAT. Prefer assumptions to be true, produce cores that witness cases when not all assumptions can be met.
+       by default, preferred sat ignores the assumptions.
+     */
+    virtual lbool preferred_sat(expr_ref_vector const& asms, vector<expr_ref_vector>& cores);
+
     /**
        \brief Display the content of this solver.
     */