repropagate outside pop_levels

src/math/polysat/solver.cpp

@@ -80,6 +80,7 @@ namespace polysat {
             SASSERT(var_queue_invariant());
             if (is_conflict() && at_base_level()) { LOG_H2("UNSAT"); return l_false; }
             else if (is_conflict()) resolve_conflict();
+            else if (can_repropagate()) repropagate();
             else if (should_add_pwatch()) add_pwatch();
             else if (can_propagate()) propagate();
             else if (!can_decide()) { LOG_H2("SAT"); VERIFY(verify_sat()); return l_true; }
@@ -216,6 +217,38 @@ namespace polysat {
         SASSERT(eval_invariant());
     }
 
+    bool solver::can_repropagate() {
+        return !m_repropagate_units.empty() || !m_repropagate_lits.empty();
+    }
+
+    void solver::repropagate() {
+        while (!m_repropagate_units.empty() && !is_conflict()) {
+            clause& cl = *m_repropagate_units.back();
+            m_repropagate_units.pop_back();
+            VERIFY_EQ(cl.size(), 1);
+            sat::literal lit = cl[0];
+            switch (m_bvars.value(lit)) {
+            case l_undef:
+                assign_propagate(lit, cl);
+                break;
+            case l_false:
+                set_conflict(cl);
+                break;
+            case l_true:
+                /* ok */
+                break;
+            default:
+                UNREACHABLE();
+                break;
+            }
+        }
+        while (!m_repropagate_lits.empty() && !is_conflict()) {
+            sat::literal lit = m_repropagate_lits.back();
+            m_repropagate_lits.pop_back();
+            repropagate(lit);
+        }
+    }
+
     /**
      * Propagate assignment to a Boolean variable
      */
@@ -239,6 +272,7 @@ namespace polysat {
      * Trigger boolean watchlists for the given literal
      */
     void solver::repropagate(sat::literal lit) {
+        LOG_H2("Re-propagate " << lit_pp(*this, lit));
 #ifndef NDEBUG
         SASSERT(!m_is_propagating);
         flet<bool> save_(m_is_propagating, true);
@@ -402,6 +436,7 @@ namespace polysat {
      * Return true if a new watch was found; or false to keep the existing one.
      */
     bool solver::repropagate(sat::literal lit, clause& cl) {
+        LOG("Re-propagate " << lit << " in " << cl);
         SASSERT(m_bvars.is_undef(lit));
         SASSERT(cl.size() >= 2);
         unsigned idx = (cl[0] == lit) ? 1 : 0;
@@ -547,8 +582,6 @@ namespace polysat {
         unsigned const target_level = m_level - num_levels;
         using replay_item = std::variant<sat::literal, pvar>;
         vector<replay_item> replay;
-        sat::literal_vector repropagate_queue;
-        ptr_vector<clause> repropagate_units;
         LOG("Pop " << num_levels << " levels (lvl " << m_level << " -> " << target_level << ")");
 #if ENABLE_LINEAR_SOLVER
         m_linear_solver.pop(num_levels);
@@ -630,15 +663,15 @@ namespace polysat {
                     SASSERT(!m_bvars.is_decision(lit));
                     replay.push_back(lit);
                 } else {
-                    repropagate_queue.push_back(lit);
-                    // Unit clauses are not stored in watch lists and must be re-propagated separately.
                     clause* reason = m_bvars.reason(lit);
                     if (reason && reason->size() == 1) {
-                        verbose_stream() << "undo unit " << lit << "\n";
                         VERIFY(m_bvars.is_bool_propagation(lit));
                         VERIFY_EQ(lit, (*reason)[0]);
-                        repropagate_units.push_back(reason);
+                        // Unit clauses are not stored in watch lists and must be re-propagated separately.
+                        m_repropagate_units.push_back(reason);
                     }
+                    else
+                        m_repropagate_lits.push_back(lit);
                     m_bvars.unassign(lit);
                 }
                 m_search.pop();
@@ -661,16 +694,10 @@ namespace polysat {
         // NOTE: the same may happen if L is a propagation/evaluation/assumption, and there now exists a new clause that propagates L at an earlier level.
         // TODO: for assumptions this isn't implemented yet. But if we can bool-propagate an assumption from other literals,
         //       it means that the external dependency on the assumed literal is unnecessary and a resulting unsat core may be smaller.
-        // TODO: combine with replay, or at least make sure it can't interfere.
         // TODO: we still may miss unit clauses, if we add a unit clause after the literal was assigned by some other cause.
         //       (reason is not a unit clause, so we don't add it to repropagate_units, and it is not stored in watchlists, so repropagate(lit) will miss it as well).
         //       unit clauses learned from conflict analysis should be fine, because we backtrack to level 0 then.
-        for (clause* cl : repropagate_units) {
+
-            SASSERT_EQ(cl->size(), 1);
-            assign_propagate((*cl)[0], *cl);
-        }
-        for (sat::literal lit : repropagate_queue)
-            repropagate(lit);
         // Replay:
         // (since levels on the search stack may be out of order)
         for (unsigned j = replay.size(); j-- > 0; ) {

src/math/polysat/solver.h

@@ -190,6 +190,8 @@ namespace polysat {
 #if 0
         constraints              m_pwatch_trail;
 #endif
+        ptr_vector<clause>       m_repropagate_units;
+        sat::literal_vector      m_repropagate_lits;
 
         ptr_vector<clause const> m_lemmas;  ///< the non-asserting lemmas
         unsigned                 m_lemmas_qhead = 0;
@@ -252,6 +254,8 @@ namespace polysat {
         void erase_pwatch(pvar v, constraint* c);
         void erase_pwatch(constraint* c);
 
+        bool can_repropagate();
+        void repropagate();
         void repropagate(sat::literal lit);
         bool repropagate(sat::literal lit, clause& cl);
         void propagate_clause(clause& cl);