From: Gereon Kremer Date: Sun, 16 Aug 2020 00:28:27 +0000 (+0200) Subject: (cad solver) Use the current model as initial assignment (#4893) X-Git-Tag: cvc5-1.0.0~2997 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=f4f7f148082535c23e24a0b92cdf2612f0598072;p=cvc5.git (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. --- 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 CDCAC::getUnsatIntervals( return res; } +bool CDCAC::sampleOutsideWithInitial(const std::vector& 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 CDCAC::requiredCoefficients( const poly::Polynomial& p) const { @@ -327,7 +362,7 @@ std::vector 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 @@ -57,6 +57,14 @@ class CDCAC /** Collect variables from the constraints and compute a variable ordering. */ 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. @@ -81,6 +89,16 @@ class CDCAC */ std::vector 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& 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 d_initialAssignment; }; } // namespace cad