What we should do is generate a class of instances of 3-SAT that are expected to be hard, and then try the solver on them and see what the runtime looks like as

What we should do is generate a class of instances of 3-SAT that are expected to be hard, and then try the solver on them and see what the runtime looks like as a function of the size of the input. Recently someone claimed a polynomial-time graph coloring algorithm. I generated hard instances, their "solver" blew up. Claim debunked. It should be simple enough to do the same for this (for some definition of simple). The key lies in generating hard instances. As cperciva has said in http://news.ycombinator.com/item?id=2121837 http://news.ycombinator.com/item?id=2121837 - most instances of most NPC problems are "easy."