Before an unbeliever comments (as I would do myself if I wouldn't know the algorithm): This algorithm involves enumerating f(M, t) where M is the Gödel number of a turing machine T, t an integer and f the output of T after t steps on the original input. This output is interpreted as variable assignment. If it satisfies the formula, the SAT instance is satisfiable. Otherwise the enumeration continues.

If P=NP there is a turing machine that always outputs a satisfying assignment if one exists with t being polynomial bounded by the input size. As this turing machine is constant, the algorithm runs in poly-time.

So, in simpler terms (for me):

- start with a file size (let's say 4kb), and a duration (let's say 1 hour).

- generate all possible files of the given size (there are 2^32768 of them), mark them as executable and run them. If they don't finish after the given duration, kill them.

- check the output of each program that didn't crash. If one matches the solution, OK. If it doesn't, try again with a longer duration and larger size.

It doesn't just solve SAT. At galactic scales, it will either be the optimal solution to any problem, or be as fast as checking the answer, whatever is slower. If all that code generation thing doesn't depend on the input size, it is constant time. That the constant is many times the age of the universe doesn't change the complexity class.

Yeah, you got the point ;) This however only works for problems where you can validate a solution in polynomial time. There is still the problem what happens when a solution does not exist. Even in this case, the algorithm must terminate in polynomial time.

Interesting, I don’t remember this proof (maybe I learned it, but it’s been a couple of years since university). Do you remember the “stop condition”? At some point the algorithm would have to “give up” and declare the problem unsatisfiable.

I don't know. You could also enumerate all proofs and check whether P is a proof that a turing machine T solves SAT in polytime (if P=NP, this requires a finite number of steps ^) and then run T.

^ It would be funny though if P=NP, but for no turing machine exists a proof that it solves SAT. This would have to be ruled out for the algorithm to work.

Can you give a reference, or a hint on where to read more? This sounds really interesting, but Google has failed me.

Actually, I don't know anymore where I read about this idea - if you find out, please let me know! I've added a description of the algorithm.