Narrow conflicting constraint after backjumping

src/math/polysat/conflict.cpp

@@ -148,6 +148,7 @@ namespace polysat {
             SASSERT(m_vars.empty());
             SASSERT(m_bail_vars.empty());
             SASSERT(m_lemmas.empty());
+            SASSERT(m_narrow_queue.empty());
         }
         return is_empty;
     }
@@ -159,6 +160,7 @@ namespace polysat {
         m_relevant_vars.reset();
         m_var_occurrences.reset();
         m_lemmas.reset();
+        m_narrow_queue.reset();
         m_kind = conflict_kind_t::ok;
         m_level = UINT_MAX;
         SASSERT(empty());
@@ -211,6 +213,7 @@ namespace polysat {
     void conflict::init(signed_constraint c) {
         SASSERT(empty());
         m_level = s.m_level;
+        m_narrow_queue.push_back(c.blit());  // if the conflict is only due to a missed propagation of c
         set_impl(c);
         logger().begin_conflict();
     }
@@ -535,6 +538,15 @@ namespace polysat {
         return std::move(m_lemmas);
     }
 
+    sat::literal_vector conflict::take_narrow_queue() {
+#ifndef NDEBUG
+        on_scope_exit check_empty([this]() {
+            SASSERT(m_narrow_queue.empty());
+        });
+#endif
+        return std::move(m_narrow_queue);
+    }
+
 #if 0
     void conflict::learn_side_lemmas() {
         auto needs_side_lemma = [this](sat::literal lit) -> bool {

src/math/polysat/conflict.h

@@ -111,6 +111,11 @@ namespace polysat {
         // Additional lemmas that justify new constraints generated during conflict resolution
         clause_ref_vector m_lemmas;
 
+        // Store constraints that should be narrowed after backjumping.
+        // This allows us to perform propagations that are missed by the two-watched-variables scheme,
+        // e.g., because one of the watched variables is unassigned but irrelevant (e.g., x is irrelevant in x*y if y := 0).
+        sat::literal_vector m_narrow_queue;
+
         conflict_kind_t m_kind = conflict_kind_t::ok;
 
         // Level at which the conflict was discovered
@@ -233,6 +238,9 @@ namespace polysat {
 
         clause_ref_vector const& side_lemmas() const { return m_lemmas; }
 
+        /** Move the literals to be narrowed out of the conflict */
+        sat::literal_vector take_narrow_queue();
+
         std::ostream& display(std::ostream& out) const;
     };
 

src/math/polysat/solver.cpp

@@ -869,8 +869,24 @@ namespace polysat {
         // SASSERT(lemma_invariant(lemma, old_assignment));
 #endif
         clause_ref_vector side_lemmas = m_conflict.take_side_lemmas();
+        sat::literal_vector narrow_queue = m_conflict.take_narrow_queue();
         m_conflict.reset();
         backjump(jump_level);
+        for (sat::literal lit : narrow_queue) {
+            switch (m_bvars.value(lit)) {
+            case l_true:
+                lit2cnstr(lit).narrow(*this, false);
+                break;
+            case l_false:
+                lit2cnstr(~lit).narrow(*this, false);
+                break;
+            case l_undef:
+                /* do nothing */
+                break;
+            default:
+                UNREACHABLE();
+            }
+        }
         for (auto cl : side_lemmas)
             add_clause(*cl);
         SASSERT(lemma_invariant_part2(lemma_invariant_todo));