Hacker News Reader

Can you please share your personal experience of using SAT solver with real world problem?

Not SAT but this a recent example of using Mixed Integer Programming in real life: https://medium.com/netflix-techblog/predictive-cpu-isolation... (I'm one of the author of the article)

Cracking product keys for... Uh... Research. You reverse engineer the binary, enter the conditions into an sat solver and boom. But I don't think most keys are implemented this way these days.

Also if you want cool, check out uc Santa Barbara's team for the darpa cyber challenge a few years ago for an autonomous hacking system. Their framework, angr, makes use a lot of sat solvers although I didn't quite understand everything when I read their technical docs

Based on my experience, most key requiring programs use public key crypto and pin their public key in the binary to verify the signature, which is the key.

That hasn't been my experience.

I've seen some that use public key crypto, but mostly they do not because even the smallest secure cryptosystems have signatures on the order of at least 20 bytes (and more conventional choices more like 256-bit ECDSA... 64 bytes)-- which, after conversion to typeable characters, are a bit unwieldy.

Reply on news.ycombinator.com