From f5a9b1de720d6c77815ebb0ea9d6e911905885d1 Mon Sep 17 00:00:00 2001 From: Tim King Date: Fri, 3 May 2013 21:55:40 -0400 Subject: [PATCH] Adding cut offs for likely integer infeasible paths. --- src/theory/arith/approx_simplex.cpp | 2 +- src/theory/arith/attempt_solution_simplex.cpp | 4 +- src/theory/arith/soi_simplex.cpp | 6 +-- src/theory/arith/theory_arith_private.cpp | 48 +++++++++++++------ src/theory/arith/theory_arith_private.h | 2 + 5 files changed, 41 insertions(+), 21 deletions(-) diff --git a/src/theory/arith/approx_simplex.cpp b/src/theory/arith/approx_simplex.cpp index 55e52fc53..ef3ea0484 100644 --- a/src/theory/arith/approx_simplex.cpp +++ b/src/theory/arith/approx_simplex.cpp @@ -155,7 +155,7 @@ private: }; #warning "set back to 0" -int ApproxGLPK::s_verbosity = 1; +int ApproxGLPK::s_verbosity = 0; }/* CVC4::theory::arith namespace */ }/* CVC4::theory namespace */ diff --git a/src/theory/arith/attempt_solution_simplex.cpp b/src/theory/arith/attempt_solution_simplex.cpp index c8d5b6f68..9db56ff68 100644 --- a/src/theory/arith/attempt_solution_simplex.cpp +++ b/src/theory/arith/attempt_solution_simplex.cpp @@ -103,12 +103,12 @@ Result::Sat AttemptSolutionSDP::attempt(const ApproximateSimplex::Solution& sol) Assert(toAdd != ARITHVAR_SENTINEL); Trace("arith::forceNewBasis") << toRemove << " " << toAdd << endl; - Message() << toRemove << " " << toAdd << endl; + //Message() << toRemove << " " << toAdd << endl; d_linEq.pivotAndUpdate(toRemove, toAdd, newValues[toRemove]); Trace("arith::forceNewBasis") << needsToBeAdded.size() << "to go" << endl; - Message() << needsToBeAdded.size() << "to go" << endl; + //Message() << needsToBeAdded.size() << "to go" << endl; needsToBeAdded.remove(toAdd); bool conflict = processSignals(); diff --git a/src/theory/arith/soi_simplex.cpp b/src/theory/arith/soi_simplex.cpp index 6095727a3..d7e1808e4 100644 --- a/src/theory/arith/soi_simplex.cpp +++ b/src/theory/arith/soi_simplex.cpp @@ -591,7 +591,7 @@ void SumOfInfeasibilitiesSPD::quickExplain(){ d_qeConflict.clear(); d_errorSet.pushFocusInto(d_qeConflict); - cout << d_qeConflict.size() << " "; + //cout << d_qeConflict.size() << " "; uint32_t size = d_qeConflict.size(); if(size > 2){ @@ -611,7 +611,7 @@ void SumOfInfeasibilitiesSPD::quickExplain(){ d_qeSgns.clear(); } - cout << d_qeConflict.size() << endl; + //cout << d_qeConflict.size() << endl; Assert(d_qeInSoi.empty()); Assert(d_qeInUAndNotInSoi.empty()); @@ -813,7 +813,7 @@ WitnessImprovement SumOfInfeasibilitiesSPD::SOIConflict(){ if(options::soiQuickExplain()){ quickExplain(); Node conflict = generateSOIConflict(d_qeConflict); - cout << conflict << endl; + //cout << conflict << endl; d_conflictChannel(conflict); }else{ diff --git a/src/theory/arith/theory_arith_private.cpp b/src/theory/arith/theory_arith_private.cpp index 504727c0b..08907880e 100644 --- a/src/theory/arith/theory_arith_private.cpp +++ b/src/theory/arith/theory_arith_private.cpp @@ -114,6 +114,7 @@ TheoryArithPrivate::TheoryArithPrivate(TheoryArith& containing, context::Context d_fullCheckCounter(0), d_cutCount(c, 0), d_cutInContext(c), + d_likelyIntegerInfeasible(c, false), d_statistics() { srand(79); @@ -1574,9 +1575,11 @@ bool TheoryArithPrivate::solveRealRelaxation(Theory::Effort effortLevel){ static const int32_t relaxationLimit = 10000; static const int32_t mipLimit = 200000; + //cout << "start" << endl; d_qflraStatus = simplex.findModel(false); + //cout << "end" << endl; if(d_qflraStatus == Result::SAT_UNKNOWN || - (d_qflraStatus == Result::SAT && !hasIntegerModel())){ + (d_qflraStatus == Result::SAT && !hasIntegerModel() && !d_likelyIntegerInfeasible)){ ApproximateSimplex* approxSolver = ApproximateSimplex::mkApproximateSimplexSolver(d_partialModel); approxSolver->setPivotLimit(relaxationLimit); @@ -1588,23 +1591,27 @@ bool TheoryArithPrivate::solveRealRelaxation(Theory::Effort effortLevel){ case ApproximateSimplex::ApproxSat: { relaxSolution = approxSolver->extractRelaxation(); - approxSolver->setPivotLimit(mipLimit); - mipRes = approxSolver->solveMIP(); - d_errorSet.reduceToSignals(); - Message() << "here" << endl; - if(mipRes == ApproximateSimplex::ApproxSat){ - mipSolution = approxSolver->extractMIP(); - d_qflraStatus = d_attemptSolSimplex.attempt(mipSolution); - //d_linEq.applySolution(mipSolution.newBasis, mipSolution.newValues); - }else{ + + if(d_likelyIntegerInfeasible){ d_qflraStatus = d_attemptSolSimplex.attempt(relaxSolution); - //d_linEq.applySolution(relaxSolution.newBasis, relaxSolution.newValues); - // if(d_qflraStatus != UNSAT){ - // d_likelyIntegerUnsat = true; - // } + }else{ + approxSolver->setPivotLimit(mipLimit); + mipRes = approxSolver->solveMIP(); + d_errorSet.reduceToSignals(); + //Message() << "here" << endl; + if(mipRes == ApproximateSimplex::ApproxSat){ + mipSolution = approxSolver->extractMIP(); + d_qflraStatus = d_attemptSolSimplex.attempt(mipSolution); + }else{ + if(mipRes == ApproximateSimplex::ApproxUnsat){ + d_likelyIntegerInfeasible = true; + } + d_qflraStatus = d_attemptSolSimplex.attempt(relaxSolution); + } } options::arithStandardCheckVarOrderPivots.set(pass2Limit); if(d_qflraStatus != Result::UNSAT){ d_qflraStatus = simplex.findModel(false); } + //Message() << "done" << endl; } break; case ApproximateSimplex::ApproxUnsat: @@ -1624,12 +1631,14 @@ bool TheoryArithPrivate::solveRealRelaxation(Theory::Effort effortLevel){ } if(d_qflraStatus == Result::SAT_UNKNOWN){ - Message() << "got sat unknown" << endl; + //Message() << "got sat unknown" << endl; vector toCut = cutAllBounded(); if(toCut.size() > 0){ branchVector(toCut); emmittedConflictOrSplit = true; }else{ + //Message() << "splitting" << endl; + d_qflraStatus = simplex.findModel(noPivotLimit); } } @@ -2659,6 +2668,10 @@ bool TheoryArithPrivate::propagateMightSucceed(ArithVar v, bool ub) const{ ConstraintType t = ub ? UpperBound : LowerBound; const DeltaRational& a = d_partialModel.getAssignment(v); + if(isInteger(v) && !a.isIntegral()){ + return true; + } + Constraint strongestPossible = d_constraintDatabase.getBestImpliedBound(v, t, a); if(strongestPossible == NullConstraint){ return false; @@ -2754,6 +2767,11 @@ bool TheoryArithPrivate::tryToPropagate(RowIndex ridx, bool rowUp, ArithVar v, b d_partialModel.strictlyGreaterThanLowerBound(v, bound); if(weaker){ ConstraintType t = vUb ? UpperBound : LowerBound; + + if(isInteger(v)){ + //cout << "maybe" << endl; + //cout << bound << endl; + } Constraint implied = d_constraintDatabase.getBestImpliedBound(v, t, bound); if(implied != NullConstraint){ return rowImplicationCanBeApplied(ridx, rowUp, implied); diff --git a/src/theory/arith/theory_arith_private.h b/src/theory/arith/theory_arith_private.h index f6fb42a9c..3da064a80 100644 --- a/src/theory/arith/theory_arith_private.h +++ b/src/theory/arith/theory_arith_private.h @@ -570,6 +570,8 @@ private: context::CDO d_cutCount; context::CDHashSet > d_cutInContext; + context::CDO d_likelyIntegerInfeasible; + /** These fields are designed to be accessible to TheoryArith methods. */ class Statistics { public: -- 2.30.2