4 ms·

A very interesting application of constraint programming is the Unison compiler https://unison-code.github.io/ https://unison-code.github.io/, which uses constr

A very interesting application of constraint programming is the Unison compiler https://unison-code.github.io/ https://unison-code.github.io/, which uses constraint models to solve compiler backend problems for llvm. As a simple example, register allocation can be modeled as a graph coloring problem for which there is an edge between every variable which must be live at the same time and colors represent registers, but he unison model is sophisticated beyond this. We use a simpler related model in our project VIBES https://github.com/draperlaboratory/VIBES https://github.com/draperlaboratory/VIBES which is a micropatching compiler (it uses the constraints to compile code in such a way it can fit in place, has the right stuff in the right registers, etc.)

mzl 4y ago
VIBES seems like a very cool project. Do you have any example MiniZinc files that show how the generated problems look? Also, I would encourage you to generate some interesting instances and submit to the MiniZinc challenge (last years call for problems: https://www.minizinc.org/challenge2022/call_for_problems.html https://www.minizinc.org/challenge2022/call_for_problems.htm...). It is a good way to get your problems into the hands of solver developers.
- philzook 4y ago
  Thanks for the suggestion! I've known we should be submitting our verification problems to smtcomp, but hadn't thought about minizinc challenges Our current model is here https://github.com/draperlaboratory/VIBES/blob/main/resources/minizinc/model.mzn https://github.com/draperlaboratory/VIBES/blob/main/resource... We don't have any parameter files committed to the repo, they are generated by the compiler. It has been on my todo list for a while to completely refactor this model. Currently, the constraint solve can take 10s on our hardest problems so far, which would be nice to get down, but not our biggest blocker.
  - mzl 4y ago
    Thanks, and nice to see! Even if 10 seconds is often fast enough for solving a problem, I can imagine that it would be good to get down. From the code I guess that you use Chuffed, have you also tested other solvers? OR-Tools with parallel solving feels like the standard thing to try. I can also imagine that the time will start to go up significantly if larger patches are specified, but perhaps that is not a very common use-case. Having some example instances for ease of testing would be fun, and make it easier for a drive-by constraint programmer to try it out. Hoping to see it in the competition next year. Problems that are mostly reasonably fast to solve can still be interesting IMHO, especially when they are probably only fast because some solvers (Chuffed/OR-Tools) have very good automatic heuristics.
richard_shelton 4y ago
By the way, there is a similar work to Unison project. Its basic idea is to automate the compiler backend generation with help of SMT solver. The article: https://link.springer.com/epdf/10.1134/S0361768821070082?sharing_token=CDjt7dJgYDFRgNDmg4oImkckSORA_DxfnEvY7GoQybbiao8nJP2kL8gzSL48VIVrQ311UIiVSEVzfxxx570Rn1YmYOvi2Pe8cEABfNDVC8ME3qEgOBRRgJScY_cpZURIaJaXxtb5r6kZaawlBZBYuj4qvaA6GJnEpXdAGUiyNLU%3D https://link.springer.com/epdf/10.1134/S0361768821070082?sha...

mzl 4y ago

VIBES seems like a very cool project. Do you have any example MiniZinc files that show how the generated problems look? Also, I would encourage you to generate some interesting instances and submit to the MiniZinc challenge (last years call for problems: https://www.minizinc.org/challenge2022/call_for_problems.html https://www.minizinc.org/challenge2022/call_for_problems.htm...). It is a good way to get your problems into the hands of solver developers.

philzook 4y ago
Thanks for the suggestion! I've known we should be submitting our verification problems to smtcomp, but hadn't thought about minizinc challenges Our current model is here https://github.com/draperlaboratory/VIBES/blob/main/resources/minizinc/model.mzn https://github.com/draperlaboratory/VIBES/blob/main/resource... We don't have any parameter files committed to the repo, they are generated by the compiler. It has been on my todo list for a while to completely refactor this model. Currently, the constraint solve can take 10s on our hardest problems so far, which would be nice to get down, but not our biggest blocker.
- mzl 4y ago
  Thanks, and nice to see! Even if 10 seconds is often fast enough for solving a problem, I can imagine that it would be good to get down. From the code I guess that you use Chuffed, have you also tested other solvers? OR-Tools with parallel solving feels like the standard thing to try. I can also imagine that the time will start to go up significantly if larger patches are specified, but perhaps that is not a very common use-case. Having some example instances for ease of testing would be fun, and make it easier for a drive-by constraint programmer to try it out. Hoping to see it in the competition next year. Problems that are mostly reasonably fast to solve can still be interesting IMHO, especially when they are probably only fast because some solvers (Chuffed/OR-Tools) have very good automatic heuristics.

richard_shelton 4y ago

By the way, there is a similar work to Unison project. Its basic idea is to automate the compiler backend generation with help of SMT solver. The article: https://link.springer.com/epdf/10.1134/S0361768821070082?sharing_token=CDjt7dJgYDFRgNDmg4oImkckSORA_DxfnEvY7GoQybbiao8nJP2kL8gzSL48VIVrQ311UIiVSEVzfxxx570Rn1YmYOvi2Pe8cEABfNDVC8ME3qEgOBRRgJScY_cpZURIaJaXxtb5r6kZaawlBZBYuj4qvaA6GJnEpXdAGUiyNLU%3D https://link.springer.com/epdf/10.1134/S0361768821070082?sha...