I'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

I'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...