BaB gets stuck on an example problem

[castrong]

BaB appears to run forever when trying to solve a problem on a relatively small network. The network has layer sizes [1, 10, 4, 1], so there are only 16 nodes total. I ran it for several hours with no resolution, and a println inside the loop in the output_bound function in BaB.jl showed that global_approx - global_concrete was remaining constant. An issue with reluplex I saw before came from numerical issues where it would repeatedly think a node that was already fixed was violated from small numerical violations in the result returned from the optimizer. I wonder if something similar could be happening here to cause it to fall into some sort of an infinite loop.

Code to reproduce the issue:

# Setup problem
network = NeuralVerification.read_nnet("./test_rand/networks/rand_[1,10,4,1]_3.nnet")
input_set = NeuralVerification.Hyperrectangle([0.18480275917946454], [0.6737285743432531])
output_set = NeuralVerification.Hyperrectangle([-0.1103027448779359], [0.9482755730682704])
problem = NeuralVerification.Problem(network, input_set, output_set)

# BaB Problem
println(NeuralVerification.solve(NeuralVerification.BaB(), problem))

Network:

//Default header text.
3, 1, 1, 10,
1, 10, 4, 1,
This line extraneous
-6.55e4,
6.55e4,
0.0,0.0,
1.0,1.0,
0.5288322389598363,
0.9823479701889837,
-0.5370789843033767,
-0.6263944851903522,
0.8971037043271797,
-0.802149016020731,
-0.6506999340714135,
0.9262012389766037,
0.03793705401523262,
-0.48287090754589146,
-0.6396030243168989,
-0.07336989391175264,
0.6348597054162952,
0.0482645113529645,
0.1921283453146474,
0.19997122595307992,
-0.09040415116558531,
-0.7532703509068335,
0.8801314550640673,
0.6640872178337465,
0.056674958167578726, 0.15445231894531286, -0.8263951384621664, -0.8694522989776954, -0.25418017585238006, 0.9586053750447525, -0.24627106224512962, 0.965702425851183, 0.19121822301940306, -0.5904194344887888,
0.011143978631912521, -0.822653382380937, 0.3164795494607673, -0.36975727437930095, 0.957297373679391, -0.3298287969334641, 0.006619748099108591, -0.6271523021609804, 0.25658155164872243, -0.8559382256105543,
-0.6402439454154596, 0.6757712495549013, -0.05786803222093395, -0.13834098396467143, -0.443813494042117, 0.0862127472144465, -0.6347596682197061, -0.5037016661679949, -0.8582507677657771, 0.08903020583983112,
-0.5176111310429126, -0.10355107470752722, 0.7744781778659333, 0.7205321670017155, 0.10109704829500155, -0.2864020619978742, -0.6260918478070154, 0.7217029739447907, 0.4297788124923083, -0.9844047983689155,
0.2641123726837802,
0.028585968331774403,
0.06068658450837505,
0.4517535541843194,
0.8670791194974665, -0.35750313130254696, 0.024010063821840788, 0.8662035529181007,
0.32595512763536316,

[changliuliu]

The problem was that BaB kept splitting the first input domain since it is not deleted from the queue. This issue has been addressed in this commit