The computer proof was found by applying powerful search techniques guided by general search tactics. Unlike some previous results in the area of automated theorem proving, this time several aspects of the computer proof could be called creative by mathematicians' standards. Deep Blue's performance and the resolution of Robbin's theorem are good examples of a qualitative change in performance of compute- intensive approaches compared to just a few years ago. In my own work, on stochastic reasoning and search methods, our most recent procedures can handle problem encodings with tens of thousands of variables and several million constraints . Being able to tackle problem encodings of this size has led to a qualitative difference in the kinds of tasks that one might consider for general search and reasoning methods.
Automatic planning is one of our application areas.
I predict that this is just the beginning of a shift to compute-intensive methods. Given the tremendous difficulty of supplying a program with certain kinds of domain-specific knowledge, we may in fact be better off attacking the inherent combinatorics head on. I don't mean to suggest that simply faster machines and implementations will be sufficient. Further research on search and reasoning procedures and on problem encodings will certainly be needed. Also, there are still many examples where general methods quickly become ineffective.