Adding a heuristic to more eagerly split bounded integer variables.

3 files changed, 108 insertions, 30 deletions

diff --git a/src/theory/arith/options b/src/theory/arith/options
index ab377c8a1..719c826ae 100644
--- a/src/theory/arith/options
+++ b/src/theory/arith/options
@@ -55,4 +55,9 @@ option arithMLTrick --enable-miplib-trick/--disable-miplib-trick bool :default f
  turns on the preprocessing step of attempting to infer bounds on miplib problems
 /turns off the preprocessing step of attempting to infer bounds on miplib problems
 
+option doCutAllBounded --enable-cut-all-bounded/--disable-cut-all-bounded bool :default false :read-write
+ turns on the integer solving step of periodically cutting all integer variables that have both upper and lower bounds
+/ turns off the integer solving step of periodically cutting all integer variables that have both upper and lower bounds
+
+
 endmodule
diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp
index 39ded7991..52f234129 100644
--- a/src/theory/arith/theory_arith.cpp
+++ b/src/theory/arith/theory_arith.cpp
@@ -88,6 +88,7 @@ TheoryArith::TheoryArith(context::Context* c, context::UserContext* u, OutputCha
   d_deltaComputeCallback(this),
   d_basicVarModelUpdateCallBack(d_simplex),
   d_DELTA_ZERO(0),
+  d_fullCheckCounter(0),
   d_statistics()
 {
 }
@@ -1730,6 +1731,20 @@ void TheoryArith::check(Effort effortLevel){
   }
   Assert( d_currentPropagationList.empty());
 
+  if(!emmittedConflictOrSplit && fullEffort(effortLevel)){
+    ++d_fullCheckCounter;
+  }
+  static const int CUT_ALL_BOUNDED_PERIOD = 10;
+  if(!emmittedConflictOrSplit && fullEffort(effortLevel) &&
+     d_fullCheckCounter % CUT_ALL_BOUNDED_PERIOD == 1){
+    vector<Node> lemmas = cutAllBounded();
+    //output the lemmas
+    for(vector<Node>::const_iterator i = lemmas.begin(); i != lemmas.end(); ++i){
+      d_out->lemma(*i);
+      ++(d_statistics.d_externalBranchAndBounds);
+    }
+    emmittedConflictOrSplit = lemmas.size() > 0;
+  }
 
   if(!emmittedConflictOrSplit && fullEffort(effortLevel)){
     emmittedConflictOrSplit = splitDisequalities();
@@ -1776,6 +1791,55 @@ void TheoryArith::check(Effort effortLevel){
   Debug("arith") << "TheoryArith::check end" << std::endl;
 }
 
+Node TheoryArith::branchIntegerVariable(ArithVar x) const {
+  const DeltaRational& d = d_partialModel.getAssignment(x);
+  Assert(!d.isIntegral());
+  const Rational& r = d.getNoninfinitesimalPart();
+  const Rational& i = d.getInfinitesimalPart();
+  Trace("integers") << "integers: assignment to [[" << d_arithvarNodeMap.asNode(x) << "]] is " << r << "[" << i << "]" << endl;
+
+  Assert(! (r.getDenominator() == 1 && i.getNumerator() == 0));
+  Assert(!d.isIntegral());
+  TNode var = d_arithvarNodeMap.asNode(x);
+  Integer floor_d = d.floor();
+
+  Node ub = Rewriter::rewrite(NodeManager::currentNM()->mkNode(kind::LEQ, var, mkRationalNode(floor_d)));
+  Node lb = ub.notNode();
+
+
+  Node lem = NodeManager::currentNM()->mkNode(kind::OR, ub, lb);
+  Trace("integers") << "integers: branch & bound: " << lem << endl;
+  if(d_valuation.isSatLiteral(lem[0])) {
+    Debug("integers") << "    " << lem[0] << " == " << d_valuation.getSatValue(lem[0]) << endl;
+  } else {
+    Debug("integers") << "    " << lem[0] << " is not assigned a SAT literal" << endl;
+  }
+  if(d_valuation.isSatLiteral(lem[1])) {
+    Debug("integers") << "    " << lem[1] << " == " << d_valuation.getSatValue(lem[1]) << endl;
+    } else {
+    Debug("integers") << "    " << lem[1] << " is not assigned a SAT literal" << endl;
+  }
+  return lem;
+}
+
+std::vector<Node> TheoryArith::cutAllBounded() const{
+  vector<Node> lemmas;
+  if(options::doCutAllBounded() && getNumberOfVariables() > 0){
+    for(ArithVar iter = 0; iter != getNumberOfVariables(); ++iter){
+    //Do not include slack variables
+      const DeltaRational& d = d_partialModel.getAssignment(iter);
+      if(isInteger(iter) && !isSlackVariable(iter) &&
+         d_partialModel.hasUpperBound(iter) &&
+         d_partialModel.hasLowerBound(iter) &&
+         !d.isIntegral()){
+        Node lem = branchIntegerVariable(iter);
+        lemmas.push_back(lem);
+      }
+    }
+  }
+  return lemmas;
+}
+
 /** Returns true if the roundRobinBranching() issues a lemma. */
 Node TheoryArith::roundRobinBranch(){
   if(hasIntegerModel()){
@@ -1785,36 +1849,40 @@ Node TheoryArith::roundRobinBranch(){
 
     Assert(isInteger(v));
     Assert(!isSlackVariable(v));
-
-    const DeltaRational& d = d_partialModel.getAssignment(v);
-    const Rational& r = d.getNoninfinitesimalPart();
-    const Rational& i = d.getInfinitesimalPart();
-    Trace("integers") << "integers: assignment to [[" << d_arithvarNodeMap.asNode(v) << "]] is " << r << "[" << i << "]" << endl;
-
-    Assert(! (r.getDenominator() == 1 && i.getNumerator() == 0));
-    Assert(!d.isIntegral());
-
-    TNode var = d_arithvarNodeMap.asNode(v);
-    Integer floor_d = d.floor();
-    Integer ceil_d = d.ceiling();
-
-    Node leq = Rewriter::rewrite(NodeManager::currentNM()->mkNode(kind::LEQ, var, mkRationalNode(floor_d)));
-    Node geq = Rewriter::rewrite(NodeManager::currentNM()->mkNode(kind::GEQ, var, mkRationalNode(ceil_d)));
-
-
-    Node lem = NodeManager::currentNM()->mkNode(kind::OR, leq, geq);
-    Trace("integers") << "integers: branch & bound: " << lem << endl;
-    if(d_valuation.isSatLiteral(lem[0])) {
-      Debug("integers") << "    " << lem[0] << " == " << d_valuation.getSatValue(lem[0]) << endl;
-    } else {
-      Debug("integers") << "    " << lem[0] << " is not assigned a SAT literal" << endl;
-    }
-    if(d_valuation.isSatLiteral(lem[1])) {
-      Debug("integers") << "    " << lem[1] << " == " << d_valuation.getSatValue(lem[1]) << endl;
-    } else {
-      Debug("integers") << "    " << lem[1] << " is not assigned a SAT literal" << endl;
-    }
-    return lem;
+    return branchIntegerVariable(v);
+
+    // Assert(isInteger(v));
+    // Assert(!isSlackVariable(v));
+
+    // const DeltaRational& d = d_partialModel.getAssignment(v);
+    // const Rational& r = d.getNoninfinitesimalPart();
+    // const Rational& i = d.getInfinitesimalPart();
+    // Trace("integers") << "integers: assignment to [[" << d_arithvarNodeMap.asNode(v) << "]] is " << r << "[" << i << "]" << endl;
+
+    // Assert(! (r.getDenominator() == 1 && i.getNumerator() == 0));
+    // Assert(!d.isIntegral());
+
+    // TNode var = d_arithvarNodeMap.asNode(v);
+    // Integer floor_d = d.floor();
+    // Integer ceil_d = d.ceiling();
+
+    // Node leq = Rewriter::rewrite(NodeManager::currentNM()->mkNode(kind::LEQ, var, mkRationalNode(floor_d)));
+    // Node geq = Rewriter::rewrite(NodeManager::currentNM()->mkNode(kind::GEQ, var, mkRationalNode(ceil_d)));
+
+
+    // Node lem = NodeManager::currentNM()->mkNode(kind::OR, leq, geq);
+    // Trace("integers") << "integers: branch & bound: " << lem << endl;
+    // if(d_valuation.isSatLiteral(lem[0])) {
+    //   Debug("integers") << "    " << lem[0] << " == " << d_valuation.getSatValue(lem[0]) << endl;
+    // } else {
+    //   Debug("integers") << "    " << lem[0] << " is not assigned a SAT literal" << endl;
+    // }
+    // if(d_valuation.isSatLiteral(lem[1])) {
+    //   Debug("integers") << "    " << lem[1] << " == " << d_valuation.getSatValue(lem[1]) << endl;
+    // } else {
+    //   Debug("integers") << "    " << lem[1] << " is not assigned a SAT literal" << endl;
+    // }
+    // return lem;
   }
 }
 
diff --git a/src/theory/arith/theory_arith.h b/src/theory/arith/theory_arith.h
index 7d1150fb1..31f9bfcaf 100644
--- a/src/theory/arith/theory_arith.h
+++ b/src/theory/arith/theory_arith.h
@@ -537,6 +537,11 @@ private:
   /** Debugging only routine. Prints the model. */
   void debugPrintModel();
 
+  /** Counts the number of fullCheck calls to arithmetic. */
+  uint32_t d_fullCheckCounter;
+  std::vector<Node> cutAllBounded() const;
+  Node branchIntegerVariable(ArithVar x) const;
+
   /** These fields are designed to be accessible to TheoryArith methods. */
   class Statistics {
   public: