""" 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, github repository: https://github.com/google/or-tools). It has won multiple gold medals at the MiniZinc challenge (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). """
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.
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.
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.
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.