Polysat: conflict explanation prototype (#5353)

* display constraint's extra info in one place

* Add stub for conflict explainer

* Add helper functions to check whether constraint is active at base level

* Add helper class tmp_assign

* Add clause_builder; it skips unnecessary literals during clause creation

* some fixes

* Use clause_builder for forbidden intervals

* remove old comments

* fixes/comments in solver

* print redundant clauses

* First pass at conflict_explainer

* remove unused model class

* Choose value for k

* also print min/max k

src/math/polysat/CMakeLists.txt

@@ -3,6 +3,7 @@ z3_add_component(polysat
     boolean.cpp
     constraint.cpp
     eq_constraint.cpp
+    explain.cpp
     forbidden_intervals.cpp
     justification.cpp
     linear_solver.cpp

src/math/polysat/constraint.cpp

@@ -154,6 +154,13 @@ namespace polysat {
         return ult(lvl, sign, a + shift, b + shift, d);
     }
 
+    std::ostream& constraint::display_extra(std::ostream& out) const {
+        out << " @" << level() << " (b" << bvar() << ")";
+        if (is_undef())
+            out << " [inactive]";
+        return out;
+    }
+
     bool constraint::propagate(solver& s, pvar v) {
         LOG_H3("Propagate " << s.m_vars[v] << " in " << *this);
         SASSERT(!vars().empty());
@@ -194,12 +201,13 @@ namespace polysat {
     }
 
     clause_ref clause::from_literals(unsigned lvl, p_dependency_ref const& d, sat::literal_vector literals, constraint_ref_vector constraints) {
-        return alloc(clause, lvl, d, literals, constraints);
+        return alloc(clause, lvl, d, std::move(literals), std::move(constraints));
     }
 
     bool clause::is_always_false(solver& s) const {
         return std::all_of(m_literals.begin(), m_literals.end(), [&s](sat::literal lit) {
             constraint *c = s.m_constraints.lookup(lit.var());
+            tmp_assign _t(c, lit);
             return c->is_always_false();
         });
     }
@@ -207,6 +215,7 @@ namespace polysat {
     bool clause::is_currently_false(solver& s) const {
         return std::all_of(m_literals.begin(), m_literals.end(), [&s](sat::literal lit) {
             constraint *c = s.m_constraints.lookup(lit.var());
+            tmp_assign _t(c, lit);
             return c->is_currently_false(s);
         });
     }
@@ -247,6 +256,35 @@ namespace polysat {
         return out;
     }
 
+    void clause_builder::reset() {
+        m_literals.reset();
+        m_new_constraints.reset();
+        SASSERT(empty());
+    }
+
+    clause_ref clause_builder::build(unsigned lvl, p_dependency_ref const& d) {
+        clause_ref cl = clause::from_literals(lvl, d, std::move(m_literals), std::move(m_new_constraints));
+        SASSERT(empty());
+        return cl;
+    }
+
+    void clause_builder::push_literal(sat::literal lit) {
+        if (m_solver.active_at_base_level(lit))
+            return;
+        m_literals.push_back(lit);
+    }
+
+    void clause_builder::push_new_constraint(constraint_ref c) {
+        SASSERT(c);
+        SASSERT(c->is_undef());
+        sat::literal lit{c->bvar()};
+        tmp_assign _t(c, lit);
+        if (c->is_always_false())
+            return;
+        m_literals.push_back(lit);
+        m_new_constraints.push_back(std::move(c));
+    }
+
     std::ostream& constraints_and_clauses::display(std::ostream& out) const {
         bool first = true;
         for (auto c : units()) {

src/math/polysat/constraint.h

@@ -93,7 +93,7 @@ namespace polysat {
         unsigned         m_ref_count = 0;
         // bool             m_stored = false;  ///< Whether it has been inserted into the constraint_manager to be tracked by level
         unsigned         m_storage_level;  ///< Controls lifetime of the constraint object. Always a base level (for external dependencies the level at which it was created, and for others the maximum storage level of its external dependencies).
-        unsigned         m_active_level = UINT_MAX;  ///< Level at which the constraint was activated. Possibly different from m_storage_level because constraints in lemmas may become activated only at a higher level.
+        // unsigned         m_active_level = UINT_MAX;  ///< Level at which the constraint was activated. Possibly different from m_storage_level because constraints in lemmas may become activated only at a higher level. NOTE: this is actually the level of the corresponding bool_var.
         ckind_t          m_kind;
         p_dependency_ref m_dep;
         unsigned_vector  m_vars;
@@ -108,6 +108,9 @@ namespace polysat {
             m_manager->insert_bv2c(bvar(), this);
         }
 
+    protected:
+        std::ostream& display_extra(std::ostream& out) const;
+
     public:
         void inc_ref() { m_ref_count++; }
         void dec_ref() { SASSERT(m_ref_count > 0); m_ref_count--; if (!m_ref_count) dealloc(this); }
@@ -138,6 +141,13 @@ namespace polysat {
         unsigned_vector& vars() { return m_vars; }
         unsigned_vector const& vars() const { return m_vars; }
         unsigned level() const { return m_storage_level; }
+        // unsigned active_level() const {
+        //     SASSERT(!is_undef());
+        //     return m_manager->m_bvars.level(bvar());
+        // }
+        // unsigned active_at_base_level(solver& s) const {
+        //     return !is_undef() && active_level() <= s.base_level();
+        // }
         sat::bool_var bvar() const { return m_bvar; }
         sat::literal blit() const { SASSERT(m_bvalue != l_undef); return m_bvalue == l_true ? sat::literal(m_bvar) : ~sat::literal(m_bvar); }
         bool sign() const { return m_sign; }
@@ -230,6 +240,33 @@ namespace polysat {
 
     inline std::ostream& operator<<(std::ostream& out, clause const& c) { return c.display(out); }
 
+    /// Builds a clause from literals and constraints.
+    /// Takes care to
+    /// - skip literals that are active at the base level,
+    /// - skip trivial new constraints such as "4 <= 1".
+    class clause_builder {
+        solver& m_solver;
+        sat::literal_vector m_literals;
+        constraint_ref_vector m_new_constraints;
+
+    public:
+        clause_builder(solver& s): m_solver(s) {}
+
+        bool empty() const { return m_literals.empty() && m_new_constraints.empty(); }
+        void reset();
+
+        /// Build the clause. This will reset the clause builder so it can be reused.
+        clause_ref build(unsigned lvl, p_dependency_ref const& d);
+
+        /// Add a literal to the clause.
+        /// Intended to be used for literals representing a constraint that already exists.
+        void push_literal(sat::literal lit);
+        /// Add a constraint to the clause that does not yet exist in the solver so far.
+        /// By convention, this will add the positive literal for this constraint.
+        /// (TODO: we might need to change this later; but then we will add a second argument for the literal or the sign.)
+        void push_new_constraint(constraint_ref c);
+    };
+
     // Container for unit constraints and clauses.
     class constraints_and_clauses {
         constraint_ref_vector m_units;
@@ -289,4 +326,37 @@ namespace polysat {
 
     inline std::ostream& operator<<(std::ostream& out, constraints_and_clauses const& c) { return c.display(out); }
 
+
+    /// Temporarily assign a constraint according to the sign of the given literal.
+    class tmp_assign final {
+        constraint* m_constraint;
+        bool m_should_unassign = false;
+    public:
+        tmp_assign(constraint* c, sat::literal lit):
+            m_constraint(c) {
+            SASSERT(c);
+            SASSERT(c->bvar() == lit.var());
+            if (c->is_undef()) {
+                c->assign(!lit.sign());
+                m_should_unassign = true;
+            }
+            else
+                SASSERT(c->blit() == lit);
+        }
+        tmp_assign(constraint_ref const& c, sat::literal lit): tmp_assign(c.get(), lit) {}
+        void revert() {
+            if (m_should_unassign) {
+                m_constraint->unassign();
+                m_should_unassign = false;
+            }
+        }
+        ~tmp_assign() {
+            revert();
+        }
+        tmp_assign(tmp_assign&) = delete;
+        tmp_assign(tmp_assign&&) = delete;
+        tmp_assign& operator=(tmp_assign&) = delete;
+        tmp_assign& operator=(tmp_assign&&) = delete;
+    };
+
 }

src/math/polysat/eq_constraint.cpp

@@ -19,10 +19,8 @@ Author:
 namespace polysat {
 
     std::ostream& eq_constraint::display(std::ostream& out) const {
-        out << p() << (sign() == pos_t ? " == 0" : " != 0") << " @" << level() << " b" << bvar();
-        if (is_undef())
-            out << " [inactive]";
-        return out;
+        out << p() << (sign() == pos_t ? " == 0" : " != 0");
+        return display_extra(out);
     }
 
     constraint_ref eq_constraint::resolve(solver& s, pvar v) {

src/math/polysat/explain.cpp

@@ -0,0 +1,186 @@
+/*++
+Copyright (c) 2021 Microsoft Corporation
+
+Module Name:
+
+    Conflict explanation / resolution
+
+Author:
+
+    Nikolaj Bjorner (nbjorner) 2021-03-19
+    Jakob Rath 2021-04-6
+
+--*/
+#include "math/polysat/explain.h"
+#include "math/polysat/log.h"
+
+namespace polysat {
+
+    conflict_explainer::conflict_explainer(solver& s, constraints_and_clauses const& conflict):
+        m_solver(s), m_conflict(conflict) {}
+
+    clause_ref conflict_explainer::resolve(pvar v, ptr_vector<constraint> const& cjust) {
+        LOG_H3("Attempting to explain conflict for v" << v);
+        m_var = v;
+        m_cjust_v = cjust;
+
+        for (auto* c : cjust)
+            m_conflict.push_back(c);
+
+        // TODO: we should share work done for examining constraints between different resolution methods
+        clause_ref lemma;
+        if (!lemma) lemma = by_polynomial_superposition();
+        if (!lemma) lemma = by_ugt_x();
+        if (!lemma) lemma = by_ugt_y();
+        if (!lemma) lemma = by_ugt_z();
+
+        if (lemma) {
+            LOG("New lemma: " << *lemma);
+            for (auto* c : lemma->new_constraints()) {
+                LOG("New constraint: " << show_deref(c));
+            }
+        }
+
+        m_var = null_var;
+        m_cjust_v.reset();
+        return lemma;
+    }
+
+    clause_ref conflict_explainer::by_polynomial_superposition() {
+        if (m_conflict.units().size() != 2 || m_conflict.clauses().size() > 0)
+            return nullptr;
+        constraint* c1 = m_conflict.units()[0];
+        constraint* c2 = m_conflict.units()[1];
+        if (c1 == c2)
+            return nullptr;
+        if (!c1->is_eq() || !c2->is_eq())
+            return nullptr;
+        if (c1->is_positive() && c2->is_positive()) {
+            pdd a = c1->to_eq().p();
+            pdd b = c2->to_eq().p();
+            pdd r = a;
+            if (!a.resolve(m_var, b, r) && !b.resolve(m_var, a, r))
+                return nullptr;
+            p_dependency_ref d(m_solver.m_dm.mk_join(c1->dep(), c2->dep()), m_solver.m_dm);
+            unsigned lvl = std::max(c1->level(), c2->level());
+            constraint_ref c = m_solver.m_constraints.eq(lvl, pos_t, r, d);
+            c->assign(true);
+            return clause::from_unit(c);
+        }
+        return nullptr;
+    }
+
+    /// [x] zx > yx  ==>  ...
+    clause_ref conflict_explainer::by_ugt_x() {
+        LOG_H3("Try zx > yx");
+        for (auto* c : m_conflict.units())
+            LOG("Constraint: " << show_deref(c));
+        for (auto* c : m_conflict.clauses())
+            LOG("Clause: " << show_deref(c));
+
+        // Find constraint of desired shape
+        for (auto* c : m_conflict.units()) {
+            if (!c->is_ule())
+                continue;
+            pdd lhs = c->to_ule().lhs();
+            pdd rhs = c->to_ule().rhs();
+            if (lhs.degree(m_var) != 1)
+                continue;
+            if (rhs.degree(m_var) != 1)
+                continue;
+            pdd y = lhs;
+            pdd rest = lhs;
+            rhs.factor(m_var, 1, y, rest);
+            if (!rest.is_zero())
+                continue;
+            pdd z = lhs;
+            lhs.factor(m_var, 1, z, rest);
+            if (!rest.is_zero())
+                continue;
+
+            if (c->is_positive()) {
+                // zx <= yx
+                NOT_IMPLEMENTED_YET();
+            }
+            else {
+                SASSERT(c->is_negative());
+                // zx > yx
+
+                unsigned const lvl = c->level();
+
+                pdd x = m_solver.var(m_var);
+                unsigned const p = m_solver.size(m_var);
+
+                clause_builder clause(m_solver);
+                // Omega^*(x, y)
+                push_omega_mul(clause, lvl, p, x, y);
+                // z > y
+                constraint_ref z_gt_y = m_solver.m_constraints.ult(lvl, pos_t, y, z, null_dep());
+                LOG("z>y: " << show_deref(z_gt_y));
+                clause.push_new_constraint(std::move(z_gt_y));
+
+                p_dependency_ref d(c->dep(), m_solver.m_dm);
+                return clause.build(lvl, d);
+            }
+
+        }
+        return nullptr;
+    }
+
+    /// [y] y >= z' /\ zx > yx  ==>  ...
+    clause_ref conflict_explainer::by_ugt_y() {
+        return nullptr;
+    }
+
+    /// [z] y' >= z /\ zx > yx  ==>  ...
+    clause_ref conflict_explainer::by_ugt_z() {
+        return nullptr;
+    }
+
+    /// Add Ω*(x, y) to the clause.
+    ///
+    /// @param[in] p    bit width
+    void conflict_explainer::push_omega_mul(clause_builder& clause, unsigned level, unsigned p, pdd const& x, pdd const& y) {
+        LOG_H3("Omega^*(x, y)");
+        LOG("x = " << x);
+        LOG("y = " << y);
+        auto& pddm = m_solver.sz2pdd(p);
+        unsigned min_k = 0;
+        unsigned max_k = p - 1;
+        unsigned k = p/2;
+
+        rational x_val;
+        if (m_solver.try_eval(x, x_val)) {
+            unsigned x_bits = x_val.bitsize();
+            LOG("eval x: " << x << " := " << x_val << " (x_bits: " << x_bits << ")");
+            SASSERT(x_val < rational::power_of_two(x_bits));
+            min_k = x_bits;
+        }
+
+        rational y_val;
+        if (m_solver.try_eval(y, y_val)) {
+            unsigned y_bits = y_val.bitsize();
+            LOG("eval y: " << y << " := " << y_val << " (y_bits: " << y_bits << ")");
+            SASSERT(y_val < rational::power_of_two(y_bits));
+            max_k = p - y_bits;
+        }
+
+        SASSERT(min_k <= max_k);  // in this case, cannot choose k s.t. both literals are false
+
+        // TODO: could also choose other value for k (but between the bounds)
+        if (min_k == 0)
+            k = max_k;
+        else
+            k = min_k;
+
+        LOG("k = " << k << "; min_k = " << min_k << "; max_k = " << max_k << "; p = " << p);
+        SASSERT(min_k <= k && k <= max_k);
+
+        // x >= 2^k
+        constraint_ref c1 = m_solver.m_constraints.ult(level, pos_t, pddm.mk_val(rational::power_of_two(k)), x, null_dep());
+        // y > 2^{p-k}
+        constraint_ref c2 = m_solver.m_constraints.ule(level, pos_t, pddm.mk_val(rational::power_of_two(p-k)), y, null_dep());
+        clause.push_new_constraint(std::move(c1));
+        clause.push_new_constraint(std::move(c2));
+    }
+}

src/math/polysat/explain.h

@@ -0,0 +1,43 @@
+/*++
+Copyright (c) 2021 Microsoft Corporation
+
+Module Name:
+
+    Conflict explanation / resolution
+
+Author:
+
+    Nikolaj Bjorner (nbjorner) 2021-03-19
+    Jakob Rath 2021-04-6
+
+--*/
+#pragma once
+#include "math/polysat/constraint.h"
+#include "math/polysat/interval.h"
+#include "math/polysat/solver.h"
+
+namespace polysat {
+
+    // TODO: later, we probably want to update this class incrementally (adding/removing constraints as we go back through the trail)
+    // TODO: indexing of constraints/clauses?
+    class conflict_explainer {
+        solver& m_solver;
+        constraints_and_clauses m_conflict;
+        pvar m_var = null_var;
+        ptr_vector<constraint> m_cjust_v;
+
+
+        clause_ref by_polynomial_superposition();
+
+        clause_ref by_ugt_x();
+        clause_ref by_ugt_y();
+        clause_ref by_ugt_z();
+
+        p_dependency_ref null_dep() const { return m_solver.mk_dep_ref(null_dependency); }
+        void push_omega_mul(clause_builder& clause, unsigned level, unsigned p, pdd const& x, pdd const& y);
+    public:
+        conflict_explainer(solver& s, constraints_and_clauses const& conflict);
+
+        clause_ref resolve(pvar v, ptr_vector<constraint> const& cjust_v);
+    };
+}

src/math/polysat/forbidden_intervals.cpp

@@ -99,21 +99,20 @@ namespace polysat {
             // => the side conditions of that interval are enough to produce a conflict
             auto& full_record = records.back();
             SASSERT(full_record.interval.is_full());
-            sat::literal_vector literals;
-            constraint_ref_vector new_constraints;
-            literals.push_back(~full_record.src->blit());  // TODO: only do this if it's not a base-level constraint! (from unit clauses, e.g., external constraints)
-            if (full_record.neg_cond) {
-                literals.push_back(sat::literal(full_record.neg_cond.get()->bvar()));
-                new_constraints.push_back(std::move(full_record.neg_cond));
-            }
+            clause_builder clause(s);
+            clause.push_literal(~full_record.src->blit());
+            if (full_record.neg_cond)
+                clause.push_new_constraint(std::move(full_record.neg_cond));
             unsigned lemma_lvl = full_record.src->level();
             p_dependency_ref lemma_dep(full_record.src->dep(), s.m_dm);
-            out_lemma = clause::from_literals(lemma_lvl, lemma_dep, std::move(literals), std::move(new_constraints));
+            out_lemma = clause.build(lemma_lvl, lemma_dep);
             return true;
         }
 
-        if (records.empty())
+        if (records.empty()) {
+            LOG("aborted (no intervals)");
             return false;
+        }
 
         SASSERT(longest_i != UINT_MAX);
         LOG("longest: i=" << longest_i << "; " << records[longest_i].interval);
@@ -123,6 +122,7 @@ namespace polysat {
         // Select a sequence of covering intervals
         unsigned_vector seq;
         if (!find_covering_sequence(records, longest_i, modulus, seq)) {
+            LOG("aborted (intervals do not cover domain)");
             return false;
         }
         LOG("seq: " << seq);
@@ -145,14 +145,11 @@ namespace polysat {
         // then the forbidden intervals cover the whole domain and we have a conflict.
         // We learn the negation of this conjunction.
 
-        sat::literal_vector literals;
-        constraint_ref_vector new_constraints;
+        clause_builder clause(s);
         // Add negation of src constraints as antecedents (may be resolved during backtracking)
         for (unsigned const i : seq) {
-            // TODO: don't add base-level constraints! (from unit clauses, e.g., external constraints)
-            //       (maybe extract that into a helper function on 'clause'... it could sort out base-level and other constraints; add the first to lemma_dep and the other to antecedents)
             sat::literal src_lit = records[i].src->blit();
-            literals.push_back(~src_lit);
+            clause.push_literal(~src_lit);
         }
         // Add side conditions and interval constraints
         for (unsigned seq_i = seq.size(); seq_i-- > 0; ) {
@@ -167,17 +164,14 @@ namespace polysat {
             auto const& rhs = next_hi - next_lo;
             constraint_ref c = s.m_constraints.ult(lemma_lvl, neg_t, lhs, rhs, s.mk_dep_ref(null_dependency));
             LOG("constraint: " << *c);
-            literals.push_back(sat::literal(c->bvar()));
-            new_constraints.push_back(std::move(c));
+            clause.push_new_constraint(std::move(c));
             // Side conditions
             // TODO: check whether the condition is subsumed by c?  maybe at the end do a "lemma reduction" step, to try and reduce branching?
             constraint_ref& neg_cond = records[i].neg_cond;
-            if (neg_cond) {
-                literals.push_back(sat::literal(neg_cond->bvar()));
-                new_constraints.push_back(std::move(neg_cond));
-            }
+            if (neg_cond)
+                clause.push_new_constraint(std::move(neg_cond));
         }
-        out_lemma = clause::from_literals(lemma_lvl, lemma_dep, std::move(literals), std::move(new_constraints));
+        out_lemma = clause.build(lemma_lvl, lemma_dep);
         return true;
     }
 

src/math/polysat/solver.cpp

@@ -17,6 +17,7 @@ Author:
 --*/
 
 #include "math/polysat/solver.h"
+#include "math/polysat/explain.h"
 #include "math/polysat/log.h"
 #include "math/polysat/forbidden_intervals.h"
 
@@ -550,6 +551,13 @@ namespace polysat {
                 m_bvars.reset_marks();
                 set_marks(*lemma.get());
             }
+            else {
+                // lemma = resolve(conflict_var);
+                conflict_explainer cx(*this, m_conflict);
+                lemma = cx.resolve(conflict_var, {});
+                LOG("resolved: " << show_deref(lemma));
+                // std::abort();
+            }
         }
 
         for (unsigned i = m_search.size(); i-- > 0; ) {
@@ -615,6 +623,8 @@ namespace polysat {
                 SASSERT(m_bvars.is_propagation(var));
                 clause_ref new_lemma = resolve_bool(lit);
                 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();
@@ -622,10 +632,11 @@ namespace polysat {
                     report_unsat();
                     return;
                 }
-                if (!new_lemma->is_currently_false(*this)) {
-                    backtrack(i, lemma);
-                    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);
                 reset_marks();
                 m_bvars.reset_marks();
@@ -642,12 +653,26 @@ namespace polysat {
             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));
+
+        // 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();
+            }
+        }
+
         return lemma;  // currently modified in-place
     }
 
@@ -764,17 +789,14 @@ namespace polysat {
         IF_LOGGING(log_viable());
         LOG("Boolean assignment: " << m_bvars);
 
+        // To make a guess, we need to find an unassigned literal that is not false in the current model.
         auto is_suitable = [this](sat::literal lit) -> bool {
             if (m_bvars.value(lit) == l_false)  // already assigned => cannot decide on this (comes from either lemma LHS or previously decided literals that are now changed to propagation)
                 return false;
             SASSERT(m_bvars.value(lit) != l_true);  // cannot happen in a valid lemma
             constraint* c = m_constraints.lookup(lit.var());
-            c->assign(!lit.sign());
-            bool result = true;
-            if (c->is_currently_false(*this))
-                result = false;
-            c->unassign();
-            return result;
+            tmp_assign _t(c, lit);
+            return !c->is_currently_false(*this);
         };
 
         // constraint *choice = nullptr;
@@ -782,19 +804,15 @@ namespace polysat {
         unsigned num_choices = 0;  // TODO: should probably cache this?
 
         for (sat::literal lit : lemma) {
-            IF_LOGGING({
-                auto value = m_bvars.value(lit);
-                auto c = m_constraints.lookup(lit.var());
-                bool is_false;
-                if (value == l_undef) {
-                    c->assign(!lit.sign());
-                    is_false = c->is_currently_false(*this);
-                    c->unassign();
-                }
-                else
-                    is_false = c->is_currently_false(*this);
-                LOG_V("Checking: lit=" << lit << ", value=" << value << ", constraint=" << show_deref(c) << ", currently_false=" << is_false);
-            });
+            // IF_LOGGING({
+            //     auto value = m_bvars.value(lit);
+            //     auto c = m_constraints.lookup(lit.var());
+            //     bool is_false;
+            //     LOG_V("Checking: lit=" << lit << ", value=" << value << ", constraint=" << show_deref(c));
+            //     tmp_assign _t(c, lit);
+            //     is_false = c->is_currently_false(*this);
+            //     LOG_V("Checking: lit=" << lit << ", value=" << value << ", constraint=" << show_deref(c) << ", currently_false=" << is_false);
+            // });
             if (is_suitable(lit)) {
                 num_choices++;
                 if (choice == sat::null_literal)
@@ -886,7 +904,9 @@ namespace polysat {
             //       - Guess x = 0.
             //       - We have a conflict but we don't know. It will be discovered when y and z are assigned,
             //         and then may lead to an assertion failure through this call to narrow.
-            c->narrow(*this);
+            // TODO: what to do with "unassigned" constraints at this point? (we probably should have resolved those away, even in the 'backtrack' case.)
+            if (!c->is_undef())  // TODO: this check to be removed once this is fixed properly.
+                c->narrow(*this);
             if (is_conflict()) {
                 LOG_H1("Conflict during revert_decision/narrow!");
                 return;
@@ -1048,10 +1068,19 @@ namespace polysat {
      * Return residue of superposing p and q with respect to v.
      */
     clause_ref solver::resolve(pvar v) {
+        LOG_H3("Resolve v" << v);
         SASSERT(!m_cjust[v].empty());
         SASSERT(m_justification[v].is_propagation());
-        LOG("resolve pvar " << v);
-        if (m_cjust[v].size() != 1)
+        LOG("Conflict: " << m_conflict);
+        LOG("cjust[v" << v << "]: " << m_cjust[v]);
+
+        conflict_explainer cx(*this, m_conflict);
+        clause_ref res = cx.resolve(v, m_cjust[v]);
+        LOG("resolved: " << show_deref(res));
+        // std::abort();
+        return res;
+/*
+            if (m_cjust[v].size() != 1)
             return nullptr;
         constraint* d = m_cjust[v].back();
         constraint_ref res = d->resolve(*this, v);
@@ -1062,6 +1091,7 @@ namespace polysat {
         }
         else
             return nullptr;
+*/
     }
 
     /**
@@ -1085,7 +1115,10 @@ namespace polysat {
         if (!lemma)
             return;
         LOG("Lemma: " << show_deref(lemma));
-        SASSERT(lemma->size() > 1);
+        // SASSERT(lemma->size() > 1);
+        if (lemma->size() < 2) {
+            LOG_H1("TODO: this should be treated as unit constraint and asserted at the base level!");
+        }
         clause* cl = m_constraints.insert(lemma);
         m_redundant_clauses.push_back(cl);
     }
@@ -1132,7 +1165,18 @@ namespace polysat {
     unsigned solver::base_level() const {
         return m_base_levels.empty() ? 0 : m_base_levels.back();
     }
-        
+
+    bool solver::active_at_base_level(sat::bool_var bvar) const {
+        return m_bvars.is_assigned(bvar) && m_bvars.level(bvar) <= base_level();
+    }
+
+    bool solver::try_eval(pdd const& p, rational& out_value) const {
+        pdd r = p.subst_val(assignment());
+        if (r.is_val())
+            out_value = r.val();
+        return r.is_val();
+    }
+
     std::ostream& solver::display(std::ostream& out) const {
         for (auto p : assignment()) {
             auto v = p.first;
@@ -1146,6 +1190,14 @@ namespace polysat {
         out << "Redundant:\n";
         for (auto* c : m_redundant)
             out << "\t" << *c << "\n";
+        out << "Redundant clauses:\n";
+        for (auto* cl : m_redundant_clauses) {
+            out << "\t" << *cl << "\n";
+            for (auto lit : *cl) {
+                auto c = m_constraints.lookup(lit.var());
+                out << "\t\t" << lit.var() << ": " << *c << "\n";
+            }
+        }
         return out;
     }
 

src/math/polysat/solver.h

@@ -47,6 +47,8 @@ namespace polysat {
         friend class var_constraint;
         friend class ule_constraint;
         friend class clause;
+        friend class clause_builder;
+        friend class conflict_explainer;
         friend class forbidden_intervals;
         friend class linear_solver;
 
@@ -244,9 +246,15 @@ namespace polysat {
         p_dependency* mk_dep(unsigned dep) { return dep == null_dependency ? nullptr : m_dm.mk_leaf(dep); }
         p_dependency_ref mk_dep_ref(unsigned dep) { return p_dependency_ref(mk_dep(dep), m_dm); }
 
+        /// Evaluate term under the current assignment.
+        bool try_eval(pdd const& p, rational& out_value) const;
+
         bool is_conflict() const { return !m_conflict.empty(); }
         bool at_base_level() const;
         unsigned base_level() const;
+        bool active_at_base_level(sat::bool_var bvar) const;
+        bool active_at_base_level(sat::literal lit) const { return active_at_base_level(lit.var()); }
+        bool active_at_base_level(constraint& c) const { return active_at_base_level(c.bvar()); }
 
         void resolve_conflict();
         void backtrack(unsigned i, clause_ref lemma);

src/math/polysat/ule_constraint.cpp

@@ -19,10 +19,8 @@ Author:
 namespace polysat {
 
     std::ostream& ule_constraint::display(std::ostream& out) const {
-        out << m_lhs << (sign() == pos_t ? " <=u " : " >u ") << m_rhs << " @" << level() << " b" << bvar();
-        if (is_undef())
-            out << " [inactive]";
-        return out;
+        out << m_lhs << (sign() == pos_t ? " <= " : " > ") << m_rhs;
+        return display_extra(out);
     }
 
     constraint_ref ule_constraint::resolve(solver& s, pvar v) {

src/math/polysat/var_constraint.cpp

@@ -18,7 +18,8 @@ Author:
 namespace polysat {
 
     std::ostream& var_constraint::display(std::ostream& out) const {
-        return out << "v" << m_var << ": " << m_viable << "\n";
+        out << "v" << m_var << ": " << m_viable << "\n";
+        return display_extra(out);
     }
 
     constraint_ref var_constraint::resolve(solver& s, pvar v) {