(cad solver) Use the current model as initial assignment (#4893)

This PR implements a first naive way to employ the linear model (obtained from the nonlinear extension) to guide the initial sampling within the cad solver.

2 files changed, 57 insertions, 1 deletions

diff --git a/src/theory/arith/nl/cad/cdcac.cpp b/src/theory/arith/nl/cad/cdcac.cpp
index 4725eb198..9c58a0007 100644
--- a/src/theory/arith/nl/cad/cdcac.cpp
+++ b/src/theory/arith/nl/cad/cdcac.cpp
@@ -78,6 +78,19 @@ void CDCAC::computeVariableOrdering()
   }
 }
 
+void CDCAC::retrieveInitialAssignment(NlModel& model, const Node& ran_variable)
+{
+  d_initialAssignment.clear();
+  Trace("cdcac") << "Retrieving initial assignment:" << std::endl;
+  for (const auto& var : d_variableOrdering)
+  {
+    Node v = getConstraints().varMapper()(var);
+    Node val = model.computeConcreteModelValue(v);
+    poly::Value value = node_to_value(val, ran_variable);
+    Trace("cdcac") << "\t" << var << " = " << value << std::endl;
+    d_initialAssignment.emplace_back(value);
+  }
+}
 Constraints& CDCAC::getConstraints() { return d_constraints; }
 const Constraints& CDCAC::getConstraints() const { return d_constraints; }
 
@@ -121,6 +134,28 @@ std::vector<CACInterval> CDCAC::getUnsatIntervals(
   return res;
 }
 
+bool CDCAC::sampleOutsideWithInitial(const std::vector<CACInterval>& infeasible,
+                                     poly::Value& sample,
+                                     std::size_t cur_variable)
+{
+  if (cur_variable < d_initialAssignment.size())
+  {
+    const poly::Value& suggested = d_initialAssignment[cur_variable];
+    for (const auto& i : infeasible)
+    {
+      if (poly::contains(i.d_interval, suggested))
+      {
+        d_initialAssignment.clear();
+        return sampleOutside(infeasible, sample);
+      }
+    }
+    Trace("cdcac") << "Using suggested initial value" << std::endl;
+    sample = suggested;
+    return true;
+  }
+  return sampleOutside(infeasible, sample);
+}
+
 std::vector<poly::Polynomial> CDCAC::requiredCoefficients(
     const poly::Polynomial& p) const
 {
@@ -327,7 +362,7 @@ std::vector<CACInterval> CDCAC::getUnsatCover(std::size_t cur_variable)
   }
   poly::Value sample;
 
-  while (sampleOutside(intervals, sample))
+  while (sampleOutsideWithInitial(intervals, sample, cur_variable))
   {
     if (!checkIntegrality(cur_variable, sample))
     {
diff --git a/src/theory/arith/nl/cad/cdcac.h b/src/theory/arith/nl/cad/cdcac.h
index bd64a9ceb..3434b23e6 100644
--- a/src/theory/arith/nl/cad/cdcac.h
+++ b/src/theory/arith/nl/cad/cdcac.h
@@ -58,6 +58,14 @@ class CDCAC
   void computeVariableOrdering();
 
   /**
+   * Extract an initial assignment from the given model.
+   * This initial assignment is used to guide sampling if possible.
+   * The ran_variable should be the variable used to encode real algebraic
+   * numbers in the model and is simply passed on to node_to_value.
+   */
+  void retrieveInitialAssignment(NlModel& model, const Node& ran_variable);
+
+  /**
    * Returns the constraints as a non-const reference. Can be used to add new
    * constraints.
    */
@@ -82,6 +90,16 @@ class CDCAC
   std::vector<CACInterval> getUnsatIntervals(std::size_t cur_variable) const;
 
   /**
+   * Sample outside of the set of intervals.
+   * Uses a given initial value from mInitialAssignment if possible.
+   * Returns whether a sample was found (true) or the infeasible intervals cover
+   * the whole real line (false).
+   */
+  bool sampleOutsideWithInitial(const std::vector<CACInterval>& infeasible,
+                                poly::Value& sample,
+                                std::size_t cur_variable);
+
+  /**
    * Collects the coefficients required for projection from the given
    * polynomial. Implements Algorithm 6.
    */
@@ -155,6 +173,9 @@ class CDCAC
 
   /** The object computing the variable ordering. */
   VariableOrdering d_varOrder;
+
+  /** The linear assignment used as an initial guess. */
+  std::vector<poly::Value> d_initialAssignment;
 };
 
 }  // namespace cad