<p>There is a nice paper that helps visualize the internal structure of SAT instances. See <a href="http://portal.acm.org/citation.cfm?id=1286020">Visualizing SAT Instances and Runs of the DPLL Algorithm</a> by Carsten Sienz (Appeared in SAT 2004). Basically, it draws a graph which the author calls "variable interaction graph" (according to some rules) to visualize the relation between the satisfied clauses. The author shows this by several partial runs of DPLL.</p>

<p>The main claim is that these visualization techniques could be used to detect structure and design an appropiate algorithm for it. However, it is still not clear how can we detect efficiently structures like the one presented in the paper. It is well known that SAT algorithms for one specific problem behave poorly in other problems. So there is "no-free-lunch", although this claim cannot be formally stated as far as I know.</p>

CC BY-SA 2.5
2011-01-14T23:36:24.687Z
I think the relevant "no-free-lunch" theorem is the "no free lunch for search" http://www.no-free-lunch.org/ . Basically we can't afford search over all possible problem structures, and have to bias our search towards particular structures. I think that's OK since human algorithm designers do that already
Yaroslav Bulatov
CC BY-SA 2.5
2011-01-14T23:15:34.493Z
2011-01-14T23:15:34.493Z
Marcos Villagra
<p>What are obstacles to making SAT solvers competitive with specialized graph algorithms? In other words, is it feasible to expect SAT solvers that can replace the role of algorithm designer -- ie, be able to automatically recognize problem structure and then solve it as quickly as a specialized algorithm?</p>

<p>Here some examples I think are challenging for today's SAT solvers:</p>

<ul>
<li><p>Counting independent sets of size $k$. Encoding "x is an independent set of size k" gives a large formula which is hard to solve. An ideal SAT solver would recognize that this problem is easy on bounded tree-width graph with an addition of an extra "count" variable for bags.</p></li>
<li><p>Finding minimum Steiner tree. Again, "Steiner tree" has a global constraint, however, a specialized algorithm (like <a href="http://arxiv.org/abs/0807.3373">here</a>) makes the task easier by adding an extra variable </p></li>
<li><p>Any problem that reduces to planar perfect matchings.</p></li>
</ul>

CC BY-SA 2.5
2011-01-14T23:08:49.340Z
isn't this already happening ? It's a popular trick to reduce a problem to SAT and then run a solver.
Suresh Venkat
CC BY-SA 2.5
2011-01-14T23:37:59.037Z
Yes, but are they competitive? I'm wondering if there is any SAT solver which could take a simple set of constraints describing Eulerian subgraph of a planar graph, and do #SAT in polynomial time
Yaroslav Bulatov
<ds.algorithms><graph-theory><sat>
Making SAT solvers competitive with specialized algorithms
Yaroslav Bulatov
# Making SAT solvers competitive with specialized algorithms

(Asked by: username_0 on 2011-01-14)

What are obstacles to making SAT solvers competitive with specialized graph algorithms? In other words, is it feasible to expect SAT solvers that can replace the role of algorithm designer -- ie, be able to automatically recognize problem structure and then solve it as quickly as a specialized algorithm?

Here some examples I think are challenging for today's SAT solvers:

* Counting independent sets of size $k$. Encoding "x is an independent set of size k" gives a large formula which is hard to solve. An ideal SAT solver would recognize that this problem is easy on bounded tree-width graph with an addition of an extra "count" variable for bags.
* Finding minimum Steiner tree. Again, "Steiner tree" has a global constraint, however, a specialized algorithm (like [here](http://arxiv.org/abs/0807.3373)) makes the task easier by adding an extra variable
* Any problem that reduces to planar perfect matchings.

**Tags:** ds.algorithms, graph-theory, sat
> **Comments:**
> **username_1**: isn't this already happening ? It's a popular trick to reduce a problem to SAT and then run a solver.  
> **username_0**: Yes, but are they competitive? I'm wondering if there is any SAT solver which could take a simple set of constraints describing Eulerian subgraph of a planar graph, and do #SAT in polynomial time  

---

## 1 answers

### Answer by username_2 on 2011-01-14. Score: 7

There is a nice paper that helps visualize the internal structure of SAT instances. See [Visualizing SAT Instances and Runs of the DPLL Algorithm](http://portal.acm.org/citation.cfm?id=1286020) by Carsten Sienz (Appeared in SAT 2004). Basically, it draws a graph which the author calls "variable interaction graph" (according to some rules) to visualize the relation between the satisfied clauses. The author shows this by several partial runs of DPLL.

The main claim is that these visualization techniques could be used to detect structure and design an appropiate algorithm for it. However, it is still not clear how can we detect efficiently structures like the one presented in the paper. It is well known that SAT algorithms for one specific problem behave poorly in other problems. So there is "no-free-lunch", although this claim cannot be formally stated as far as I know.

> **Comments:**
> **username_0**: I think the relevant "no-free-lunch" theorem is the "no free lunch for search" http://www.no-free-lunch.org/ . Basically we can't afford search over all possible problem structures, and have to bias our search towards particular structures. I think that's OK since human algorithm designers do that already  

---

