I’d be curious if someone here could explain the initial nonsensical answer for the coin change problem.

I understand that not giving the lower bounds effectively lets it find an arbitrarily low (generally very negative) number of coins that satisfy the problem (so the minimization would basically go to negative infinity).

But why would it respond with “to get 37 in the lowest number of coins I’ll give you 37 ones”?

Or is this kind of like “if the answer to your minimization problem is negative infinity, the answer is undefined behavior”?

This is good too: https://yurichev.com/writings/SAT_SMT_by_example.pdf

I also was inspired to play around with Z3 after reading a Hillel Wayne article.

I used it to solve the new NYT game, Pips: https://kerrigan.dev/blog/nyt-pips

Those of you wondering about how to use z3, please consider coding in static python (not z3py) and then transpile to smt2.

You'll be able to solve bigger problems with familiar/legible syntax and even use the code in production.

The way you can write code of the target DSL without wrapping it in a string both gives me fears and excitement:

    solver.assert((&x + 4).eq(7));

This was such a pleasure to read! Thank you for sharing!

My understanding is that solvers are like regexes. They can easily get out of hand in runtime complexity. At least this is what I have experienced from iOS's AutoLayout solver

Would a SQL optimizer use a generic solver as described here or are there special algorithms for such problems?

Does someone, with some experience on this subject, has an opinion on the best solver with binding in Python for a begginer? The OP use Z3 but also mentionned MiniZinc and I heard about Google OR-Tools.

Constraint solvers are a cool bit of magic. The article underplays how hard it is to model problems for them, but when you do have a problem that you can shape into a sat problem... it feels like cheating.

I have read that article too and very interest in the solver

This is great. So many times I’ve wondered how to actually use z3 and I couldn’t figure it out. Thank you!