# Making SAT solvers competitive with specialized algorithms

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) makes the task easier by adding an extra variable

• Any problem that reduces to planar perfect matchings.

• isn't this already happening ? It's a popular trick to reduce a problem to SAT and then run a solver. Jan 14 '11 at 23:08
• 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 Jan 14 '11 at 23:37