When using minizinc or other constraint programming tools to solve puzzles that require a single solution, I typically run them asking for 2 solutions. If I get 1 solution only, I know the puzzle is well formed, if I get more than one solution I know the puzzle is mal-formed.

For example, in https://zayenz.se/blog/post/benchmarking-linkedin-queens/#te... I took a large number of LinkedIn Queens puzzles, and I filtered out the ones that were not well-formed so that they wouldn't mess up the benchmarking and statistics.

Any tool that can solver hard problems will also have non-trivial runtime behavior. That is an unfortunate fact. But you are also correct in that combinatorial optimizaton solvers (CP, SAT, SMT, MIP, ...) often have quite sharp edges that are non-intuitive.

For the iOS AutoLayout, what kind of issues have you seen, and how complex were the problems?

It’s a familiar error for iOS developers: “constraints are too complex to solve”

If you want to work in Python, I would either use OR-Tools which has a Python library or CPMpy which is a solver agnostic Python library using numpy style for modeling combinatorial optimization problems.

There is a Python package for MiniZinc, but it is aimed at structuring calls to MiniZinc, not as a modeling layer for MiniZinc.

Personally, I think it is better to start with constraint programming style modeling as it is more flexible, and then move to SMT style models like Z3 if or when it is needed. One of the reasons I think CP is a better initial choice is the focus on higher-level concepts and global constraints.

If you do want to start with SMT though, z3 has quite good bindings. I found it intuitive to use, and its ability to give you answers to very hard problems is like owning a magic wand.

One missing thing in Rust is that the comparison operators are hard-coded to return bool values, which means that it is not possible to build up full expression trees form normal code using operator overloading. Thus the need for functions like `eq`.

In general, for modeling layers embedded in programming languages, having operator overloading makes the code so much better to work with. Modeling layers where one has to use functions or strings that are evaluated are much harder to work with.

I'm a bit skeptical. When used right; operator overloading is an elegant extension of a language. But all too often i feel they are a too powerful abstraction tool that can be abused to make a library utterly incomprehensible and make intuition about language syntax unreliable. I see this in c++ at times.

In particular if you've looked at linear algebra libraries that have two or three different multiplication operators (cross, dot, bitwise), if they commit to use functions from the start they end up faar more readable than any attempt to abuse operator overloading.

I prefer;

- DSL (domain specific language, especially for symbolic solving such as mathematica)

- Strings (That's just a DSL hiding in a parse() function, that can be called from a different language. Write the code as if its a DSL, but without pulling in a new tech stack)

- Functions, but preferable in a chain-able style. sym("a").add(1).eq(sym("b")).solve() is better than solve(eq(add(1,a),b))

I have seen operator overloading done right... but I've also cursed loudly at it done badly.

Rust in particular use up most symbols for other things (borrow checker takes alot of them, and "==" is forced to be consistent) so you end up with only "+ - * /" as overload-able. "+" and "-" being the least abused from my experience perhaps makes that a good compromise.

I would say that for the specific use-case of a modeling layer for something like constraint programming, SMT, or MIP, full operator overloading is superior. I've written such layers in many languages and used them in even more languages, and it really does help a _lot_ to have the standard mathematical expressions. All the other alternatives become way to cumbersome to write effective models with in my experience.

Is it worth having operator overloading in a language or not? That is a different question. People do bad things with every feature, including operator overloading. I'm slightly in favor of it, but I'm not a fan of using it for anything other than either immediate arithmetic or creating expressions trees representing arithmetic.

Has there been any published example of where this solver outperforms a classical solver?

Manual verification of releases and chain-of-trust systems help a lot. See for example https://lucumr.pocoo.org/2019/7/29/dependency-scaling/

The MiniZinc Coursera courses (https://www.minizinc.org/resources/#courses-title) are useful to get a good basis for understanding constraint programming. It’s not a fast solution being full courses, but it is a very good resource.

I get what you are saying, but this is not libraries that implement dynamic programming.

There are general libraries for dynamic programing that are interesitng, see for example https://didp.ai/

Looks interesting.

Would it be possible to use it as a MiniZinc backend?

Yes, that’s possible. JuLS’ CP layer can map FlatZinc constraints directly, so it could be used as a MiniZinc backend. We haven’t built that bridge yet, but it’s a natural extension and something we’d welcome contributions on.

Would be interesting to see in next years MiniZinc challenge as a way to compare with other solvers.

The point of these types of systems is that you can store energy when it is cheap to do so (there is an abundance of wind and/or solar energy) and use it later.