bailout for saturation lemmas

src/math/polysat/conflict.cpp

@@ -100,9 +100,6 @@ namespace polysat {
             for (auto const& lit : cb)
                 out_indent() << lit << ": " << s.lit2cnstr(lit) << '\n';
             out().flush();
-
-            // if (m_conflicts == 9)
-            //     std::exit(0);
         }
 
         void end_conflict(search_state const& search, viable const& v) {
@@ -197,7 +194,7 @@ namespace polysat {
         m_var_occurrences.reset();
         m_bail_vars.reset();
         m_conflict_var = null_var;
-        m_bailout = false;
+        m_kind = conflict_kind_t::ok;
         SASSERT(empty());        
     }
 
@@ -345,12 +342,18 @@ namespace polysat {
         return m_literals.contains(lit.index());
     }
 
-    void conflict::set_bailout() {
+    void conflict::set_bailout_gave_up() {
-        SASSERT(!is_bailout());
+        SASSERT(m_kind == conflict_kind_t::ok);
-        m_bailout = true;
+        m_kind = conflict_kind_t::bailout_gave_up;
         s.m_stats.m_num_bailouts++;
     }
 
+    void conflict::set_bailout_lemma() {
+        SASSERT(m_kind == conflict_kind_t::ok);
+        m_kind = conflict_kind_t::bailout_lemma;
+        // s.m_stats.m_num_bailouts++;
+    }
+
     struct inference_resolve : public inference {
         sat::literal m_lit;
         clause const& m_clause;
@@ -487,6 +490,8 @@ namespace polysat {
 
         SASSERT(v != conflict_var());
 
+        bool has_saturated = false;
+
         auto const& j = s.m_justification[v];
 
         if (j.is_decision() && m_bail_vars.contains(v))
@@ -517,11 +522,20 @@ namespace polysat {
             // TODO: as a last resort, substitute v by m_value[v]?
             if (try_eliminate(v))
                 return true;
-            if (!try_saturate(v))
+            LOG("try-saturate v" << v);
+            if (try_saturate(v))
+                has_saturated = true;
+            else
                 break;
         }
         LOG("bailout v" << v);
-        set_bailout();
+        if (has_saturated) {
+            // NOTE: current saturation rules create valid lemmas that do not depend on the variable assignment
+            set_bailout_lemma();
+            return true;
+        }
+        else
+            set_bailout_gave_up();
     bailout:
         if (s.is_assigned(v) && j.is_decision())
             m_vars.insert(v);

src/math/polysat/conflict.h

@@ -98,6 +98,12 @@ namespace polysat {
         std::ostream& display(std::ostream& out) const override { return out << m_name; }
     };
 
+    enum class conflict_kind_t {
+        ok,
+        bailout_gave_up,
+        bailout_lemma,
+    };
+
     /** Conflict state, represented as core (~negation of clause). */
     class conflict {
         solver& s;
@@ -106,13 +112,19 @@ namespace polysat {
         uint_set m_vars;                    // variable assignments used as premises
         uint_set m_bail_vars;
 
-        friend class inference_logger;
-        scoped_ptr<inference_logger> m_logger;
-
         // 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;
 
+        /** Whether we are in a bailout state.
+         * We enter a bailout state when we give up on proper conflict resolution,
+         * or want to learn a lemma without fine-grained backtracking.
+         */
+        conflict_kind_t m_kind = conflict_kind_t::ok;
+
+        friend class inference_logger;
+        scoped_ptr<inference_logger> m_logger;
+
         bool_vector m_bvar2mark;                  // mark of Boolean variables
 
         void set_mark(signed_constraint c);
@@ -120,9 +132,6 @@ namespace polysat {
 
         void minimize_vars(signed_constraint c);
 
-        /** Whether we are in a bailout state. We enter a bailout state when we give up on proper conflict resolution.  */
-        bool m_bailout = false;
-
         constraint_manager& cm() const;
         scoped_ptr_vector<explainer> ex_engines;
         scoped_ptr_vector<variable_elimination_engine> ve_engines;
@@ -143,9 +152,10 @@ namespace polysat {
 
         pvar conflict_var() const { return m_conflict_var; }
 
-        bool is_bailout() const { return m_bailout; }
+        bool is_bailout() const { return m_kind != conflict_kind_t::ok; }
-
+        bool is_bailout_lemma() const { return m_kind == conflict_kind_t::bailout_lemma; }
-        void set_bailout();
+        void set_bailout_gave_up();
+        void set_bailout_lemma();
 
         bool empty() const;
         void reset();

src/math/polysat/saturation.cpp

@@ -73,6 +73,7 @@ namespace polysat {
         LOG("consequent " << c << " value: " << c.bvalue(s) << " is-false: " << c.is_currently_false(s) << " " << core.contains(~c));
 
         // ensure new core is a conflict
+        // TODO: don't we need to check the m_new_constraints too? or maybe that is implicit in the rules (should check it)
         if (!c.is_currently_false(s) && c.bvalue(s) != l_false)
             return false;
 
@@ -99,7 +100,7 @@ namespace polysat {
         core.reset();
         for (auto d : m_new_constraints)
             core.insert(d);
-        if (c.bvalue(s) != l_false)
+        if (c.bvalue(s) != l_false)  // conflict is due to the evaluation of c, so it depends on the variable values
             core.insert_vars(c);
         core.insert(~c);       
         core.log_inference(inf_name);

src/math/polysat/solver.cpp

@@ -27,8 +27,6 @@ Author:
 
 namespace polysat {
 
-
-
     solver::solver(reslimit& lim): 
         m_lim(lim),
         m_viable(*this),
@@ -93,7 +91,6 @@ namespace polysat {
         return check_sat();
     }
 
-
     dd::pdd_manager& solver::sz2pdd(unsigned sz) const {
         m_pdd.reserve(sz + 1);
         if (!m_pdd[sz])
@@ -643,6 +640,11 @@ namespace polysat {
                     revert_decision(v);
                     return;
                 }
+                if (m_conflict.is_bailout_lemma()) {
+                    m_conflict.end_conflict();
+                    backtrack_lemma();
+                    return;
+                }
                 m_search.pop_assignment();
             }
             else {
@@ -677,7 +679,44 @@ namespace polysat {
     }
 
     /**
-     * Simpler backracking for forbidden interval lemmas:
+     * Simple backtracking for lemmas:
+     * jump to the level where the lemma can be (bool-)propagated,
+     * even without reverting the last decision.
+     */
+    void solver::backtrack_lemma() {
+        clause_ref lemma = m_conflict.build_lemma().build();
+        LOG_H2("backtrack_lemma: " << show_deref(lemma));
+        SASSERT(lemma);
+
+        // find second-highest level of the literals in the lemma
+        unsigned max_level = 0;  // could be simplified if we're sure that always max_level == m_level
+        unsigned jump_level = 0;
+        for (auto lit : *lemma) {
+            if (!m_bvars.is_assigned(lit))
+                continue;
+            unsigned lit_level = m_bvars.level(lit);
+            if (lit_level > max_level) {
+                jump_level = max_level;
+                max_level = lit_level;
+            } else if (max_level > lit_level && lit_level > jump_level) {
+                jump_level = lit_level;
+            }
+        }
+
+        jump_level = std::max(jump_level, base_level());
+
+        // LOG("current lvl: " << m_level);
+        // LOG("base level:  " << base_level());
+        // LOG("max_level:   " << max_level);
+        // LOG("jump_level:  " << jump_level);
+
+        m_conflict.reset();
+        backjump(jump_level);
+        learn_lemma(*lemma);
+    }
+
+    /**
+     * Simpler backtracking for forbidden interval lemmas:
      * since forbidden intervals already gives us a lemma where the conflict variable has been eliminated,
      * we can backtrack to the last relevant decision and learn this lemma.
      */
@@ -914,7 +953,7 @@ namespace polysat {
         LOG_H3("Reverting boolean decision: " << lit << " " << m_conflict);
         SASSERT(m_bvars.is_decision(var));
 
-        clause_builder reason_builder = m_conflict.build_lemma();        
+        clause_builder reason_builder = m_conflict.build_lemma();
 
         SASSERT(std::find(reason_builder.begin(), reason_builder.end(), ~lit));
         clause_ref reason = reason_builder.build();

src/math/polysat/solver.h

@@ -205,6 +205,7 @@ namespace polysat {
 
         void resolve_conflict();
         void backtrack_fi();
+        void backtrack_lemma();
         void revert_decision(pvar v);
         void revert_bool_decision(sat::literal lit);