Solving P vs NP with computer

Solution 1:

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?

Solution 2:

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.)

See also my answer on CS.SE to Is it NP-hard to decide whether P=NP?

Solution 3:

Just an additional note:

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:

Iterate through every possible string:
  Compile this string with your favorite compiler of your favorite language.

See if this program is a polynomial time algorithm to solve the problem. So, if P=NP, we will eventually hit the algorithm this way, after insanely large number of iterations. Note that the number of iterations is constant; not dependent on the size of the input, notwithstanding the times that we will get programs that just happen to run correctly. Also, note, that we don't know how long to let such a program run; therefore we bound it by a number of steps. See wikipedia/P_versus_NP_problem#Polynomial-time_algorithms for details. Given an NP-complete problem that is polynomial-time verifiable, we will get our solution to the problem. Though we might not know if the program that works for our particular problem works in general for all problems, ie. if it is the algorithm, in truth, this in itself can be considered the algorithm.