Towards Proof Minimization (#889)

Author: omriisack

CHANGELOG.md

@@ -7,6 +7,7 @@
   - 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
   - Support Sub of two variables, "Mul" of two constants, Slice, and ConstantOfShape in the python onnx parser
+  - Renamed SmtCore module to SearchTreeHandler
 
 ## Version 2.0.0
 

maraboupy/MarabouCore.cpp

@@ -833,8 +833,8 @@ PYBIND11_MODULE( MarabouCore, m )
         .value( "NUM_POPS", Statistics::StatisticsUnsignedAttribute::NUM_POPS )
         .value( "CURRENT_DECISION_LEVEL",
                 Statistics::StatisticsUnsignedAttribute::CURRENT_DECISION_LEVEL )
-        .value( "NUM_PL_SMT_ORIGINATED_SPLITS",
-                Statistics::StatisticsUnsignedAttribute::NUM_PL_SMT_ORIGINATED_SPLITS )
+        .value( "NUM_PL_SEARCH_TREE_ORIGINATED_SPLITS",
+                Statistics::StatisticsUnsignedAttribute::NUM_PL_SEARCH_TREE_ORIGINATED_SPLITS )
         .value( "NUM_VISITED_TREE_STATES",
                 Statistics::StatisticsUnsignedAttribute::NUM_VISITED_TREE_STATES )
         .value( "PP_NUM_TIGHTENING_ITERATIONS",
@@ -862,8 +862,8 @@ PYBIND11_MODULE( MarabouCore, m )
     py::enum_<Statistics::StatisticsLongAttribute>( m, "StatisticsLongAttribute" )
         .value( "NUM_TIGHTENINGS_FROM_EXPLICIT_BASIS",
                 Statistics::StatisticsLongAttribute::NUM_TIGHTENINGS_FROM_EXPLICIT_BASIS )
-        .value( "TOTAL_TIME_SMT_CORE_MICRO",
-                Statistics::StatisticsLongAttribute::TOTAL_TIME_SMT_CORE_MICRO )
+        .value( "TOTAL_TIME_SEARCH_TREE_HANDLER_MICRO",
+                Statistics::StatisticsLongAttribute::TOTAL_TIME_SEARCH_TREE_HANDLER_MICRO )
         .value( "TOTAL_TIME_PERFORMING_VALID_CASE_SPLITS_MICRO",
                 Statistics::StatisticsLongAttribute::TOTAL_TIME_PERFORMING_VALID_CASE_SPLITS_MICRO )
         .value( "PREPROCESSING_TIME_MICRO",

src/common/Pair.h

@@ -33,6 +33,11 @@ template <class L, class R> class Pair
     {
     }
 
+    Pair( const Pair<L, R> &other )
+        : _container( other._container )
+    {
+    }
+
     L &first()
     {
         return _container.first;

src/common/Statistics.cpp

@@ -24,7 +24,7 @@ Statistics::Statistics()
     _unsignedAttributes[NUM_PL_CONSTRAINTS] = 0;
     _unsignedAttributes[NUM_ACTIVE_PL_CONSTRAINTS] = 0;
     _unsignedAttributes[NUM_PL_VALID_SPLITS] = 0;
-    _unsignedAttributes[NUM_PL_SMT_ORIGINATED_SPLITS] = 0;
+    _unsignedAttributes[NUM_PL_SEARCH_TREE_ORIGINATED_SPLITS] = 0;
     _unsignedAttributes[NUM_PRECISION_RESTORATIONS] = 0;
     _unsignedAttributes[CURRENT_DECISION_LEVEL] = 0;
     _unsignedAttributes[MAX_DECISION_LEVEL] = 0;
@@ -43,6 +43,7 @@ Statistics::Statistics()
     _unsignedAttributes[NUM_CERTIFIED_LEAVES] = 0;
     _unsignedAttributes[NUM_DELEGATED_LEAVES] = 0;
     _unsignedAttributes[NUM_LEMMAS] = 0;
+    _unsignedAttributes[NUM_LEMMAS_USED] = 0;
     _unsignedAttributes[CERTIFIED_UNSAT] = 0;
 
     _longAttributes[NUM_MAIN_LOOP_ITERATIONS] = 0;
@@ -82,7 +83,7 @@ Statistics::Statistics()
     _longAttributes[TOTAL_TIME_PRECISION_RESTORATION] = 0;
     _longAttributes[TOTAL_TIME_CONSTRAINT_MATRIX_BOUND_TIGHTENING_MICRO] = 0;
     _longAttributes[TOTAL_TIME_APPLYING_STORED_TIGHTENINGS_MICRO] = 0;
-    _longAttributes[TOTAL_TIME_SMT_CORE_MICRO] = 0;
+    _longAttributes[TOTAL_TIME_SEARCH_TREE_HANDLER_MICRO] = 0;
     _longAttributes[TOTAL_TIME_UPDATING_SOI_PHASE_PATTERN_MICRO] = 0;
     _longAttributes[NUM_PROPOSED_PHASE_PATTERN_UPDATE] = 0;
     _longAttributes[NUM_ACCEPTED_PHASE_PATTERN_UPDATE] = 0;
@@ -208,11 +209,11 @@ void Statistics::print()
     printf( "\t\t[%.2lf%%] Applying stored bound-tightening: %llu milli\n",
             printPercents( totalTimeApplyingStoredTighteningsMicro, timeMainLoopMicro ),
             totalTimeApplyingStoredTighteningsMicro / 1000 );
-    unsigned long long totalTimeSmtCoreMicro =
-        getLongAttribute( Statistics::TOTAL_TIME_SMT_CORE_MICRO );
-    printf( "\t\t[%.2lf%%] SMT core: %llu milli\n",
-            printPercents( totalTimeSmtCoreMicro, timeMainLoopMicro ),
-            totalTimeSmtCoreMicro / 1000 );
+    unsigned long long totalTimeSearchTreeMicro =
+        getLongAttribute( Statistics::TOTAL_TIME_SEARCH_TREE_HANDLER_MICRO );
+    printf( "\t\t[%.2lf%%] Search Tree Handler : %llu milli\n",
+            printPercents( totalTimeSearchTreeMicro, timeMainLoopMicro ),
+            totalTimeSearchTreeMicro / 1000 );
     unsigned long long totalTimePerformingSymbolicBoundTightening =
         getLongAttribute( Statistics::TOTAL_TIME_PERFORMING_SYMBOLIC_BOUND_TIGHTENING );
     printf( "\t\t[%.2lf%%] Symbolic Bound Tightening: %llu milli\n",
@@ -234,7 +235,7 @@ void Statistics::print()
         totalTimePerformingValidCaseSplitsMicro + totalTimeHandlingStatisticsMicro +
         totalTimeExplicitBasisBoundTighteningMicro + totalTimeDegradationChecking +
         totalTimePrecisionRestoration + totalTimeConstraintMatrixBoundTighteningMicro +
-        totalTimeApplyingStoredTighteningsMicro + totalTimeSmtCoreMicro +
+        totalTimeApplyingStoredTighteningsMicro + totalTimeSearchTreeMicro +
         totalTimePerformingSymbolicBoundTightening;
 
     printf( "\t\t[%.2lf%%] Unaccounted for: %llu milli\n",
@@ -270,11 +271,11 @@ void Statistics::print()
         printAverage( timeConstraintFixingStepsMicro / 1000, numConstraintFixingSteps ) );
     printf( "\tNumber of active piecewise-linear constraints: %u / %u\n"
             "\t\tConstraints disabled by valid splits: %u. "
-            "By SMT-originated splits: %u\n",
+            "By Search-Tree--originated splits: %u\n",
             getUnsignedAttribute( Statistics::NUM_ACTIVE_PL_CONSTRAINTS ),
             getUnsignedAttribute( Statistics::NUM_PL_CONSTRAINTS ),
             getUnsignedAttribute( Statistics::NUM_PL_VALID_SPLITS ),
-            getUnsignedAttribute( Statistics::NUM_PL_SMT_ORIGINATED_SPLITS ) );
+            getUnsignedAttribute( Statistics::NUM_PL_SEARCH_TREE_ORIGINATED_SPLITS ) );
     printf( "\tLast reported degradation: %.10lf. Max degradation so far: %.10lf. "
             "Restorations so far: %u\n",
             getDoubleAttribute( Statistics::CURRENT_DEGRADATION ),
@@ -314,7 +315,7 @@ void Statistics::print()
             getUnsignedAttribute( Statistics::CURRENT_TABLEAU_M ),
             getUnsignedAttribute( Statistics::CURRENT_TABLEAU_N ) );
 
-    printf( "\t--- SMT Core Statistics ---\n" );
+    printf( "\t--- Search Tree Handler Statistics ---\n" );
     printf(
         "\tTotal depth is %u. Total visited states: %u. Number of splits: %u. Number of pops: %u\n",
         getUnsignedAttribute( Statistics::CURRENT_DECISION_LEVEL ),
@@ -428,6 +429,8 @@ void Statistics::print()
     printf( "\tNumber of leaves to delegate: %u\n",
             getUnsignedAttribute( Statistics::NUM_DELEGATED_LEAVES ) );
     printf( "\tNumber of lemmas: %u\n", getUnsignedAttribute( Statistics::NUM_LEMMAS ) );
+    printf( "\tNumber of lemmas used in proof minimization: %u\n",
+            getUnsignedAttribute( Statistics::NUM_LEMMAS_USED ) );
 }
 
 unsigned long long Statistics::getTotalTimeInMicro() const

src/common/Statistics.h

@@ -31,12 +31,12 @@ class Statistics
         NUM_PL_CONSTRAINTS,
         NUM_ACTIVE_PL_CONSTRAINTS,
         NUM_PL_VALID_SPLITS,
-        NUM_PL_SMT_ORIGINATED_SPLITS,
+        NUM_PL_SEARCH_TREE_ORIGINATED_SPLITS,
 
         // Precision restoration
         NUM_PRECISION_RESTORATIONS,
 
-        // Current and max stack depth in the SMT core
+        // Current and max stack depth in the Search Tree Handler
         CURRENT_DECISION_LEVEL,
         MAX_DECISION_LEVEL,
 
@@ -71,6 +71,7 @@ class Statistics
         NUM_CERTIFIED_LEAVES,
         NUM_DELEGATED_LEAVES,
         NUM_LEMMAS,
+        NUM_LEMMAS_USED,
 
         // 1 if returned UNSAT and proof was certified by proof checker, 0 otherwise.
         CERTIFIED_UNSAT,
@@ -188,8 +189,8 @@ class Statistics
         // Total amount of time spent applying previously stored bound tightenings
         TOTAL_TIME_APPLYING_STORED_TIGHTENINGS_MICRO,
 
-        // Total amount of time spent within the SMT core
-        TOTAL_TIME_SMT_CORE_MICRO,
+        // Total amount of time spent within the search tree core
+        TOTAL_TIME_SEARCH_TREE_HANDLER_MICRO,
 
         // Total time heuristically updating the SoI phase pattern
         TOTAL_TIME_UPDATING_SOI_PHASE_PATTERN_MICRO,

src/configuration/GlobalConfiguration.cpp

@@ -62,7 +62,7 @@ const unsigned GlobalConfiguration::MAX_SIMPLEX_PIVOT_SEARCH_ITERATIONS = 5;
 const DivideStrategy GlobalConfiguration::SPLITTING_HEURISTICS = DivideStrategy::ReLUViolation;
 const unsigned GlobalConfiguration::INTERVAL_SPLITTING_FREQUENCY = 10;
 const unsigned GlobalConfiguration::INTERVAL_SPLITTING_THRESHOLD = 10;
-const unsigned GlobalConfiguration::BOUND_TIGHTING_ON_CONSTRAINT_MATRIX_FREQUENCY = 100;
+const unsigned GlobalConfiguration::BOUND_TIGHTENING_ON_CONSTRAINT_MATRIX_FREQUENCY = 100;
 const unsigned GlobalConfiguration::ROW_BOUND_TIGHTENER_SATURATION_ITERATIONS = 20;
 const double GlobalConfiguration::COST_FUNCTION_ERROR_THRESHOLD = 0.0000000001;
 
@@ -119,6 +119,9 @@ const bool GlobalConfiguration::WRITE_JSON_PROOF = false;
 const unsigned GlobalConfiguration::BACKWARD_BOUND_PROPAGATION_DEPTH = 3;
 const unsigned GlobalConfiguration::MAX_ROUNDS_OF_BACKWARD_ANALYSIS = 10;
 
+const bool GlobalConfiguration::ANALYZE_PROOF_DEPENDENCIES = false;
+const bool GlobalConfiguration::MINIMIZE_PROOF_DEPENDENCIES = false;
+
 #ifdef ENABLE_GUROBI
 const unsigned GlobalConfiguration::GUROBI_NUMBER_OF_THREADS = 1;
 const bool GlobalConfiguration::GUROBI_LOGGING = false;
@@ -128,7 +131,7 @@ const bool GlobalConfiguration::GUROBI_LOGGING = false;
 const bool GlobalConfiguration::DNC_MANAGER_LOGGING = false;
 const bool GlobalConfiguration::ENGINE_LOGGING = false;
 const bool GlobalConfiguration::TABLEAU_LOGGING = false;
-const bool GlobalConfiguration::SMT_CORE_LOGGING = false;
+const bool GlobalConfiguration::SEARCH_TREE_HANDLER_LOGGING = false;
 const bool GlobalConfiguration::DANTZIGS_RULE_LOGGING = false;
 const bool GlobalConfiguration::BASIS_FACTORIZATION_LOGGING = false;
 const bool GlobalConfiguration::PREPROCESSOR_LOGGING = false;
@@ -174,8 +177,8 @@ void GlobalConfiguration::print()
     printf( "  GAUSSIAN_ELIMINATION_PIVOT_SCALE_THRESHOLD: %.15lf\n",
             GAUSSIAN_ELIMINATION_PIVOT_SCALE_THRESHOLD );
     printf( "  MAX_SIMPLEX_PIVOT_SEARCH_ITERATIONS: %u\n", MAX_SIMPLEX_PIVOT_SEARCH_ITERATIONS );
-    printf( "  BOUND_TIGHTING_ON_CONSTRAINT_MATRIX_FREQUENCY: %u\n",
-            BOUND_TIGHTING_ON_CONSTRAINT_MATRIX_FREQUENCY );
+    printf( "  BOUND_TIGHTENING_ON_CONSTRAINT_MATRIX_FREQUENCY: %u\n",
+            BOUND_TIGHTENING_ON_CONSTRAINT_MATRIX_FREQUENCY );
     printf( "  COST_FUNCTION_ERROR_THRESHOLD: %.15lf\n", COST_FUNCTION_ERROR_THRESHOLD );
     printf( "  USE_HARRIS_RATIO_TEST: %s\n", USE_HARRIS_RATIO_TEST ? "Yes" : "No" );
 

src/configuration/GlobalConfiguration.h

@@ -139,7 +139,7 @@ class GlobalConfiguration
     static const unsigned INTERVAL_SPLITTING_THRESHOLD;
 
     // How often should we perform full bound tightening, on the entire contraints matrix A.
-    static const unsigned BOUND_TIGHTING_ON_CONSTRAINT_MATRIX_FREQUENCY;
+    static const unsigned BOUND_TIGHTENING_ON_CONSTRAINT_MATRIX_FREQUENCY;
 
     // When the row bound tightener is asked to run until saturation, it can enter an infinite loop
     // due to tiny increments in bounds. This number limits the number of iterations it can perform.
@@ -263,6 +263,15 @@ class GlobalConfiguration
      */
     static const unsigned MAX_ROUNDS_OF_BACKWARD_ANALYSIS;
 
+    /* Analyze lemma dependencies when producing proofs
+     */
+    static const bool ANALYZE_PROOF_DEPENDENCIES;
+
+    /* Minimize the number of lemma dependencies when producing proofs
+     */
+    static const bool MINIMIZE_PROOF_DEPENDENCIES;
+
+
 #ifdef ENABLE_GUROBI
     /*
       The number of threads Gurobi spawns
@@ -277,7 +286,7 @@ class GlobalConfiguration
     static const bool DNC_MANAGER_LOGGING;
     static const bool ENGINE_LOGGING;
     static const bool TABLEAU_LOGGING;
-    static const bool SMT_CORE_LOGGING;
+    static const bool SEARCH_TREE_HANDLER_LOGGING;
     static const bool DANTZIGS_RULE_LOGGING;
     static const bool BASIS_FACTORIZATION_LOGGING;
     static const bool PREPROCESSOR_LOGGING;

src/engine/AbsoluteValueConstraint.cpp

@@ -152,7 +152,9 @@ void AbsoluteValueConstraint::notifyLowerBound( unsigned variable, double bound
                                                                        Tightening::UB,
                                                                        { variable, variable },
                                                                        Tightening::UB,
-                                                                       getType() );
+                                                                       *this,
+                                                                       false,
+                                                                       fUpperBound );
                 else if ( proofs && phaseFixed() )
                 {
                     std::shared_ptr<TableauRow> tighteningRow =
@@ -232,7 +234,9 @@ void AbsoluteValueConstraint::notifyUpperBound( unsigned variable, double bound
                                                                        Tightening::UB,
                                                                        { variable, variable },
                                                                        Tightening::UB,
-                                                                       getType() );
+                                                                       *this,
+                                                                       false,
+                                                                       fUpperBound );
                 else if ( proofs && phaseFixed() )
                 {
                     std::shared_ptr<TableauRow> tighteningRow =
@@ -406,7 +410,7 @@ AbsoluteValueConstraint::getSmartFixes( ITableau * /* tableau */ ) const
 
 List<PiecewiseLinearCaseSplit> AbsoluteValueConstraint::getCaseSplits() const
 {
-    ASSERT( _phaseStatus == PhaseStatus::PHASE_NOT_FIXED );
+    ASSERT( getPhaseStatus() == PhaseStatus::PHASE_NOT_FIXED );
 
     List<PiecewiseLinearCaseSplit> splits;
     splits.append( getNegativeSplit() );
@@ -476,14 +480,14 @@ PiecewiseLinearCaseSplit AbsoluteValueConstraint::getPositiveSplit() const
 
 bool AbsoluteValueConstraint::phaseFixed() const
 {
-    return _phaseStatus != PhaseStatus::PHASE_NOT_FIXED;
+    return getPhaseStatus() != PhaseStatus::PHASE_NOT_FIXED;
 }
 
 PiecewiseLinearCaseSplit AbsoluteValueConstraint::getImpliedCaseSplit() const
 {
-    ASSERT( _phaseStatus != PHASE_NOT_FIXED );
+    ASSERT( getPhaseStatus() != PHASE_NOT_FIXED );
 
-    if ( _phaseStatus == ABS_PHASE_POSITIVE )
+    if ( getPhaseStatus() == ABS_PHASE_POSITIVE )
         return getPositiveSplit();
 
     return getNegativeSplit();
@@ -512,8 +516,8 @@ void AbsoluteValueConstraint::dump( String &output ) const
                  _f,
                  _b,
                  _constraintActive ? "Yes" : "No",
-                 _phaseStatus,
-                 phaseToString( _phaseStatus ).ascii() );
+                 getPhaseStatus(),
+                 phaseToString( getPhaseStatus() ).ascii() );
 
     output +=
         Stringf( "b in [%s, %s], ",
@@ -826,7 +830,7 @@ void AbsoluteValueConstraint::fixPhaseIfNeeded()
         setPhaseStatus( ABS_PHASE_POSITIVE );
         if ( proofs )
             _boundManager->addLemmaExplanationAndTightenBound(
-                _posAux, 0, Tightening::UB, { _b }, Tightening::LB, getType() );
+                _posAux, 0, Tightening::UB, { _b }, Tightening::LB, *this, true, 0 );
         return;
     }
 
@@ -836,7 +840,7 @@ void AbsoluteValueConstraint::fixPhaseIfNeeded()
         setPhaseStatus( ABS_PHASE_NEGATIVE );
         if ( proofs )
             _boundManager->addLemmaExplanationAndTightenBound(
-                _negAux, 0, Tightening::UB, { _b }, Tightening::UB, getType() );
+                _negAux, 0, Tightening::UB, { _b }, Tightening::UB, *this, true, 0 );
         return;
     }
 
@@ -849,8 +853,14 @@ void AbsoluteValueConstraint::fixPhaseIfNeeded()
     {
         setPhaseStatus( ABS_PHASE_NEGATIVE );
         if ( proofs )
-            _boundManager->addLemmaExplanationAndTightenBound(
-                _negAux, 0, Tightening::UB, { _b, _f }, Tightening::UB, getType() );
+            _boundManager->addLemmaExplanationAndTightenBound( _negAux,
+                                                               0,
+                                                               Tightening::UB,
+                                                               { _b, _f },
+                                                               Tightening::UB,
+                                                               *this,
+                                                               true,
+                                                               getUpperBound( _b ) );
         return;
     }
 
@@ -860,8 +870,14 @@ void AbsoluteValueConstraint::fixPhaseIfNeeded()
     {
         setPhaseStatus( ABS_PHASE_POSITIVE );
         if ( proofs )
-            _boundManager->addLemmaExplanationAndTightenBound(
-                _posAux, 0, Tightening::UB, { _b, _f }, Tightening::LB, getType() );
+            _boundManager->addLemmaExplanationAndTightenBound( _posAux,
+                                                               0,
+                                                               Tightening::UB,
+                                                               { _b, _f },
+                                                               Tightening::LB,
+                                                               *this,
+                                                               true,
+                                                               -getLowerBound( _b ) );
         return;
     }
 
@@ -871,6 +887,9 @@ void AbsoluteValueConstraint::fixPhaseIfNeeded()
         if ( existsUpperBound( _posAux ) && FloatUtils::isZero( getUpperBound( _posAux ) ) )
         {
             setPhaseStatus( ABS_PHASE_POSITIVE );
+            if ( proofs )
+                _boundManager->addLemmaExplanationAndTightenBound(
+                    _posAux, 0, Tightening::UB, { _posAux }, Tightening::UB, *this, true, 0 );
             return;
         }
 
@@ -880,14 +899,17 @@ void AbsoluteValueConstraint::fixPhaseIfNeeded()
             setPhaseStatus( ABS_PHASE_NEGATIVE );
             if ( proofs )
                 _boundManager->addLemmaExplanationAndTightenBound(
-                    _negAux, 0, Tightening::UB, { _posAux }, Tightening::LB, getType() );
+                    _negAux, 0, Tightening::UB, { _posAux }, Tightening::LB, *this, true, 0 );
             return;
         }
 
         // Option 7: negAux has become zero, phase is negative
         if ( existsUpperBound( _negAux ) && FloatUtils::isZero( getUpperBound( _negAux ) ) )
         {
             setPhaseStatus( ABS_PHASE_NEGATIVE );
+            if ( proofs )
+                _boundManager->addLemmaExplanationAndTightenBound(
+                    _negAux, 0, Tightening::UB, { _negAux }, Tightening::UB, *this, true, 0 );
             return;
         }
 
@@ -897,7 +919,7 @@ void AbsoluteValueConstraint::fixPhaseIfNeeded()
             setPhaseStatus( ABS_PHASE_POSITIVE );
             if ( proofs )
                 _boundManager->addLemmaExplanationAndTightenBound(
-                    _posAux, 0, Tightening::UB, { _negAux }, Tightening::LB, getType() );
+                    _posAux, 0, Tightening::UB, { _negAux }, Tightening::LB, *this, true, 0 );
             return;
         }
     }