# 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?

• What do you exactly mean by "variants of SAT"? – Giorgio Camerani Apr 5 '11 at 14:41
• @Walter: Sorry if this is not the right word, I meant things like $k$-SAT, Planar-SAT, NAE-SAT, and so on... but I should probably enclose those two words between parentheses, since I don't know whether that matters when using SAT solvers. – Anthony Labarre Apr 5 '11 at 14:46
• Don't worry, it is the right word, I should have understood that. From a purely practical point of view, however, I don't think that it matters (what matters most is how parsimonious your encoding is). Could you provide some further details on the optimization problem you're trying to solve? I'm very interested in practical applications of SAT and in the engineering aspects of SAT solving. – Giorgio Camerani Apr 5 '11 at 16:24
• It sounds a little bit confusing that you are talking about an optimization prob but at the same time about SAT. Typically for optimality you need something stronger, e.g. MAX-SAT. Maybe you could clarify that. – Mikolas Apr 5 '11 at 18:54
• this question might be somewhat related: cstheory.stackexchange.com/q/4314/4506 – Mikolas Apr 8 '11 at 17:27