Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Steepest edge #1

Merged
merged 32 commits into from
Jul 31, 2017
Merged
Show file tree
Hide file tree
Changes from 28 commits
Commits
Show all changes
32 commits
Select commit Hold shift + click to select a range
ff0520a
Skeleton code for steepest edge pivot selection (SteepestEdge.*)
rachellim Jul 13, 2017
73f5f74
Started writing code for steepest edge, with placeholder functions an…
rachellim Jul 13, 2017
8c82523
Merge branch 'master' of https://github.com/guykatzz/Marabou
rachellim Jul 13, 2017
0e5ff0c
Have logic for computing max (squared) gradient, need to implement ge…
rachellim Jul 13, 2017
f27acfc
Added skeleton code for initializing and updating gamma values in tab…
rachellim Jul 14, 2017
e50b626
Added a test for init gamma
rachellim Jul 15, 2017
49086e4
Started implementing update for gamma
rachellim Jul 17, 2017
7dcaa4c
Trying to debug update gamma function
rachellim Jul 17, 2017
0e7c5ba
Gamma update worked for lp feasible 2. Figure out why / what cases ga…
rachellim Jul 18, 2017
6d1715c
Seems to work for regress cases (computed manually what gamma should …
rachellim Jul 18, 2017
ce1d86a
Wrote tests on update function (verified by checking against manually…
rachellim Jul 19, 2017
1bf3749
Fixed up tests for update
rachellim Jul 19, 2017
225d546
Added test for selection rule
rachellim Jul 19, 2017
49e6be8
Merge branch 'master' of https://github.com/guykatzz/Marabou
rachellim Jul 19, 2017
184017f
Have logic for computing max (squared) gradient, need to implement ge…
rachellim Jul 13, 2017
af17332
Added skeleton code for initializing and updating gamma values in tab…
rachellim Jul 14, 2017
7bef25b
Added a test for init gamma
rachellim Jul 15, 2017
d8839d6
Started implementing update for gamma
rachellim Jul 17, 2017
d5908f9
Trying to debug update gamma function
rachellim Jul 17, 2017
0badbd5
Gamma update worked for lp feasible 2. Figure out why / what cases ga…
rachellim Jul 18, 2017
b6444d5
Seems to work for regress cases (computed manually what gamma should …
rachellim Jul 18, 2017
18cdea7
Wrote tests on update function (verified by checking against manually…
rachellim Jul 19, 2017
e8d3268
Fixed up tests for update
rachellim Jul 19, 2017
3c77698
Added test for selection rule
rachellim Jul 19, 2017
8b15840
Resolved merge/rebase conflicts
rachellim Jul 19, 2017
4c69ef9
Cleaned up comments
rachellim Jul 19, 2017
5bfb1ed
Added updateGamma to degenerate pivots as well
rachellim Jul 19, 2017
cdb3177
minor changes
guykatzz Jul 19, 2017
a3772c2
more minor stuff
guykatzz Jul 19, 2017
05f42cc
Saved wokring variables - work, nu, alpha as permanent so no memory l…
rachellim Jul 31, 2017
0554d5b
Fixed merge conflicts
rachellim Jul 31, 2017
f286005
Merge branch 'master' into steepest-edge
rachellim Jul 31, 2017
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
5 changes: 3 additions & 2 deletions src/reluplex/Engine.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -24,7 +24,8 @@ Engine::Engine()
_smtCore.setStatistics( &_statistics );
_tableau->setStatistics( &_statistics );

_activeEntryStrategy = &_nestedDantzigsRule;
// _activeEntryStrategy = &_nestedDantzigsRule;
_activeEntryStrategy = &_steepestEdgeRule;
}

Engine::~Engine()
Expand Down Expand Up @@ -191,7 +192,7 @@ void Engine::processInputQuery( const InputQuery &inputQuery )
unsigned m = equations.size();
unsigned n = inputQuery.getNumberOfVariables();
_tableau->setDimensions( m, n );

// Current variables are [0,..,n-1], so the next variable is n.
FreshVariables::setNextVariable( n );

Expand Down
4 changes: 3 additions & 1 deletion src/reluplex/Engine.h
Original file line number Diff line number Diff line change
Expand Up @@ -21,6 +21,7 @@
#include "Map.h"
#include "SmtCore.h"
#include "Statistics.h"
#include "SteepestEdge.h"

class InputQuery;
class PiecewiseLinearConstraint;
Expand Down Expand Up @@ -67,7 +68,7 @@ class Engine : public IEngine
void storeTableauState( TableauState &state ) const;
void restoreTableauState( const TableauState &state );

private:
private:
/*
Collect and print various statistics.
*/
Expand Down Expand Up @@ -99,6 +100,7 @@ class Engine : public IEngine
BlandsRule _blandsRule;
DantzigsRule _dantzigsRule;
NestedDantzigsRule _nestedDantzigsRule;
SteepestEdgeRule _steepestEdgeRule;
EntrySelectionStrategy *_activeEntryStrategy;

/*
Expand Down
2 changes: 2 additions & 0 deletions src/reluplex/ITableau.h
Original file line number Diff line number Diff line change
Expand Up @@ -82,6 +82,8 @@ class ITableau
virtual void computeMultipliers() = 0;
virtual void computeReducedCost( unsigned nonBasic ) = 0;
virtual const double *getCostFunction() const = 0;
// TODO: not sure if i'm allowed to add to this virtual class?
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

That's fine

virtual const double *getSteepestEdgeGamma() const = 0;
virtual void dumpCostFunction() const = 0;
virtual void computeD() = 0;
virtual void computeAssignment() = 0;
Expand Down
98 changes: 98 additions & 0 deletions src/reluplex/SteepestEdge.cpp
Original file line number Diff line number Diff line change
@@ -0,0 +1,98 @@
/********************* */
/*! \file SteepestEdge.cpp
** \verbatim
** Top contributors (to current version):
** Rachel Lim
** This file is part of the Marabou project.
** Copyright (c) 2016-2017 by the authors listed in the file AUTHORS
** in the top-level source directory) and their institutional affiliations.
** All rights reserved. See the file COPYING in the top-level source
** directory for licensing information.\endverbatim
**/

#include "FloatUtils.h"
#include "ITableau.h"
#include "ReluplexError.h"
#include "SteepestEdge.h"

bool SteepestEdgeRule::select( ITableau &tableau )
{
/***************************************************************
* Chooses most eligible nonbasic variable xN[q] according
* to steepest edge pivot selection rules.
*
* c[j]**2
* q = arg max -----------
* j in J gamma[j]
*
* where
* J = set of indices of eligible non-basic variables
* c[j] = reduced cost of nonbasic variable j
* gamma[j] = steepest edge weight
*
* Sets entering variable of the tableau to q.
***************************************************************/

// Calculate entire cost function
// TODO: integrate with Duligur's partial pricing?
tableau.computeCostFunction();

List<unsigned> candidates;
tableau.getEntryCandidates( candidates );

if ( candidates.empty() )
return false;

const double *costFunction = tableau.getCostFunction();
const double *gamma = tableau.getSteepestEdgeGamma();

List<unsigned>::const_iterator candidate = candidates.begin();
unsigned maxIndex = *candidate;
double maxValue = computeGradient( *candidate, costFunction, gamma );
++candidate;

while ( candidate != candidates.end() )
{
double contenderValue = computeGradient( *candidate, costFunction, gamma );
if ( FloatUtils::gt( contenderValue, maxValue ) )
{
maxIndex = *candidate;
maxValue = contenderValue;
}
++candidate;
}

tableau.setEnteringVariable( maxIndex );
return true;
}

double SteepestEdgeRule::computeGradient( const unsigned j, const double *c, const double *gamma )
{
/* Computes the (square of the) gradient in the step direction of the
* j-th nonbasic var.
*
* Step direction for candidate j,
* p[j] = [ -inv(B)*AN*e[j]; e[j] ]
* (where e[j] is the j-th standard unit vector)
*
* Let gamma[j] = || p[j] || ** 2
* c'*p[j] c[j]
* Gradient of cost function wrt p[j] = -------- = --------
* ||p[j]|| ||p[j]||
*
* This function returns c[j]**2 / gamma[j]
*
* Note: gamma[j] is costly to compute from scratch, but after each pivot operation, we
* can update gamma more cheaply using a recurrence relation. See Goldfarb and Reid (1977),
* Forrest and Goldfarb (1992).
*/
return (c[j] * c[j]) / gamma[j];
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Are we sure gamma[j] isn't zero?

Copy link
Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

It shouldn't be, because it's the weight of the vector p[j] (the direction the variable x moves in if you increment nonbasic variable Xj). We can add an ASSERT to be sure?

Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Sure, let's add an assert

}

//
// Local Variables:
// compile-command: "make -C .. "
// tags-file-name: "../TAGS"
// c-basic-offset: 4
// End:
//
42 changes: 42 additions & 0 deletions src/reluplex/SteepestEdge.h
Original file line number Diff line number Diff line change
@@ -0,0 +1,42 @@
/********************* */
/*! \file SteepestEdge.h
** \verbatim
** Top contributors (to current version):
** Rachel Lim
** This file is part of the Marabou project.
** Copyright (c) 2016-2017 by the authors listed in the file AUTHORS
** in the top-level source directory) and their institutional affiliations.
** All rights reserved. See the file COPYING in the top-level source
** directory for licensing information.\endverbatim
**/

#ifndef __SteepestEdge_h__
#define __SteepestEdge_h__

#include "EntrySelectionStrategy.h"

class SteepestEdgeRule : public EntrySelectionStrategy
{
public:
/*
Apply steepest edge pivot selection rule: choose the candidate that maximizes the
magnitude of the gradient of the cost function with respect to the step direction.
*/
bool select( ITableau &tableau );

private:
/*
Helper function to compute gradient of cost function with respect to edge direction.
*/
double computeGradient( const unsigned j, const double *c, const double *gamma );
};

#endif // __SteepestEdge_h__

//
// Local Variables:
// compile-command: "make -C .. "
// tags-file-name: "../TAGS"
// c-basic-offset: 4
// End:
//
Loading