<p>Not sure if that is what you're looking for but here is one: <a href="http://ieeexplore.ieee.org/xpls/abs_all.jsp?arnumber=4605925&amp;tag=1">J.M. Silva, Practical applications of Boolean Satisfiability</a>.</p>

CC BY-SA 2.5
2011-04-06T07:31:00.710Z
I could not access it through your link, [here's another one](http://eprints.ecs.soton.ac.uk/15340/1/jpms-wodes08.pdf). At first glance, the paper seems quite interesting, but more focused on applications than what I am looking for.
Anthony Labarre
CC BY-SA 2.5
2011-04-07T00:12:49.643Z
@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.
Mikolas
CC BY-SA 2.5
2011-04-05T18:44:22.163Z
2011-04-05T18:44:22.163Z
Mikolas
<p>Chapter 2 of the <a href="http://www.st.ewi.tudelft.nl/sat/handbook/">Handbook of Satisfiability</a> 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:</p>

<ul>
<li><strong>Chromatic number</strong>: see <a href="http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.45.9473&amp;rep=rep1&amp;type=pdf">Iyama and Miyazaki</a></li>
<li><strong>Clique</strong>: see <a href="http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.45.9473&amp;rep=rep1&amp;type=pdf">Iyama and Miyazaki</a></li>
<li><strong>Hamiltonian circuit</strong>: see <a href="http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.45.9473&amp;rep=rep1&amp;type=pdf">Iyama and Miyazaki</a></li>
<li><strong>$n$-queens</strong>: see <a href="http://ieeexplore.ieee.org/xpls/abs_all.jsp?arnumber=54670&amp;tag=1">Nadel</a></li>
<li><strong>Stable marriage</strong>: see <a href="http://www.springerlink.com/index/1JMWPWRJF7X3V29Y.pdf">Gent et al.</a></li>
</ul>

CC BY-SA 3.0
2011-04-21T12:58:21.867Z
2011-04-21T12:58:21.867Z
Anthony Labarre
<p>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 <a href="http://dx.doi.org/10.1145/234782.234783">the survey on cubic graphs by Greenlaw and Petreschi</a>, if any comparison can be made between the two.</p>

<p>Has such a survey eluded me because it does not exist, or because I just missed it?</p>

CC BY-SA 2.5
2011-04-05T14:41:17.713Z
What do you exactly mean by "variants of SAT"?
Giorgio Camerani
CC BY-SA 2.5
2011-04-05T14:46:41.993Z
@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
CC BY-SA 2.5
2011-04-05T16:24:51.707Z
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
CC BY-SA 2.5
2011-04-05T18:54:36.960Z
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
CC BY-SA 3.0
2011-04-08T17:27:10.050Z
this question might be somewhat related: http://cstheory.stackexchange.com/q/4314/4506
Mikolas
CC BY-SA 3.0
2012-09-20T00:56:17.047Z
yes SAT is amazing in how many problems can be translated to it, but unless your problem is rather unusual, it might have its own [more efficient] methods in the literature. translating to SAT is interesting to study "why" problem instances are hard or easy based on its constraint graph structure, but not always such a good idea to get the fastest algorithmic solution. another rule of thumb is to estimate how many clauses/variables your instances will have and compare that to known benchmarks of the algorithms.
vzn
<ds.algorithms><reference-request><sat><optimization>
Survey of transformations related to the use of SAT solvers
Anthony Labarre
# Survey of transformations related to the use of SAT solvers

(Asked by: username_0 on 2011-04-05)

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](http://dx.doi.org/10.1145/234782.234783), 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?

**Tags:** ds.algorithms, reference-request, sat, optimization
> **Comments:**
> **username_1**: What do you exactly mean by "variants of SAT"?  
> **username_0**: @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.  
> **username_1**: 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.  
> **username_2**: 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.  
> **username_2**: this question might be somewhat related: http://cstheory.stackexchange.com/q/4314/4506  
> **username_3**: yes SAT is amazing in how many problems can be translated to it, but unless your problem is rather unusual, it might have its own [more efficient] methods in the literature. translating to SAT is interesting to study "why" problem instances are hard or easy based on its constraint graph structure, but not always such a good idea to get the fastest algorithmic solution. another rule of thumb is to estimate how many clauses/variables your instances will have and compare that to known benchmarks of the algorithms.  

---

## 2 answers

### Answer by username_0 on 2011-04-21. Score: 9 | Accepted answer

Chapter 2 of the [Handbook of Satisfiability](http://www.st.ewi.tudelft.nl/sat/handbook/) 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:

* **Chromatic number**: see [Iyama and Miyazaki](http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.45.9473&rep=rep1&type=pdf)
* **Clique**: see [Iyama and Miyazaki](http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.45.9473&rep=rep1&type=pdf)
* **Hamiltonian circuit**: see [Iyama and Miyazaki](http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.45.9473&rep=rep1&type=pdf)
* **$n$-queens**: see [Nadel](http://ieeexplore.ieee.org/xpls/abs_all.jsp?arnumber=54670&tag=1)
* **Stable marriage**: see [Gent et al.](http://www.springerlink.com/index/1JMWPWRJF7X3V29Y.pdf)


---

### Answer by username_2 on 2011-04-05. Score: 10

Not sure if that is what you're looking for but here is one: [J.M. Silva, Practical applications of Boolean Satisfiability](http://ieeexplore.ieee.org/xpls/abs_all.jsp?arnumber=4605925&tag=1).

> **Comments:**
> **username_0**: I could not access it through your link, [here's another one](http://eprints.ecs.soton.ac.uk/15340/1/jpms-wodes08.pdf). At first glance, the paper seems quite interesting, but more focused on applications than what I am looking for.  
> **username_2**: @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.  

---

