3 ms·

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

• mochomocha 7y ago
  Not SAT but this a recent example of using Mixed Integer Programming in real life: https://medium.com/netflix-techblog/predictive-cpu-isolation-of-containers-at-netflix-91f014d856c7 https://medium.com/netflix-techblog/predictive-cpu-isolation... (I'm one of the author of the article)
• ackbar03 7y ago
  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
  • xfer 7y ago
    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.
    • nullc 7y ago
      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.