A dumb introduction to z3
asibahi.github.io
A dumb introduction to z3
1–10 of 42 posts
Re: A dumb introduction to z3
#2This is good too: https://yurichev.com/writings/SAT_SMT_by_example.pdf
Re: A dumb introduction to z3
#3Constraint 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.
Re: A dumb introduction to z3
#4I’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”?
Re: A dumb introduction to z3
#5This 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.
Re: A dumb introduction to z3
#6Constraint 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.
Going one abstraction deeper, SAT solvers are black magic.
Re: A dumb introduction to z3
#7Constraint 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.
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.
Re: A dumb introduction to z3
#8I’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”?…
> 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...
Re: A dumb introduction to z3
#9Constraint 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...
Re: A dumb introduction to z3
#10I 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