# Solving P vs NP with computer

Is it possible to build a computer program that would (eventually) bring a solution to the P vs. NP question?

-
see also empirical results in cs papers and is “Experimental Complexity Theory” being used to solve open problems? tcs.se. it is possible an empirical attack could lead to insights, but because the P=?NP question is about an infinite number of cases, strictly speaking its impossible. another possibility: automated theorem proving –  vzn Nov 6 '13 at 19:25
–  vzn Feb 18 '14 at 2:54

Nobody knows. I suppose if there is a polynomial-time algorithm for 3-SAT (or some other NP-complete problem) then a computer could find it and prove P = NP. And if there is a proof that P isn't NP, well, I suppose a computer could find that, too. Why - are you looking for something to work on this summer?

-
Not necessarily. It is also conceivable that there is an algorithm that always solves 3SAT in polynomial time, but that it is not provable that it does so. –  Henning Makholm Jun 11 '12 at 13:50
Hm.. @realazthat you should probably write an answer. –  user2468 Sep 11 '12 at 0:22

The statement $\mathsf{P}\overset{?}{=}\mathsf{NP}$ (there is a polynomial time Turing machine correctly solving SAT on all inputs) is a first order statement with an alternation of quantifiers and first-order logic is not decidable. There is no algorithm that given such a sentence will tell you if the statement is true or false.

Regarding the provability in a certain theory (say ZFC) the theorems of an effective theory are computably enumerable, i.e. you can list all provable theorems in them and if the statement is provable you will eventually find it. However there is no computable upper bound on the space and time needed to find the proof and the proof can be huge (needing more symbols than all particles in the universe).

Using computers for deciding much simpler problems (propositional tautologies) is considered to be inefficient although there is a lot of theoretical and industrial interest in the topic (Google for "SAT solver"). The most advanced SAT-solvers fail to answer in reasonable time on simple tautologies like Pigeon Hole Principle (there is no injection from a set of size n+1 to a set of size n). They would take years to answer on the instance n=100.

Also note that given a first order formula $\varphi$ and a natural number $n$ in unary, deciding whether there is a size $n$ proof in first order logic for $\varphi$ is itself an $\mathsf{NP\text{-}complete}$ problem.

### Clarification regarding the relevance of the answer to the question:

Existence of a program to decide a particular instance is not the real question because obviously there always exists such a machine (though we may not know what it is or how to find it). Consider two programs, one always output "Yes", the other always output "No". So one of these two programs is capable of solving the problem correctly. Which one? We don't know!

So we there exists a program that answers a particular instance of a problem. But to write it we need to know the answer to the instance in the first place. That is not what people mean when they say can we write a program to solve a particular instance of a problem. What is mean is not existence. We want to write such a program without knowing the answer to the question. That is not helpful nor what is meant when one is asking for solving a problem using computer programs.

So naturally the problem is writing an algorithm that will find the answer to the problem (here provability) on this instance ($\mathsf{P}$ vs. $\mathsf{NP}$). But what we know about this particular instance that would make it different from any other instance of the problem? Not much. The algorithm needs to work on similar instances also. So the problem naturally generalized to the problem of finding an algorithm that solves this and similar instances.

If someone gives us a graph and asks us to check if it has a $\mathsf{NP\text{-}hard}$ property, we would answer by pointing out that the problem is $\mathsf{NP\text{-}hard}$ in general and is not believed to be solvable efficiently. (Though a generic instance hardness result would be more powerful than the general hardness result.)

Let's consider an example: if I give you an instance of a graph where there is not any clear property which would make it an easy instance it is not unusual to say the problem of checking if the graph has a Hamiltonian circuit is $\mathsf{NP\text{-}hard}$ in general. We don't know anything about the instance. However if the person tells us that the graph is supposed to have some nice properties, e.g. it is planner or it is the Peterson graph then we can say consider algorithms which work on instances that have such properties.

Now let's return to the question. AFAIK there is no evidence that this particular instance (of provability of a first-order arithmetic sentence in ZFC or PA) is easier than any other instance, so the statement about the general difficulty of the problem is relevant. If at some point someone gives us particular useful properties about the instance such that deciding the problem on such instances is easier then one might use computers after that point. In other words, the problem because a different one. But coming up with such properties and a particular algorithm efficiently solving instances with such properties are not done by computers.

(Think about the statement constructively not in the classical sense of existence, we want a computer program to decide these instances, not a non-constructive proof of existence of a program which no one knows what it is. As Bridges writes in his book on computability, in practice no one is going to pay any attention if you give them two algorithms and tell them one of the two algorithms correctly decides the problem they are interested in but no one knows which one.)

-
You generalized the question, pointed out that the generalized question is undecidable, and apparently concluded that the original question is hard. This is analogous to saying “solving the Hamiltonian circuit problem on the Petersen graph is hard because the Hamiltonian circuit problem is NP-complete.” –  Tsuyoshi Ito Jun 13 '12 at 13:13
@TsuyoshiIto I think he was actually saying that the original question could be as hard (i.e. undecidable) as the general question. Unlike the Hamiltonian circuit problem on the Petersen graph, it is unknown whether $\mathsf{P}\overset{?}{=}\mathsf{NP}$ is decidable. –  Quinn Culver Jun 13 '12 at 13:21
@Quinn Culver: I am afraid that you are mixing up the decidability in the computability theory and the decidability (in a specific theory) in the formal logic theory. A single question (such as "is P=NP provable in ZFC?") cannot be undecidable in the computability sense. –  Tsuyoshi Ito Jun 13 '12 at 13:43
@TsuyoshiIto I meant that it is unknown whether $\mathsf{P}=\mathsf{NP}$ is even provable or refutable. –  Quinn Culver Jun 13 '12 at 14:30
I downvoted for reasons already explained by Tsuyoshi Ito. The claim "First-order logic is not decidable. There is no algorithm that given such a sentence will tell you if the statement is true or false" is extremely misleading, because the second clause does not follow from the first. –  MJD Jul 25 '12 at 2:22

There is an existing algorithm that runs in polynomial time, iff (if and only if) $P=NP$. But with an absolutely huge constant. It basically works as follows:
Well, one can argue about figuring that out, but in truth you don't need to. Such an algorithm exists, since we are operating under the assumption $P=NP$, and you will eventually reach it. The time that this takes is not dependent on the size of the input; it is thus a "constant" amount of time (some constant hehe). Of course you might reach a program that just "happens" to work before reaching the correct-in-all-cases algorithm. –  Realz Slaw Sep 11 '12 at 4:15
Just to be clear, this entire operation in itself would be the algorithm. It doesn't solve the orginal question in total; only if $P=NP$, we already solved the problem. Circular argument. I just thought it would be a good point, and was originally an edit in your answer. Jennifer Dylan suggested I make this a separate answer, so I did. –  Realz Slaw Sep 11 '12 at 4:25