Looking for Literature Source for Following idea

Question

I am quite certain that I am not the first to entertain the idea that I am going to present. However, it would be helpful if I can find any literature related to the idea.

The idea is to construct a Turing Machine M with the property that if P=NP then M will solve 3-SAT in polynomial time. (The choice of 3-SAT is arbitrary. It could be really any problem in NP).

Just to be clear, this is not a claim that P=NP. In fact, I believe the opposite. I merely state that if P=NP, then M will provide a polynomial-time solution. If you are looking for an efficient solution, I should warn that this is far from efficient.

M is constructed as follows: first, assume a canonical encoding for all Turing Machines, and apply a numbering to these machines. So, there is a Turing Machine number 1, a number 2, etc. The idea of a Universal Turing Machine that can read the format for a provided machine and then simulate that machine's running on separate input is pretty well known. M will employ a Universal Turing Machine to construct and simulate each Turing Machine in turn.

It first simulates the running of Turing Machine 1 for a single step.
It then looks at the output of Turing Machine 1.
It the simulates the running of Turing Machine 1 for two steps and looks at output, then proceeds to simulate Turing Machine 2 for 2 steps. It continues and loops in this fashion, in turn running Turing Machine 1 for k steps then 2 for k steps ... then eventually machine k for k steps.

After each simulation run, it examines the output of the run. If the output is an assignment of variables satisfying the 3-SAT problem instance, M halts in an accept state. If on the other hand, the output is a proof-string in some verifiable proof-language with the proven result that the problem instance is not satisfiable, M halts in a reject state. (For a proof-language, we could for example, use the Peano Axioms with Second-Order logic and the basic Hilbert-style logical axioms. I leave it as an exercise for the reader to figure out that if P=NP, a valid proof-language exists and is polynomial-time verifiable).

I will claim here that M will solve 3-SAT in polynomial time if and only if P=NP. Eventually, the algorithm will find some magical Turing Machine with number K, which just so happens to be an efficient solver for the 3-SAT problem, and is able to provide a proof of its results for either success or failure. K will eventually be simulated running poly(strlen(input)) steps for some polynomial. The polynomial for M is roughly the square of the polynomial for k in the largest factor, but with some terrible constants in the polynomial.

To reiterate my question here: I want to know if there is a literature source that employs this idea. I am somewhat less interested in discussing the idea itself.

Answer 1

It seems that this idea is attributed to Levin (It is called optimal search). I believe this fact is well known. A similar algorithm is described in wikipedia for instance, although using the subset sum problem. In this article from scholarpedia you can find several references on the subject, including a pointer to the original algorithm and to some other optimal search algorithms.

Comment 1: Levin's optimal search guarantees that if $\varphi$ is a satisfiable instance then a solution will be found in polynomial time assuming $P=NP$. If $\varphi$ is not satisfiable the algorithm may not terminate.

Comment 2: As Jaroslaw Blasiok pointed out in another answer, this algorithm does not decide Sat only assuming P=NP.

Answer 2

The idea of diagonally running all possible Turing machines has been previously used by Leonid Levin in what is now famously called Levins Universal Search. Unfortunately, and contrary to the extremely common misconception, for what I know variations on Levins universal search are NOT able to provide explicit algorithm solving SAT (decision problem) in polynomial time, given solely the assumption that P=NP - and neither your algorithm does.

The caveat of proposed reasoning lies (as very often) in the "easy exercise left to the reader" - I was unable to prove the exercise myself and I do not believe that its statement is true, namely:

Assuming P=NP, there are polynomial-size ZFC proofs of unsatisfiability of given Boolean formula.

Moreover: I can not see how to prove the existence of polynomially short ZFC proofs for unsatisfiability under the (stronger) assumption that "P=NP is provable in ZFC". It becomes easy however under the yet stronger assumption, namely:

(*) There exists machine M running in polynomial time which provably solves SAT.

And this is, I believe, the correct assumption under which your algorithm solves SAT in polynomial time. Above by "provably solves SAT" I mean: there exists a machine M, and a ZFC proof that M solves SAT.

Note that this assumption is still slightly weaker than the following one: (**) There exist machine M, which provably runs in polynomial time and provably solves SAT.

Under (**) one can have explicit construction achieving the same goal which is even simpler: enumerate all the ZFC proofs until you find the correct machine M (spending constant time), and then run M on this given instance.

It is true, however, that under the P=NP assumption there exist some polynomially verifiable proof system with short proofs for unsatisfiability of any given unsatisfiable formula. Unfortunately, we know neither the proof system nor the verifier offhand, so it is not helpful in this setting.

The original paper of Levin on the algorithm (1973, "Universal search problems") applied it in the following setting: suppose you have an explicit and fast algorithm A for computing function f, and algorithm B for checking whether a value x is in range of f. Then given x, you can explicitly find some value in preimage $f^{-1}(x)$ up to a constant factor as fast as the optimal algorithm for finding it.

Note that this scheme applies, for example, to the FACTORING problem; here f is just multiplication (defined only for factors other than \pm 1) and B is primarity checking. Hence Levins universal search would be (up to a constant factor) optimal algorithm for FACTORING, if that optimal algorithm is slower than the known algorithm for primarity checking - otherwise, the primarity checking becomes dominant.

Moreover, using the Levins method under the P=NP assumption one can provide an explicit algorithm for solving a decision problem in $NP\cap co-NP$, given that one already has explicitly both NP and co-NP verifiers (I.e. Verifiers for YES-instance witnesses, and NO-instance witnesses). Yet another interesting example: if we know the time-bound of the optimal SAT solver offhand, Levins method can be used to solve SAT correctly on all but finitely many instances - still falling short of solving the SAT decision problem as it is stated.