From: Tim King Date: Thu, 31 Jan 2013 21:34:12 +0000 (-0500) Subject: Adding a heuristic to more eagerly split bounded integer variables. X-Git-Tag: cvc5-1.0.0~7438 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=9d7f0244034f1807e28b8ded23f4d6104ecf5263;p=cvc5.git Adding a heuristic to more eagerly split bounded integer variables. --- 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 lemmas = cutAllBounded(); + //output the lemmas + for(vector::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 TheoryArith::cutAllBounded() const{ + vector 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 cutAllBounded() const; + Node branchIntegerVariable(ArithVar x) const; + /** These fields are designed to be accessible to TheoryArith methods. */ class Statistics { public: