Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Apply bounds after performing row bound tightening #338

Conversation

wu-haoze
Copy link
Collaborator

Currently in solve() after we perform explicitBasisBoundTightening() we do not apply the updated bounds to _tableau until we have called **_tableau->allBoundsValid()"" and performSymbolicBoundTightening(). This could result in non-trivial delay in concluding UNSAT. This PR fixes this issue.
Runtime comparison pending...

@wu-haoze wu-haoze requested a review from guykatzz July 30, 2020 17:43
@guykatzz
Copy link
Collaborator

The change LGTM. Lets see what the performance gain is.

@guykatzz
Copy link
Collaborator

Hi Andrew,
Did the experiments finish running for this PR? Was there an improvement?

@wu-haoze
Copy link
Collaborator Author

Hi Andrew,
Did the experiments finish running for this PR? Was there an improvement?

Hi Guy, on the commonly solved instances, there seem to be 10% runtime improvement. However, occasionally Marabou throws Error with the new changes, so I'm looking into that.

@wu-haoze
Copy link
Collaborator Author

On 40 acas, 40 mnist, 60 taxinet benchmarks, the two runs solve the same number of queries within 1 hour.
This branch: 29663 sec
Master: 31447 sec

@wu-haoze wu-haoze merged commit 5d6ae02 into NeuralNetworkVerification:master Aug 13, 2020
@wu-haoze wu-haoze deleted the apply-bounds-after-tightening branch August 13, 2020 14:43
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

2 participants