4 ms·
An interesting thing about this is that you can transform the integer factorization problem into SAT quite easily (I have code that does it). The resulting SAT
by tgflynn 14y ago
An interesting thing about this is that you can transform the integer factorization problem into SAT quite easily (I have code that does it). The resulting SAT problems seem to be hard to solve for heuristic SAT solvers once you get beyond a very small number of bits for the integer sizes.
- mjn 14y agoI'm not very familiar with the literature, but there are some people using SAT solvers in that manner to do a kind of automated cryptanalysis. Here's one paper that encoded the DES procedure into a SAT problem, and looked at how SAT solvers fare on it: http://www.ing.unitn.it/~massacci/papers/mass-marr-00-JAR.pdf http://www.ing.unitn.it/~massacci/papers/mass-marr-00-JAR.pd...