Looking for Literature Source for Following idea 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.
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.