Fix missing boolean propagation after boolean conflict

Usually in SAT solving, the conflict clause has at least two false literals at the max level (otherwise, the last literal would have been propagated at an earlier level).
But here we are adding clauses on demand; so after backtracking we may have the case that the conflict clause has exactly one undefined literal that must be propagated explicitly.

src/math/polysat/clause.h

@@ -35,6 +35,7 @@ namespace polysat {
 
         unsigned m_ref_count = 0;  // TODO: remove refcount once we confirm it's not needed anymore
         bool m_redundant = redundant_default;
+        bool m_active = false;  // clause is active iff it has been added to the solver and boolean watchlists
         sat::literal_vector m_literals;
         char const* m_name = "";
 
@@ -53,6 +54,8 @@ namespace polysat {
             SASSERT(count(m_literals, sat::null_literal) == 0);
         }
 
+        void set_active() { m_active = true; }
+
     public:
         void inc_ref() { m_ref_count++; }
         void dec_ref() { SASSERT(m_ref_count > 0); m_ref_count--; if (!m_ref_count) dealloc(this); }
@@ -77,6 +80,8 @@ namespace polysat {
         void set_redundant(bool r) { m_redundant = r; }
         bool is_redundant() const { return m_redundant; }
 
+        bool is_active() const { return m_active; }
+
         void set_name(char const* name) { m_name = name; }
         char const* name() const { return m_name; }
     };

src/math/polysat/conflict.cpp

@@ -216,7 +216,7 @@ namespace polysat {
         logger().begin_conflict();
     }
 
-    void conflict::init(clause const& cl) {
+    void conflict::init(clause& cl) {
         LOG("Conflict: clause " << cl);
         SASSERT(empty());
         m_level = s.m_level;
@@ -225,6 +225,14 @@ namespace polysat {
             SASSERT_EQ(c.bvalue(s), l_false);
             insert(~c);
         }
+
+        // NOTE: usually in SAT solving, the conflict clause has at least two false literals at the max level.
+        //       (otherwise, the last literal would have been propagated at an earlier level.)
+        //       This is not true if we add clauses on demand;
+        //       after backtracking we may have the case that the conflict clause has
+        //       exactly one undefined literal that must be propagated explicitly.
+        m_lemmas.push_back(&cl);
+
         SASSERT(!empty());
         logger().begin_conflict();
     }
@@ -330,6 +338,10 @@ namespace polysat {
         // TODO: pass to inference_logger (with name)
    }
 
+    void conflict::restore_lemma(clause_ref lemma) {
+        m_lemmas.push_back(std::move(lemma));
+    }
+
     void conflict::remove(signed_constraint c) {
         SASSERT(contains(c));
         m_literals.remove(c.blit().index());

src/math/polysat/conflict.h

@@ -131,7 +131,7 @@ namespace polysat {
         /** conflict because the constraint c is false under current variable assignment */
         void init(signed_constraint c);
         /** boolean conflict with the given clause */
-        void init(clause const& cl);
+        void init(clause& cl);
         /** conflict because there is no viable value for the variable v, by interval reasoning */
         void init_by_viable_interval(pvar v);
         /** conflict because there is no viable value for the variable v, by fallback solver */
@@ -157,11 +157,14 @@ namespace polysat {
         /** Evaluate constraint under assignment and insert it into conflict state. */
         void insert_eval(signed_constraint c);
 
-        /** Add a side lemma to the conflict; to be learned in addition to the main lemma after conflict resolution finishes. */
+        /** Add a lemma to the conflict, to be added after conflict resolution */
         void add_lemma(char const* name, std::initializer_list<signed_constraint> cs);
         void add_lemma(char const* name, signed_constraint const* cs, size_t cs_len);
         void add_lemma(char const* name, clause_ref lemma);
 
+        /** Re-add a lemma to the conflict that we were unable to add after the previous conflict. */
+        void restore_lemma(clause_ref lemma);
+
         /** Remove c from core */
         void remove(signed_constraint c);
         void remove_var(pvar v);

src/math/polysat/constraint_manager.cpp

@@ -69,9 +69,11 @@ namespace polysat {
         m_clauses[clause_level].push_back(cl);
     }
 
-    void constraint_manager::store(clause* cl, bool value_propagate) {
+    void constraint_manager::store(clause* cl) {
+        VERIFY(!cl->is_active());
         register_clause(cl);
-        watch(*cl, value_propagate);
+        watch(*cl);
+        cl->set_active();
     }
 
     // Release constraints at the given level and above.
@@ -137,12 +139,11 @@ namespace polysat {
         SASSERT(std::all_of(cl.begin() + 1, cl.end(), [&](auto lit) { return get_watch_level(lit) <= get_watch_level(cl[1]); }));
     }
 
-    void constraint_manager::watch(clause& cl, bool value_propagate) {
+    void constraint_manager::watch(clause& cl) {
         if (cl.empty())
             return;
 
-        if (value_propagate) {
+        {
-#if 1
             // First, try to bool-propagate.
             // Otherwise, we might get a clause-conflict and a missed propagation after resolving the conflict.
             // With this, we will get a constraint-conflict instead.
@@ -180,7 +181,6 @@ namespace polysat {
                     s.assign_eval(~lit);
                 }
             }
-#endif
         }
 
         if (cl.size() == 1) {

src/math/polysat/constraint_manager.h

@@ -75,7 +75,7 @@ namespace polysat {
         void gc_clauses();
 
         void normalize_watch(clause& cl);
-        void watch(clause& cl, bool value_propagate);
+        void watch(clause& cl);
         void unwatch(clause& cl);
 
         void register_clause(clause* cl);
@@ -90,7 +90,7 @@ namespace polysat {
         constraint_manager(solver& s);
         ~constraint_manager();
 
-        void store(clause* cl, bool value_propagate);
+        void store(clause* cl);
 
         /// Release clauses at the given level and above.
         void release_level(unsigned lvl);

src/math/polysat/solver.cpp

@@ -1019,22 +1019,28 @@ namespace polysat {
                 UNREACHABLE();
             }
             if (is_conflict()) {
-                // TODO: the remainder of the narrow_queue as well as the lemmas are forgotten.
+                // The remainder of narrow_queue is forgotten at this point,
-                //       should we just insert them into the new conflict to carry them along?
+                // but keep the lemmas for later.
+                for (clause* lemma : lemmas)
+                    m_conflict.restore_lemma(lemma);
                 return;
             }
         }
 
-        for (clause* lemma : lemmas) {
+        for (auto it = lemmas.begin(); it != lemmas.end(); ++it) {
-            add_clause(*lemma);
+            clause& lemma = **it;
+            if (!lemma.is_active())
+                add_clause(lemma);
+            else
+                propagate_clause(lemma);
             // NOTE: currently, the backjump level is an overapproximation,
             //       since the level of evaluated constraints may not be exact (see TODO in assign_eval).
             // For this reason, we may actually get a conflict at this point
             // (because the actual jump_level of the lemma may be lower that best_level.)
             if (is_conflict()) {
-                // until this is fixed (if possible; and there may be other causes of conflict at this point),
+                // Keep the remaining lemmas for later.
-                // we just forget about the remaining lemmas and restart conflict analysis.
+                for (; it != lemmas.end(); ++it)
-                // TODO: we could also insert the remaining lemmas into the conflict and keep them for later.
+                    m_conflict.restore_lemma(*it);
                 return;
             }
         }
@@ -1063,6 +1069,24 @@ namespace polysat {
         }
     }  // backjump_and_learn
 
+    // Explicit boolean propagation over the given clause, without relying on watch lists
+    void solver::propagate_clause(clause& cl) {
+        sat::literal prop = sat::null_literal;
+        for (sat::literal lit : cl) {
+            if (m_bvars.is_true(lit))
+                return;  // clause is true
+            if (m_bvars.is_false(lit))
+                continue;
+            SASSERT(!m_bvars.is_assigned(lit));
+            if (prop != sat::null_literal)
+                return;  // two or more undef literals
+            prop = lit;
+        }
+        if (prop == sat::null_literal)
+            return;
+        assign_propagate(prop, cl);
+    }
+
     unsigned solver::level(sat::literal lit0, clause const& cl) {
         unsigned lvl = 0;
         for (auto lit : cl) {
@@ -1174,6 +1198,7 @@ namespace polysat {
         LOG((clause.is_redundant() ? "Lemma: ": "Aux: ") << clause);
         for (sat::literal lit : clause) {
             LOG("   " << lit_pp(*this, lit));
+            // TODO: move into constraint_manager::watch
             if (!m_bvars.is_assigned(lit)) {
                 switch (lit2cnstr(lit).eval(*this)) {
                 case l_true:
@@ -1190,12 +1215,11 @@ namespace polysat {
             if (m_bvars.value(lit) == l_true) {
                 // in this case the clause is useless
                 LOG("   Clause is already true, skipping...");
-                // SASSERT(false);  // should never happen (at least for redundant clauses)
                 return;
             }
         }
         SASSERT(!clause.empty());
-        m_constraints.store(&clause, true);
+        m_constraints.store(&clause);
 
         // Defer add_pwatch until the next solver iteration, because during propagation of a variable v the watchlist for v is locked.
         // NOTE: for non-redundant clauses, pwatching its constraints is required for soundness.

src/math/polysat/solver.h

@@ -253,6 +253,8 @@ namespace polysat {
         void erase_pwatch(pvar v, constraint* c);
         void erase_pwatch(constraint* c);
 
+        void propagate_clause(clause& cl);
+
         void set_conflict_at_base_level(dependency dep) { m_conflict.init_at_base_level(dep); }
         void set_conflict(signed_constraint c) { m_conflict.init(c); }
         void set_conflict(clause& cl) { m_conflict.init(cl); }