Merge pull request #1 from guykatzz/steepest-edge

Steepest edge

src/reluplex/Engine.cpp

@@ -25,7 +25,8 @@ Engine::Engine()
     _tableau->setStatistics( &_statistics );
 
     //    _activeEntryStrategy = &_nestedDantzigsRule;
-    _activeEntryStrategy = &_dantzigsRule;
+    _activeEntryStrategy = &_steepestEdgeRule;
+    // _activeEntryStrategy = &_dantzigsRule;
     // _activeEntryStrategy = &_blandsRule;
 }
 
@@ -213,7 +214,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 );
 

src/reluplex/Engine.h

@@ -22,6 +22,7 @@
 #include "NestedDantzigsRule.h"
 #include "SmtCore.h"
 #include "Statistics.h"
+#include "SteepestEdge.h"
 
 class InputQuery;
 class PiecewiseLinearConstraint;
@@ -68,7 +69,7 @@ class Engine : public IEngine
     void storeTableauState( TableauState &state ) const;
     void restoreTableauState( const TableauState &state );
 
-private:
+private:    
     /*
       Collect and print various statistics.
     */
@@ -100,6 +101,7 @@ class Engine : public IEngine
     BlandsRule _blandsRule;
     DantzigsRule _dantzigsRule;
     NestedDantzigsRule _nestedDantzigsRule;
+    SteepestEdgeRule _steepestEdgeRule;
     EntrySelectionStrategy *_activeEntryStrategy;
 
     /*

src/reluplex/ITableau.h

@@ -85,6 +85,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?
+    virtual const double *getSteepestEdgeGamma() const = 0; 
     virtual void dumpCostFunction() const = 0;
     virtual void computeD() = 0;
     virtual void computeAssignment() = 0;

src/reluplex/SteepestEdge.cpp

@@ -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];
+}
+
+//
+// Local Variables:
+// compile-command: "make -C .. "
+// tags-file-name: "../TAGS"
+// c-basic-offset: 4
+// End:
+//

src/reluplex/SteepestEdge.h

@@ -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:
+//