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

Gurobi ILP solver for protocol selection #321

Open
wants to merge 12 commits into
base: master
Choose a base branch
from
Open

Conversation

rolph-recto
Copy link
Collaborator

@rolph-recto rolph-recto commented Jan 16, 2022

Adds support for using Gurobi as a solver for protocol selection. Because Gurobi is not on a Maven repository, this change copies JAR files from a local Gurobi installation, whose directory is specified by the GUROBI_HOME environment variable.

Because this creates a dependency on Gurobi being installed on the build machine, I wrote this PR so that it can the toggled on/off during compilation by the gurobiSolver property for the compiler Gradle subproject. By default the Gurobi solver will not be compiled; to turn it on, change the project.ext.set("gurobiSolver", "false") line on compiler/build.gradle.kts file so that false is true instead.

In the cli subproject, I added a command line option to change between the z3 and gurobi solvers with --solver. Because the set of protocol selection solvers are not known until runtime, I use the Reflections library to get the set of solvers by reflection.

@codecov
Copy link

codecov bot commented Jan 16, 2022

Codecov Report

Merging #321 (85b436a) into master (57fb943) will decrease coverage by 0.01%.
The diff coverage is 42.85%.

@@             Coverage Diff              @@
##             master     #321      +/-   ##
============================================
- Coverage     62.72%   62.70%   -0.02%     
  Complexity     1255     1255              
============================================
  Files           245      245              
  Lines          9724     9731       +7     
  Branches       1449     1450       +1     
============================================
+ Hits           6099     6102       +3     
- Misses         3359     3362       +3     
- Partials        266      267       +1     
Impacted Files Coverage Δ
...io/github/apl_cornell/viaduct/selection/Solvers.kt 66.66% <42.85%> (-33.34%) ⬇️

📣 Codecov can now indicate which changes are the most critical in Pull Requests. Learn more

@cacay
Copy link
Member

cacay commented Jan 23, 2022

The Optimus Scala library can apparently interface with Gurobi. Maybe we can use that library, or look into how they interface with Gurobi.

cacay added 6 commits July 6, 2022 14:29
* master: (147 commits)
  Bump log4j-core from 2.17.2 to 2.18.0 in /examples (#470)
  Bump log4j-slf4j-impl from 2.17.2 to 2.18.0 (#465)
  Bump log4j-core from 2.17.2 to 2.18.0 (#466)
  Bump log4j-slf4j-impl from 2.17.2 to 2.18.0 in /examples (#469)
  Bump mkdocs-material from 8.3.8 to 8.3.9 in /docs (#468)
  Simplify CommitmentDispatchCodeGenerator (#463)
  Contract changes draft (#460)
  Cleanup task dependencies in build (#461)
  Fix name of Main package in CLI (#458)
  Bump mkdocs-material from 8.3.6 to 8.3.8 in /docs (#457)
  Bump kotlinx-coroutines-core from 1.6.2 to 1.6.3 (#453)
  Bump kotlinx-coroutines-core from 1.6.2 to 1.6.3 in /examples (#455)
  Bump mkdocs-material from 8.3.4 to 8.3.6 in /docs (#456)
  Bump org.jetbrains.dokka from 1.6.21 to 1.7.0 (#454)
  Bump plugin.serialization from 1.6.21 to 1.7.0 (#447)
  Bump jvm from 1.6.21 to 1.7.0 in /examples (#451)
  Bump multiplatform from 1.6.21 to 1.7.0 (#446)
  Bump actions/setup-python from 3 to 4 (#444)
  Bump kotlinpoet from 1.11.0 to 1.12.0 (#445)
  Bump clikt from 3.4.2 to 3.5.0 (#443)
  ...
Copy link
Member

@cacay cacay left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I improved build integration and the logic for dynamically discovering if Gurobi exists.

@cacay cacay linked an issue Jul 6, 2022 that may be closed by this pull request
@cacay cacay self-requested a review July 9, 2022 02:57
Copy link
Member

@cacay cacay left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

The Gurobi solver finds solutions to impossible problems. We need to fix that before merging.

Also, Gurobi prints a bunch of crap to stdout. That needs to be suppressed.

* origin/master:
  Reorganize protocol selection so we can add multiple solvers (#473)
  Rename `Plaintext` to `Cleartext` (#472)
  Move package `apl.prettyprinting` to `viaduct.prettyprinting` (#471)
  Implement code generation for functions (#462)
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.

ILP solver
2 participants