Backward analysis (#760)

* Backward analysis

* change log

CHANGELOG.md

@@ -2,15 +2,18 @@
 
 ## Next Release
 
+* Changes in core solving module:
+  - Added proof producing versions of `Sign`, `Max`, `Absolute Value` and `Disjunction` constraints.
+  - Added support for `LeakyRelu`, `Clip`, `Round`, `Softmax`.
+  - Added support for forward-backward abstract interpretation.
+
 * Dependency changes:
   - Dropped support for Python 3.7
   - Now use ONNX 1.15.0 (up from 1.12.0) in both C++ and Python backends.
   - The class `MarabouONNXNetwork` no longer depends on `torch` in Python backend.
 
 * Marabou now prints errors on `stderr` rather than `stdout`
 
-* Added proof producing versions of `Sign`, `Max`, `Absolute Value` and `Disjunction` constraints.
-
 * Changes to command-line ONNX support:
   - Fixed bug with variable lower bounds not being set correctly.
   - Fixed bug with sigmoid operators not being parsed correctly.

src/common/GurobiWrapper.cpp

@@ -93,7 +93,6 @@ void GurobiWrapper::resetModel()
 
 void GurobiWrapper::reset()
 {
-    _nameToVariable.clear();
     _model->reset();
 }
 

src/common/GurobiWrapper.h

@@ -148,6 +148,11 @@ class GurobiWrapper
         _model->getEnv().set( GRB_IntParam_OutputFlag, verbosity );
     }
 
+    inline bool containsVariable( String name ) const
+    {
+        return _nameToVariable.exists( name );
+    }
+
     // Set number of threads
     inline void setNumberOfThreads( unsigned threads )
     {
@@ -345,6 +350,10 @@ class GurobiWrapper
     };
     void setTimeLimit( double ){};
     void setVerbosity( unsigned ){};
+    bool containsVariable( String /*name*/ ) const
+    {
+        return false;
+    };
     void setNumberOfThreads( unsigned ){};
     void nonConvex(){};
     double getObjectiveBound()

src/configuration/GlobalConfiguration.cpp

@@ -114,6 +114,9 @@ const double GlobalConfiguration::MINIMAL_COEFFICIENT_FOR_TIGHTENING = 0.01;
 const double GlobalConfiguration::LEMMA_CERTIFICATION_TOLERANCE = 0.000001;
 const bool GlobalConfiguration::WRITE_JSON_PROOF = false;
 
+const unsigned GlobalConfiguration::BACKWARD_BOUND_PROPAGATION_DEPTH = 3;
+const unsigned GlobalConfiguration::MAX_ROUNDS_OF_BACKWARD_ANALYSIS = 10;
+
 #ifdef ENABLE_GUROBI
 const unsigned GlobalConfiguration::GUROBI_NUMBER_OF_THREADS = 1;
 const bool GlobalConfiguration::GUROBI_LOGGING = false;

src/configuration/GlobalConfiguration.h

@@ -249,6 +249,14 @@ class GlobalConfiguration
      */
     static const bool WRITE_JSON_PROOF;
 
+    /* How many layers after the current layer do we encode in backward analysis.
+     */
+    static const unsigned BACKWARD_BOUND_PROPAGATION_DEPTH;
+
+    /* How many rounds of backward analysis to perform?
+     */
+    static const unsigned MAX_ROUNDS_OF_BACKWARD_ANALYSIS;
+
 #ifdef ENABLE_GUROBI
     /*
       The number of threads Gurobi spawns

src/configuration/OptionParser.cpp

@@ -255,7 +255,8 @@ void OptionParser::initialize()
             boost::program_options::value<std::string>(
                 &( ( *_stringOptions )[Options::MILP_SOLVER_BOUND_TIGHTENING_TYPE] ) )
                 ->default_value( ( *_stringOptions )[Options::MILP_SOLVER_BOUND_TIGHTENING_TYPE] ),
-            "The MILP solver bound tightening type: lp/lp-inc/milp/milp-inc/iter-prop/none." )
+            "The MILP solver bound tightening type: "
+            "lp/fb-once/fb-converge/lp-inc/milp/milp-inc/iter-prop/none." )
 #endif
         ;
 

src/configuration/Options.cpp

@@ -201,6 +201,10 @@ MILPSolverBoundTighteningType Options::getMILPSolverBoundTighteningType() const
             return MILPSolverBoundTighteningType::LP_RELAXATION;
         else if ( strategyString == "lp-inc" )
             return MILPSolverBoundTighteningType::LP_RELAXATION_INCREMENTAL;
+        if ( strategyString == "backward-once" )
+            return MILPSolverBoundTighteningType::BACKWARD_ANALYSIS_ONCE;
+        if ( strategyString == "backward-converge" )
+            return MILPSolverBoundTighteningType::BACKWARD_ANALYSIS_CONVERGE;
         else if ( strategyString == "milp" )
             return MILPSolverBoundTighteningType::MILP_ENCODING;
         else if ( strategyString == "milp-inc" )

src/engine/Engine.cpp

@@ -198,6 +198,9 @@ bool Engine::solve( unsigned timeoutInSeconds )
     for ( auto &nlConstraint : _nlConstraints )
         nlConstraint->registerBoundManager( &_boundManager );
 
+    // Before encoding, make sure all valid constraints are applied.
+    applyAllValidConstraintCaseSplits();
+
     if ( _solveWithMILP )
         return solveWithMILPEncoding( timeoutInSeconds );
 
@@ -223,8 +226,6 @@ bool Engine::solve( unsigned timeoutInSeconds )
         printf( "\n---\n" );
     }
 
-    applyAllValidConstraintCaseSplits();
-
     bool splitJustPerformed = true;
     struct timespec mainLoopStart = TimeUtils::sampleMicro();
     while ( true )
@@ -914,6 +915,7 @@ bool Engine::calculateBounds( InputQuery &inputQuery )
         performSymbolicBoundTightening( &( *_preprocessedQuery ) );
         performSimulation();
         performMILPSolverBoundedTightening( &( *_preprocessedQuery ) );
+        performAdditionalBackwardAnalysisIfNeeded();
 
         if ( _networkLevelReasoner && Options::get()->getBool( Options::DUMP_BOUNDS ) )
             _networkLevelReasoner->dumpBounds();
@@ -1390,6 +1392,7 @@ void Engine::initializeNetworkLevelReasoning()
 
     if ( _networkLevelReasoner )
     {
+        _networkLevelReasoner->computeSuccessorLayers();
         _networkLevelReasoner->setTableau( _tableau );
         if ( Options::get()->getBool( Options::DUMP_TOPOLOGY ) )
         {
@@ -1417,6 +1420,7 @@ bool Engine::processInputQuery( InputQuery &inputQuery, bool preprocess )
             performSymbolicBoundTightening( &( *_preprocessedQuery ) );
             performSimulation();
             performMILPSolverBoundedTightening( &( *_preprocessedQuery ) );
+            performAdditionalBackwardAnalysisIfNeeded();
         }
 
         if ( GlobalConfiguration::PL_CONSTRAINTS_ADD_AUX_EQUATIONS_AFTER_PREPROCESSING )
@@ -1576,19 +1580,19 @@ void Engine::performMILPSolverBoundedTightening( InputQuery *inputQuery )
 
         // TODO: Remove this block after getting ready to support sigmoid with MILP Bound
         // Tightening.
-        if ( Options::get()->getMILPSolverBoundTighteningType() !=
-                 MILPSolverBoundTighteningType::NONE &&
+        if ( _milpSolverBoundTighteningType != MILPSolverBoundTighteningType::NONE &&
              _preprocessedQuery->getNonlinearConstraints().size() > 0 )
             throw MarabouError( MarabouError::FEATURE_NOT_YET_SUPPORTED,
                                 "Marabou doesn't support sigmoid with MILP Bound Tightening" );
 
-        switch ( Options::get()->getMILPSolverBoundTighteningType() )
+        switch ( _milpSolverBoundTighteningType )
         {
         case MILPSolverBoundTighteningType::LP_RELAXATION:
         case MILPSolverBoundTighteningType::LP_RELAXATION_INCREMENTAL:
+        case MILPSolverBoundTighteningType::BACKWARD_ANALYSIS_ONCE:
+        case MILPSolverBoundTighteningType::BACKWARD_ANALYSIS_CONVERGE:
             _networkLevelReasoner->lpRelaxationPropagation();
             break;
-
         case MILPSolverBoundTighteningType::MILP_ENCODING:
         case MILPSolverBoundTighteningType::MILP_ENCODING_INCREMENTAL:
             _networkLevelReasoner->MILPPropagation();
@@ -1631,12 +1635,34 @@ void Engine::performMILPSolverBoundedTightening( InputQuery *inputQuery )
     }
 }
 
+void Engine::performAdditionalBackwardAnalysisIfNeeded()
+{
+    if ( _milpSolverBoundTighteningType == MILPSolverBoundTighteningType::BACKWARD_ANALYSIS_ONCE ||
+         _milpSolverBoundTighteningType ==
+             MILPSolverBoundTighteningType::BACKWARD_ANALYSIS_CONVERGE )
+    {
+        unsigned tightened = performSymbolicBoundTightening( &( *_preprocessedQuery ) );
+        if ( _verbosity > 0 )
+            printf( "Backward analysis tightened %u bounds\n", tightened );
+        while ( tightened &&
+                _milpSolverBoundTighteningType ==
+                    MILPSolverBoundTighteningType::BACKWARD_ANALYSIS_CONVERGE &&
+                GlobalConfiguration::MAX_ROUNDS_OF_BACKWARD_ANALYSIS )
+        {
+            performMILPSolverBoundedTightening( &( *_preprocessedQuery ) );
+            tightened = performSymbolicBoundTightening( &( *_preprocessedQuery ) );
+            if ( _verbosity > 0 )
+                printf( "Backward analysis tightened %u bounds\n", tightened );
+        }
+    }
+}
+
 void Engine::performMILPSolverBoundedTighteningForSingleLayer( unsigned targetIndex )
 {
     if ( _produceUNSATProofs )
         return;
 
-    if ( _networkLevelReasoner && _isGurobyEnabled && !_performLpTighteningAfterSplit &&
+    if ( _networkLevelReasoner && _isGurobyEnabled && _performLpTighteningAfterSplit &&
          _milpSolverBoundTighteningType != MILPSolverBoundTighteningType::NONE )
     {
         _networkLevelReasoner->obtainCurrentBounds();
@@ -1649,13 +1675,13 @@ void Engine::performMILPSolverBoundedTighteningForSingleLayer( unsigned targetIn
             break;
         case MILPSolverBoundTighteningType::LP_RELAXATION_INCREMENTAL:
             return;
-
         case MILPSolverBoundTighteningType::MILP_ENCODING:
             _networkLevelReasoner->MILPTighteningForOneLayer( targetIndex );
             break;
         case MILPSolverBoundTighteningType::MILP_ENCODING_INCREMENTAL:
             return;
-
+        case MILPSolverBoundTighteningType::BACKWARD_ANALYSIS_ONCE:
+        case MILPSolverBoundTighteningType::BACKWARD_ANALYSIS_CONVERGE:
         case MILPSolverBoundTighteningType::ITERATIVE_PROPAGATION:
         case MILPSolverBoundTighteningType::NONE:
             return;
@@ -2379,11 +2405,11 @@ void Engine::performSimulation()
     _networkLevelReasoner->simulate( &simulations );
 }
 
-void Engine::performSymbolicBoundTightening( InputQuery *inputQuery )
+unsigned Engine::performSymbolicBoundTightening( InputQuery *inputQuery )
 {
     if ( _symbolicBoundTighteningType == SymbolicBoundTighteningType::NONE ||
          ( !_networkLevelReasoner ) || _produceUNSATProofs )
-        return;
+        return 0;
 
     struct timespec start = TimeUtils::sampleMicro();
 
@@ -2459,6 +2485,7 @@ void Engine::performSymbolicBoundTightening( InputQuery *inputQuery )
                                   TimeUtils::timePassed( start, end ) );
     _statistics.incLongAttribute( Statistics::NUM_TIGHTENINGS_FROM_SYMBOLIC_BOUND_TIGHTENING,
                                   numTightenedBounds );
+    return numTightenedBounds;
 }
 
 bool Engine::shouldExitDueToTimeout( unsigned timeout ) const

src/engine/Engine.h

@@ -677,7 +677,7 @@ class Engine
       Perform a round of symbolic bound tightening, taking into
       account the current state of the piecewise linear constraints.
     */
-    void performSymbolicBoundTightening( InputQuery *inputQuery = nullptr );
+    unsigned performSymbolicBoundTightening( InputQuery *inputQuery = nullptr );
 
     /*
       Perform a simulation which calculates concrete values of each layer with
@@ -723,6 +723,8 @@ class Engine
                                       const List<unsigned> &basicRows );
     void performMILPSolverBoundedTightening( InputQuery *inputQuery = nullptr );
 
+    void performAdditionalBackwardAnalysisIfNeeded();
+
     /*
       Call MILP bound tightening for a single layer.
     */

src/engine/MILPSolverBoundTighteningType.h

@@ -31,8 +31,11 @@ enum class MILPSolverBoundTighteningType {
     MILP_ENCODING_INCREMENTAL = 3,
     // Encode full queries and tries to fix relus until fix point
     ITERATIVE_PROPAGATION = 4,
+    // Perform backward analysis
+    BACKWARD_ANALYSIS_ONCE = 5,
+    BACKWARD_ANALYSIS_CONVERGE = 6,
     // Option to have no MILP bound tightening performed
-    NONE = 5,
+    NONE = 10,
 };
 
 #endif // __MILPSolverBoundTighteningType_h__

src/input_parsers/OnnxParser.cpp

@@ -2108,4 +2108,4 @@ void OnnxParser::tanhEquations( onnx::NodeProto &node, bool makeEquations )
     {
         _query.addTanh( inputVars[i], outputVars[i] );
     }
-}
+}