13
$\begingroup$

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?

Improve this question
$\endgroup$
6
  • $\begingroup$ What do you exactly mean by "variants of SAT"? $\endgroup$
    – Giorgio Camerani
    Commented Apr 5, 2011 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
    Commented Apr 5, 2011 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
    Commented Apr 5, 2011 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
    Commented Apr 5, 2011 at 18:54
  • $\begingroup$ this question might be somewhat related: cstheory.stackexchange.com/q/4314/4506 $\endgroup$
    – Mikolas
    Commented Apr 8, 2011 at 17:27

2 Answers 2

Reset to default
10
$\begingroup$

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

Improve this answer
$\endgroup$
2
  • 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
    Commented Apr 6, 2011 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
    Commented Apr 7, 2011 at 0:12
9
$\begingroup$

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:

Improve this answer
$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

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