combine backtracking methods

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

src/math/lp/nla_stellensatz2.cpp

@@ -487,14 +487,9 @@ namespace nla {
             m_solver.update_values(m_values);
             return false;
         }
-        while (backtrack(m_core)) {            
+        m_conflict_dep.reset();
-            r = m_solver.solve(m_core);
+        m_conflict_dep.append(m_core);
-            TRACE(arith, tout << "backtrack search " << r << ": " << m_core << "\n");
+        verbose_stream() << "is-linear-conflict\n";
-            if (r == l_false)
-                continue;
-            m_solver.update_values(m_values);
-            return false;
-        }        
         return true;
     }
 
@@ -595,47 +590,6 @@ namespace nla {
         return {degree, lc, rest};
     }
 
-    //
-    // check if core depends on an assumption
-    // identify the maximal assumption
-    // undo m_constraints down to max_ci.
-    // negate max_ci
-    // propagate it using remaining external and assumptions.
-    // find a new satisfying assignment (if any) before continuing.
-    // 
-    bool stellensatz2::backtrack(svector<lp::constraint_index> const &core) {
-        ++c().lp_settings().stats().m_stellensatz.m_num_backtracks;
-        ++m_stats.m_num_backtracks;
-        SASSERT(well_formed());
-        m_constraints_in_conflict.reset();
-        svector<lp::constraint_index> external, assumptions;
-        for (auto ci : core)
-            explain_constraint(ci, external, assumptions);
-        TRACE(arith, display(tout << "backtrack core " << core << "external " << external << " assumptions "
-                                  << assumptions << "\n");
-              for (auto a : assumptions) display_constraint(tout, a););
-        if (assumptions.empty())
-            return false;
-        lp::constraint_index max_ci = 0;
-        for (auto ci : assumptions) 
-            max_ci = std::max(ci, max_ci);
-
-        assumptions.erase(max_ci);
-        SASSERT(all_of(assumptions, [&](lp::constraint_index ci) { return m_levels[ci] < m_levels[max_ci]; }));
-        external.append(assumptions);
-        backtrack(max_ci, external);
-        SASSERT(well_formed());
-        return true;
-    }
-
-    bool stellensatz2::core_is_linear(svector<lp::constraint_index> const &core) {
-        m_constraints_in_conflict.reset();
-        svector<lp::constraint_index> external, assumptions;
-        for (auto ci : core)
-            explain_constraint(ci, external, assumptions);
-        return all_of(assumptions, [&](auto ci) { return has_term_offset(m_constraints[ci].p); });
-    }
-
     void stellensatz2::explain_constraint(lp::constraint_index ci, svector<lp::constraint_index> &external,
                                          svector<lp::constraint_index> &assumptions) {
         if (m_constraints_in_conflict.contains(ci))
@@ -936,12 +890,12 @@ namespace nla {
                 is_sat = resolve_conflict();
             else if (should_propagate())
                 propagate();
+            else if (is_linear_conflict())
+                continue;
             else if (primal_saturate())
                 continue;
             else if (is_feasible())
                 is_sat = l_true;
-            else if (is_linear_conflict())
-                is_sat = l_false;
             else if (should_dual_saturate())
                 dual_saturate();
             else if (!decide())
@@ -1001,11 +955,28 @@ namespace nla {
     }
 
     //
-    // Conflict resolution is similar to CDCL
+    // Conflict resolution is similar to CDCL:
     // walk m_bounds based on the propagated bounds
     // flip the last decision and backjump to the UIP.
     //     
     lbool stellensatz2::resolve_conflict() {
+        verbose_stream() << "resolve conflict\n";
+        ++c().lp_settings().stats().m_stellensatz.m_num_backtracks;
+
+        auto ci = find_backtrack_constraint();
+        if (!ci)
+            return l_false;
+        SASSERT(is_decision(*ci));
+
+        svector<lp::constraint_index> deps;
+        for (auto ci : m_conflict_marked_ci) 
+            deps.push_back(ci);        
+
+        backtrack(*ci, deps);        
+        return l_undef;
+    }
+
+    std::optional<lp::constraint_index> stellensatz2::find_backtrack_constraint() {
         SASSERT(is_conflict());
         TRACE(arith, tout << "resolving conflict: " << m_conflict_dep << "\n"; display_constraint(tout, m_conflict);
               display(tout););
@@ -1029,7 +1000,6 @@ namespace nla {
 
             mark_dependencies(ci);
             m_conflict_marked_ci.remove(ci);
-            //m_conflict = resolve(m_conflict, ci);
             if (conflict_level == 0)
                 m_core.push_back(ci);
 
@@ -1039,31 +1009,15 @@ namespace nla {
                   tout << "is_decision: " << found_decision << "\n"; display_constraint(tout, ci);
                   tout << "new conflict: "; display_constraint(tout, m_conflict););
         }
-        #if 0
-        if (constraint_is_conflict(m_conflict)) {
-            TRACE(arith, tout << "Conflict " << m_conflict << "\n");
-            m_core.push_back(m_conflict);
-            reset_conflict();
-            return l_false;
-        }
-        #endif
         SASSERT(found_decision == (conflict_level != 0));
         if (!found_decision) {
             for (auto ci : m_conflict_marked_ci)
-                m_core.push_back(ci);            
+                m_core.push_back(ci);
             reset_conflict();
             TRACE(arith, tout << "conflict " << m_core << "\n");
-            return l_false;
+            return std::nullopt;
         }
-
+        return ci;
-        SASSERT(is_decision(ci));
-
-        svector<lp::constraint_index> deps;
-        for (auto ci : m_conflict_marked_ci) 
-            deps.push_back(ci);
-        
-        backtrack(ci, deps);        
-        return l_undef;
     }
 
     // ~(x >= k) == -x > -k == -x >= -k + 1 if k integer
@@ -1204,12 +1158,6 @@ namespace nla {
         }, j);
     }
 
-    void stellensatz2::mark_dependencies(u_dependency* d) { 
-        auto cdeps = antecedents(d);
-        for (auto a : cdeps)
-            m_conflict_marked_ci.insert(a);
-    }
-
     void stellensatz2::mark_dependencies(lp::constraint_index ci) {
         for (auto cij : justification_range(*this, m_justifications[ci]))
             m_conflict_marked_ci.insert(cij);
@@ -1347,7 +1295,7 @@ namespace nla {
     // 
     
     bool stellensatz2::primal_saturate() {
-
+        verbose_stream() << "primal saturate " << m_constraints.size() << "\n";
         init_levels();
         unsigned num_fixed = 0;
         unsigned num_levels = m_level2var.size();
@@ -1386,6 +1334,9 @@ namespace nla {
                 // backtrack decision to max variable in ci
                 level = std::min(max_level(m_constraints[conflict]) - 1, level);
         }
+        if (is_feasible())
+            return false;
+
         if (num_rounds >= max_rounds)
             return false;
         if (constraint_size < m_constraints.size()) {
@@ -2307,6 +2258,7 @@ namespace nla {
     }
       
     void stellensatz2::propagate() {
+        verbose_stream() << "propagate\n";
         while (m_prop_qhead < m_polynomial_queue.size() && !is_conflict() && c().reslim().inc()) {
             auto [p, ci] = m_polynomial_queue[m_prop_qhead++];
             propagate_intervals(p, ci);

src/math/lp/nla_stellensatz2.h

@@ -219,6 +219,7 @@ namespace nla {
         bool can_continue_search();
         lbool search();
         lbool resolve_conflict();
+        std::optional<lp::constraint_index> find_backtrack_constraint();
         void backtrack(lp::constraint_index ci, svector<lp::constraint_index> const &deps);
         constraint negate_constraint(constraint const &c);
 
@@ -226,7 +227,6 @@ namespace nla {
         void init_levels();
         void insert_max_var(lp::constraint_index ci);
         void pop_bound();
-        void mark_dependencies(u_dependency *d);
         void mark_dependencies(lp::constraint_index ci);
         bool should_propagate() const { return m_prop_qhead < m_polynomial_queue.size(); }
         bool should_dual_saturate() { return false; }
@@ -430,8 +430,6 @@ namespace nla {
         void explain_constraint(lemma_builder& new_lemma, lp::constraint_index ci, lp::explanation &ex);
         void explain_constraint(lp::constraint_index ci, svector<lp::constraint_index> &external,
                                 svector<lp::constraint_index> &assumptions);
-        bool backtrack(svector<lp::constraint_index> const& core);
-        bool core_is_linear(svector<lp::constraint_index> const &core);
 
         bool well_formed();
         bool well_formed_var(lpvar v);