Implemented basic knapsack cut

Author: liamjdavis

src/configuration/OptionParser.cpp

@@ -136,7 +136,11 @@ void OptionParser::initialize()
         "prove-unsat",
         boost::program_options::bool_switch( &( ( *_boolOptions )[Options::PRODUCE_PROOFS] ) )
             ->default_value( ( *_boolOptions )[Options::PRODUCE_PROOFS] ),
-        "Produce proofs of UNSAT and check them" )
+        "Produce proofs of UNSAT and check them" )(
+        "knapsack-cuts",
+        boost::program_options::bool_switch( &( ( *_boolOptions )[Options::KNAPSACK_CUTS] ) )
+            ->default_value( ( *_boolOptions )[Options::KNAPSACK_CUTS] ),
+        "Learn knapsack cuts at UNSAT leaves to prune subsumed subproblems" )
 #ifdef ENABLE_GUROBI
 #endif // ENABLE_GUROBI
         ;

src/configuration/Options.cpp

@@ -55,6 +55,7 @@ void Options::initializeDefaultValues()
     _boolOptions[DEBUG_ASSIGNMENT] = false;
     _boolOptions[PRODUCE_PROOFS] = false;
     _boolOptions[DO_NOT_MERGE_CONSECUTIVE_WEIGHTED_SUM_LAYERS] = false;
+    _boolOptions[KNAPSACK_CUTS] = false;
 
     /*
       Int options

src/configuration/Options.h

@@ -83,6 +83,11 @@ class Options
         // logically-consecutive weighted sum layers into a single
         // weighted sum layer, to reduce the number of variables
         DO_NOT_MERGE_CONSECUTIVE_WEIGHTED_SUM_LAYERS,
+
+        // Enable knapsack cuts: at each UNSAT leaf, learn a linear cut
+        // group over upstream ReLU phase indicators that prunes any
+        // subproblem in which the group is implied.
+        KNAPSACK_CUTS,
     };
 
     enum IntOptions {

src/engine/Engine.cpp

@@ -58,6 +58,7 @@ Engine::Engine()
     , _lastIterationWithProgress( 0 )
     , _symbolicBoundTighteningType( Options::get()->getSymbolicBoundTighteningType() )
     , _solveWithMILP( Options::get()->getBool( Options::SOLVE_WITH_MILP ) )
+    , _useKnapsackCuts( Options::get()->getBool( Options::KNAPSACK_CUTS ) )
     , _lpSolverType( Options::get()->getLPSolverType() )
     , _gurobi( nullptr )
     , _milpEncoder( nullptr )
@@ -200,6 +201,9 @@ bool Engine::solve( double timeoutInSeconds )
     // Before encoding, make sure all valid constraints are applied.
     applyAllValidConstraintCaseSplits();
 
+    if ( _useKnapsackCuts )
+        _knapsackCutManager.initialize( _networkLevelReasoner, _plConstraints, &_boundManager );
+
     if ( _solveWithMILP )
         return solveWithMILPEncoding( timeoutInSeconds );
 
@@ -243,6 +247,8 @@ bool Engine::solve( double timeoutInSeconds )
                 _statistics.print();
             }
 
+            if ( _useKnapsackCuts )
+                _knapsackCutManager.printSummary();
             _exitCode = Engine::TIMEOUT;
             _statistics.timeout();
             return false;
@@ -257,6 +263,8 @@ bool Engine::solve( double timeoutInSeconds )
                 _statistics.print();
             }
 
+            if ( _useKnapsackCuts )
+                _knapsackCutManager.printSummary();
             _exitCode = Engine::QUIT_REQUESTED;
             return false;
         }
@@ -294,6 +302,9 @@ bool Engine::solve( double timeoutInSeconds )
                 performBoundTighteningAfterCaseSplit();
                 informLPSolverOfBounds();
                 splitJustPerformed = false;
+
+                if ( _useKnapsackCuts && _knapsackCutManager.checkPruning() )
+                    throw InfeasibleQueryException();
             }
 
             if ( _searchTreeHandler.needToSplit() )
@@ -342,6 +353,8 @@ bool Engine::solve( double timeoutInSeconds )
                             ASSERT( _UNSATCertificateCurrentPointer );
                             ( **_UNSATCertificateCurrentPointer ).setSATSolutionFlag();
                         }
+                        if ( _useKnapsackCuts )
+                            _knapsackCutManager.printSummary();
                         _exitCode = Engine::SAT;
                         return true;
                     }
@@ -356,6 +369,8 @@ bool Engine::solve( double timeoutInSeconds )
                             printf( "\nEngine::solve: at leaf node but solving inconclusive\n" );
                             _statistics.print();
                         }
+                        if ( _useKnapsackCuts )
+                            _knapsackCutManager.printSummary();
                         _exitCode = Engine::UNKNOWN;
                         return false;
                     }
@@ -407,6 +422,9 @@ bool Engine::solve( double timeoutInSeconds )
             if ( _produceUNSATProofs )
                 explainSimplexFailure();
 
+            if ( _useKnapsackCuts )
+                _knapsackCutManager.collectFromCurrentLeaf();
+
             if ( !_searchTreeHandler.popSplit() )
             {
                 mainLoopEnd = TimeUtils::sampleMicro();
@@ -417,6 +435,8 @@ bool Engine::solve( double timeoutInSeconds )
                     printf( "\nEngine::solve: unsat query\n" );
                     _statistics.print();
                 }
+                if ( _useKnapsackCuts )
+                    _knapsackCutManager.printSummary();
                 _exitCode = Engine::UNSAT;
                 return false;
             }

src/engine/Engine.h

@@ -32,6 +32,7 @@
 #include "IEngine.h"
 #include "IQuery.h"
 #include "JsonWriter.h"
+#include "KnapsackCutManager.h"
 #include "LPSolverType.h"
 #include "LinearExpression.h"
 #include "MILPEncoder.h"
@@ -502,6 +503,13 @@ class Engine
     */
     bool _solveWithMILP;
 
+    /*
+      Knapsack cuts: learned at UNSAT leaves, evaluated at every new
+      search node to prune subsumed subproblems.
+    */
+    bool _useKnapsackCuts;
+    KnapsackCutManager _knapsackCutManager;
+
     /*
       The solver to solve the LP during the complete search.
     */

src/engine/KnapsackCut.h

@@ -0,0 +1,65 @@
+/*********************                                                        */
+/*! \file KnapsackCut.h
+ ** \verbatim
+ ** This file is part of the Marabou project.
+ ** Copyright (c) 2017-2024 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
+ **
+ ** KnapsackCut implements a topology-aware cutting plane for ReLU networks.
+ **
+ ** For a ReLU neuron b with pre-activation pre_b = sum_i W_bi * post_i + bias_b,
+ ** the cut encodes: if the weighted combination of upstream phase indicators
+ ** exceeds a threshold, then b's phase is guaranteed.
+ **
+ ** A cut group (from a single UNSAT leaf) prunes a subproblem when ALL cuts
+ ** in the group are satisfied, meaning all target neurons are in their
+ ** UNSAT-leaf phases.
+ **
+ ** Only "furthest" fixes are included: neurons with no downstream fixed neurons.
+ **
+ ** Cut for active phase (pre_b >= 0):
+ **   sum_i a_i * z_i + c >= 0
+ **   where a_i = W_bi * lb_i (if W_bi > 0) or W_bi * ub_i (if W_bi < 0)
+ **         c = bias_b + folded constant contributions
+ **
+ ** Cut for inactive phase (pre_b <= 0), negated to >= form:
+ **   sum_i a_i * z_i + c >= 0
+ **   where a_i = -W_bi * ub_i (if W_bi > 0) or -W_bi * lb_i (if W_bi < 0)
+ **         c = -bias_b + folded constant contributions
+ **/
+
+#ifndef __KnapsackCut_h__
+#define __KnapsackCut_h__
+
+#include "Map.h"
+#include "Vector.h"
+
+struct KnapsackCut
+{
+    // The pre-activation variable (b) of the target ReLU
+    unsigned targetBVar;
+
+    // Phase of the target at the UNSAT leaf (true = active, false = inactive)
+    bool isActive;
+
+    // NLR layer and neuron indices for identification
+    unsigned reluLayerIdx;
+    unsigned neuronIdx;
+
+    // Coefficients keyed by upstream ReLU f-variable
+    // coeff[f_var] = contribution when upstream neuron is active (z=1)
+    Map<unsigned, double> coefficients;
+
+    // Constant term (folded bias + non-phase-indicator contributions)
+    double constant;
+};
+
+struct KnapsackCutGroup
+{
+    Vector<KnapsackCut> cuts;
+    unsigned depth;
+};
+
+#endif // __KnapsackCut_h__