diff options
author | Gereon Kremer <gereon.kremer@cs.rwth-aachen.de> | 2020-08-16 02:28:27 +0200 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-08-15 19:28:27 -0500 |
commit | f4f7f148082535c23e24a0b92cdf2612f0598072 (patch) | |
tree | 68ae2c80605b49f4320329da1d86d6ebaf3554fb | |
parent | a1e951127f7a3af158ca1408e62bd46d5cb065ff (diff) |
(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.
-rw-r--r-- | src/theory/arith/nl/cad/cdcac.cpp | 37 | ||||
-rw-r--r-- | src/theory/arith/nl/cad/cdcac.h | 21 |
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 |