From: Andrew Reynolds Date: Mon, 12 Jul 2021 20:59:25 +0000 (-0500) Subject: Add branch and bound (#6865) X-Git-Tag: cvc5-1.0.0~1501 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=ea0b6105f1bd2ce86ce2f5a07a6255801d6d7e64;p=cvc5.git Add branch and bound (#6865) This PR moves https://github.com/cvc5/cvc5/blob/master/src/theory/arith/theory_arith_private.cpp#L3451 to its own module. The next PR will connect this module to theory_arith / theory_arith_private. Towards ensuring type constraints are met for linear arithmetic models. --- diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 9fce77c80..bc0a922d2 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -358,6 +358,8 @@ libcvc5_add_sources( theory/arith/bound_counts.h theory/arith/bound_inference.cpp theory/arith/bound_inference.h + theory/arith/branch_and_bound.cpp + theory/arith/branch_and_bound.h theory/arith/callbacks.cpp theory/arith/callbacks.h theory/arith/congruence_manager.cpp diff --git a/src/theory/arith/branch_and_bound.cpp b/src/theory/arith/branch_and_bound.cpp new file mode 100644 index 000000000..22859977b --- /dev/null +++ b/src/theory/arith/branch_and_bound.cpp @@ -0,0 +1,143 @@ +/****************************************************************************** + * Top contributors (to current version): + * Andrew Reynolds + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * in the top-level source directory and their institutional affiliations. + * All rights reserved. See the file COPYING in the top-level source + * directory for licensing information. + * **************************************************************************** + * + * Branch and bound for arithmetic + */ + +#include "theory/arith/branch_and_bound.h" + +#include "options/arith_options.h" +#include "proof/eager_proof_generator.h" +#include "proof/proof_node.h" +#include "theory/arith/arith_utilities.h" +#include "theory/rewriter.h" +#include "theory/theory.h" + +using namespace cvc5::kind; + +namespace cvc5 { +namespace theory { +namespace arith { + +BranchAndBound::BranchAndBound(ArithState& s, + InferenceManager& im, + PreprocessRewriteEq& ppre, + ProofNodeManager* pnm) + : d_astate(s), + d_im(im), + d_ppre(ppre), + d_pfGen(new EagerProofGenerator(pnm, s.getUserContext())), + d_pnm(pnm) +{ +} + +TrustNode BranchAndBound::branchIntegerVariable(TNode var, Rational value) +{ + TrustNode lem = TrustNode::null(); + NodeManager* nm = NodeManager::currentNM(); + Integer floor = value.floor(); + if (options::brabTest()) + { + Trace("integers") << "branch-round-and-bound enabled" << std::endl; + Integer ceil = value.ceiling(); + Rational f = value - floor; + // Multiply by -1 to get abs value. + Rational c = (value - ceil) * (-1); + Integer nearest = (c > f) ? floor : ceil; + + // Prioritize trying a simple rounding of the real solution first, + // it that fails, fall back on original branch and bound strategy. + Node ub = + Rewriter::rewrite(nm->mkNode(LEQ, var, mkRationalNode(nearest - 1))); + Node lb = + Rewriter::rewrite(nm->mkNode(GEQ, var, mkRationalNode(nearest + 1))); + Node right = nm->mkNode(OR, ub, lb); + Node rawEq = nm->mkNode(EQUAL, var, mkRationalNode(nearest)); + Node eq = Rewriter::rewrite(rawEq); + // Also preprocess it before we send it out. This is important since + // arithmetic may prefer eliminating equalities. + TrustNode teq; + if (Theory::theoryOf(eq) == THEORY_ARITH) + { + teq = d_ppre.ppRewriteEq(eq); + eq = teq.isNull() ? eq : teq.getNode(); + } + Node literal = d_astate.getValuation().ensureLiteral(eq); + Trace("integers") << "eq: " << eq << "\nto: " << literal << std::endl; + d_im.requirePhase(literal, true); + Node l = nm->mkNode(OR, literal, right); + Trace("integers") << "l: " << l << std::endl; + if (proofsEnabled()) + { + Node less = nm->mkNode(LT, var, mkRationalNode(nearest)); + Node greater = nm->mkNode(GT, var, mkRationalNode(nearest)); + // TODO (project #37): justify. Thread proofs through *ensureLiteral*. + Debug("integers::pf") << "less: " << less << std::endl; + Debug("integers::pf") << "greater: " << greater << std::endl; + Debug("integers::pf") << "literal: " << literal << std::endl; + Debug("integers::pf") << "eq: " << eq << std::endl; + Debug("integers::pf") << "rawEq: " << rawEq << std::endl; + Pf pfNotLit = d_pnm->mkAssume(literal.negate()); + // rewrite notLiteral to notRawEq, using teq. + Pf pfNotRawEq = + literal == rawEq + ? pfNotLit + : d_pnm->mkNode( + PfRule::MACRO_SR_PRED_TRANSFORM, + {pfNotLit, + teq.getGenerator()->getProofFor(teq.getProven())}, + {rawEq.negate()}); + Pf pfBot = d_pnm->mkNode( + PfRule::CONTRA, + {d_pnm->mkNode(PfRule::ARITH_TRICHOTOMY, + {d_pnm->mkAssume(less.negate()), pfNotRawEq}, + {greater}), + d_pnm->mkAssume(greater.negate())}, + {}); + std::vector assumptions = { + literal.negate(), less.negate(), greater.negate()}; + // Proof of (not (and (not (= v i)) (not (< v i)) (not (> v i)))) + Pf pfNotAnd = d_pnm->mkScope(pfBot, assumptions); + Pf pfL = d_pnm->mkNode(PfRule::MACRO_SR_PRED_TRANSFORM, + {d_pnm->mkNode(PfRule::NOT_AND, {pfNotAnd}, {})}, + {l}); + lem = d_pfGen->mkTrustNode(l, pfL); + } + else + { + lem = TrustNode::mkTrustLemma(l, nullptr); + } + } + else + { + Node ub = Rewriter::rewrite(nm->mkNode(LEQ, var, mkRationalNode(floor))); + Node lb = ub.notNode(); + if (proofsEnabled()) + { + lem = + d_pfGen->mkTrustNode(nm->mkNode(OR, ub, lb), PfRule::SPLIT, {}, {ub}); + } + else + { + lem = TrustNode::mkTrustLemma(nm->mkNode(OR, ub, lb), nullptr); + } + } + + Trace("integers") << "integers: branch & bound: " << lem << std::endl; + return lem; +} + +bool BranchAndBound::proofsEnabled() const { return d_pnm != nullptr; } + +} // namespace arith +} // namespace theory +} // namespace cvc5 diff --git a/src/theory/arith/branch_and_bound.h b/src/theory/arith/branch_and_bound.h new file mode 100644 index 000000000..4281ba678 --- /dev/null +++ b/src/theory/arith/branch_and_bound.h @@ -0,0 +1,73 @@ +/****************************************************************************** + * Top contributors (to current version): + * Andrew Reynolds + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * in the top-level source directory and their institutional affiliations. + * All rights reserved. See the file COPYING in the top-level source + * directory for licensing information. + * **************************************************************************** + * + * Branch and bound for arithmetic + */ + +#include "cvc5_private.h" + +#ifndef CVC5__THEORY__ARITH__BRANCH_AND_BOUND__H +#define CVC5__THEORY__ARITH__BRANCH_AND_BOUND__H + +#include + +#include "expr/node.h" +#include "proof/proof_node_manager.h" +#include "proof/trust_node.h" +#include "theory/arith/arith_state.h" +#include "theory/arith/inference_manager.h" +#include "theory/arith/pp_rewrite_eq.h" +#include "util/rational.h" + +namespace cvc5 { +namespace theory { +namespace arith { + +/** + * Class is responsible for constructing branch and bound lemmas. It is + * agnostic to the state of solver; instead is simply given (variable, value) + * pairs in branchIntegerVariable below and constructs the appropriate lemma. + */ +class BranchAndBound +{ + public: + BranchAndBound(ArithState& s, + InferenceManager& im, + PreprocessRewriteEq& ppre, + ProofNodeManager* pnm); + ~BranchAndBound() {} + /** + * Branch variable, called when integer var has given value + * in the current model, returns a split to eliminate this model. + */ + TrustNode branchIntegerVariable(TNode var, Rational value); + + private: + /** Are proofs enabled? */ + bool proofsEnabled() const; + /** Reference to the state */ + ArithState& d_astate; + /** Reference to the inference manager */ + InferenceManager& d_im; + /** Reference to the preprocess rewriter for equality */ + PreprocessRewriteEq& d_ppre; + /** Proof generator. */ + std::unique_ptr d_pfGen; + /** Proof node manager */ + ProofNodeManager* d_pnm; +}; + +} // namespace arith +} // namespace theory +} // namespace cvc5 + +#endif