From 15c094fa32015ce5b3ee8e21d736793c0c9870c4 Mon Sep 17 00:00:00 2001
From: Jakob Rath <git@jakobrath.eu>
Date: Mon, 6 Sep 2021 18:00:21 +0200
Subject: [PATCH] Add fallback lemma

---
 src/math/polysat/search_state.h |  4 +++
 src/math/polysat/solver.cpp     | 61 +++++++++++++++++++++++++--------
 src/math/polysat/solver.h       |  2 ++
 3 files changed, 52 insertions(+), 15 deletions(-)

diff --git a/src/math/polysat/search_state.h b/src/math/polysat/search_state.h
index 08bee4b22..9b975a297 100644
--- a/src/math/polysat/search_state.h
+++ b/src/math/polysat/search_state.h
@@ -65,6 +65,10 @@ namespace polysat {
         void push_boolean(sat::literal lit);
         void pop();
 
+        using const_iterator = decltype(m_items)::const_iterator;
+        const_iterator begin() const { return m_items.begin(); }
+        const_iterator end() const { return m_items.end(); }
+
         std::ostream& display(std::ostream& out) const;
     };
 
diff --git a/src/math/polysat/solver.cpp b/src/math/polysat/solver.cpp
index 924d2272b..829bb1723 100644
--- a/src/math/polysat/solver.cpp
+++ b/src/math/polysat/solver.cpp
@@ -661,17 +661,14 @@ namespace polysat {
         LOG_H3("Reverting decision: pvar " << v << " := " << val);
         SASSERT(m_justification[v].is_decision());
 
-        backjump(m_justification[v].level()-1);
-
-        if (m_conflict.is_bailout()) {
-            m_viable.add_non_viable(v, val);
-            // TODO: need to add fallback lemma
-            return;
-        }
-
-        clause_ref lemma = m_conflict.build_lemma();
+        clause_ref lemma;
+        if (m_conflict.is_bailout())
+            lemma = mk_fallback_lemma(m_justification[v].level());
+        else
+            lemma = m_conflict.build_lemma();
         m_conflict.reset();
 
+        backjump(m_justification[v].level()-1);
         // TODO: we need to decide_bool on the clause (learn_lemma takes care of this).
         //       if the lemma was asserting, then this will propagate the last literal. otherwise we do the enumerative guessing as normal.
         //       we need to exclude the current value of v. narrowing of the guessed constraint *should* take care of it but we cannot count on that.
@@ -698,16 +695,45 @@ namespace polysat {
         }
         */
     }
-    
+
+    bool solver::is_decision(search_item const& item) const {
+        if (item.is_assignment())
+            return m_justification[item.var()].is_decision();
+        else
+            return m_bvars.is_decision(item.lit().var());
+    }
+
+    /** Create fallback lemma that excludes the current search state */
+    clause_ref solver::mk_fallback_lemma(unsigned lvl) {
+        LOG_H3("Creating fallback lemma for level " << lvl);
+        LOG_V("m_search: " << m_search);
+        clause_builder lemma(*this);
+        unsigned todo = lvl;
+        unsigned i = 0;
+        while (todo > 0) {
+            auto const& item = m_search[i++];
+            if (!is_decision(item))
+                continue;
+            LOG_V("Adding: " << item);
+            if (item.is_assignment()) {
+                pvar v = item.var();
+                auto c = ~m_constraints.eq(0, var(v) - m_value[v]);
+                m_constraints.ensure_bvar(c.get());
+                lemma.push_literal(c.blit());
+            } else {
+                sat::literal lit = item.lit();
+                lemma.push_literal(~lit);
+            }
+            --todo;
+        }
+        return lemma.build();
+    }
+
     void solver::revert_bool_decision(sat::literal lit) {
         sat::bool_var const var = lit.var();
         LOG_H3("Reverting boolean decision: " << lit);
         SASSERT(m_bvars.is_decision(var));
 
-        if (m_conflict.is_bailout()) {
-            NOT_IMPLEMENTED_YET();
-        }
-
         // TODO:
         // Current situation: we have a decision for boolean literal L on top of the stack, and a conflict core.
         //
@@ -726,7 +752,11 @@ namespace polysat {
         //      (L')^{L' \/ ¬L \/ ...}
         //      again L is in core, unless we core-reduced it away
 
-        clause_ref reason = m_conflict.build_lemma();
+        clause_ref reason;
+        if (m_conflict.is_bailout())
+            reason = mk_fallback_lemma(m_bvars.level(var));
+        else
+            reason = m_conflict.build_lemma();
         m_conflict.reset();
 
         bool contains_lit = std::any_of(reason->begin(), reason->end(), [lit](auto reason_lit) { return reason_lit == ~lit; });
@@ -747,6 +777,7 @@ namespace polysat {
         }
 
         // The lemma where 'lit' comes from.
+        // Currently, boolean decisions always come from guessing a literal of a learned non-unit lemma.
         clause* lemma = m_bvars.lemma(var);  // need to grab this while 'lit' is still assigned
         SASSERT(lemma);
 
diff --git a/src/math/polysat/solver.h b/src/math/polysat/solver.h
index c44e3c089..04555e630 100644
--- a/src/math/polysat/solver.h
+++ b/src/math/polysat/solver.h
@@ -168,6 +168,7 @@ namespace polysat {
 
         void assign_core(pvar v, rational const& val, justification const& j);
         bool is_assigned(pvar v) const { return !m_justification[v].is_unassigned(); }
+        bool is_decision(search_item const& item) const;
 
 
         bool should_search();
@@ -216,6 +217,7 @@ namespace polysat {
         void resolve_bool(sat::literal lit);
         void revert_decision(pvar v);
         void revert_bool_decision(sat::literal lit);
+        clause_ref mk_fallback_lemma(unsigned lvl);
 
         void report_unsat();
         void learn_lemma(pvar v, clause_ref lemma);