4 ms·

MiniZinc is a fairly simple-to-understand and open source constraint language: https://www.minizinc.org https://www.minizinc.org I learned about it when a fri

MiniZinc is a fairly simple-to-understand and open source constraint language: https://www.minizinc.org https://www.minizinc.org I learned about it when a friend gave me a programming challenge: https://gcanyon.wordpress.com/2009/10/28/a-programming-puzzle-from-einav/ https://gcanyon.wordpress.com/2009/10/28/a-programming-puzzl... She was going to work in PHP, I wrote a solution in J, and a commenter solved it in MiniZinc. Here is their solution in MiniZinc: http://www.hakank.org/minizinc/einav_puzzle.mzn http://www.hakank.org/minizinc/einav_puzzle.mzn

hakank 4y ago
Hi again Geoff. Here are some other constraint modelling implementations of this problem: http://hakank.org/common_cp_models/#einavpuzzle http://hakank.org/common_cp_models/#einavpuzzle .
- gcanyon 4y ago
  WOW it surely is a small world — at least our corner of it. I was very glad your page with the MiniZinc solution was still up! Edit to add: holy moses, all those solutions! I need to reach out to Einav to let her know she is famous :-)
sterlind 4y ago
as a note, I've tried MiniZinc for modeling a problem in the past, and the language/ecosystem simply wasn't up to my task. iirc, function calls in MiniZinc are expanded/unrolled when the model is generated, rather than the function definition and its callers being symbolically translated into the model. this is no fault of MiniZinc, I simply thought that an SMT solver would be sufficient and it wasn't. I need a mixed-integer or non-linear program solver, and ended up approaching it with a computer algebra system to generate my models and passing it to Gurobi or HiGHS. tl;dr there's different types of hard, and SMT solvers are only good at some types of hard.
- hakank 4y ago
  One interesting development in the latter years is the mix of Constraint programming and SAT solvers. For example Google OR-tools (https://developers.google.com/optimization/ https://developers.google.com/optimization/ ) which mixes CP, SAT and MIP. It has won most of the MiniZinc Challenge categories (https://www.minizinc.org/challenge.html https://www.minizinc.org/challenge.html ) several years now. The Chuffed solver is another solver mixing CP and SAT.
  - sterlind 4y ago
    isn't or-tools just a wrapper library for a bunch of solvers? I must be missing something.
    - hakank 4y ago
      Yes, OR-tools has a lot of solvers. The solver I talked about is the CP-SAT solver. It's described (https://www.minizinc.org/challenge2022/description_or-tools_cp-sat.txt https://www.minizinc.org/challenge2022/description_or-tools_... ) as: """ CP-SAT is a discrete optimization solver built on top of a SAT engine. It is available within the OR-Tools open-source repository (website: https://developers.google.com/optimization https://developers.google.com/optimization, github repository: https://github.com/google/or-tools https://github.com/google/or-tools). It has won multiple gold medals at the MiniZinc challenge (https://www.minizinc.org/challenge.html https://www.minizinc.org/challenge.html) since its debut in 2017. The CP-SAT solver is architectured around five components: The base layer is a clause learning SAT solver. Above the SAT layer sits a Constraint Programming (CP) module with Boolean, integer and interval variables, and standard integer, scheduling and routing constraints. Alongside the CP solver, a simplex provides a global linear relaxation. Its integration with the CP and SAT layers enable the CP-SAT solver to solve MIP problems with the same techniques as (commercial) MIP solvers: relaxation, cuts, heuristics and duality based techniques. Both the CP and MIP modules rely on a unified protobuf representation of the model that can serve as a file format, as well as an intermediate representation of the model during all phases of the solve (input format, presolved model, LNS fragment). On top, the search layer implements a robust information-sharing portfolio of specialized workers that offers both good and fast solutions, and superior optimality proving capabilities. This work was presented at the CPAIOR 2020 masterclass. The recording is available on youtube (https://www.youtube.com/watch?v=lmy1ddn4cyw https://www.youtube.com/watch?v=lmy1ddn4cyw). """
OJFord 4y ago
That news section could do with a constraint or two! (Almost ordered dates..)
ceceron 4y ago
I totally agree. MiniZinc is a great tool to prototype solvers for combinatorial optimization problems. It's mature (but still growing) and has support for many different solvers, not only from the Constraint Programming/SAT family. You can easily switch to MIP solvers (like Gurobi) or even try some local search approaches. It has very good documentation, reasonable IDE and AFAIK three great courses on Coursera for beginners. I have been teaching it myself[1] and all my students were amazed how quickly one can develop a working prototype for real-life industrial problems. [1] https://gitlab.com/agh-courses/2021-2022/constraint-programming https://gitlab.com/agh-courses/2021-2022/constraint-programm...
wjnc 4y ago
Ha I just started the course in MiniZinc on Coursera and it is very nice and creative. One tidbit for someone with a mostly econometrics background that (for me, a starter in the language with some exposure to linear optimization in the past) it was hard getting it to perform operations that use floats. For me that took away most toy problems I am interested in. But it’s blazing fast for complex discrete optimization and very forgiving in the language, so at least it’s a great learn.
- hakank 4y ago
  Constraint programming solvers tends to focus on finite domain (integers) but there are some solvers that has some supports for floats as decision variables. You can try some of these solvers. For non linear models: * Gecode (included in the MiniZincIDE distribtion) * JaCoP (https://github.com/radsz/jacop https://github.com/radsz/jacop) * OptiMathSAT (https://optimathsat.disi.unitn.it/pages/fznreference.html https://optimathsat.disi.unitn.it/pages/fznreference.html) For linear models: * CBC (included in the MiniZincIDE distribution)

hakank 4y ago

Hi again Geoff. Here are some other constraint modelling implementations of this problem: http://hakank.org/common_cp_models/#einavpuzzle http://hakank.org/common_cp_models/#einavpuzzle .

gcanyon 4y ago
WOW it surely is a small world — at least our corner of it. I was very glad your page with the MiniZinc solution was still up! Edit to add: holy moses, all those solutions! I need to reach out to Einav to let her know she is famous :-)

sterlind 4y ago

as a note, I've tried MiniZinc for modeling a problem in the past, and the language/ecosystem simply wasn't up to my task. iirc, function calls in MiniZinc are expanded/unrolled when the model is generated, rather than the function definition and its callers being symbolically translated into the model. this is no fault of MiniZinc, I simply thought that an SMT solver would be sufficient and it wasn't. I need a mixed-integer or non-linear program solver, and ended up approaching it with a computer algebra system to generate my models and passing it to Gurobi or HiGHS. tl;dr there's different types of hard, and SMT solvers are only good at some types of hard.

hakank 4y ago
One interesting development in the latter years is the mix of Constraint programming and SAT solvers. For example Google OR-tools (https://developers.google.com/optimization/ https://developers.google.com/optimization/ ) which mixes CP, SAT and MIP. It has won most of the MiniZinc Challenge categories (https://www.minizinc.org/challenge.html https://www.minizinc.org/challenge.html ) several years now. The Chuffed solver is another solver mixing CP and SAT.
- sterlind 4y ago
  isn't or-tools just a wrapper library for a bunch of solvers? I must be missing something.
  - hakank 4y ago
    Yes, OR-tools has a lot of solvers. The solver I talked about is the CP-SAT solver. It's described (https://www.minizinc.org/challenge2022/description_or-tools_cp-sat.txt https://www.minizinc.org/challenge2022/description_or-tools_... ) as: """ CP-SAT is a discrete optimization solver built on top of a SAT engine. It is available within the OR-Tools open-source repository (website: https://developers.google.com/optimization https://developers.google.com/optimization, github repository: https://github.com/google/or-tools https://github.com/google/or-tools). It has won multiple gold medals at the MiniZinc challenge (https://www.minizinc.org/challenge.html https://www.minizinc.org/challenge.html) since its debut in 2017. The CP-SAT solver is architectured around five components: The base layer is a clause learning SAT solver. Above the SAT layer sits a Constraint Programming (CP) module with Boolean, integer and interval variables, and standard integer, scheduling and routing constraints. Alongside the CP solver, a simplex provides a global linear relaxation. Its integration with the CP and SAT layers enable the CP-SAT solver to solve MIP problems with the same techniques as (commercial) MIP solvers: relaxation, cuts, heuristics and duality based techniques. Both the CP and MIP modules rely on a unified protobuf representation of the model that can serve as a file format, as well as an intermediate representation of the model during all phases of the solve (input format, presolved model, LNS fragment). On top, the search layer implements a robust information-sharing portfolio of specialized workers that offers both good and fast solutions, and superior optimality proving capabilities. This work was presented at the CPAIOR 2020 masterclass. The recording is available on youtube (https://www.youtube.com/watch?v=lmy1ddn4cyw https://www.youtube.com/watch?v=lmy1ddn4cyw). """

OJFord 4y ago

That news section could do with a constraint or two! (Almost ordered dates..)

ceceron 4y ago

I totally agree. MiniZinc is a great tool to prototype solvers for combinatorial optimization problems. It's mature (but still growing) and has support for many different solvers, not only from the Constraint Programming/SAT family. You can easily switch to MIP solvers (like Gurobi) or even try some local search approaches. It has very good documentation, reasonable IDE and AFAIK three great courses on Coursera for beginners. I have been teaching it myself[1] and all my students were amazed how quickly one can develop a working prototype for real-life industrial problems. [1] https://gitlab.com/agh-courses/2021-2022/constraint-programming https://gitlab.com/agh-courses/2021-2022/constraint-programm...

wjnc 4y ago

Ha I just started the course in MiniZinc on Coursera and it is very nice and creative. One tidbit for someone with a mostly econometrics background that (for me, a starter in the language with some exposure to linear optimization in the past) it was hard getting it to perform operations that use floats. For me that took away most toy problems I am interested in. But it’s blazing fast for complex discrete optimization and very forgiving in the language, so at least it’s a great learn.

hakank 4y ago
Constraint programming solvers tends to focus on finite domain (integers) but there are some solvers that has some supports for floats as decision variables. You can try some of these solvers. For non linear models: * Gecode (included in the MiniZincIDE distribtion) * JaCoP (https://github.com/radsz/jacop https://github.com/radsz/jacop) * OptiMathSAT (https://optimathsat.disi.unitn.it/pages/fznreference.html https://optimathsat.disi.unitn.it/pages/fznreference.html) For linear models: * CBC (included in the MiniZincIDE distribution)