From 29f5a9be53b572d2369d70947942563825c2fa27 Mon Sep 17 00:00:00 2001 From: Tim King Date: Sat, 30 Oct 2010 19:18:36 +0000 Subject: [PATCH] Adds a hueristic from Alberto's thesis. For a fixed window the row count is used to select which non-basic variable is a row in made basic. --- src/theory/arith/row_vector.cpp | 56 +++++++++++++++++++++++++++++---- src/theory/arith/row_vector.h | 37 ++++++---------------- src/theory/arith/simplex.cpp | 56 ++++++++++++++++++++++++++++----- src/theory/arith/simplex.h | 3 +- src/theory/arith/tableau.cpp | 2 +- src/theory/arith/tableau.h | 8 +++++ 6 files changed, 120 insertions(+), 42 deletions(-) diff --git a/src/theory/arith/row_vector.cpp b/src/theory/arith/row_vector.cpp index 6835fc435..f3b979bfd 100644 --- a/src/theory/arith/row_vector.cpp +++ b/src/theory/arith/row_vector.cpp @@ -5,6 +5,31 @@ using namespace CVC4; using namespace CVC4::theory; using namespace CVC4::theory::arith ; +bool RowVector::isSorted(const VarCoeffArray& arr, bool strictlySorted) { + if(arr.size() >= 2){ + NonZeroIterator curr = arr.begin(); + NonZeroIterator end = arr.end(); + ArithVar prev = getArithVar(*curr); + ++curr; + for(;curr != end; ++curr){ + ArithVar v = getArithVar(*curr); + if(strictlySorted && prev > v) return false; + if(!strictlySorted && prev >= v) return false; + prev = v; + } + } + return true; +} + +bool RowVector::noZeroCoefficients(const VarCoeffArray& arr){ + for(NonZeroIterator curr = arr.begin(), end = arr.end(); + curr != end; ++curr){ + const Rational& coeff = getCoefficient(*curr); + if(coeff == 0) return false; + } + return true; +} + void RowVector::zip(const vector< ArithVar >& variables, const vector< Rational >& coefficients, VarCoeffArray& output){ @@ -24,16 +49,26 @@ void RowVector::zip(const vector< ArithVar >& variables, } RowVector::RowVector(const vector< ArithVar >& variables, - const vector< Rational >& coefficients){ + const vector< Rational >& coefficients, + std::vector& counts): + d_rowCount(counts) +{ zip(variables, coefficients, d_entries); std::sort(d_entries.begin(), d_entries.end(), cmp); + for(NonZeroIterator i=beginNonZero(), end=endNonZero(); i != end; ++i){ + ++d_rowCount[getArithVar(*i)]; + } + Assert(isSorted(d_entries, true)); Assert(noZeroCoefficients(d_entries)); } -void RowVector::merge(VarCoeffArray& arr, const VarCoeffArray& other, const Rational& c){ +void RowVector::merge(VarCoeffArray& arr, + const VarCoeffArray& other, + const Rational& c, + std::vector& counts){ VarCoeffArray copy = arr; arr.clear(); @@ -48,12 +83,18 @@ void RowVector::merge(VarCoeffArray& arr, const VarCoeffArray& other, const Rati arr.push_back(*curr1); ++curr1; }else if(getArithVar(*curr1) > getArithVar(*curr2)){ + ++counts[getArithVar(*curr2)]; + arr.push_back( make_pair(getArithVar(*curr2), c * getCoefficient(*curr2))); ++curr2; }else{ Rational res = getCoefficient(*curr1) + c * getCoefficient(*curr2); if(res != 0){ + ++counts[getArithVar(*curr2)]; + arr.push_back(make_pair(getArithVar(*curr1), res)); + }else{ + --counts[getArithVar(*curr2)]; } ++curr1; ++curr2; @@ -64,6 +105,8 @@ void RowVector::merge(VarCoeffArray& arr, const VarCoeffArray& other, const Rati ++curr1; } while(curr2 != end2){ + ++counts[getArithVar(*curr2)]; + arr.push_back(make_pair(getArithVar(*curr2), c * getCoefficient(*curr2))); ++curr2; } @@ -80,7 +123,7 @@ void RowVector::multiply(const Rational& c){ void RowVector::addRowTimesConstant(const Rational& c, const RowVector& other){ Assert(c != 0); - merge(d_entries, other.d_entries, c); + merge(d_entries, other.d_entries, c, d_rowCount); } void RowVector::printRow(){ @@ -93,14 +136,15 @@ void RowVector::printRow(){ ReducedRowVector::ReducedRowVector(ArithVar basic, const vector& variables, - const vector& coefficients): - RowVector(variables, coefficients), d_basic(basic){ + const vector& coefficients, + std::vector& count): + RowVector(variables, coefficients, count), d_basic(basic){ VarCoeffArray justBasic; justBasic.push_back(make_pair(basic, Rational(-1))); - merge(d_entries,justBasic, Rational(1)); + merge(d_entries,justBasic, Rational(1), d_rowCount); Assert(wellFormed()); } diff --git a/src/theory/arith/row_vector.h b/src/theory/arith/row_vector.h index d68f8bc30..efb64d1c7 100644 --- a/src/theory/arith/row_vector.h +++ b/src/theory/arith/row_vector.h @@ -36,34 +36,13 @@ public: * isSorted(arr, strictlySorted) is then equivalent to * If i= 2){ - NonZeroIterator curr = arr.begin(); - NonZeroIterator end = arr.end(); - ArithVar prev = getArithVar(*curr); - ++curr; - for(;curr != end; ++curr){ - ArithVar v = getArithVar(*curr); - if(strictlySorted && prev > v) return false; - if(!strictlySorted && prev >= v) return false; - prev = v; - } - } - return true; - } + static bool isSorted(const VarCoeffArray& arr, bool strictlySorted); /** * noZeroCoefficients(arr) is equivalent to * 0 != getCoefficient(arr[i]) for all i. */ - static bool noZeroCoefficients(const VarCoeffArray& arr){ - for(NonZeroIterator curr = arr.begin(), end = arr.end(); - curr != end; ++curr){ - const Rational& coeff = getCoefficient(*curr); - if(coeff == 0) return false; - } - return true; - } + static bool noZeroCoefficients(const VarCoeffArray& arr); /** * Zips together an array of variables and coefficients and appends @@ -73,7 +52,7 @@ public: const std::vector< Rational >& coefficients, VarCoeffArray& output); - static void merge(VarCoeffArray& arr, const VarCoeffArray& other, const Rational& c); + static void merge(VarCoeffArray& arr, const VarCoeffArray& other, const Rational& c, std::vector& count); protected: @@ -84,6 +63,8 @@ protected: */ VarCoeffArray d_entries; + std::vector& d_rowCount; + NonZeroIterator lower_bound(ArithVar x_j) const{ return std::lower_bound(d_entries.begin(), d_entries.end(), make_pair(x_j,0), cmp); } @@ -92,10 +73,11 @@ protected: public: - RowVector() : d_entries() {} + //RowVector() : d_entries() {} RowVector(const std::vector< ArithVar >& variables, - const std::vector< Rational >& coefficients); + const std::vector< Rational >& coefficients, + std::vector& counts); //Iterates over the nonzero entries in the Vector @@ -154,7 +136,8 @@ public: ReducedRowVector(ArithVar basic, const std::vector< ArithVar >& variables, - const std::vector< Rational >& coefficients); + const std::vector< Rational >& coefficients, + std::vector& count); ArithVar basic() const{ diff --git a/src/theory/arith/simplex.cpp b/src/theory/arith/simplex.cpp index e435fd3dc..e30d935f3 100644 --- a/src/theory/arith/simplex.cpp +++ b/src/theory/arith/simplex.cpp @@ -306,6 +306,9 @@ template ArithVar SimplexDecisionProcedure::selectSlack(ArithVar x_i){ ReducedRowVector* row_i = d_tableau.lookup(x_i); + ArithVar slack = ARITHVAR_SENTINEL; + uint32_t numRows = std::numeric_limits::max(); + for(ReducedRowVector::NonZeroIterator nbi = row_i->beginNonZero(), end = row_i->endNonZero(); nbi != end; ++nbi){ ArithVar nonbasic = getArithVar(*nbi); @@ -315,24 +318,63 @@ ArithVar SimplexDecisionProcedure::selectSlack(ArithVar x_i){ int cmp = a_ij.cmp(d_constants.d_ZERO); if(above){ // beta(x_i) > u_i if( cmp < 0 && d_partialModel.strictlyBelowUpperBound(nonbasic)){ - return nonbasic; + if(d_pivotStage){ + if(d_tableau.getRowCount(nonbasic) < numRows){ + slack = nonbasic; + numRows = d_tableau.getRowCount(nonbasic); + } + }else{ + slack = nonbasic; break; + } }else if( cmp > 0 && d_partialModel.strictlyAboveLowerBound(nonbasic)){ - return nonbasic; + if(d_pivotStage){ + if(d_tableau.getRowCount(nonbasic) < numRows){ + slack = nonbasic; + numRows = d_tableau.getRowCount(nonbasic); + } + }else{ + slack = nonbasic; break; + } } }else{ //beta(x_i) < l_i if(cmp > 0 && d_partialModel.strictlyBelowUpperBound(nonbasic)){ - return nonbasic; - }else if(cmp < 0 && d_partialModel.strictlyAboveLowerBound(nonbasic)){ - return nonbasic; + if(d_pivotStage){ + if(d_tableau.getRowCount(nonbasic) < numRows){ + slack = nonbasic; + numRows = d_tableau.getRowCount(nonbasic); + } + }else{ + slack = nonbasic; break; + } + }else if(cmp < 0 && d_partialModel.strictlyAboveLowerBound(nonbasic)){if(d_pivotStage){ + if(d_tableau.getRowCount(nonbasic) < numRows){ + slack = nonbasic; + numRows = d_tableau.getRowCount(nonbasic); + } + }else{ + slack = nonbasic; break; + } } } } - return ARITHVAR_SENTINEL; + + return slack; } Node SimplexDecisionProcedure::updateInconsistentVars(){ + Node possibleConflict = privateUpdateInconsistentVars(); + Assert(!possibleConflict.isNull() || d_griggioRuleQueue.empty()); + Assert(!possibleConflict.isNull() || d_possiblyInconsistent.empty()); d_pivotStage = true; - return privateUpdateInconsistentVars(); + + while(!d_griggioRuleQueue.empty()){ + d_griggioRuleQueue.pop(); + } + while(!d_possiblyInconsistent.empty()){ + d_possiblyInconsistent.pop(); + } + + return possibleConflict; } //corresponds to Check() in dM06 diff --git a/src/theory/arith/simplex.h b/src/theory/arith/simplex.h index 440d7063c..e753ebc28 100644 --- a/src/theory/arith/simplex.h +++ b/src/theory/arith/simplex.h @@ -75,7 +75,8 @@ public: d_activityMonitor(am), d_out(out), d_tableau(tableau), - d_numVariables(0) + d_numVariables(0), + d_pivotStage(true) {} void increaseMax() {d_numVariables++;} diff --git a/src/theory/arith/tableau.cpp b/src/theory/arith/tableau.cpp index 3c1cd36ba..1d58c5e1d 100644 --- a/src/theory/arith/tableau.cpp +++ b/src/theory/arith/tableau.cpp @@ -34,7 +34,7 @@ void Tableau::addRow(ArithVar basicVar, //The new basic variable cannot already be a basic variable Assert(!isActiveBasicVariable(basicVar)); d_activeBasicVars.insert(basicVar); - ReducedRowVector* row_current = new ReducedRowVector(basicVar,variables, coeffs); + ReducedRowVector* row_current = new ReducedRowVector(basicVar,variables, coeffs,d_rowCount); d_rowsTable[basicVar] = row_current; //A variable in the row may have been made non-basic already. diff --git a/src/theory/arith/tableau.h b/src/theory/arith/tableau.h index 758e5d92d..5e34ac1a2 100644 --- a/src/theory/arith/tableau.h +++ b/src/theory/arith/tableau.h @@ -97,6 +97,8 @@ private: ActivityMonitor& d_activityMonitor; ArithVarDenseSet& d_basicManager; + std::vector d_rowCount; + public: /** * Constructs an empty tableau. @@ -111,6 +113,7 @@ public: void increaseSize(){ d_activeBasicVars.increaseSize(); d_rowsTable.push_back(NULL); + d_rowCount.push_back(0); } ArithVarSet::iterator begin(){ @@ -133,6 +136,11 @@ private: } public: + uint32_t getRowCount(ArithVar x){ + Assert(x < d_rowCount.size()); + return d_rowCount[x]; + } + void addRow(ArithVar basicVar, const std::vector& coeffs, const std::vector& variables); -- 2.30.2