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 9fce77c8051bb15f43bd257face243197e10c535..bc0a922d2fccaf57231d02216a08d0d0c47874cf 100644 (file)
--- 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 (file)
index 0000000..2285997
--- /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<Node> 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 (file)
index 0000000..4281ba6
--- /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 <map>
+
+#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<EagerProofGenerator> d_pfGen;
+  /** Proof node manager */
+  ProofNodeManager* d_pnm;
+};
+
+}  // namespace arith
+}  // namespace theory
+}  // namespace cvc5
+
+#endif