-
Notifications
You must be signed in to change notification settings - Fork 93
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
Polarity-based Splitting Heuristics #266
Polarity-based Splitting Heuristics #266
Conversation
Add mapping from Index to PlConstraint in NetworkLevelReasoner
is it ready for review? it is tagged with |
Not yet. Still need to fix something. Will ping when it's ready. |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
requested minor cosmetic changes
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
LGTM
* add run time estimate threhsold * Add Polarity to DivideStrategy Add mapping from Index to PlConstraint in NetworkLevelReasoner * implementing polarity based heuristics (WIP) * set default to polarity * Polarity * fix bug * fix another bug * change back to default * add some documentation * remove set splitting strategy * clean up * clean up * turn off logging * set default back to relu violation * clean up * cosmetic * add comment in smtcore * remove return statements
* add run time estimate threhsold * Add Polarity to DivideStrategy Add mapping from Index to PlConstraint in NetworkLevelReasoner * implementing polarity based heuristics (WIP) * set default to polarity * Polarity * fix bug * fix another bug * change back to default * add some documentation * remove set splitting strategy * clean up * clean up * turn off logging * set default back to relu violation * clean up * cosmetic * add comment in smtcore * remove return statements
Add polarity-based splitting heuristics as one of the internal splitting strategy.
On 180 ACAS benchmarks with 20 min timeout, new strategy solved 116 instance in 13390 secs. Original splitting strategy solved 116 instances in 17142 secs.
Still need to add/fix some tests.