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”?
gopalv 2 hours ago [-]
> 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.
imo this is the pdf that many people like me used to learn SAT/SMT.
sophacles 3 hours ago [-]
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.
ngruhn 2 hours ago [-]
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...
mikestorrent 2 hours ago [-]
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.
pkoird 2 hours ago [-]
Going one abstraction deeper, SAT solvers are black magic.
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."
I used it to solve the new NYT game, Pips: https://kerrigan.dev/blog/nyt-pips