On another note, anyone actually run into a random k-SAT problem in "real life"?
Because there's a lot of research into solving SAT "pretty quickly", one of the half-reasonable ways to approach an NP-complete problem is to find an efficient reduction and use a premade SAT solver/heuristic. I don't think nearly as much work has gone into that sort of thing as, say, integer programming (http://en.wikipedia.org/wiki/Integer_programming), but I remember reading something about it a couple of years ago.
Of course, when people realise their problem is NP-complete they tend to go a different way with things. The usual answers are:
1. Problems in practice are small enough for brute-force (or a simple backtracking search)
2. We probably don't need optimality, just use some kind of heuristic or metaheuristic.
From what I've heard, researchers are actually rejoicing, once they are proven a problem is in NP (instead of something worse or unknown status): because that's means it's quite likely that most of it's instances are tractable and we know lots about how to solve NP problems.
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.
Because there's a lot of research into solving SAT "pretty quickly", one of the half-reasonable ways to approach an NP-complete problem is to find an efficient reduction and use a premade SAT solver/heuristic. I don't think nearly as much work has gone into that sort of thing as, say, integer programming (http://en.wikipedia.org/wiki/Integer_programming), but I remember reading something about it a couple of years ago.
Of course, when people realise their problem is NP-complete they tend to go a different way with things. The usual answers are:
1. Problems in practice are small enough for brute-force (or a simple backtracking search)
2. We probably don't need optimality, just use some kind of heuristic or metaheuristic.
3. Too hard, let's do something else.