[ebiederm]

How does it follow that there is no point in trying for formal correctness? In many problems there is an interesting subset that is quickly solvable even when the general case is not.

SAT solvers in practice are quick on just about everything.

SAT solvers being programs that solve the original NP-compete problem.