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”?
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...
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."
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.
solver.assert((&x + 4).eq(7));
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.
You can literally watch as the excitement and faith of the execs happens when the issue of explainability arises, as blaming the solver is not sufficient to save their own hides. I've seen it hit a dead end at multiple $bigcos this way.