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.