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

Add support for different branching heuristics #221

Merged
merged 24 commits into from
Mar 2, 2020

Conversation

wu-haoze
Copy link
Collaborator

@wu-haoze wu-haoze commented Feb 26, 2020

This PR is needed both for DnC Relu Splitting (the CAV submission) and for experimenting with different branching heuristics within the SmtCore.

  1. Each plConstraint keeps a score that will be used to select the branching plConstraint.
  2. Add a pickBranchPLConstraint() method in the SmtCore that returns the PL Constraint with the highest score when branching is required.
  3. A strategy to pick the earliest ReLU is implemented (2 more SAT and 5 more UNSAT on all ACAS benchmarks with a 30 minutes timeout).

Future PR will include the polarity based branching heuristic, and relusplitting in the DnC module.

src/engine/Engine.h Outdated Show resolved Hide resolved
src/engine/IEngine.h Outdated Show resolved Hide resolved
src/engine/MaxConstraint.h Outdated Show resolved Hide resolved
src/engine/ReluConstraint.h Outdated Show resolved Hide resolved
src/engine/SmtCore.cpp Outdated Show resolved Hide resolved
src/engine/tests/MockEngine.h Outdated Show resolved Hide resolved
@ahmed-irfan
Copy link
Collaborator

@anwu1219 there are conflict with the current master

@wu-haoze
Copy link
Collaborator Author

@anwu1219 there are conflict with the current master

Fixed now.

@guykatzz
Copy link
Collaborator

LGTM

@wu-haoze wu-haoze merged commit 187d5d5 into NeuralNetworkVerification:master Mar 2, 2020
@wu-haoze wu-haoze deleted the relusplit-pr branch May 19, 2020 00:31
AleksandarZeljic pushed a commit to AleksandarZeljic/Marabou that referenced this pull request Oct 9, 2020
…tion#221)

* polarity based direction heuristic

* Update ReluConstraint.cpp

* add more documentation and mino fixes for polarity-based direction heuristic

* add relu divider

* Update PiecewiseLinearConstraint.h

* add unit tests

* some changes

* remove ReluDivider for now

* add branching heuristic

* sanity check

* refactoring for modular branching decision

* relusplit-pr

* aesthetics

* clean up

* changes in style, terminology, removed _score definition in children classes

* add setScore method and invoke in acasParser

* rename branching to splitting

* minor

* rename branching to splitting

* remove extra line
matanost pushed a commit that referenced this pull request Nov 2, 2021
* polarity based direction heuristic

* Update ReluConstraint.cpp

* add more documentation and mino fixes for polarity-based direction heuristic

* add relu divider

* Update PiecewiseLinearConstraint.h

* add unit tests

* some changes

* remove ReluDivider for now

* add branching heuristic

* sanity check

* refactoring for modular branching decision

* relusplit-pr

* aesthetics

* clean up

* changes in style, terminology, removed _score definition in children classes

* add setScore method and invoke in acasParser

* rename branching to splitting

* minor

* rename branching to splitting

* remove extra line
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
Development

Successfully merging this pull request may close these issues.

3 participants