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?

  • $\begingroup$ What do you exactly mean by "variants of SAT"? $\endgroup$ – Giorgio Camerani Apr 5 '11 at 14:41
  • $\begingroup$ @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. $\endgroup$ – Anthony Labarre Apr 5 '11 at 14:46
  • 4
    $\begingroup$ 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. $\endgroup$ – Giorgio Camerani Apr 5 '11 at 16:24
  • $\begingroup$ 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. $\endgroup$ – Mikolas Apr 5 '11 at 18:54
  • $\begingroup$ this question might be somewhat related: cstheory.stackexchange.com/q/4314/4506 $\endgroup$ – Mikolas Apr 8 '11 at 17:27

Not sure if that is what you're looking for but here is one: J.M. Silva, Practical applications of Boolean Satisfiability.

| cite | improve this answer | |
  • 2
    $\begingroup$ I could not access it through your link, here's another one. At first glance, the paper seems quite interesting, but more focused on applications than what I am looking for. $\endgroup$ – Anthony Labarre Apr 6 '11 at 7:31
  • $\begingroup$ @Anthony well you did say you are interested in the practical aspect :-) Anyhow, the existing mainstream solvers do not really differentiate between different types of SAT. In the past there has been some work on exploiting binary clauses, for instance. But the existing solvers just use DPLL+unit prop+clause learning. However, some of the preprocessors exploit the structure. But again, not really from the point of view of complexity th. classification. $\endgroup$ – Mikolas Apr 7 '11 at 0:12

Chapter 2 of the Handbook of Satisfiability surveys the aspects to bear in mind when designing those transformations, as well as a list of references that answer my question. This helped me find a few examples that one can have a look at to familiarise oneself with these transformations:

| cite | improve this answer | |

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.