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’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”?
It has to do with the algorithm Z3 uses to do optimization I think (there are different ones).
It works in a "bottom-up" manner, first giving the minimization goal its lowest possible value and then it tries to "work its way up" to something satisfiable.
So in this case there's something like:
goal = c1 + c2 + c3
minimize goal
(even if you write minimize (c1 + c2 + c3), it's still creating that goal variable internally, so to speak)
It now wants to give goal the lowest possible value it can assign it, even if not satisfiable, to start the process. It looks at the bounds of c1, c2 and c3 to determine this, and they're all -infinity.
The lowest possible value of goal is -infinity, which the optimizer has no idea what to do with, and just basically gives up. When used as an application, Z3 will tell you something's wrong by spitting this out in the terminal:
(+ c1 c2 c3) |-> (* (- 1) oo)
A different optimization algorithm, like one that works "top-down" (find the first satisfiable assignment, then make it better) would actually be able to converge. I think OptiMathSAT would be able to handle it because it also does top-down reasoning for this.
CP solvers and MIP solvers all enforce variable bounds so they don't have this issue.
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));
My subconsciousness shouts "MISSING QUOTES" while my ratio says "Calm down, that's nice and clean and safe and how it's supposed to be - ever has been".
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.
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
16 comments
[ 2.8 ms ] story [ 39.8 ms ] threadhttps://www.hakank.org/
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”?
It works in a "bottom-up" manner, first giving the minimization goal its lowest possible value and then it tries to "work its way up" to something satisfiable.
So in this case there's something like:
goal = c1 + c2 + c3 minimize goal
(even if you write minimize (c1 + c2 + c3), it's still creating that goal variable internally, so to speak)
It now wants to give goal the lowest possible value it can assign it, even if not satisfiable, to start the process. It looks at the bounds of c1, c2 and c3 to determine this, and they're all -infinity.
The lowest possible value of goal is -infinity, which the optimizer has no idea what to do with, and just basically gives up. When used as an application, Z3 will tell you something's wrong by spitting this out in the terminal:
(+ c1 c2 c3) |-> (* (- 1) oo)
A different optimization algorithm, like one that works "top-down" (find the first satisfiable assignment, then make it better) would actually be able to converge. I think OptiMathSAT would be able to handle it because it also does top-down reasoning for this.
CP solvers and MIP solvers all enforce variable bounds so they don't have this issue.
I used it to solve the new NYT game, Pips: https://kerrigan.dev/blog/nyt-pips
You'll be able to solve bigger problems with familiar/legible syntax and even use the code in production.
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