Polysat: conflict resolution wip (#5529)

* conflict_core doesn't need gc() anymore

* update comments, ensure_bvar for new constraints

* Make sure constraints can only be created through constraint_manager

* fix constraint::display if no boolean variable is assigned

* Move clause into separate file

* Add conflict_core binary resolution

* conflict_core additions

* reactivate conflict resolution outer loop

* wip

* seems commented includes break CI build

src/math/polysat/CMakeLists.txt

@@ -1,6 +1,7 @@
 z3_add_component(polysat
   SOURCES
     boolean.cpp
+    clause.cpp
     clause_builder.cpp
     conflict_core.cpp
     constraint.cpp
@@ -14,6 +15,7 @@ z3_add_component(polysat
     solver.cpp
     ule_constraint.cpp
     viable.cpp
+    variable_elimination.cpp
   COMPONENT_DEPENDENCIES
     util
     dd

src/math/polysat/clause.cpp

@@ -0,0 +1,58 @@
+/*++
+Copyright (c) 2021 Microsoft Corporation
+
+Module Name:
+
+    polysat clauses
+
+Author:
+
+    Nikolaj Bjorner (nbjorner) 2021-03-19
+    Jakob Rath 2021-04-6
+
+--*/
+
+#include "math/polysat/clause.h"
+#include "math/polysat/solver.h"
+
+namespace polysat {
+
+    clause_ref clause::from_unit(signed_constraint c, p_dependency_ref d) {
+        SASSERT(c->has_bvar());
+        unsigned const lvl = c->level();
+        sat::literal_vector lits;
+        lits.push_back(c.blit());
+        return clause::from_literals(lvl, std::move(d), std::move(lits));
+    }
+
+    clause_ref clause::from_literals(unsigned lvl, p_dependency_ref d, sat::literal_vector literals) {
+        return alloc(clause, lvl, std::move(d), std::move(literals));
+    }
+
+    bool clause::is_always_false(solver& s) const {
+        return std::all_of(m_literals.begin(), m_literals.end(), [&s](sat::literal lit) {
+            signed_constraint c = s.m_constraints.lookup(lit);
+            return c.is_always_false();
+        });
+    }
+
+    bool clause::is_currently_false(solver& s) const {
+        return std::all_of(m_literals.begin(), m_literals.end(), [&s](sat::literal lit) {
+            signed_constraint c = s.m_constraints.lookup(lit);
+            return c.is_currently_false(s);
+        });
+    }
+
+    std::ostream& clause::display(std::ostream& out) const {
+        bool first = true;
+        for (auto lit : *this) {
+            if (first)
+                first = false;
+            else
+                out << " \\/ ";
+            out << lit;
+        }
+        return out;
+    }
+
+}

src/math/polysat/clause.h

@@ -0,0 +1,85 @@
+/*++
+Copyright (c) 2021 Microsoft Corporation
+
+Module Name:
+
+    polysat clauses
+
+Author:
+
+    Nikolaj Bjorner (nbjorner) 2021-03-19
+    Jakob Rath 2021-04-6
+
+--*/
+#pragma once
+#include "math/polysat/boolean.h"
+#include "math/polysat/types.h"
+
+namespace polysat {
+
+    class signed_constraint;
+
+    class clause;
+    using clause_ref = ref<clause>;
+    using clause_ref_vector = sref_vector<clause>;
+
+    /// Disjunction of constraints represented by boolean literals
+    // NB code review:
+    // right, ref-count is unlikely the right mechanism.
+    // In the SAT solver all clauses are managed in one arena (auxiliarary and redundant)
+    // and deleted when they exist the arena.
+    //
+    class clause {
+        friend class constraint_manager;
+
+        unsigned m_ref_count = 0;  // TODO: remove refcount once we confirm it's not needed anymore
+        unsigned m_level;
+        unsigned m_next_guess = 0;  // next guess for enumerative backtracking
+        p_dependency_ref m_dep;
+        sat::literal_vector m_literals;
+
+        /* TODO: embed literals to save an indirection?
+        unsigned m_num_literals;
+        constraint* m_literals[0];
+
+        static size_t object_size(unsigned m_num_literals) {
+            return sizeof(clause) + m_num_literals * sizeof(constraint*);
+        }
+        */
+
+        clause(unsigned lvl, p_dependency_ref d, sat::literal_vector literals):
+            m_level(lvl), m_dep(std::move(d)), m_literals(std::move(literals)) {
+            SASSERT(std::count(m_literals.begin(), m_literals.end(), sat::null_literal) == 0);
+        }
+
+    public:
+        void inc_ref() { m_ref_count++; }
+        void dec_ref() { SASSERT(m_ref_count > 0); m_ref_count--; if (!m_ref_count) dealloc(this); }
+
+        static clause_ref from_unit(signed_constraint c, p_dependency_ref d);
+        static clause_ref from_literals(unsigned lvl, p_dependency_ref d, sat::literal_vector literals);
+
+        p_dependency* dep() const { return m_dep; }
+        unsigned level() const { return m_level; }
+
+        bool empty() const { return m_literals.empty(); }
+        unsigned size() const { return m_literals.size(); }
+        sat::literal operator[](unsigned idx) const { return m_literals[idx]; }
+
+        using const_iterator = typename sat::literal_vector::const_iterator;
+        const_iterator begin() const { return m_literals.begin(); }
+        const_iterator end() const { return m_literals.end(); }
+
+        bool is_always_false(solver& s) const;
+        bool is_currently_false(solver& s) const;
+
+        unsigned next_guess() {
+            SASSERT(m_next_guess < size());
+            return m_next_guess++;
+        }
+
+        std::ostream& display(std::ostream& out) const;
+    };
+
+    inline std::ostream& operator<<(std::ostream& out, clause const& c) { return c.display(out); }
+}

src/math/polysat/conflict_core.cpp

@@ -16,6 +16,7 @@ Author:
 #include "math/polysat/solver.h"
 #include "math/polysat/log.h"
 #include "math/polysat/log_helper.h"
+#include <algorithm>
 
 namespace polysat {
 
@@ -46,40 +47,71 @@ namespace polysat {
         m_needs_model = true;
     }
 
-    void conflict_core::set(pvar v, vector<signed_constraint> const& cjust_v) {
-        LOG("Conflict for v" << v << ": " << cjust_v);
+    void conflict_core::set(pvar v) {
+        LOG("Conflict: v" << v);
         SASSERT(empty());
-        NOT_IMPLEMENTED_YET();
         m_conflict_var = v;
-        m_constraints.append(cjust_v);
-        if (cjust_v.empty())
-            m_constraints.push_back({});
         m_needs_model = true;
     }
 
-    void conflict_core::resolve(sat::bool_var var, clause const& cl) {
-        // TODO: fix the implementation: should resolve the given clause with the current conflict core.
-#if 0
-        DEBUG_CODE({
-            bool this_has_pos = std::count(begin(), end(), sat::literal(var)) > 0;
-            bool this_has_neg = std::count(begin(), end(), ~sat::literal(var)) > 0;
-            bool other_has_pos = std::count(other.begin(), other.end(), sat::literal(var)) > 0;
-            bool other_has_neg = std::count(other.begin(), other.end(), ~sat::literal(var)) > 0;
-            SASSERT(!this_has_pos || !this_has_neg);  // otherwise this is tautology
-            SASSERT(!other_has_pos || !other_has_neg);  // otherwise other is tautology
-            SASSERT((this_has_pos && other_has_neg) || (this_has_neg && other_has_pos));
-        });
-        // The resolved var should not be one of the new constraints
-        int j = 0;
-        for (auto lit : m_literals)
-            if (lit.var() != var)
-                m_literals[j++] = lit;
-        m_literals.shrink(j);
-        for (sat::literal lit : other)
-            if (lit.var() != var)
-                m_literals.push_back(lit);
-        return true;
-#endif
+    void conflict_core::push(signed_constraint c) {
+        SASSERT(!empty());  // should use set() to enter conflict state
+        // Skip trivial constraints
+        // (e.g., constant ones such as "4 > 1"... only true ones should appear, otherwise the lemma would be a tautology)
+        if (c.is_always_true())
+            return;
+        SASSERT(!c.is_always_false());
+        m_constraints.push_back(c);
     }
 
+    void conflict_core::resolve(constraint_manager const& m, sat::bool_var var, clause const& cl) {
+        // Note: core: x, y, z; corresponds to clause ~x \/ ~y \/ ~z
+        //       clause: x \/ u \/ v
+        //       resolvent: ~y \/ ~z \/ u \/ v; as core: y, z, ~u, ~v
+
+        SASSERT(var != sat::null_bool_var);
+        DEBUG_CODE({
+            bool core_has_pos = std::count_if(begin(), end(), [var](auto c){ return c.blit() == sat::literal(var); }) > 0;
+            bool core_has_neg = std::count_if(begin(), end(), [var](auto c){ return c.blit() == ~sat::literal(var); }) > 0;
+            bool clause_has_pos = std::count(cl.begin(), cl.end(), sat::literal(var)) > 0;
+            bool clause_has_neg = std::count(cl.begin(), cl.end(), ~sat::literal(var)) > 0;
+            SASSERT(!core_has_pos || !core_has_neg);  // otherwise core is tautology
+            SASSERT(!clause_has_pos || !clause_has_neg);  // otherwise clause is tautology
+            SASSERT((core_has_pos && clause_has_pos) || (core_has_neg && clause_has_neg));
+        });
+
+        int j = 0;
+        for (auto c : m_constraints)
+            if (c->bvar() == var)
+                m_constraints[j++] = c;
+        m_constraints.shrink(j);
+
+        for (sat::literal lit : cl)
+            if (lit.var() != var)
+                m_constraints.push_back(m.lookup(~lit));
+    }
+
+    clause_ref conflict_core::build_lemma(solver& s, unsigned trail_idx) {
+        sat::literal_vector literals;
+        p_dependency_ref dep = s.mk_dep_ref(null_dependency);
+        unsigned lvl = 0;
+
+        // TODO: another core reduction step?
+
+        for (auto c : m_constraints) {
+            if (c->unit_clause()) {
+                dep = s.m_dm.mk_join(dep, c->unit_dep());
+                continue;
+            }
+            lvl = std::max(lvl, c->level());
+            s.m_constraints.ensure_bvar(c.get());
+            literals.push_back(~c.blit());
+        }
+
+        if (m_needs_model) {
+            // TODO: add equalities corresponding to model up to trail_idx
+        }
+
+        return clause::from_literals(lvl, std::move(dep), std::move(literals));
+    }
 }

src/math/polysat/conflict_core.h

@@ -16,14 +16,12 @@ Author:
 
 namespace polysat {
 
+    class solver;
+
     /** Conflict state, represented as core (~negation of clause). */
     class conflict_core {
         vector<signed_constraint> m_constraints;
 
-        /** Storage for new constraints that may not yet have a boolean variable yet */
-        // TODO: not necessary anymore, if we keep constraint_manager::gc()
-        ptr_vector<constraint> m_storage;
-
         // If this is not null_var, the conflict was due to empty viable set for this variable.
         // Can be treated like "v = x" for any value x.
         pvar m_conflict_var = null_var;
@@ -35,21 +33,20 @@ namespace polysat {
         //       For example: if we have 4x+y=2 and y=0, then we have a conflict no matter the value of x, so we should drop x=? from the core.
 
     public:
-        ~conflict_core() {
-            gc();
-        }
-
         vector<signed_constraint> const& constraints() const { return m_constraints; }
         bool needs_model() const { return m_needs_model; }
+        pvar conflict_var() const { return m_conflict_var; }
+
+        bool is_bailout() const { return m_constraints.size() == 1 && !m_constraints[0]; }
 
         bool empty() const {
-            return m_constraints.empty() && !m_needs_model;
+            return m_constraints.empty() && !m_needs_model && m_conflict_var == null_var;
         }
 
         void reset() {
             m_constraints.reset();
             m_needs_model = false;
-            gc();
+            m_conflict_var = null_var;
             SASSERT(empty());
         }
 
@@ -58,20 +55,21 @@ namespace polysat {
         /** conflict because the constraint c is false under current variable assignment */
         void set(signed_constraint c);
         /** conflict because there is no viable value for the variable v */
-        void set(pvar v, vector<signed_constraint> const& cjust_v);
+        void set(pvar v);
 
-        /** Garbage-collect temporary constraints */
-        void gc() {
-            for (auto* c : m_storage)
-                if (!c->has_bvar())
-                    dealloc(c);
-            m_storage.reset();
-        }
+        void push(signed_constraint c);
 
         /** Perform boolean resolution with the clause upon variable 'var'.
          * Precondition: core/clause contain complementary 'var'-literals.
          */
-        void resolve(sat::bool_var var, clause const& cl);
+        void resolve(constraint_manager const& m, sat::bool_var var, clause const& cl);
+
+        /** Convert the core into a lemma to be learned. */
+        clause_ref build_lemma(solver& s, unsigned trail_idx);
+
+        using const_iterator = decltype(m_constraints)::const_iterator;
+        const_iterator begin() { return constraints().begin(); }
+        const_iterator end() { return constraints().end(); }
 
         std::ostream& display(std::ostream& out) const;
     };

src/math/polysat/constraint.cpp

@@ -13,6 +13,7 @@ Author:
 --*/
 
 #include "math/polysat/constraint.h"
+#include "math/polysat/clause.h"
 #include "math/polysat/solver.h"
 #include "math/polysat/log.h"
 #include "math/polysat/log_helper.h"
@@ -21,9 +22,6 @@ Author:
 
 namespace polysat {
 
-    //static_assert(!std::is_copy_assignable_v<scoped_signed_constraint>);
-    //static_assert(!std::is_copy_constructible_v<scoped_signed_constraint>);
-
     void constraint_manager::assign_bv2c(sat::bool_var bv, constraint* c) {
         SASSERT_EQ(get_bv2c(bv), nullptr);
         SASSERT(!c->has_bvar());
@@ -42,8 +40,9 @@ namespace polysat {
         return m_bv2constraint.get(bv, nullptr);
     }
 
-    void constraint_manager::assign_bvar(constraint* c) {
-        assign_bv2c(m_bvars.new_var(), c);
+    void constraint_manager::ensure_bvar(constraint* c) {
+        if (!c->has_bvar())
+            assign_bv2c(m_bvars.new_var(), c);
     }
 
     void constraint_manager::erase_bvar(constraint* c) {
@@ -141,16 +140,6 @@ namespace polysat {
         if (it == m_constraint_table.end()) {
             store(c1);
             m_constraint_table.insert(c1);
-            // Assuming c is a temporary constraint, we need to:
-            //     1. erase(c);
-            //     2. m_constraint_table.remove(c);
-            // before we dealloc it.
-            // But even if we don't do this, there is not a real memory leak because the constraint will be deallocated properly when the level is popped.
-            // So maybe the best way is to just do periodic GC passes where we throw out constraints that do not have a boolean variable,
-            // instead of precise lifetime tracking for temprorary constraints.
-            // It should be safe to do a GC pass outside of conflict resolution.
-            // TODO: if this is the path we take, then we can drop the scoped_signed_constraint and the scoped_constraint_ptr classes.
-            // TODO: we could maintain a counter of temporary constraints (#constraints - #bvars) to decide when to do a GC, or just do it after every conflict resolution
             return c1;
         }
         constraint* c0 = *it;
@@ -182,6 +171,7 @@ namespace polysat {
 
     bool constraint_manager::should_gc() {
         // TODO: maybe replace this by a better heuristic
+        // maintain a counter of temporary constraints? (#constraints - #bvars)
         return true;
     }
 
@@ -241,7 +231,9 @@ namespace polysat {
     }
 
     std::ostream& constraint::display_extra(std::ostream& out, lbool status) const {
-        out << " @" << level() << " (b" << bvar() << ")";
+        out << " @" << level() << " (b";
+        if (has_bvar()) { out << bvar(); } else { out << "_"; }
+        out << ")";
         (void)status;
         // if (is_positive()) out << " [pos]";
         // if (is_negative()) out << " [neg]";
@@ -277,42 +269,4 @@ namespace polysat {
         narrow(s, is_positive);
     }
 
-    clause_ref clause::from_unit(signed_constraint c, p_dependency_ref d) {
-        SASSERT(c->has_bvar());
-        unsigned const lvl = c->level();
-        sat::literal_vector lits;
-        lits.push_back(c.blit());
-        return clause::from_literals(lvl, std::move(d), std::move(lits));
-    }
-
-    clause_ref clause::from_literals(unsigned lvl, p_dependency_ref d, sat::literal_vector literals) {
-        return alloc(clause, lvl, std::move(d), std::move(literals));
-    }
-
-    bool clause::is_always_false(solver& s) const {
-        return std::all_of(m_literals.begin(), m_literals.end(), [&s](sat::literal lit) {
-            signed_constraint c = s.m_constraints.lookup(lit);
-            return c.is_always_false();
-        });
-    }
-
-    bool clause::is_currently_false(solver& s) const {
-        return std::all_of(m_literals.begin(), m_literals.end(), [&s](sat::literal lit) {
-            signed_constraint c = s.m_constraints.lookup(lit);
-            return c.is_currently_false(s);
-        });
-    }
-
-    std::ostream& clause::display(std::ostream& out) const {
-        bool first = true;
-        for (auto lit : *this) {
-            if (first)
-                first = false;
-            else
-                out << " \\/ ";
-            out << lit;
-        }
-        return out;
-    }
-
 }

src/math/polysat/constraint.h

@@ -13,13 +13,9 @@ Author:
 --*/
 #pragma once
 #include "math/polysat/boolean.h"
+#include "math/polysat/clause.h"
 #include "math/polysat/types.h"
 #include "math/polysat/interval.h"
-#include "math/polysat/log.h"
-#include "util/map.h"
-#include "util/ref.h"
-#include "util/ref_vector.h"
-#include <type_traits>
 
 namespace polysat {
 
@@ -30,11 +26,6 @@ namespace polysat {
     class ule_constraint;
     class signed_constraint;
 
-
-    class clause;
-    using clause_ref = ref<clause>;
-    using clause_ref_vector = sref_vector<clause>;
-
     using constraint_table = ptr_hashtable<constraint, obj_ptr_hash<constraint>, deref_eq<constraint>>;
 
     // Manage constraint lifetime, deduplication, and connection to boolean variables/literals.
@@ -71,9 +62,9 @@ namespace polysat {
         constraint_manager(bool_var_manager& bvars): m_bvars(bvars) {}
         ~constraint_manager();
 
-        void assign_bvar(constraint* c);
+        void ensure_bvar(constraint* c);
         void erase_bvar(constraint* c);
-        sat::literal get_or_assign_blit(signed_constraint& c);
+        // sat::literal get_or_assign_blit(signed_constraint& c);
 
         clause* store(clause_ref cl);
 
@@ -129,6 +120,7 @@ namespace polysat {
          */
         // NB code review: the convention would make sense. Unfortunately, elsewhere in z3 we use "true" for negative literals
         // and "false" for positive literals. It is called the "sign" bit.
+        // TODO: replace parameter 'is_positive' everywhere by 'sign'? (also in signed_constraint)
         sat::bool_var       m_bvar = sat::null_bool_var;
 
         constraint(constraint_manager& m, unsigned lvl, ckind_t k):
@@ -169,7 +161,7 @@ namespace polysat {
 
         clause* unit_clause() const { return m_unit_clause; }
         void set_unit_clause(clause* cl) { SASSERT(cl); SASSERT(!m_unit_clause || m_unit_clause == cl); m_unit_clause = cl; }
-        p_dependency* unit_dep() const;
+        p_dependency* unit_dep() const { return m_unit_clause ? m_unit_clause->dep() : nullptr; }
 
         /** Precondition: all variables other than v are assigned.
          *
@@ -200,9 +192,8 @@ namespace polysat {
             SASSERT_EQ(blit(), lit);
         }
 
-        void negate() {
-            m_positive = !m_positive;
-        }
+        void negate() { m_positive = !m_positive; }
+        signed_constraint operator~() const { return {get(), !is_positive()}; }
 
         bool is_positive() const { return m_positive; }
         bool is_negative() const { return !is_positive(); }
@@ -210,6 +201,7 @@ namespace polysat {
         bool propagate(solver& s, pvar v) { return get()->propagate(s, is_positive(), v); }
         void propagate_core(solver& s, pvar v, pvar other_v) { get()->propagate_core(s, is_positive(), v, other_v); }
         bool is_always_false() { return get()->is_always_false(is_positive()); }
+        bool is_always_true() { return get()->is_always_false(is_negative()); }
         bool is_currently_false(solver& s) { return get()->is_currently_false(s, is_positive()); }
         bool is_currently_true(solver& s) { return get()->is_currently_true(s, is_positive()); }
         void narrow(solver& s) { get()->narrow(s, is_positive()); }
@@ -219,7 +211,6 @@ namespace polysat {
         sat::literal blit() const { return sat::literal(bvar(), is_negative()); }
         constraint* get() const { return m_constraint; }
 
-
         explicit operator bool() const { return !!m_constraint; }
         bool operator!() const { return !m_constraint; }
         constraint* operator->() const { return get(); }
@@ -243,71 +234,4 @@ namespace polysat {
     inline std::ostream& operator<<(std::ostream& out, signed_constraint const& c) {
         return c.display(out);
     }
-
-    inline signed_constraint operator~(signed_constraint const& c) {
-        return {c.get(), !c.is_positive()};
-    }
-
-
-    /// Disjunction of constraints represented by boolean literals
-    // NB code review:
-    // right, ref-count is unlikely the right mechanism.
-    // In the SAT solver all clauses are managed in one arena (auxiliarary and redundant)
-    // and deleted when they exist the arena.
-    //
-    class clause {
-        friend class constraint_manager;
-
-        unsigned m_ref_count = 0;  // TODO: remove refcount once we confirm it's not needed anymore
-        unsigned m_level;
-        unsigned m_next_guess = 0;  // next guess for enumerative backtracking
-        p_dependency_ref m_dep;
-        sat::literal_vector m_literals;
-
-        /* TODO: embed literals to save an indirection?
-        unsigned m_num_literals;
-        constraint* m_literals[0];
-
-        static size_t object_size(unsigned m_num_literals) {
-            return sizeof(clause) + m_num_literals * sizeof(constraint*);
-        }
-        */
-
-        clause(unsigned lvl, p_dependency_ref d, sat::literal_vector literals):
-            m_level(lvl), m_dep(std::move(d)), m_literals(std::move(literals)) {
-            SASSERT(std::count(m_literals.begin(), m_literals.end(), sat::null_literal) == 0);
-        }
-
-    public:
-        void inc_ref() { m_ref_count++; }
-        void dec_ref() { SASSERT(m_ref_count > 0); m_ref_count--; if (!m_ref_count) dealloc(this); }
-
-        static clause_ref from_unit(signed_constraint c, p_dependency_ref d);
-        static clause_ref from_literals(unsigned lvl, p_dependency_ref d, sat::literal_vector literals);
-
-        p_dependency* dep() const { return m_dep; }
-        unsigned level() const { return m_level; }
-
-        bool empty() const { return m_literals.empty(); }
-        unsigned size() const { return m_literals.size(); }
-        sat::literal operator[](unsigned idx) const { return m_literals[idx]; }
-
-        using const_iterator = typename sat::literal_vector::const_iterator;
-        const_iterator begin() const { return m_literals.begin(); }
-        const_iterator end() const { return m_literals.end(); }
-
-        bool is_always_false(solver& s) const;
-        bool is_currently_false(solver& s) const;
-
-        unsigned next_guess() {
-            SASSERT(m_next_guess < size());
-            return m_next_guess++;
-        }
-
-        std::ostream& display(std::ostream& out) const;
-    };
-
-    inline std::ostream& operator<<(std::ostream& out, clause const& c) { return c.display(out); }
-
-    inline p_dependency* constraint::unit_dep() const { return m_unit_clause ? m_unit_clause->dep() : nullptr; }
 }

src/math/polysat/eq_constraint.h

@@ -18,12 +18,16 @@ Author:
 namespace polysat {
 
     class eq_constraint final : public constraint {
+        friend class constraint_manager;
+
         pdd m_poly;
-    public:
+
         eq_constraint(constraint_manager& m, unsigned lvl, pdd const& p):
             constraint(m, lvl, ckind_t::eq_t), m_poly(p) {
             m_vars.append(p.free_vars());
         }
+
+    public:
         ~eq_constraint() override {}
         pdd const & p() const { return m_poly; }
         std::ostream& display(std::ostream& out, lbool status) const override;

src/math/polysat/explain.cpp

@@ -22,6 +22,7 @@ namespace polysat {
         return false;
     }
 
+#if 0
     conflict_explainer::conflict_explainer(solver& s): m_solver(s) {
         inference_engines.push_back(alloc(inf_polynomial_superposition));
     }
@@ -32,6 +33,7 @@ namespace polysat {
                 return true;
         return false;
     }
+#endif
 
 
 
@@ -582,7 +584,4 @@ namespace polysat {
 //         return true;
 //     }
 
-    void conflict_explainer::resolve()
-    {
-    }
 }

src/math/polysat/explain.h

@@ -29,7 +29,7 @@ namespace polysat {
         virtual bool perform(conflict_explainer& ce) = 0;
     };
 
-    class inf_polynomial_superposition : public inference_engine {
+    class inf_polynomial_superposition final : public inference_engine {
     public:
         bool perform(conflict_explainer& ce) override;
     };
@@ -40,14 +40,35 @@ namespace polysat {
     // clause_ref by_ugt_z();
     // clause_ref y_ule_ax_and_x_ule_z();
 
+
+    class core_saturation final {
+        scoped_ptr_vector<inference_engine> inference_engines;
+    public:
+        /// Derive new constraints from constraints containing the variable v (i.e., at least one premise must contain v)
+        bool saturate(pvar v, conflict_core& core) { NOT_IMPLEMENTED_YET(); return false; }
+    };
+
+
+
+
+
+
+
+#if 0
     class conflict_explainer {
         solver& m_solver;
 
-        conflict_core m_conflict;
+        // conflict_core m_conflict;
+        vector<constraint> m_new_assertions;  // to be inserted into Gamma (conclusions from saturation)
 
         scoped_ptr_vector<inference_engine> inference_engines;
 
         bool push_omega_mul(clause_builder& clause, unsigned level, unsigned p, pdd const& x, pdd const& y);
+
+        // Gamma
+        // search_state& search() { return m_solver.m_search; }
+        // Core
+        // conflict_core& conflict() { return m_solver.m_conflict; }
     public:
         /** Create empty conflict */
         conflict_explainer(solver& s);
@@ -58,7 +79,7 @@ namespace polysat {
         bool saturate();
 
         /** resolve conflict state against assignment to v */
-        void resolve(pvar v, ptr_vector<constraint> const& cjust_v);
+        void resolve(pvar v, ptr_vector<constraint> const& cjust_v);  // TODO: try variable elimination of 'v', if not possible, core saturation and core reduction. (actually reduction could be one specific VE method).
         void resolve(sat::literal lit);
 
         // TODO: move conflict resolution from solver into this class.
@@ -68,4 +89,5 @@ namespace polysat {
         /** conflict resolution until first (relevant) decision */
         void resolve();
     };
+#endif
 }

src/math/polysat/solver.cpp

@@ -20,6 +20,7 @@ Author:
 #include "math/polysat/explain.h"
 #include "math/polysat/log.h"
 #include "math/polysat/forbidden_intervals.h"
+#include "math/polysat/variable_elimination.h"
 
 // For development; to be removed once the linear solver works well enough
 #define ENABLE_LINEAR_SOLVER 0
@@ -142,6 +143,7 @@ namespace polysat {
         VERIFY(at_base_level());
         SASSERT(c);
         SASSERT(activate || dep != null_dependency);  // if we don't activate the constraint, we need the dependency to access it again later.
+        m_constraints.ensure_bvar(c.get());
         clause* unit = m_constraints.store(clause::from_unit(c, mk_dep_ref(dep)));
         c->set_unit_clause(unit);
         if (dep != null_dependency)
@@ -399,17 +401,19 @@ namespace polysat {
     }
 
     void solver::set_conflict(pvar v) {
-        m_conflict.set(v, m_cjust[v]);
+        m_conflict.set(v);
     }
 
     void solver::set_marks(conflict_core const& cc) {
+        if (cc.conflict_var() != null_var)
+            set_mark(cc.conflict_var());
         for (auto c : cc.constraints())
             if (c)
                 set_marks(*c);
     }
 
     void solver::set_marks(constraint const& c) {
-        if (c.bvar() != sat::null_bool_var)
+        if (c.has_bvar())
             m_bvars.set_mark(c.bvar());
         for (auto v : c.vars())
             set_mark(v);
@@ -440,183 +444,110 @@ namespace polysat {
 
         SASSERT(is_conflict());
 
-        NOT_IMPLEMENTED_YET();  // TODO: needs to be refactored to use conflict_core, will be moved to conflict_explainer
-
-        /*
-        if (m_conflict.units().size() == 1 && !m_conflict.units()[0]) {
+        if (m_conflict.is_bailout()) {
             report_unsat();
             return;
         }
 
-        pvar conflict_var = null_var;
-        clause_ref lemma;
-        for (auto v : m_conflict.vars(m_constraints))
-            if (!m_viable.has_viable(v)) {
-                SASSERT(conflict_var == null_var || conflict_var == v);  // at most one variable can be empty
-                conflict_var = v;
-            }
-        reset_marks();
-        m_bvars.reset_marks();
-        set_marks(m_conflict);
-
-        if (m_conflict.clauses().empty() && conflict_var != null_var) {
-            LOG_H2("Conflict due to empty viable set for pvar " << conflict_var);
-            clause_ref new_lemma;
-            if (forbidden_intervals::explain(*this, m_conflict.units(), conflict_var, new_lemma)) {
-                SASSERT(new_lemma);
-                clause& cl = *new_lemma.get();
-                LOG_H3("Lemma from forbidden intervals (size: " << cl.size() << ")");
-                for (sat::literal lit : cl) {
-                    LOG("Literal: " << lit);
-                    constraint* c = m_constraints.lookup(lit.var());
-                    for (auto v : c->vars())
-                        set_mark(v);
-                }
-                SASSERT(cl.size() > 0);
-                lemma = std::move(new_lemma);
-                m_conflict.reset();
-                m_conflict.push_back(lemma);
-                reset_marks();
-                m_bvars.reset_marks();
-                set_marks(*lemma.get());
-            }
-            else {
-                conflict_explainer cx(*this, m_conflict);
-                lemma = cx.resolve(conflict_var, {});
-                LOG("resolved: " << show_deref(lemma));
-                // SASSERT(false && "pause on explanation");
-            }
+        if (m_conflict.conflict_var() != null_var) {
+            // This case corresponds to a propagation of conflict_var, except it's not explicitly on the stack.
+            resolve_value(m_conflict.conflict_var());
         }
 
+        reset_marks();
+        set_marks(m_conflict);
+
         for (unsigned i = m_search.size(); i-- > 0; ) {
+            LOG("Conflict: " << m_conflict);
             auto const& item = m_search[i];
             if (item.is_assignment()) {
                 // Resolve over variable assignment
                 pvar v = item.var();
-                LOG_H2("Working on pvar " << v);
+                LOG_H2("Working on pvar v" << v);
                 if (!is_marked(v))
                     continue;
                 justification& j = m_justification[v];
                 LOG("Justification: " << j);
-                if (j.level() <= base_level()) {
-                    report_unsat();
-                    return;
-                }
+                if (j.level() <= base_level())
+                    break;
                 if (j.is_decision()) {
-                    revert_decision(v, lemma);
+                    revert_decision(v);
                     return;
                 }
                 SASSERT(j.is_propagation());
-                LOG("Lemma: " << show_deref(lemma));
-                clause_ref new_lemma = resolve(v);
-                LOG("New Lemma: " << show_deref(new_lemma));
-                // SASSERT(new_lemma); // TODO: only for debugging, to have a breakpoint on resolution failure
-                if (!new_lemma) {
-                    backtrack(i, lemma);
+                if (!resolve_value(v)) {
+                    resolve_bailout(i);
                     return;
                 }
-                if (new_lemma->is_always_false(*this)) {
-                    clause* cl = new_lemma.get();
-                    learn_lemma(v, std::move(new_lemma));
-                    m_conflict.reset();
-                    m_conflict.push_back(cl);
-                    report_unsat();
-                    return;
-                }
-                if (!new_lemma->is_currently_false(*this)) {
-                    backtrack(i, lemma);
-                    return;
-                }
-                lemma = std::move(new_lemma);
                 reset_marks();
-                m_bvars.reset_marks();
-                set_marks(*lemma.get());
-                m_conflict.reset();
-                m_conflict.push_back(lemma.get());
+                set_marks(m_conflict);
             }
             else {
                 // Resolve over boolean literal
                 SASSERT(item.is_boolean());
                 sat::literal const lit = item.lit();
-                LOG_H2("Working on boolean literal " << lit);
+                LOG_H2("Working on blit " << lit);
                 sat::bool_var const var = lit.var();
                 if (!m_bvars.is_marked(var))
                     continue;
-                if (m_bvars.level(var) <= base_level()) {
-                    report_unsat();
-                    return;
-                }
+                if (m_bvars.level(var) <= base_level())
+                    break;
                 if (m_bvars.is_decision(var)) {
-                    // SASSERT(std::count(lemma->begin(), lemma->end(), ~lit) > 0);
-                    revert_bool_decision(lit, lemma);
+                    revert_bool_decision(lit);
                     return;
                 }
                 SASSERT(m_bvars.is_propagation(var));
-                LOG("Lemma: " << show_deref(lemma));
-                clause_ref new_lemma = resolve_bool(lit);
-                if (!new_lemma) {
-                    backtrack(i, lemma);
-                    return;
-                }
-                SASSERT(new_lemma);
-                LOG("new_lemma: " << show_deref(new_lemma));
-                LOG("new_lemma is always false: " << new_lemma->is_always_false(*this));
-                if (new_lemma->is_always_false(*this)) {
-                    // learn_lemma(v, new_lemma);
-                    m_conflict.reset();
-                    m_conflict.push_back(std::move(new_lemma));
-                    report_unsat();
-                    return;
-                }
-                LOG("new_lemma is currently false: " << new_lemma->is_currently_false(*this));
-                // if (!new_lemma->is_currently_false(*this)) {
-                //     backtrack(i, lemma);
-                //     return;
-                // }
-                lemma = std::move(new_lemma);
+                resolve_bool(lit);
                 reset_marks();
-                m_bvars.reset_marks();
-                set_marks(*lemma.get());
-                m_conflict.reset();
-                m_conflict.push_back(lemma.get());
+                set_marks(m_conflict);
             }
         }
         report_unsat();
-        */
     }
 
-    clause_ref solver::resolve_bool(sat::literal lit) {
-        NOT_IMPLEMENTED_YET();  return nullptr;
-        /*
-        if (m_conflict.size() != 1)
-            return nullptr;
-        if (m_conflict.clauses().size() != 1)
-            return nullptr;
-        LOG_H3("resolve_bool");
-        clause* lemma = m_conflict.clauses()[0];
-        SASSERT(lemma);
-        SASSERT(m_bvars.is_propagation(lit.var()));
-        clause* other = m_bvars.reason(lit.var());
-        SASSERT(other);
-        LOG("lemma: " << show_deref(lemma));
-        LOG("other: " << show_deref(other));
-        VERIFY(lemma->resolve(lit.var(), *other));
-        LOG("resolved: " << show_deref(lemma));
+    /** Conflict resolution case where propagation 'v := ...' is on top of the stack */
+    bool solver::resolve_value(pvar v) {
+        SASSERT(m_justification[v].is_propagation());
+        // Conceptually:
+        // - Value Resolution
+        // - Variable Elimination
+        // - if VE isn't possible, try to derive new constraints using core saturation
 
-        // unassign constraints whose current value does not agree with their occurrence in the lemma
-        for (sat::literal lit : *lemma) {
-            constraint *c = m_constraints.lookup(lit.var());
-            if (!c->is_undef() && c ->blit() != lit) {
-                LOG("unassigning: " << show_deref(c));
-                c->unassign();
-            }
+        // Value Resolution
+        for (auto c : m_cjust[v])
+            m_conflict.push(c);
+
+        // Variable elimination
+        while (true) {
+            // TODO:
+            // 1. Try variable elimination of 'v'
+            // 2. If not possible, try saturation and core reduction (actually reduction could be one specific VE method?).
+            // 3. as a last resort, substitute v by m_value[v]?
+
+            variable_elimination ve;
+            if (ve.perform(v, m_conflict))
+                return true;
+
+            core_saturation cs;
+            if (!cs.saturate(v, m_conflict))
+                return false;
         }
 
-        return lemma;  // currently modified in-place
-        */
+        return false;
     }
 
-    void solver::backtrack(unsigned i, clause_ref lemma) {
+    /** Conflict resolution case where boolean literal 'lit' is on top of the stack */
+    void solver::resolve_bool(sat::literal lit) {
+        LOG_H3("resolve_bool: " << lit);
+        SASSERT(m_bvars.is_propagation(lit.var()));
+
+        clause* other = m_bvars.reason(lit.var());
+        m_conflict.resolve(m_constraints, lit.var(), *other);
+    }
+
+    void solver::resolve_bailout(unsigned i) {
+        // TODO: conflict resolution failed or was aborted. what to do with the current conflict core?
+        //      (we could still use it as lemma, but it probably doesn't help much)
         NOT_IMPLEMENTED_YET();
         /*
         do {
@@ -766,7 +697,7 @@ namespace polysat {
      * In general form it can rely on factoring.
      * Root finding can further prune viable.
      */
-    void solver::revert_decision(pvar v, clause_ref reason) {
+    void solver::revert_decision(pvar v) {
         rational val = m_value[v];
         LOG_H3("Reverting decision: pvar " << v << " := " << val);
         NOT_IMPLEMENTED_YET();
@@ -818,7 +749,7 @@ namespace polysat {
         */
     }
     
-    void solver::revert_bool_decision(sat::literal lit, clause_ref reason) {
+    void solver::revert_bool_decision(sat::literal lit) {
         sat::bool_var const var = lit.var();
         LOG_H3("Reverting boolean decision: " << lit);
         SASSERT(m_bvars.is_decision(var));
@@ -1010,6 +941,7 @@ namespace polysat {
     }
     
     void solver::reset_marks() {
+        m_bvars.reset_marks();
         LOG_V("-------------------------- (reset variable marks)");
         m_marks.reserve(m_vars.size());
         m_clock++;

src/math/polysat/solver.h

@@ -53,6 +53,7 @@ namespace polysat {
         friend class ule_constraint;
         friend class clause;
         friend class clause_builder;
+        friend class conflict_core;
         friend class conflict_explainer;
         friend class forbidden_intervals;
         friend class linear_solver;
@@ -191,8 +192,6 @@ namespace polysat {
 
         unsigned                 m_conflict_level { 0 };
 
-        clause_ref resolve_bool(sat::literal lit);
-
         bool can_decide() const { return !m_free_vars.empty(); }
         void decide();
         void decide(pvar v);
@@ -211,10 +210,13 @@ namespace polysat {
         unsigned base_level() const;
 
         void resolve_conflict();
-        void backtrack(unsigned i, clause_ref lemma);
+        bool resolve_value(pvar v);
+        void resolve_bool(sat::literal lit);
+        void resolve_bailout(unsigned i);
+        void revert_decision(pvar v);
+        void revert_bool_decision(sat::literal lit);
+
         void report_unsat();
-        void revert_decision(pvar v, clause_ref reason);
-        void revert_bool_decision(sat::literal lit, clause_ref reason);
         void learn_lemma(pvar v, clause_ref lemma);
         void backjump(unsigned new_level);
         void add_lemma(clause_ref lemma);

src/math/polysat/types.h

@@ -14,6 +14,7 @@ Author:
 #include "util/dependency.h"
 #include "util/trail.h"
 #include "util/lbool.h"
+#include "util/map.h"
 #include "util/rlimit.h"
 #include "util/scoped_ptr_vector.h"
 #include "util/var_queue.h"

src/math/polysat/ule_constraint.h

@@ -18,9 +18,11 @@ Author:
 namespace polysat {
 
     class ule_constraint final : public constraint {
+        friend class constraint_manager;
+
         pdd m_lhs;
         pdd m_rhs;
-    public:
+
         ule_constraint(constraint_manager& m, unsigned lvl, pdd const& l, pdd const& r):
             constraint(m, lvl, ckind_t::ule_t), m_lhs(l), m_rhs(r) {
             m_vars.append(l.free_vars());
@@ -28,6 +30,8 @@ namespace polysat {
                 if (!m_vars.contains(v))
                     m_vars.push_back(v);
         }
+
+    public:
         ~ule_constraint() override {}
         pdd const& lhs() const { return m_lhs; }
         pdd const& rhs() const { return m_rhs; }

src/math/polysat/variable_elimination.cpp

@@ -0,0 +1,19 @@
+/*++
+Copyright (c) 2021 Microsoft Corporation
+
+Module Name:
+
+    Polysat variable elimination
+
+Author:
+
+    Nikolaj Bjorner (nbjorner) 2021-03-19
+    Jakob Rath 2021-04-6
+
+--*/
+#include "math/polysat/variable_elimination.h"
+
+namespace polysat {
+
+
+}

src/math/polysat/variable_elimination.h

@@ -0,0 +1,52 @@
+/*++
+Copyright (c) 2021 Microsoft Corporation
+
+Module Name:
+
+    Polysat variable elimination
+
+Author:
+
+    Nikolaj Bjorner (nbjorner) 2021-03-19
+    Jakob Rath 2021-04-6
+
+--*/
+#pragma once
+#include "math/polysat/conflict_core.h"
+
+namespace polysat {
+
+    class variable_elimination_engine {
+    public:
+        virtual ~variable_elimination_engine() {}
+        virtual bool perform(pvar v, conflict_core& core) = 0;
+    };
+
+    // discovers when a variable has already been removed... (special case of ve_reduction?)
+    class ve_trivial final : public variable_elimination_engine {
+    public:
+        bool perform(pvar v, conflict_core& core) override { NOT_IMPLEMENTED_YET(); return false; }
+    };
+
+    // ve by core reduction: try core reduction on all constraints that contain the variable to be eliminated.
+    // if we cannot eliminate all such constraints, then should we keep all of them instead of eliminating only some? since they might still be useful for saturation.
+    class ve_reduction final : public variable_elimination_engine {
+    public:
+        bool perform(pvar v, conflict_core& core) override { NOT_IMPLEMENTED_YET(); return false; }
+    };
+
+    class ve_forbidden_intervals final : public variable_elimination_engine {
+    public:
+        bool perform(pvar v, conflict_core& core) override { NOT_IMPLEMENTED_YET(); return false; }
+    };
+
+    class variable_elimination final {
+        scoped_ptr_vector<variable_elimination_engine> ve_engines;
+
+    public:
+        variable_elimination() {}
+
+        /// Try to eliminate the variable v from the given core
+        bool perform(pvar v, conflict_core& core) { NOT_IMPLEMENTED_YET(); return false; }
+    };
+}