Backward forward algorithm (#845)

* Add files via upload

Added assignment and store-into-other NLR tests for every activation function.

* Revert last change.

* Added assginment, store-into-other NLR tests for every activation function.

* Add files via upload

0-2-0: Implementing layer simulations for every activation function.

* Add files via upload

0-2-1: Testing layer simulations for every activation function.

* Add files via upload

0-3-0: Implementing interval arithmetic for all activation functions.

* Add files via upload

0-3-1: Adding interval arithmetic tests for all activation functions.

* 0-4-0: Implementing symbolic bound tightening for every activation function.

0-4-0: Implementing symbolic bound tightening for every activation function.

* 0-4-1: Adding symbolic bound tightening tests for all activation functions.

0-4-1: Adding symbolic bound tightening tests for all activation functions.

* 0-5-0: Adding rounding constant for LP relaxation propagation.

0-5-0: Adding rounding constant for LP relaxation propagation.

* 0-5-1: Implementing forward-backward LP propagation algorithm for all activation functions.

0-5-1: Implementing forward-backward LP propagation algorithm for all activation functions.

* 0-5-2: Adding forward-backward LP propagation tests for all activation functions.

0-5-2: Adding forward-backward LP propagation tests for all activation functions.

* 0-5---3: Minor fix.

0-5---3: Minor fix.

* 0-5--4: Another fix.

0-5--4: Another fix.

* 0-5---5: Fixing fix 0-5--4 for this branch.

0-5---5: Fixing fix 0-5--4 for this branch.

* 0-5---6: Corrections in Backward-Forward Algorithm, SBT

0-5--6:
Changes in Backward-Forward Algorithm:
- Bug fixes: Sigmoid (wrong bias for bounds, unlike in DeepPoly), Softmax (missing two assignments lead to NaN values when bounds equal zero).
- Improvements: Absolute Value, Round (stricter initial range for target variable).
- Minor fixes: Bilinear (removed unnecessary epsilon and unused variable).

Changes in SBT:
- Same Bilinear minor fix.

* 0-5--7: clang-format

* Update CHANGELOG.md

* Update OptionParser.cpp

---------

Co-authored-by: Haoze(Andrew) Wu <[email protected]>

CHANGELOG.md

@@ -4,6 +4,7 @@
   - Adding incremental infrastructure which allows pushing and popping constraints to/from the InputQuery.
   - Dropped support for parsing Tensorflow network format. Newest Marabou version that supports Tensorflow is at commit 190555573e4702.
   - Fixed bug in the parsing of `transpose` nodes in command line C++ parser.
+  - Implemented forward-backward abstract interpretation, symbolic bound tightening, interval arithmetic and simulations for all activation functions.
   - Added the BaBSR heuristic as a new branching strategy for ReLU Splitting
 
 ## Version 2.0.0

src/configuration/GlobalConfiguration.cpp

@@ -71,6 +71,7 @@ const unsigned GlobalConfiguration::SIMULATION_RANDOM_SEED = 1;
 const bool GlobalConfiguration::USE_HARRIS_RATIO_TEST = true;
 
 const double GlobalConfiguration::SYMBOLIC_TIGHTENING_ROUNDING_CONSTANT = 0.00000000001;
+const double GlobalConfiguration::LP_TIGHTENING_ROUNDING_CONSTANT = 0.00000001;
 
 const double GlobalConfiguration::SIGMOID_CUTOFF_CONSTANT = 20;
 

src/configuration/GlobalConfiguration.h

@@ -195,8 +195,9 @@ class GlobalConfiguration
       Symbolic bound tightening options
     */
 
-    // Symbolic tightening rounding constant
+    // Symbolic tightening, LP rounding constants
     static const double SYMBOLIC_TIGHTENING_ROUNDING_CONSTANT;
+    static const double LP_TIGHTENING_ROUNDING_CONSTANT;
 
     static const double SIGMOID_CUTOFF_CONSTANT;
 

src/configuration/OptionParser.cpp

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

src/engine/Engine.cpp

@@ -1579,7 +1579,11 @@ void Engine::performMILPSolverBoundedTightening( Query *inputQuery )
 
         // TODO: Remove this block after getting ready to support sigmoid with MILP Bound
         // Tightening.
-        if ( _milpSolverBoundTighteningType != MILPSolverBoundTighteningType::NONE &&
+        if ( ( _milpSolverBoundTighteningType == MILPSolverBoundTighteningType::MILP_ENCODING ||
+               _milpSolverBoundTighteningType ==
+                   MILPSolverBoundTighteningType::MILP_ENCODING_INCREMENTAL ||
+               _milpSolverBoundTighteningType ==
+                   MILPSolverBoundTighteningType::ITERATIVE_PROPAGATION ) &&
              _preprocessedQuery->getNonlinearConstraints().size() > 0 )
             throw MarabouError( MarabouError::FEATURE_NOT_YET_SUPPORTED,
                                 "Marabou doesn't support sigmoid with MILP Bound Tightening" );