CDR: Re: Minesweeper and defeating modern encryption technology

[Sampo A Syreeni]

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 at iki.fi>, aka decoy, student/math/Helsinki university