Survey of transformations related to the use of SAT solvers I am starting to investigate the possibility of relying on a SAT solver to tackle an optimisation problem I'm interested in, and am currently looking for a survey that would feature examples of "clever" transformations to variants of SAT (i.e., transformations that result in a problem of reasonable size, since I'm not interested in proving hardness results but in actually solving the problem), approximately in the spirit of what can be found in the survey on cubic graphs by Greenlaw and Petreschi, if any comparison can be made between the two.

Has such a survey eluded me because it does not exist, or because I just missed it?
Not sure if that is what you're looking for but here is one: J.M. Silva, Practical applications of Boolean Satisfiability.