search

NeuralNetworkVerification / Marabou

Other
241 stars 86 forks source link

Call to Engine::applyBoundTightenings() may have no effect. #624

Closed marcel-v closed 4 months ago

marcel-v commented 1 year ago

Hi,

investigating this issue, I also found another one: It seem that a call to Engine::applyBoundTightenings() will never have an effect. At least I can observe such behavior at this point for the given query.

The cause seems to be that, while the recent tightenings in BoundManager have not been feed to the Tableau yet, the bound of the tightening will only be set "inside" Tableau if the bound is tighter than the bound already present in Tableau. However, here Tableau actually uses the bounds of BoundManager. Hence the tightening call to Tableau has no effect. Now, the main issue is that only if the bound would be set in Tableau the variable watchers (like the piecewise-linear constraints) will be notified to effectively prune infeasible piecewise-linear cases.

Thanks in advance for any feedback!

wu-haoze commented 1 year ago

Hi @marcel-v , is this problem resolved? The applyBoundTightenings() method is not meant to be invoked from outside of the class. As you correctly point out, the applyBoundTightenings() method does not itself do any tightening. It is used to pull changes after invocations of the actual tightening functions. If you let me know if you want to achieve I can provide more pointers.

marcel-v commented 1 year ago

Yes, applyBoundTightenings() does not do any tightening itself. But apparently, at least as observed for the provided query, changes after previous tightening will also not be pulled due to this check, which essentially terminates "pulling the changes" if the updated bounds are not tighter than the bounds in BoundManager. However, at this point, BoundManager already contains the updated bounds. As a consequence, piecewise-linear constraints will not be notified of tightened bounds. However, if they would be notified some of the piecewise-linear constraints might be set to a fixed phase. I would like to achieve the latter.

idan0610 commented 4 months ago

This issue has most likely become stale and is being closed. If the problem persists, please contact us or open a new issue.