[cube2222]

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”?

[sirwhinesalot]

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.

[cube2222]

Thanks for the explanation!

> When used as an application, Z3 will tell you something's wrong by spitting this out in the terminal: (+ c1 c2 c3) |-> (* (- 1) oo)

This part is what I was looking for. I was surprised that the behavior wasn’t accompanied by any warnings in the article.

[gopalv]

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

Yes, it picked a valid result and gave up.

I got a similar nonsensical result in my run-ins[1] in with SAT solvers too, until I added a lowerbound=0.

The "real life" follow-up question in interviews was how to minimize the total number of intermediate rows for a series of joins within in a cost-based optimizer.

[1] - https://gist.github.com/t3rmin4t0r/44d8e09e17495d1c24908fc0f...

[zdance]

37 is irreducible in the problem statement, so the answer is 37.

Think about it purely in the set-theoretic sense "what is the minimal set containing 37 elements?" the answer is "the set containing 37 elements."

[Dylan16807]

The fixed 37 is the value of the coins. It's very easy to reduce the number of coins.

Either you misunderstood something or please explain more. Note that both the working and broken versions have the same 37 in them.

And the problem statement starts with no coins chosen. It had to actively choose pennies to get that broken result. If you told it about the coins in a different order, it probably would have given a different answer.