From: Gereon Kremer Date: Wed, 19 Aug 2020 21:06:57 +0000 (+0200) Subject: (cad solver) Add a partial check method. (#4904) X-Git-Tag: cvc5-1.0.0~2976 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=6710b082bc6fa8c7f67203a4013657e069479119;p=cvc5.git (cad solver) Add a partial check method. (#4904) This PR extends the CAD-based solver to enable partial checks. Essentially, we only collect the first interval that is excluded for the first variable and return that one as a lemma. This does not leave a lot of choice on "how partial" the check should be, but it is fairly easy to implement and does not add additional overhead. It also fixes some confusion in excluding_interval_to_lemma... --- diff --git a/src/theory/arith/nl/cad/cdcac.cpp b/src/theory/arith/nl/cad/cdcac.cpp index 9c58a0007..0dcf7f7a7 100644 --- a/src/theory/arith/nl/cad/cdcac.cpp +++ b/src/theory/arith/nl/cad/cdcac.cpp @@ -344,15 +344,16 @@ CACInterval CDCAC::intervalFromCharacterization( } } -std::vector CDCAC::getUnsatCover(std::size_t cur_variable) +std::vector CDCAC::getUnsatCover(std::size_t curVariable, + bool returnFirstInterval) { Trace("cdcac") << "Looking for unsat cover for " - << d_variableOrdering[cur_variable] << std::endl; - std::vector intervals = getUnsatIntervals(cur_variable); + << d_variableOrdering[curVariable] << std::endl; + std::vector intervals = getUnsatIntervals(curVariable); if (Trace.isOn("cdcac")) { - Trace("cdcac") << "Unsat intervals for " << d_variableOrdering[cur_variable] + Trace("cdcac") << "Unsat intervals for " << d_variableOrdering[curVariable] << ":" << std::endl; for (const auto& i : intervals) { @@ -362,30 +363,30 @@ std::vector CDCAC::getUnsatCover(std::size_t cur_variable) } poly::Value sample; - while (sampleOutsideWithInitial(intervals, sample, cur_variable)) + while (sampleOutsideWithInitial(intervals, sample, curVariable)) { - if (!checkIntegrality(cur_variable, sample)) + if (!checkIntegrality(curVariable, sample)) { // the variable is integral, but the sample is not. Trace("cdcac") << "Used " << sample << " for integer variable " - << d_variableOrdering[cur_variable] << std::endl; - auto new_interval = buildIntegralityInterval(cur_variable, sample); - Trace("cdcac") << "Adding integrality interval " - << new_interval.d_interval << std::endl; - intervals.emplace_back(new_interval); + << d_variableOrdering[curVariable] << std::endl; + auto newInterval = buildIntegralityInterval(curVariable, sample); + Trace("cdcac") << "Adding integrality interval " << newInterval.d_interval + << std::endl; + intervals.emplace_back(newInterval); cleanIntervals(intervals); continue; } - d_assignment.set(d_variableOrdering[cur_variable], sample); + d_assignment.set(d_variableOrdering[curVariable], sample); Trace("cdcac") << "Sample: " << d_assignment << std::endl; - if (cur_variable == d_variableOrdering.size() - 1) + if (curVariable == d_variableOrdering.size() - 1) { // We have a full assignment. SAT! Trace("cdcac") << "Found full assignment: " << d_assignment << std::endl; return {}; } // Recurse to next variable - auto cov = getUnsatCover(cur_variable + 1); + auto cov = getUnsatCover(curVariable + 1); if (cov.empty()) { // Found SAT! @@ -396,12 +397,17 @@ std::vector CDCAC::getUnsatCover(std::size_t cur_variable) auto characterization = constructCharacterization(cov); Trace("cdcac") << "Characterization: " << characterization << std::endl; - d_assignment.unset(d_variableOrdering[cur_variable]); + d_assignment.unset(d_variableOrdering[curVariable]); + + auto newInterval = + intervalFromCharacterization(characterization, curVariable, sample); + newInterval.d_origins = collectConstraints(cov); + intervals.emplace_back(newInterval); - auto new_interval = - intervalFromCharacterization(characterization, cur_variable, sample); - new_interval.d_origins = collectConstraints(cov); - intervals.emplace_back(new_interval); + if (returnFirstInterval) + { + return intervals; + } Trace("cdcac") << "Added " << intervals.back().d_interval << std::endl; Trace("cdcac") << "\tlower: " << intervals.back().d_lowerPolys @@ -421,7 +427,7 @@ std::vector CDCAC::getUnsatCover(std::size_t cur_variable) if (Trace.isOn("cdcac")) { Trace("cdcac") << "Returning intervals for " - << d_variableOrdering[cur_variable] << ":" << std::endl; + << d_variableOrdering[curVariable] << ":" << std::endl; for (const auto& i : intervals) { Trace("cdcac") << "-> " << i.d_interval << std::endl; diff --git a/src/theory/arith/nl/cad/cdcac.h b/src/theory/arith/nl/cad/cdcac.h index 3434b23e6..a6049ad61 100644 --- a/src/theory/arith/nl/cad/cdcac.h +++ b/src/theory/arith/nl/cad/cdcac.h @@ -131,8 +131,15 @@ class CDCAC * be obtained from d_assignment. If the covering is not empty, the result is * UNSAT and an infeasible subset can be extracted from the returned covering. * Implements Algorithm 2. + * @param curVariable The id of the variable (within d_variableOrdering) to + * be considered. This argument is used to manage the recursion internally and + * should always be zero if called externally. + * @param returnFirstInterval If true, the function returns after the first + * interval obtained from a recursive call. The result is not (necessarily) an + * unsat cover, but merely a list of infeasible intervals. */ - std::vector getUnsatCover(std::size_t cur_variable = 0); + std::vector getUnsatCover(std::size_t curVariable = 0, + bool returnFirstInterval = false); private: /** diff --git a/src/theory/arith/nl/cad_solver.cpp b/src/theory/arith/nl/cad_solver.cpp index a2fc1e1f1..bb1ef9911 100644 --- a/src/theory/arith/nl/cad_solver.cpp +++ b/src/theory/arith/nl/cad_solver.cpp @@ -106,6 +106,49 @@ std::vector CadSolver::checkFull() #endif } +std::vector CadSolver::checkPartial() +{ +#ifdef CVC4_POLY_IMP + std::vector lems; + auto covering = d_CAC.getUnsatCover(0, true); + if (covering.empty()) + { + d_foundSatisfiability = true; + Trace("nl-cad") << "SAT: " << d_CAC.getModel() << std::endl; + } + else + { + auto* nm = NodeManager::currentNM(); + Node first_var = + d_CAC.getConstraints().varMapper()(d_CAC.getVariableOrdering()[0]); + for (const auto& interval : covering) + { + Node premise; + Assert(!interval.d_origins.empty()); + if (interval.d_origins.size() == 1) + { + premise = interval.d_origins[0]; + } + else + { + premise = nm->mkNode(Kind::AND, interval.d_origins); + } + Node conclusion = + excluding_interval_to_lemma(first_var, interval.d_interval); + Node lemma = nm->mkNode(Kind::IMPLIES, premise, conclusion); + Trace("nl-cad") << "Excluding " << first_var << " -> " << interval.d_interval << " using " << lemma << std::endl; + lems.emplace_back(lemma, Inference::CAD_EXCLUDED_INTERVAL); + } + } + return lems; +#else + Warning() << "Tried to use CadSolver but libpoly is not available. Compile " + "with --poly." + << std::endl; + return {}; +#endif +} + bool CadSolver::constructModelIfAvailable(std::vector& assertions) { #ifdef CVC4_POLY_IMP diff --git a/src/theory/arith/nl/cad_solver.h b/src/theory/arith/nl/cad_solver.h index 9fb243897..6f6c0d43c 100644 --- a/src/theory/arith/nl/cad_solver.h +++ b/src/theory/arith/nl/cad_solver.h @@ -54,6 +54,14 @@ class CadSolver */ std::vector checkFull(); + /** + * Perform a partial check, returning either {} or a list of lemmas. + * If the result is empty, the input is satisfiable and a model is available + * for construct_model_if_available. Otherwise, the lemmas exclude some part + * of the search space. + */ + std::vector checkPartial(); + /** * If a model is available (indicated by the last call to check_full() or * check_partial()) this method puts a satisfying assignment in d_model, diff --git a/src/theory/arith/nl/poly_conversion.cpp b/src/theory/arith/nl/poly_conversion.cpp index 8345fc5a1..e3bf4712d 100644 --- a/src/theory/arith/nl/poly_conversion.cpp +++ b/src/theory/arith/nl/poly_conversion.cpp @@ -360,17 +360,18 @@ Node excluding_interval_to_lemma(const Node& variable, if (is_algebraic_number(lv)) { return nm->mkNode( - Kind::AND, + Kind::OR, nm->mkNode( - Kind::GT, variable, nm->mkConst(poly_utils::toRationalBelow(lv))), - nm->mkNode(Kind::LT, + Kind::LT, variable, nm->mkConst(poly_utils::toRationalBelow(lv))), + nm->mkNode(Kind::GT, variable, nm->mkConst(poly_utils::toRationalAbove(lv)))); } else { - return nm->mkNode( - Kind::EQUAL, variable, nm->mkConst(poly_utils::toRationalBelow(lv))); + return nm->mkNode(Kind::DISTINCT, + variable, + nm->mkConst(poly_utils::toRationalBelow(lv))); } } if (li) @@ -384,7 +385,7 @@ Node excluding_interval_to_lemma(const Node& variable, Kind::LT, variable, nm->mkConst(poly_utils::toRationalBelow(lv))); } return nm->mkNode( - Kind::AND, + Kind::OR, nm->mkNode( Kind::GT, variable, nm->mkConst(poly_utils::toRationalAbove(uv))), nm->mkNode(