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.
There is a nice paper that helps visualize the internal structure of SAT instances. See Visualizing SAT Instances and Runs of the DPLL Algorithm 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.