- 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”?
- > 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...
- 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."
- 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.
- 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
- I guess z3 is fine with it, but it confuses me that they decided pips wouldn't have unique solutions
- This is good too: https://yurichev.com/writings/SAT_SMT_by_example.pdf
- imo this is the pdf that many people like me used to learn SAT/SMT.
- 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.
- I have read that article too and very interest in the solver
- 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 took a course on SMT solvers in uni. It's so cool! They're densely packed with all these diverse and clever algorithms. And there is still this classic engineering aspect: how to wire everything up, make it modular...
- The solution is to look at a lot of examples
- Going one abstraction deeper, SAT solvers are black magic.
- Yes, explaining the "why / how did the SAT solver produce this answer?" can be more challenging than explaining some machine learning model outputs.
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.
- If you're good at doing this, you should check out the D-Wave constrained quadratic model solvers - very exciting stuff in terms of the quality of solution it can get in a very short runtime on big problems.
- This is great. So many times I’ve wondered how to actually use z3 and I couldn’t figure it out. Thank you!
