On Sat, 4 Nov 2000, Jim Choate wrote:
As to Cooks assertion, it is possible to create logical statements which are irresolvable, irrespective of time or algorithm. So it is clear that there are in fact statements which can't be resolved so there must be at least some class of NP that are not resolvable to P.
You are talking about two very different problems, here. Gödel/Turing sorta things are about problems where quantifiers over an infinite set are permitted. Gödel is about verifying a given formula for all natural numbers (a countable infinity), Turing about deciding whether any given algorithm (there are a countable infinity of these) halts. An instance of SAT, on the other hand, quantifies only over a sequence of fixed length vectors of truth values (the list of all the possible combinations of truth values to be assigned to the variables of the boolean function being tested). If you think of these vectors as binary words, there are always a finite number of these. This number is exponential in the number of variables of the function. So a valid exp-time algorithm to solve SAT is to list all the possible combinations of input values to the multivariate boolean formula, feed them through it (I seem to think that around n^2 time is needed for this) and see whether one of them really satistified it. The latter strategy does not work for Turing/Gödel-kinda situations because the computation would not halt, regardless of the function chosen. It is easy to see that the logic structure of Gödel's and Turing's theorem is far deeper than that of SAT, while SAT is the only one which admits any kind of computational complexity analysis. Sampo Syreeni <decoy@iki.fi>, aka decoy, student/math/Helsinki university