Finally found a good example of SMT solving for the book! I've been blocked for a while, because while SMT has a lot of uses, all of the easy-to-show examples are toys. But I finally realized a practical example: given some outputs an RNG, reverse-engineering the parameters! - ThreadSky

hillelwayne.com • 2 days ago

Finally found a good example of SMT solving for the book! I've been blocked for a while, because while SMT has a lot of uses, all of the easy-to-show examples are toys. But I finally realized a practical example: given some outputs an RNG, reverse-engineering the parameters!

Comments

retsl.bsky.social•1 day ago

hazelweakly.me•1 day ago

I keep wanting to learn SMT solvers so I can implement custom placement logic with constraints for Kubernetes clusters 😅

Idk if that can fit in a book but it’s funnnnn

hillelwayne.com•1 day ago

Might be possible actually! I also wonder if regular constraint solvers can work here, but they're more restricted

hillelwayne.com•1 day ago

Throw me a toy problem and I'll see what I can do

rdivyanshu.bsky.social•1 day ago

This one https://rdivyanshu.github.io/posts/2021/06/crux-mathematicorum-ma122-rosette.html

rdivyanshu.bsky.social•1 day ago

Another one if you like https://gist.github.com/rdivyanshu/a6ac8095e9e1cf6be2fbfc559838b130

hillelwayne.com•23 hours ago

I mean like, of kubernetes constraints to solve with SMT :P

jelv.is•1 day ago

I'm not sure exactly how placement works in Kubernetes, but I worked on a compiler project where we had to place code on a bunch of cores connected in a grid and minimize communication

IIRC we used a quadratic programming thing for that sub-problem, even though we used SMT solvers for other things

jelv.is•1 day ago

so if placement in Kubernetes clusters is a similar kind of problem, then that would be the first place I'd look

jelv.is•1 day ago

I did not work on that particular part of the system so my understanding is pretty hazy at best :P

hillelwayne.com•2 days ago

My best example before this was "find two distinct sets of three numbers with the same product and sum", which was suggested by @nelhage.bsky.social. It's been in the book for half a year now, but will be replaced with the reverse engineer sample in v0.9

jelv.is•2 days ago

my favorite example of using SMT solvers to model programs is to run them backwards—although that's definitely on the toy side of the spectrum :P

it's a nice example because it's easy to understand, people find it exciting, and stresses the mental model for how programs are represented as formulas

jelv.is•2 days ago

I like the PRNG version you have because it's more self-contained and more clearly useful

sandmouth.bsky.social•2 days ago

Thats a good one! Verifying bit hacks is nice https://graphics.stanford.edu/~seander/bithacks.html could also synthesize magic constants. Finding configurations in game of life is cool too (in knuth book)

bandukwala.me•1 day ago

This is basically the homework assignment I'm working on for class.

Comments

Posting Rules

Reply