From: Tim King Date: Thu, 24 Feb 2011 23:00:08 +0000 (+0000) Subject: - Adds an additional round of checks for a conflict after the difference heuristic... X-Git-Tag: cvc5-1.0.0~8693 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=b71b7d0aa648f39ea1243632b5b9867ada53109a;p=cvc5.git - Adds an additional round of checks for a conflict after the difference heuristic round has been completed. This happens immediately before switching to the variable order round. --- diff --git a/src/theory/arith/arith_priority_queue.cpp b/src/theory/arith/arith_priority_queue.cpp index 76db6b580..417115ab9 100644 --- a/src/theory/arith/arith_priority_queue.cpp +++ b/src/theory/arith/arith_priority_queue.cpp @@ -15,10 +15,10 @@ ArithPriorityQueue::ArithPriorityQueue(ArithPartialModel& pm, const Tableau& tab d_partialModel(pm), d_tableau(tableau), d_modeInUse(Collection), d_ZERO_DELTA(0,0) {} -ArithVar ArithPriorityQueue::popInconsistentBasicVariable(){ +ArithVar ArithPriorityQueue::dequeueInconsistentBasicVariable(){ AlwaysAssert(!inCollectionMode()); - Debug("arith_update") << "popInconsistentBasicVariable()" << endl; + Debug("arith_update") << "dequeueInconsistentBasicVariable()" << endl; if(inDifferenceMode()){ while(!d_diffQueue.empty()){ diff --git a/src/theory/arith/arith_priority_queue.h b/src/theory/arith/arith_priority_queue.h index 9cee8b29b..2f150b73a 100644 --- a/src/theory/arith/arith_priority_queue.h +++ b/src/theory/arith/arith_priority_queue.h @@ -116,7 +116,7 @@ public: ArithPriorityQueue(ArithPartialModel& pm, const Tableau& tableau); - ArithVar popInconsistentBasicVariable(); + ArithVar dequeueInconsistentBasicVariable(); void enqueueIfInconsistent(ArithVar basic); diff --git a/src/theory/arith/simplex.cpp b/src/theory/arith/simplex.cpp index ced76c843..25d154bae 100644 --- a/src/theory/arith/simplex.cpp +++ b/src/theory/arith/simplex.cpp @@ -15,11 +15,13 @@ SimplexDecisionProcedure::Statistics::Statistics(): d_statAssertUpperConflicts("theory::arith::AssertUpperConflicts", 0), d_statAssertLowerConflicts("theory::arith::AssertLowerConflicts", 0), d_statUpdateConflicts("theory::arith::UpdateConflicts", 0), - d_statEarlyConflicts("theory::arith::EarlyConflicts", 0), - d_statEarlyConflictImprovements("theory::arith::EarlyConflictImprovements", 0), - d_selectInitialConflictTime("theory::arith::selectInitialConflictTime"), - d_pivotsAfterConflict("theory::arith::pivotsAfterConflict", 0), - d_checksWithWastefulPivots("theory::arith::checksWithWastefulPivots", 0), + d_findConflictOnTheQueueTime("theory::arith::findConflictOnTheQueueTime"), + d_attemptBeforeDiffSearch("theory::arith::attemptBeforeDiffSearch",0), + d_successBeforeDiffSearch("theory::arith::successBeforeDiffSearch",0), + d_attemptAfterDiffSearch("theory::arith::attemptAfterDiffSearch",0), + d_successAfterDiffSearch("theory::arith::successAfterDiffSearch",0), + d_attemptDuringVarOrderSearch("theory::arith::attemptDuringVarOrderSearch",0), + d_successDuringVarOrderSearch("theory::arith::successDuringVarOrderSearch",0), d_pivotTime("theory::arith::pivotTime"), d_avgNumRowsNotContainingOnUpdate("theory::arith::avgNumRowsNotContainingOnUpdate"), d_avgNumRowsNotContainingOnPivot("theory::arith::avgNumRowsNotContainingOnPivot") @@ -29,12 +31,16 @@ SimplexDecisionProcedure::Statistics::Statistics(): StatisticsRegistry::registerStat(&d_statAssertUpperConflicts); StatisticsRegistry::registerStat(&d_statAssertLowerConflicts); StatisticsRegistry::registerStat(&d_statUpdateConflicts); - StatisticsRegistry::registerStat(&d_statEarlyConflicts); - StatisticsRegistry::registerStat(&d_statEarlyConflictImprovements); - StatisticsRegistry::registerStat(&d_selectInitialConflictTime); - StatisticsRegistry::registerStat(&d_pivotsAfterConflict); - StatisticsRegistry::registerStat(&d_checksWithWastefulPivots); + StatisticsRegistry::registerStat(&d_findConflictOnTheQueueTime); + + StatisticsRegistry::registerStat(&d_attemptBeforeDiffSearch); + StatisticsRegistry::registerStat(&d_successBeforeDiffSearch); + StatisticsRegistry::registerStat(&d_attemptAfterDiffSearch); + StatisticsRegistry::registerStat(&d_successAfterDiffSearch); + StatisticsRegistry::registerStat(&d_attemptDuringVarOrderSearch); + StatisticsRegistry::registerStat(&d_successDuringVarOrderSearch); + StatisticsRegistry::registerStat(&d_pivotTime); StatisticsRegistry::registerStat(&d_avgNumRowsNotContainingOnUpdate); @@ -47,12 +53,16 @@ SimplexDecisionProcedure::Statistics::~Statistics(){ StatisticsRegistry::unregisterStat(&d_statAssertUpperConflicts); StatisticsRegistry::unregisterStat(&d_statAssertLowerConflicts); StatisticsRegistry::unregisterStat(&d_statUpdateConflicts); - StatisticsRegistry::unregisterStat(&d_statEarlyConflicts); - StatisticsRegistry::unregisterStat(&d_statEarlyConflictImprovements); - StatisticsRegistry::unregisterStat(&d_selectInitialConflictTime); - StatisticsRegistry::unregisterStat(&d_pivotsAfterConflict); - StatisticsRegistry::unregisterStat(&d_checksWithWastefulPivots); + StatisticsRegistry::unregisterStat(&d_findConflictOnTheQueueTime); + + StatisticsRegistry::unregisterStat(&d_attemptBeforeDiffSearch); + StatisticsRegistry::unregisterStat(&d_successBeforeDiffSearch); + StatisticsRegistry::unregisterStat(&d_attemptAfterDiffSearch); + StatisticsRegistry::unregisterStat(&d_successAfterDiffSearch); + StatisticsRegistry::unregisterStat(&d_attemptDuringVarOrderSearch); + StatisticsRegistry::unregisterStat(&d_successDuringVarOrderSearch); + StatisticsRegistry::unregisterStat(&d_pivotTime); StatisticsRegistry::unregisterStat(&d_avgNumRowsNotContainingOnUpdate); @@ -299,13 +309,6 @@ void SimplexDecisionProcedure::pivotAndUpdate(ArithVar x_i, ArithVar x_j, DeltaR // Pivots ++(d_statistics.d_statPivots); - if( d_foundAConflict ){ - ++d_pivotsSinceConflict; - if(d_pivotsSinceConflict == 1){ - ++(d_statistics.d_checksWithWastefulPivots); - } - ++(d_statistics.d_pivotsAfterConflict); - } Assert(d_tableau.getNumRows() >= d_tableau.getRowCount(x_j)); double difference = ((double)d_tableau.getNumRows()) - ((double) d_tableau.getRowCount(x_j)); @@ -315,34 +318,19 @@ void SimplexDecisionProcedure::pivotAndUpdate(ArithVar x_i, ArithVar x_j, DeltaR d_queue.enqueueIfInconsistent(x_j); - // Debug found conflict - if( !d_foundAConflict ){ - DeltaRational beta_j = d_partialModel.getAssignment(x_j); - - if(d_partialModel.belowLowerBound(x_j, beta_j, true)){ - if(selectSlackBelow(x_j) == ARITHVAR_SENTINEL ){ - d_foundAConflict = true; - } - }else if(d_partialModel.aboveUpperBound(x_j, beta_j, true)){ - if(selectSlackAbove(x_j) == ARITHVAR_SENTINEL ){ - d_foundAConflict = true; - } - } - } - if(Debug.isOn("tableau")){ d_tableau.printTableau(); } } template -ArithVar SimplexDecisionProcedure::selectSlack(ArithVar x_i){ +ArithVar SimplexDecisionProcedure::selectSlack(ArithVar x_i, bool first){ ReducedRowVector& row_i = d_tableau.lookup(x_i); ArithVar slack = ARITHVAR_SENTINEL; uint32_t numRows = std::numeric_limits::max(); - bool pivotStage = d_queue.inDifferenceMode(); + bool pivotStage = !first; for(ReducedRowVector::NonZeroIterator nbi = row_i.beginNonZero(), end = row_i.endNonZero(); nbi != end; ++nbi){ @@ -404,12 +392,16 @@ Node betterConflict(TNode x, TNode y){ else return y; } -Node SimplexDecisionProcedure::selectInitialConflict() { - Node bestConflict = Node::null(); +Node SimplexDecisionProcedure::findConflictOnTheQueue(SearchPeriod type) { + TimerStat::CodeTimer codeTimer(d_statistics.d_findConflictOnTheQueueTime); - TimerStat::CodeTimer codeTimer(d_statistics.d_selectInitialConflictTime); + switch(type){ + case BeforeDiffSearch: ++(d_statistics.d_attemptBeforeDiffSearch); break; + case AfterDiffSearch: ++(d_statistics.d_attemptAfterDiffSearch); break; + case DuringVarOrderSearch: ++(d_statistics.d_attemptDuringVarOrderSearch); break; + } - int conflictChanges = 0; + Node bestConflict = Node::null(); ArithPriorityQueue::const_iterator i = d_queue.begin(); ArithPriorityQueue::const_iterator end = d_queue.end(); for(; i != end; ++i){ @@ -418,18 +410,18 @@ Node SimplexDecisionProcedure::selectInitialConflict() { if(d_tableau.isBasic(x_i)){ Node possibleConflict = checkBasicForConflict(x_i); if(!possibleConflict.isNull()){ - Node better = betterConflict(bestConflict, possibleConflict); - if(better != bestConflict){ - ++conflictChanges; - } - bestConflict = better; - ++(d_statistics.d_statEarlyConflicts); + bestConflict = betterConflict(bestConflict, possibleConflict); } } } - - if(conflictChanges > 1) ++(d_statistics.d_statEarlyConflictImprovements); + if(!bestConflict.isNull()){ + switch(type){ + case BeforeDiffSearch: ++(d_statistics.d_successBeforeDiffSearch); break; + case AfterDiffSearch: ++(d_statistics.d_successAfterDiffSearch); break; + case DuringVarOrderSearch: ++(d_statistics.d_successDuringVarOrderSearch); break; + } + } return bestConflict; } @@ -438,19 +430,18 @@ Node SimplexDecisionProcedure::updateInconsistentVars(){ return Node::null(); } - d_foundAConflict = false; - d_pivotsSinceConflict = 0; - d_queue.transitionToDifferenceMode(); Node possibleConflict = Node::null(); if(d_queue.size() > 1){ - possibleConflict = selectInitialConflict(); + possibleConflict = findConflictOnTheQueue(BeforeDiffSearch); } if(possibleConflict.isNull()){ possibleConflict = searchForFeasibleSolution(d_numVariables + 1); } - + if(d_queue.size() > 1 && possibleConflict.isNull()){ + possibleConflict = findConflictOnTheQueue(AfterDiffSearch); + } if(!d_queue.empty() && possibleConflict.isNull()){ d_queue.transitionToVariableOrderMode(); possibleConflict = searchForFeasibleSolution(0); @@ -477,12 +468,12 @@ Node SimplexDecisionProcedure::checkBasicForConflict(ArithVar basic){ const DeltaRational& beta = d_partialModel.getAssignment(basic); if(d_partialModel.belowLowerBound(basic, beta, true)){ - ArithVar x_j = selectSlackBelow(basic); + ArithVar x_j = selectSlackBelow(basic, true); if(x_j == ARITHVAR_SENTINEL ){ return generateConflictBelow(basic); } }else if(d_partialModel.aboveUpperBound(basic, beta, true)){ - ArithVar x_j = selectSlackAbove(basic); + ArithVar x_j = selectSlackAbove(basic, true); if(x_j == ARITHVAR_SENTINEL ){ return generateConflictAbove(basic); } @@ -495,10 +486,12 @@ template Node SimplexDecisionProcedure::searchForFeasibleSolution(uint32_t remainingIterations){ Debug("arith") << "updateInconsistentVars" << endl; + static const uint32_t CHECK_PERIOD = 1000; + while(!limitIterations || remainingIterations > 0){ if(Debug.isOn("paranoid:check_tableau")){ checkTableau(); } - ArithVar x_i = d_queue.popInconsistentBasicVariable(); + ArithVar x_i = d_queue.dequeueInconsistentBasicVariable(); Debug("arith::update::select") << "selectSmallestInconsistentVar()=" << x_i << endl; if(x_i == ARITHVAR_SENTINEL){ Debug("arith_update") << "No inconsistent variables" << endl; @@ -511,7 +504,7 @@ Node SimplexDecisionProcedure::searchForFeasibleSolution(uint32_t remainingItera ArithVar x_j = ARITHVAR_SENTINEL; if(d_partialModel.belowLowerBound(x_i, beta_i, true)){ - x_j = selectSlackBelow(x_i); + x_j = selectSlackBelow(x_i, !limitIterations); if(x_j == ARITHVAR_SENTINEL ){ ++(d_statistics.d_statUpdateConflicts); return generateConflictBelow(x_i); //unsat @@ -520,7 +513,7 @@ Node SimplexDecisionProcedure::searchForFeasibleSolution(uint32_t remainingItera pivotAndUpdate(x_i, x_j, l_i); }else if(d_partialModel.aboveUpperBound(x_i, beta_i, true)){ - x_j = selectSlackAbove(x_i); + x_j = selectSlackAbove(x_i, !limitIterations); if(x_j == ARITHVAR_SENTINEL ){ ++(d_statistics.d_statUpdateConflicts); return generateConflictAbove(x_i); //unsat @@ -534,6 +527,13 @@ Node SimplexDecisionProcedure::searchForFeasibleSolution(uint32_t remainingItera if(!earlyConflict.isNull()){ return earlyConflict; } + //Once every CHECK_PERIOD examine the entire queue for conflicts + // if(!limitIterations && remainingIterations % CHECK_PERIOD == 0){ + // Node earlyConflict = findConflictOnTheQueue(DuringVarOrderSearch); + // if(!earlyConflict.isNull()){ + // return earlyConflict; + // } + // } } AlwaysAssert(limitIterations && remainingIterations == 0); @@ -646,23 +646,6 @@ DeltaRational SimplexDecisionProcedure::computeRowValue(ArithVar x, bool useSafe return sum; } -/* -void SimplexDecisionProcedure::checkBasicVariable(ArithVar basic){ - Assert(d_tableau.isBasic(basic)); - if(!d_partialModel.assignmentIsConsistent(basic)){ - if(d_pivotStage){ - const DeltaRational& beta = d_partialModel.getAssignment(basic); - DeltaRational diff = d_partialModel.belowLowerBound(basic,beta,true) ? - d_partialModel.getLowerBound(basic) - beta: - beta - d_partialModel.getUpperBound(basic); - d_griggioRuleQueue.push(make_pair(basic,diff)); - }else{ - d_possiblyInconsistent.push(basic); - } - } -} -*/ - /** * This check is quite expensive. * It should be wrapped in a Debug.isOn() guard. diff --git a/src/theory/arith/simplex.h b/src/theory/arith/simplex.h index 9fed7dc0b..3b86935bd 100644 --- a/src/theory/arith/simplex.h +++ b/src/theory/arith/simplex.h @@ -108,7 +108,9 @@ public: private: template Node searchForFeasibleSolution(uint32_t maxIterations); - Node selectInitialConflict(); + enum SearchPeriod {BeforeDiffSearch, AfterDiffSearch, DuringVarOrderSearch}; + + Node findConflictOnTheQueue(SearchPeriod period); private: /** @@ -117,16 +119,22 @@ private: * in the tableau that can "take up the slack" to let x_i satisfy its bounds. * This returns TNode::null() if none exists. * + * If first is true, return the first ArithVar in the row to satisfy these conditions. + * If first is false, return the ArithVar with the smallest row count. + * * More formally one of the following conditions must be satisfied: * - above && a_ij < 0 && assignment(x_j) < upperbound(x_j) * - above && a_ij > 0 && assignment(x_j) > lowerbound(x_j) * - !above && a_ij > 0 && assignment(x_j) < upperbound(x_j) * - !above && a_ij < 0 && assignment(x_j) > lowerbound(x_j) */ - template ArithVar selectSlack(ArithVar x_i); - - ArithVar selectSlackBelow(ArithVar x_i) { return selectSlack(x_i); } - ArithVar selectSlackAbove(ArithVar x_i) { return selectSlack(x_i); } + template ArithVar selectSlack(ArithVar x_i, bool first); + ArithVar selectSlackBelow(ArithVar x_i, bool first) { + return selectSlack(x_i, first); + } + ArithVar selectSlackAbove(ArithVar x_i, bool first) { + return selectSlack(x_i, first); + } /** * Returns the smallest basic variable whose assignment is not consistent * with its upper and lower bounds. @@ -166,9 +174,6 @@ private: */ Node checkBasicForConflict(ArithVar b); - bool d_foundAConflict; // This field is used for statistics keeping ONLY! - unsigned d_pivotsSinceConflict; // This field is used for statistics keeping ONLY! - /** These fields are designed to be accessable to TheoryArith methods. */ class Statistics { public: @@ -176,11 +181,13 @@ private: IntStat d_statAssertUpperConflicts, d_statAssertLowerConflicts; IntStat d_statUpdateConflicts; - IntStat d_statEarlyConflicts, d_statEarlyConflictImprovements; - TimerStat d_selectInitialConflictTime; + TimerStat d_findConflictOnTheQueueTime; + + IntStat d_attemptBeforeDiffSearch, d_successBeforeDiffSearch; + IntStat d_attemptAfterDiffSearch, d_successAfterDiffSearch; + IntStat d_attemptDuringVarOrderSearch, d_successDuringVarOrderSearch; - IntStat d_pivotsAfterConflict, d_checksWithWastefulPivots; TimerStat d_pivotTime; AverageStat d_avgNumRowsNotContainingOnUpdate;