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.


2 Answers 2


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.

  • $\begingroup$ I just found the Wikipedia reference, and indeed, it mentions Levin, but without citation. It might be that this has simply become folklore but never used in published literature. Regardless, this is helpful. Thanks. $\endgroup$ Commented Nov 6, 2014 at 21:24
  • $\begingroup$ Welcome. I found a homepage with several references on the subject. I edited the answer to include it. $\endgroup$ Commented Nov 6, 2014 at 21:43

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.

  • 1
    $\begingroup$ If P=NP then co-NP=co-P=P=NP. So UNSATISFIABILITY is in NP, so has polynomial-sized witnesses -- you don't need to invoke a Turing machine. Can't you convert that witness into a ZFC proof that the formula is unsatisfiable? I'm not up on the mechanics of ZFC proof but the intuition that I've received from various places is that, unless you're dealing with "weird stuff", ZFC corresponds to all the things you thought you could prove anyway, before you heard about set theory. Finite objects such as a Boolean formula and a polynomial witness of its unsatisfiability aren't likely to be weird. $\endgroup$ Commented Nov 7, 2014 at 9:15
  • $\begingroup$ Yes, if P=NP, then UNSAT is in NP, and it has polynomial size witness. Namely: zero-size witness, all the work is done by the verifier, right? I have only one idea in mind how to convert this zero size witness into ZFC prove of unsatisfiability: give a ZFC proof that my machine actually solves UNSAT, and then show a run of this machine on the formula - that would be a valid proof, and this corresponds to the fact that algorithm proposed by OP works under (*). But what if there were some tricky machine which just happen to solve SAT, but this fact is unprovable? Not that I belive it is the case $\endgroup$ Commented Nov 7, 2014 at 9:28
  • 1
    $\begingroup$ The misconception I am refering to is: "if P=NP, then Levins Universal Search gives polynomial time algorithm solving NP-complete problem" or as it is sometimes stated: "It is impossible to have only nonconstructive proof of P=NP, because of Levins algorithm". Both those are false - the Wikipedia formulation presents method which stops in polytime on YES-instances of SUBSET SUM, but does not halt at all on NO-instances - it is not an algorithm deciding subset sum in polytime. OP formulation is better for the purpose, but needs stronger assumption than P=NP to decide SAT in polytime. $\endgroup$ Commented Nov 7, 2014 at 16:47
  • 1
    $\begingroup$ I am not sure if I fully understand your comment, but it seems that you are on the right track: in order to run this Levin's universal search for $NP\cap co-NP$ problems under P=NP assumption (those are just all NP problems) --- you need explicitly to have your hands on both verifiers (a verifier for YES instances and a verifier for NO instances). Note that if P=NP then unSAT is in co-NP - but you don't know explicitly the verifier for it, so you can't use it as a building block in your and Levins method. $\endgroup$ Commented Nov 7, 2014 at 23:15
  • 1
    $\begingroup$ Now the way to deal with this, as you do not know explicitly verifier for unSAT problem, would be to try to find a short proof in some formal logic we already know and can verify (let it be ZFC axioms, or Peano - we are more likely to find a short prove in the former though), that this instance is unsatisfiable. But if one wants to prove that there is such a short proof in this formal logic, one need stronger assumption than P=NP. $\endgroup$ Commented Nov 7, 2014 at 23:28

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.