Skip to content

Commit

Permalink
More stable cost function computation, to avoid cycling (#79)
Browse files Browse the repository at this point in the history 
* initial work on sparse matrix representation

* store/restore functionality

* addLastRow functionality

* getRow and getColumn

* column-merging functionality

* added an interface class

* introducing also sparse vectors

* added addLastColumn functionality

* another unittest

* get sparse columns/matrices in dense form

* WIP on storing the constraint matrix inside the tableau in sparse form

* more WIP, fixed a few bugs, still have a couple of failing tests

* fixed some test issues

* initialization

* resize _a along with the rest

* sparse lu factors

* store also the transposed versions of F and V

* starting work on the sparse GE

* some work on changing the values within an existing sparse
representation, needed for sparse factorization.
still WIP

* refactoring and new functionality for CSRMatrix: any kind of
insertions and deletions

* support for empty initialization and counting elements

* sparse GE is now working. minor bug fixes elsewhere

* compute Ft and Vt as part of the G-elimination process

* tests

* basis oracles can return also sparse columns, not just dense

* sparse LU factorization class

* switch to using the sparse factorization in the engine/tableau

* bug fix in mergeColumns, and nicer printing

* bug fix

* bug fix

* bug fix: merging columns does not delete the actual column, just
leaves it empty

* configuration changes

* optimization: since the sparse columns of A are needed all the time,
just compute them once-and-for-all

* a more efficient implementation of sparse vectors

* comments and unit tests

* cleanup

* keep _A in dense column-major format, too, instead of repeatedly
invoking toDense() to gets its columns

* bad deletes

* bug fix in test

* bug fixes: relu constraint propagation, and the handling of merged
variables in the preprocessor

* new test

* compute Ft incrementally, use it whenever sparse columns are required

* did the todo

* valgrind fixes

* debugging

* un-initialized memory

* cleanup

* fixing an issue with cost function degradation

* reinstating the anti-looping trick

* debug prints

* verify invariants

* debug info for crash

* fixing a numerical stability issue
new assertions

* cleanup

* cleanup

* removing the code with the failing assertion

* weaken a couple of too-storng assertions

* bug fix and some fine-tuning of PSE

* bug fix in LU factorization
optimizations to PSE

* WIP

* cleanup

* cleanup

* fine-tuning the computation of basic costs

* more robust comparisons

* more stable cost function computation

* changes to how the cost function is adjusted at the beginning of every
loop, due to degeneracy
  • Loading branch information
@guykatzz
guykatzz authored Jul 26, 2018
1 parent 7680567 commit 361652e
Show file tree
Hide file tree
Showing 8 changed files with 129 additions and 41 deletions.
4 changes: 2 additions & 2 deletions src/configuration/GlobalConfiguration.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -22,8 +22,8 @@ const double GlobalConfiguration::BOUND_COMPARISON_MULTIPLICATIVE_TOLERANCE = 0.
const double GlobalConfiguration::PIVOT_CHANGE_COLUMN_TOLERANCE = 0.000000001;
const double GlobalConfiguration::RATIO_CONSTRAINT_ADDITIVE_TOLERANCE = 0.0000001 * 0.3;
const double GlobalConfiguration::RATIO_CONSTRAINT_MULTIPLICATIVE_TOLERANCE = 0.001 * 0.0000001 * 0.3;
const double GlobalConfiguration::BASIC_COSTS_ADDITIVE_TOLERANCE = 0.0000001 * 0.97;
const double GlobalConfiguration::BASIC_COSTS_MULTIPLICATIVE_TOLERANCE = 0.001 * 0.0000001 * 0.97;
const double GlobalConfiguration::BASIC_COSTS_ADDITIVE_TOLERANCE = 0.0000001;
const double GlobalConfiguration::BASIC_COSTS_MULTIPLICATIVE_TOLERANCE = 0.001 * 0.0000001;
const unsigned GlobalConfiguration::DEGRADATION_CHECKING_FREQUENCY = 100;
const double GlobalConfiguration::DEGRADATION_THRESHOLD = 0.1;
const double GlobalConfiguration::ACCEPTABLE_SIMPLEX_PIVOT_THRESHOLD = 0.0001;
Expand Down
65 changes: 65 additions & 0 deletions src/engine/CostFunctionManager.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -153,6 +153,66 @@ void CostFunctionManager::computeCoreCostFunction()
_costFunctionStatus = ICostFunctionManager::COST_FUNCTION_JUST_COMPUTED;
}

void CostFunctionManager::adjustBasicCostAccuracy()
{
unsigned variable;
double assignment, lb, relaxedLb, ub, relaxedUb;

bool needToRecompute = false;
for ( unsigned i = 0; i < _m; ++i )
{
variable = _tableau->basicIndexToVariable( i );
assignment = _tableau->getBasicAssignment( i );

if ( _basicCosts[i] < 0 )
{
lb = _tableau->getLowerBound( variable );
relaxedLb =
lb -
( GlobalConfiguration::BASIC_COSTS_ADDITIVE_TOLERANCE +
GlobalConfiguration::BASIC_COSTS_MULTIPLICATIVE_TOLERANCE * FloatUtils::abs( lb ) );

// Current basic cost is negative, assignment should be too small
if ( assignment >= relaxedLb )
{
needToRecompute = true;
_basicCosts[i] = 0;
}
}
else if ( _basicCosts[i] > 0 )
{
ub = _tableau->getUpperBound( variable );
relaxedUb =
ub +
( GlobalConfiguration::BASIC_COSTS_ADDITIVE_TOLERANCE +
GlobalConfiguration::BASIC_COSTS_MULTIPLICATIVE_TOLERANCE * FloatUtils::abs( ub ) );

// Current basic cost is positive, assignment should be too large
if ( assignment <= relaxedUb )
{
needToRecompute = true;
_basicCosts[i] = 0;
}
}
else
{
/*
It seems to make sense to adjust anything that had cost 0 but should be
1 or -1, but apparently this leads to cycling.
*/
}

}

if ( needToRecompute )
{
computeMultipliers();
computeReducedCosts();

_costFunctionStatus = ICostFunctionManager::COST_FUNCTION_JUST_COMPUTED;
}
}

void CostFunctionManager::computeBasicOOBCosts()
{
unsigned variable;
Expand Down Expand Up @@ -323,6 +383,11 @@ bool CostFunctionManager::costFunctionJustComputed() const
return _costFunctionStatus == ICostFunctionManager::COST_FUNCTION_JUST_COMPUTED;
}

double CostFunctionManager::getBasicCost( unsigned basicIndex ) const
{
return _basicCosts[basicIndex];
}

//
// Local Variables:
// compile-command: "make -C ../.. "
Expand Down
11 changes: 11 additions & 0 deletions src/engine/CostFunctionManager.h
View file
Original file line number Diff line number Diff line change
Expand Up @@ -62,6 +62,17 @@ class CostFunctionManager : public ICostFunctionManager
const TableauRow *pivotRow,
const double *changeColumn );

/*
Return the basic cost of a basic variable (by index)
*/
double getBasicCost( unsigned basicIndex ) const;

/*
Check whether the basic costs are accurate with respect to the current assignment.
Adjust them and recompute the reduced costs if they are not.
*/
void adjustBasicCostAccuracy();

/*
For debugging purposes: dump the cost function.
*/
Expand Down
2 changes: 2 additions & 0 deletions src/engine/Engine.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -276,6 +276,8 @@ void Engine::performSimplexStep()

if ( _costFunctionManager->costFunctionInvalid() )
_costFunctionManager->computeCoreCostFunction();
else
_costFunctionManager->adjustBasicCostAccuracy();

DEBUG({
// Since we're performing a simplex step, there are out-of-bounds variables.
Expand Down
2 changes: 2 additions & 0 deletions src/engine/ICostFunctionManager.h
View file
Original file line number Diff line number Diff line change
Expand Up @@ -40,6 +40,8 @@ class ICostFunctionManager
double pivotElement,
const TableauRow *pivotRow,
const double *changeColumn ) = 0;
virtual double getBasicCost( unsigned basicIndex ) const = 0;
virtual void adjustBasicCostAccuracy() = 0;

virtual bool costFunctionInvalid() const = 0;
virtual bool costFunctionJustComputed() const = 0;
Expand Down
51 changes: 12 additions & 39 deletions src/engine/Tableau.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -787,16 +787,18 @@ double Tableau::ratioConstraintPerBasic( unsigned basicIndex, double coefficient

ASSERT( !FloatUtils::isZero( coefficient ) );

double basicCost = _costFunctionManager->getBasicCost( basicIndex );

if ( ( FloatUtils::isPositive( coefficient ) && decrease ) ||
( FloatUtils::isNegative( coefficient ) && !decrease ) )
{
// Basic variable is decreasing
double actualLowerBound;
if ( _basicStatus[basicIndex] == BasicStatus::ABOVE_UB )
if ( basicCost > 0 )
{
actualLowerBound = _upperBounds[basic];
}
else if ( _basicStatus[basicIndex] == BasicStatus::BELOW_LB )
else if ( basicCost < 0 )
{
actualLowerBound = FloatUtils::negativeInfinity();
}
Expand Down Expand Up @@ -825,11 +827,11 @@ double Tableau::ratioConstraintPerBasic( unsigned basicIndex, double coefficient
{
// Basic variable is increasing
double actualUpperBound;
if ( _basicStatus[basicIndex] == BasicStatus::BELOW_LB )
if ( basicCost < 0 )
{
actualUpperBound = _lowerBounds[basic];
}
else if ( _basicStatus[basicIndex] == BasicStatus::ABOVE_UB )
else if ( basicCost > 0 )
{
actualUpperBound = FloatUtils::infinity();
}
Expand Down Expand Up @@ -903,7 +905,8 @@ void Tableau::pickLeavingVariable( double *changeColumn )
// constraint.
for ( unsigned i = 0; i < _m; ++i )
{
if ( !FloatUtils::isZero( changeColumn[i], GlobalConfiguration::PIVOT_CHANGE_COLUMN_TOLERANCE ) )
if ( changeColumn[i] >= +GlobalConfiguration::PIVOT_CHANGE_COLUMN_TOLERANCE ||
changeColumn[i] <= -GlobalConfiguration::PIVOT_CHANGE_COLUMN_TOLERANCE )
{
double ratio = ratioConstraintPerBasic( i, changeColumn[i], decrease );

Expand Down Expand Up @@ -933,7 +936,8 @@ void Tableau::pickLeavingVariable( double *changeColumn )
// constraint.
for ( unsigned i = 0; i < _m; ++i )
{
if ( !FloatUtils::isZero( changeColumn[i] ) )
if ( changeColumn[i] >= +GlobalConfiguration::PIVOT_CHANGE_COLUMN_TOLERANCE ||
changeColumn[i] <= -GlobalConfiguration::PIVOT_CHANGE_COLUMN_TOLERANCE )
{
double ratio = ratioConstraintPerBasic( i, changeColumn[i], decrease );

Expand Down Expand Up @@ -1436,6 +1440,8 @@ unsigned Tableau::addEquation( const Equation &equation )
log( "addEquation failed - could not refactorize basis" );
throw ReluplexError( ReluplexError::FAILURE_TO_ADD_NEW_EQUATION );
}

computeCostFunction();
}

return auxVariable;
Expand Down Expand Up @@ -1844,38 +1850,6 @@ void Tableau::updateAssignmentForPivot()

_basicAssignmentStatus = ITableau::BASIC_ASSIGNMENT_UPDATED;

// // If the change ratio is 0, just maintain the current assignment
// if ( FloatUtils::isZero( _changeRatio ) )
// {
// ASSERT( !performingFakePivot() );

// DEBUG({
// // This should only happen when the basic variable is pressed against
// // one of its bounds
// if ( !( _basicStatus[_leavingVariable] == Tableau::AT_UB ||
// _basicStatus[_leavingVariable] == Tableau::AT_LB ||
// _basicStatus[_leavingVariable] == Tableau::BETWEEN
// ) )
// {
// printf( "Assertion violation!\n" );
// printf( "Basic (leaving) variable is: %u\n", _basicIndexToVariable[_leavingVariable] );
// printf( "Basic assignment: %.10lf. Bounds: [%.10lf, %.10lf]\n",
// _basicAssignment[_leavingVariable],
// _lowerBounds[_basicIndexToVariable[_leavingVariable]],
// _upperBounds[_basicIndexToVariable[_leavingVariable]] );
// printf( "Basic status: %u\n", _basicStatus[_leavingVariable] );
// printf( "leavingVariableIncreases = %s", _leavingVariableIncreases ? "yes" : "no" );
// exit( 1 );
// }
// });

// double basicAssignment = _basicAssignment[_leavingVariable];
// double nonBasicAssignment = _nonBasicAssignment[_enteringVariable];
// _basicAssignment[_leavingVariable] = nonBasicAssignment;
// _nonBasicAssignment[_enteringVariable] = basicAssignment;
// return;
// }

if ( performingFakePivot() )
{
// A non-basic is hopping from one bound to the other.
Expand Down Expand Up @@ -2061,7 +2035,6 @@ void Tableau::mergeColumns( unsigned x1, unsigned x2 )
if ( FloatUtils::gt( _lowerBounds[x2], _lowerBounds[x1] ) )
tightenLowerBound( x1, _lowerBounds[x2] );


/*
Merge column x2 of the constraint matrix into x1
and zero-out column x2
Expand Down
11 changes: 11 additions & 0 deletions src/engine/tests/MockCostFunctionManager.h
View file
Original file line number Diff line number Diff line change
Expand Up @@ -102,6 +102,17 @@ class MockCostFunctionManager : public ICostFunctionManager
return 0;
}

Map <unsigned, double> nextBasicCost;
double getBasicCost( unsigned basicIndex ) const
{
TS_ASSERT( nextBasicCost.exists( basicIndex ) );
return nextBasicCost[basicIndex];
}

void adjustBasicCostAccuracy()
{
}

bool costFunctionInvalid() const
{
return true;
Expand Down
24 changes: 24 additions & 0 deletions src/engine/tests/Test_Tableau.h
View file
Original file line number Diff line number Diff line change
Expand Up @@ -368,6 +368,10 @@ class TableauTestSuite : public CxxTest::TestSuite
costFunctionManager.nextCostFunction[2] = -1;
costFunctionManager.nextCostFunction[3] = -1;

costFunctionManager.nextBasicCost[0] = -1;
costFunctionManager.nextBasicCost[1] = 0;
costFunctionManager.nextBasicCost[2] = +1;

tableau->setEnteringVariableIndex( 2u );
TS_ASSERT( hasCandidates( *tableau ) );
TS_ASSERT_EQUALS( tableau->getEnteringVariable(), 2u );
Expand Down Expand Up @@ -470,6 +474,10 @@ class TableauTestSuite : public CxxTest::TestSuite
costFunctionManager.nextCostFunction[2] = -1;
costFunctionManager.nextCostFunction[3] = -1;

costFunctionManager.nextBasicCost[0] = -1;
costFunctionManager.nextBasicCost[1] = 0;
costFunctionManager.nextBasicCost[2] = +1;

tableau->setEnteringVariableIndex( 2u );
TS_ASSERT( hasCandidates( *tableau ) );
TS_ASSERT_EQUALS( tableau->getEnteringVariable(), 2u );
Expand Down Expand Up @@ -528,6 +536,10 @@ class TableauTestSuite : public CxxTest::TestSuite
costFunctionManager.nextCostFunction[2] = -1;
costFunctionManager.nextCostFunction[3] = -1;

costFunctionManager.nextBasicCost[0] = -1;
costFunctionManager.nextBasicCost[1] = 0;
costFunctionManager.nextBasicCost[2] = +1;

tableau->setEnteringVariableIndex( 2u );
TS_ASSERT( hasCandidates( *tableau ) );
TS_ASSERT_EQUALS( tableau->getEnteringVariable(), 2u );
Expand Down Expand Up @@ -669,6 +681,10 @@ class TableauTestSuite : public CxxTest::TestSuite
costFunctionManager.nextCostFunction[2] = -1;
costFunctionManager.nextCostFunction[3] = -1;

costFunctionManager.nextBasicCost[0] = -1;
costFunctionManager.nextBasicCost[1] = 0;
costFunctionManager.nextBasicCost[2] = +1;

tableau->setEnteringVariableIndex( 2u );
TS_ASSERT( hasCandidates( *tableau ) );
TS_ASSERT_EQUALS( tableau->getEnteringVariable(), 2u );
Expand Down Expand Up @@ -1005,6 +1021,10 @@ class TableauTestSuite : public CxxTest::TestSuite
costFunctionManager.nextCostFunction[2] = -1;
costFunctionManager.nextCostFunction[3] = -1;

costFunctionManager.nextBasicCost[0] = -1;
costFunctionManager.nextBasicCost[1] = 0;
costFunctionManager.nextBasicCost[2] = +1;

TS_ASSERT( hasCandidates( *tableau ) );
tableau->setEnteringVariableIndex( 3u );
tableau->computeChangeColumn();
Expand Down Expand Up @@ -1127,6 +1147,10 @@ class TableauTestSuite : public CxxTest::TestSuite
costFunctionManager.nextCostFunction[2] = -1;
costFunctionManager.nextCostFunction[3] = -1;

costFunctionManager.nextBasicCost[0] = -1;
costFunctionManager.nextBasicCost[1] = 0;
costFunctionManager.nextBasicCost[2] = +1;

TS_ASSERT_THROWS_NOTHING( tableau->computeChangeColumn() );
tableau->pickLeavingVariable();

Expand Down

0 comments on commit 361652e

Please sign in to comment.