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)
A very interesting application of constraint programming is the Unison compiler 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 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.)
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.htm...). It is a good way to get your problems into the hands of solver developers.
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/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.
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.
I've been fascinated by constraints ever since I did some work on iOS, using UIKit. The layout constraint mechanism was super cool.
I've been trying to build a programming language for UI designers, and one of the goals is to let designers describe layouts using constraint-based code that reads as close to natural language as possible.
Something like:
// "the blue box is directly beneath the red box"
BlueBox {
top: @RedBox.bottom
}
// "the red box is 10 pixels to the right of the blue box
RedBox {
left: @BlueBox.right + 10
}
Yep, looked into Cassowary after digging into AutoLayout (which is apparently based loosely on Cassowary). I struggle with the math since I'm not formally trained.
In the sense that Turing-complete languages are all equivalent, yes. But in most imperative and functional languages, you'll end up implementing your own solver (as Norvig did), and a DSL to model your problem. Why reinvent the wheel?
If you give me a choice between implementing a solver in an imperative language or a website in Prolog, I'll choose writing the solver. Every time.
Problems in the context of a programming environment where you're already using other languages. Introducing a specialized one does not necessarily make much sense.
well of course, but why not write the solver in Prolog and the website in Python? why are people so allergic to mixing languages?
if the problem is simple to describe, then sure, write a solver or use a binding. I'm just used to the problems being pretty intense and sophisticated.
I've found having a REPL in a symbolic (term-rewriting) language to be invaluable, and can't imagine going back to for-loops and endless maps of symbol tables chugging out text files for debugging.
Most constraint programming applications are written in traditional imperative languages using solver libraries like OR-Tools, Gecode, IBM CP Optimizer, and others. This is both because that works best in the larger context of most applications, but also because solver libraries are generally better than the specific solvers integrated into Prolog systems. Sure, it is possible to use Prolog to solve problems using CP, but in my experience that is a vary small part of the total usage.
I think a lot of folks have figured out it's easier to do these problems using a DSL inside a general purpose language than to try to use something like Prolog to do both.
For example, to optimize the grid, you might have a Python app that imports the GUROBI solver module and tells GUROBI to optimize. The advantage is all the file IO, directory, and database stuff gets to be handled with Python (easy easy).
We cover constraint satisfaction problems in Chapter 3 of the Classic Computer Science Problems series [0] including a very simple backtracking solver and several examples. Most of the chapter from the Python book is available for free, but it's also covered in the Java and Swift books. [1]
I created a short introductory video to the code as well. [2]
Backtracking solvers for constraint satisfaction problems (CSPs) are a subset of the world of constraint programming, as described in the linked Wikipedia article.
I used this to solve some complicated calendar scheduling routines for an app I wrote in Kotlin. Originally, I used some brute force/search methods to handle this, but the approach outlined here provided far better results, and it took less time too.
The entire space of "NP-complete techniques" is very interesting to me. At some point, you will come across an NP-complete problem, and your only choices are to either give up, or try your best to solve the problem anyway.
Constraint Programming "clicks" for me a lot more than SAT solvers, which feel more mystical. BDDs and MDDs also deserve a mention, as BDDs kinda solve the #P-complete problem (counting-NP complete problem: not only finding one valid solution, but the count of all valid solutions to an NP complete situation. Many optimization problems are #P complete, as you want to iterate over all of the valid solutions and find the best one.
Constraint programming is very elegant but metaheuristic approaches often scale much better than a traditional CP approach. Constraint based Lucas search, CBLS, is an interesting fusion
Constraint Programming is NP-complete (non-polynomial bounds, likely exponential complexity).
Simplex is provably within the polynomial bounds of complexity, ie: simplex is a so called "easy" problem in complexity theory.
--------
You're right that simplex is applied to optimization problems. Constraint programming could be seen as a "more generic" optimizer, in that it can handle integer-optimization (simplex cannot handle integer optimization at all).
Of course, integer-optimization is NP complete, which means that constraint programming is innately "inefficient" or "hard" in terms of complexity.
Not quite. Simplex is an algorithm to solve linear programming problems. Linear programming is (weakly) polynomial. The simplex algorithm itself has exponential worst case [0]. Whether there exist a polynomial-time variant of the simplex algorithm is an open problem.
Constraint programming is very broad — it encompasses many types of problems. Some of them are in P, some (most?) are in NP. In principle you can use the simplex algorithm for solving certain constraint programming problems, but mostly when people talk about constraint programming they refer to different techniques.
Constraint Programming is "on the same complexity" as any of your NP-completeness set of problems.
IE: Knapsack problem, Traveling Salesman, etc. etc.
Today, it seems more popular to use "3-SAT Solvers". But constraint programming is "more logical" for some problems to get converted into rather than 3-SAT. Consider 3-SAT and Constraint Programming to be two different "assembly languages" that you can compile your problem into, and then have a generic solver into.
Personally speaking, I think that the constraint solver problem is "easier to compile into" rather than the 3SAT problem, especially when you consider generic constraints that have very efficient solutions.
For example, it is difficult to think of the optimal alldifferent constraint within 3SAT, but in a constraint-solver framework, its just... well... alldifferent. So you can describe Sudoku as the following:
That is: numbers are 1 through 9, and constrain the problem such that each row is alldifferent, and each column is all different, and each "3x3 square" is all different.
----------
IIRC, the Alldifferent constraint can be efficiently solved using maximum flow. So you write a specialized solver for alldifferent using maximum flow (faster than 3SAT / NP Completeness), and this maximum-flow local solution can be "plugged into" the rest of the constraint solver problem, and integrates cleanly with the rest of the solver's NP-completeness search.
SAT solvers are used a lot for NP-complete problems, but they don't use the 3-SAT representation of clauses. 3-SAT is only interesting from a theoretical POV. Nobody uses it in practice.
There are also intermediate representations. For instance, pseudo-boolean retains most of the power of SAT solvers, while at the same time making problems much easier to express in terms of number of constraints needed. For instance, your Alldifferent(X11, X12, X13, X14, X15, X16, X17, X18, X19) constraint would be written as "x11 + x12 + x13 + x14 + x15 + x16 + x17 + x18 + x19 = 1". Same expressive power, on this problem.
> For instance, your Alldifferent(X11, X12, X13, X14, X15, X16, X17, X18, X19) constraint would be written as "x11 + x12 + x13 + x14 + x15 + x16 + x17 + x18 + x19 = 1". Same expressive power, on this problem.
I'm more comfortable with constraint-programming than 3SAT / SMT / etc. etc. So I'm probably getting something wrong here.
I don't think you're correct on this issue? "x11 + x12 = 1" means that "x11 or x12 are 1, and the other is zero".
EDIT: That is, the 9-set of solutions you described is:
That is, the entire set of permutations of the domain of all 9 variables participating in the constraint. What I've listed above is a *complete* Sudoku solver within the constraint-programming mindset.
--------
In most of the 3SAT / SMT solvers for Sudoku I've seen, you set up the variables as: "X111, X112, X113, X114...", which means "X11 == 1", and "X11 == 2", etc. etc. So you then do "X111 + X112 + X113... X119 == 1", meaning "X11 is either 1, 2, 3, 4, 5... 9".
Meanwhile, this entire process is simply "Domain of X11 = {1, 2, 3, 4, 5, 6, 7, 8, 9}" in the constraint-processing world, because variables can have arbitrarily sized (though finite) domains in constraint programming.
That is to say, I'm pretty sure you need 999 == 729 variables to brute-force represent the problem in 3SAT / SMT? Meanwhile, Constraint Solver trivially represents it with 81-variables (but each of these 81 variables, X11 through X99, have a domain of size 9: {1, 2, 3, 4, 5, 6, 7, 8, 9}).
There might be an easier way to represent Sudoku in 3SAT/SMT world, but again, I'm not very good with that world. I "just" know that 3SAT / SMT is a "similar but different" kind of solver and barely have used them.
--------
One can argue that "constraint programming" is simply 3SAT / SMT-solving except with arbitrarily sized domains. Rather than solely using 0 and 1 or boolean functions.
I've been told that "because everything is {0, 1}, more optimizations / inferences can be discovered" in 3SAT/SMT solvers compared to constraint programmers. Meanwhile, constraint programmers benefit from generic constraints that have a polynomial class subsolution (ie: using maximum flow, or other simpler algorithms to solve the subproblem).
It'd take a rather well-studied expert to know whether 3SAT/SMT is better for a particular problem vs constraint-programming.
> I don't think you're correct on this issue? "x11 + x12 = 1" means that "x11 or x12 are 1, and the other is zero".
and
> In most of the 3SAT / SMT solvers for Sudoku I've seen, you set up the variables as: "X111, X112, X113, X114...", which means "X11 == 1", and "X11 == 2", etc. etc. So you then do "X111 + X112 + X113... X119 == 1", meaning "X11 is either 1, 2, 3, 4, 5... 9".
Yes, I've been a bit to fast here. You're absolutely right.
> I've been told that "because everything is {0, 1}, more optimizations / inferences can be discovered" in 3SAT/SMT solvers compared to constraint programmers. Meanwhile, constraint programmers benefit from generic constraints that have a polynomial class subsolution (ie: using maximum flow, or other simpler algorithms to solve the subproblem).
Yes. SAT solvers very often outperform CSP solvers nowadays. But SAT solvers tend to lose the structure of the problem because they are so low-level. The most famous problem they fail to solve is the pigeonhole problem.
If you have, say, the problem "is there a way to put 4 pigeons into 3 different holes, knowing that there can be at most 1 pigeon per hole and at least 1 hole per pigeon?", the answer is obviously "no", but if you try to use a propositional logic representation (in other words, using a SAT solver), the solving track will grow exponentially (4 vs 3 workds well, but SAT solvers will struggle to solve 11 vs 10 in a reasonable amount of time). Pseudo-boolean solvers will be able to using "cutting-planes" strategies that work well for this specific set of problems, but these are slower in the general case.
Plus, modeling your problem in CNF to feed it to a SAT solver is usually incredibly complex and can lead to gigantic formulas if you're not careful. So most of the time, it really makes sense to first use a CSP representation, and fall back to a CNF representation if you're not satisfied with the results for some reason.
OptaPy (open source, https://www.optapy.org) solves similar use cases in Python, but using metaheuristics instead of traditional CP techniques, which helps for scaling out.
In Prolog, the predicate order matters. So, if I understand your question correctly, no. It's up to the dev to order predicates in such a way that the amount of backtracking is kept to minimal.
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