Scaling Up Exact Neural Network Compression by ReLU Stability Supplementary Material A1 Description of MILP formulation for a ReLU activation

If none is provided by the callback, the MILP solver accepts the solution as feasible. In our case, we use a lazy constraint callback for a slightly different purpose. For ease of explanation, they are in reverse order of appearance. This operation is performed in line 25. The case in which an entire layer is stably inactive is considered separately.