Query cycles indefinitely

[kjulian3]

With the latest version of Marabou (including the small fix to the iterator in Engine.cpp, #54 ), Marabou enters a cycle after running for ~2 hours. The number of splits grows until 11461, and then stays fixed at 11461 splits. Turning on tableau logging shows that the the pivots cycle between five variables and the values are not changing. This cycle continues for at least 2.5 hours after entering the cycle, and it appears to continue indefinitely.

I've attached a minimal python example to reproduce the behavior (I can convert to C++ if needed). The network used is also included. I turned the PREPROCESSOR_PL_CONSTRAINTS_ADD_AUX_EQUATIONS flag in GlobalConfiguration.cpp off because that still produces Malformed Basis errors. I've also attached a picture of the terminal output with tableau logging on to show the cycle.

Marabou_Cycle.zip

[guykatzz]

I fixed an issue that sounds very similar, but on a smaller example. Can you pull and see whether the problem still exists in your example?

[kjulian3]

After pulling and re-running the example, I get a bound violation error after running for 4 minutes:

Tableau test invariants: bound violation!
Variable 45 (non-basic #78). Assignment: -0.111673. Range: [-0.110559, -0.006102]

[guykatzz]

Hi Kyle,
It's been running for 20 minutes on my machine without the violation. Do you have the log file from your run?

[guykatzz]

Oops, I forgot to set the aux flag to false. Looking at the problem now.

[guykatzz]

I found a temporary solution that seems to solve this issue, but at the cost of reducing overall accuracy (and thus requiring more frequent restorations). I'm going to look for something better before I merge it into the master branch. Still, if you want to use the temporary solution, it's on a branch called bound_violation.

[kjulian3]

I'll take a look, thanks!

[kjulian3]

Hi Guy, I tested the example with the the bound_violation branch, but I am getting a similar error now (though after running for 40+ minutes).

I've attached the end of the log file showing the assertion violation from line 1702 of Tableau.cpp, which states:

// This should only happen when the basic variable is pressed against
// one of its bounds
ASSERT( _basicStatus[_leavingVariable] == Tableau::AT_UB ||
_basicStatus[_leavingVariable] == Tableau::AT_LB ||
_basicStatus[_leavingVariable] == Tableau::BETWEEN
);

VerticalCAS.log

[guykatzz]

Trying to figure this out, I discovered and fixed a pretty serious bug that could have resulted in cycling. Unfortunately, the assertion still fails on this example. This is now a numerical stability issue - at the time the assertion fails, the tableau is already so degraded that it acts funny.

I am working on improvements to the basis factorization code which, I hope, will improve matters. (I am also hoping they will help fix Parth's issue). It will take me a few days, at least. For now you can disable the failing assertion and see what happens - maybe the precision restoration code will kick in and save the day.