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.
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/ ) which mixes CP, SAT and MIP. It has won most of the MiniZinc Challenge categories (https://www.minizinc.org/challenge.html ) several years now. The Chuffed solver is another solver mixing CP and SAT.
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.
wow. that is impressive.. but surely this CP-SAT solver can't compete with the commercial offerings like Gurobi and CPLEX right? it'd be huge news if so... but I haven't seen it rank at all on the LP-focused benchmarks I've been looking at.
I haven't seen a comparison on LP-focused benchmarks with OR-tools CP-SAT. In the 2022 MiniZinc Challenge (https://www.minizinc.org/challenge2022/results2022.html ) both Gurobi, CPLEX (as well and SCIP and HiGHS) participated: CP-SAT was the best in all the categories it participated in.
It depends a lot on the problem to solve and how it is modeled. For some things OR-tools and/or other CP-style solvers are clearly better than MIP solvers. For others, vice verse.
A really nice thing with MiniZinc is that the same model can be used with both CP silvers like OR-Tools and MIP solvers like CPLEX and Gurobi.
I'm curious what you would have wanted MiniZinc to do?
In general, I think MiniZinc is great precisely because it is a structured way to generate a list of constraints, since this makes it possible to integrate into a variety of solvers. Sure, sometimes the generation and the interchange format can be a bit heavy and I would like better ways to manage that, but it is often still worth it IMHO.
The fact that the language is based on a relational semantics with the unfolding into a list of constraints as a model makes it possible to understand how predicates, nested Boolean contexts, reification, undefined expressions, and local variables all work in conjunction. It is a hard enough problem to solve as is, and I think adding semantic complexity on top of it would make it too hard to do.
What are you using to build your GUROBI models? I think your only options are to feed it a .MPS or .LP file if you don't use the APIs for C#, C, C++, Python, Matlab, R...etc. Or did you use something like Mathematica to go from CAS to .MPS?
Mathematica, correct. But fun fact: Mathematica has no MPS exporter. So I had to write my own, which is somehow the perf bottleneck in my whole setup now. Even after wrestling with it for several days. Apparently string operations are not its forté.
I had to look that up as I couldn't believe they don't have that feature... especially since Import[] supports .MPS. I know they have plugin support for solvers like Mosek and I think GUROBI which I assume creates a .MPS and sends to the solver. Maybe it just does it all in memory. They really need to add that lol.
it's so bizarre! why would they only do it halfway? and import is the least useful direction for them to implement.. how often are you building models outside of Mathematica to solve inside?
I can't use the Gurobi support, sadly, since my Gurobi instance is on another box (where I don't have MMA), and I needed to benchmark against HiGHS, CBC etc.
It's a good point that most people won't be using Mathematica for solving LP and MIP models as it just uses CBC as the backend anyway. I mean you could of course, but I think most folks would just use an API to call CBC more directly outside of Mathematica. I bet they could add this feature easily enough though.
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.
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.
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)
I learned about it when a friend gave me a programming challenge: 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