It's a quite common reaction in AI, yeah: once we can reduce the problem to some standard NP-problem solver, we're probably in good shape.
I believe SatPlan (1992) initiated that trend, by showing that compiling classical planning problems to SAT can get significant speedups over traditional planning algorithms in some cases. This ties into another, mostly informal hallway debate so far, over whether AI needs a replacement idea of "AI-completeness" to specify the problems that are really hard from an AI perspective. I wrote a short opinion piece on that a few years ago: http://www.kmjn.org/notes/nphard_not_always_hard.html
A more common problem than SAT not being fast enough is the reduction being intractable. It's ok if it's "big" (SAT solvers can solve for millions of variables), but it's easy for naive encodings to generate truly absurd blowups, gigabytes or more, which can make it intractable to even state the SAT problem, i.e. write it to disk or send it over a pipe. If you avoid that problem, the actual SAT-solving step is usually fast. I believe that's where some of the interest in alternatives to SAT comes from, as compilation targets, so to speak, that are easier to generate non-blown-up code for.
SAT-heritage grounding targets are still common in logic programming, though, e.g. http://potassco.sourceforge.net/ uses a SAT-like approach, though one specialized for answer-set programming rather than directly targeting SAT.
I've got a bit of a mirror image of that: I use these "AI-heritage" finite-domain solvers like SAT, ASP, clp(fd), but have been wondering lately if tools from other communities, such as integer programming, could be more useful to me for some applications. :)
My impression is that there's a little bit of tool-choice segregation by community, with OR people, AI people, software-verification people, and PLs people each having their own favorite tools, and not as much overlap as there could be.
I believe SatPlan (1992) initiated that trend, by showing that compiling classical planning problems to SAT can get significant speedups over traditional planning algorithms in some cases. This ties into another, mostly informal hallway debate so far, over whether AI needs a replacement idea of "AI-completeness" to specify the problems that are really hard from an AI perspective. I wrote a short opinion piece on that a few years ago: http://www.kmjn.org/notes/nphard_not_always_hard.html
A more common problem than SAT not being fast enough is the reduction being intractable. It's ok if it's "big" (SAT solvers can solve for millions of variables), but it's easy for naive encodings to generate truly absurd blowups, gigabytes or more, which can make it intractable to even state the SAT problem, i.e. write it to disk or send it over a pipe. If you avoid that problem, the actual SAT-solving step is usually fast. I believe that's where some of the interest in alternatives to SAT comes from, as compilation targets, so to speak, that are easier to generate non-blown-up code for.
SAT-heritage grounding targets are still common in logic programming, though, e.g. http://potassco.sourceforge.net/ uses a SAT-like approach, though one specialized for answer-set programming rather than directly targeting SAT.