A preprint by Sten-Åke Tärnlund, purporting to prove that P≠NP, is making its rounds on the internets. I noticed it through a blog post by Bruce Schneier; he quite sensibly notes that "these sorts of papers make the rounds regularly, and [Schneier's] advice is to not pay attention to any of them."

Still, someone has to try to pick such papers apart, if only to make sure that they are as worthless as statistics suggest. I'll volunteer for this one. (This mini-review was originally intended to be a comment to Schneier's posting, but grew a bit too large for that. Also, I want to use markup that plain-text comments cannot contain).

It is not easy to figure out what the author is getting at, because the paper is pithy to the point of sloppiness. Take, for example:

By comparison with other similarly terse definitions, this apparently meansDefinition 8p(a) for c·|a|^{q}some c q ∈ N any a ∈ L.

But what are the scope of the quantifiers onDefinition 8.Letp(a)abbreviatec·|a|for some^{q}candqinN, and any lista.

*c*and

*q*? Are they constant throughout the paper or can they depend on something? What can they depend on? It makes no sense in context to let them depend on

*a*... Complexity theory has no lenity for those who fail to be rigorous about order and scope of quantifiers.

Formally, the paper begins to go wrong no later than Definition 13,
where *T(s,a,u)* is defined to mean something that involve the
"truth" symbol ⊨ (or |= if your font, like mine, has no native
Unicode glyph for this symbol), which is not in the language of
**B** – but in the remainder of the paper *T(s,a,u)* is
treated as if it was a formula of **B**, and bogosity ensues.

Of course, a formal error does not mean that the idea behind the paper is flawed. But it does not bode well – one would think that an author who is smart enough to solve an open problem as famous and long-standing as this would be more careful. Indeed, a true flaw shows up:

As far as I understand it, the main argument in the paper
goes somewhat like this: Assume that you give me a Turing machine that
purports to solve SAT (*i.e.*, decide whether a propositional
formula is a tautology) in polynomial time. Then I'll try to run a
sufficiently large "pigeonhole formula" *PF _{m}* through
your machine. I already know that this formula is a tautology, but if
your machine tells me that in polynomial time, I can extract a short
proof of the formula from what the machine does. This contradicts a
theorem by Haken which says that proofs (in a certain restricted form)
of the pigeonhole formula are always long. Therefore, your machine
either does not solve SAT or does not do it in polynomial time.

~~What first meets the eye here is that the paper appears to redefine
SAT. The SAT we all know and love is about ~~
*propositional*
formulas (*i.e.*, expressions built from Boolean variables and the
Boolean operators `not`

, `and`

, `or`

and so forth). However, *PF _{m}* which the paper tries
to use the SAT solver on is not propositional. It is defined only
informally here, but for it to have any relation to Haken's theorem,
it needs to contain non-Boolean variables and equality
operators. Those belong to

*predicate calculus*, not propositional logic. However, this is not in itself damning, because satisfiability in the pure first-order theory of equality is easily seen to be in NP. A valid proof that

*this*is outside P would also solve the P=NP question.

**Correction (2008-11-09):** It turns out that there are indeed
purely propositional formalizations of the pigeonhole principle, and
the paper must be referring to one of those. I had in mind a
formula such as "(a=1 or a=2) and (b=1 or b=2) and (c=1 or c=2) implies
a=b or a=c or b=c". What I did not notice (and, in my defence, the paper
never writes out an example of its *PF _{m}*) was that we
can just expand, say, "a=b" to "(a=1 and b=1) or (a=2 and b=2)", in which
case we can take things like b=2 as propositional variables.

The true fallacy here, however, is the tacit assumption (partly
concealed as Definitions 13 and 14) that if we have a Turing machine that
recognizes tautologies, then a short proof that this machine answers
yes for a given formula corresponds to a short proof that the formula
is indeed a tautology. But this is not necessarily true; it is at
least conceivable that there is a fast Turing machine that recognizes
tautologies but that we cannot prove that this is what it does. In
that case, a trace of the Turing machine's action does not correspond
to *any* proof that the formula is a tautology, much less a
short one. And even if the machine provably recognizes tautologies, we
cannot necessarily extract a short proof in a particular formalism
from a short run of the machine.

There is various additional smoke and mirrors, including the central proposition which is stated thus:

Does this mean simply that there is some consistent extension ofTheorem 1SAT ∉ P is true in a simply consistent extensionB'of theoryB.

**B**in which SAT is not in P, or that SAT∉P is true in every consistent extension of

**B**? I cannot tell. In the former case, the proposition says nothing about the standard model for

**B**(i.e. Turing machines modeled with the standard integers, which are not necessarily a model for the extension). In the latter case, why bother speaking about extensions in the first place?

In conclusion, Schneier is right, and this can safely be ignored.

If your comments on the preprint by Sten-Åke Tärnlund is a joke then, please, ignore our remark.

ReplyDeleteBut if you just got lost, we shall try to help you to start over.

First, take a good look at the formulas of theory B, then it should be clear why

theorem 1 mentions the simply consistent extension B', introduced in definition 15.

Yes, that's right SAT ∉ P is in B', but not in B. For the Turing machines in the set U

B' is simply consistent by corollary 2. Thus there is, if you don't mind, an intended model for B'.

Unfortunately, this contradicts your comment that this model is: not necessarily a model for the extension.

Second, you are right there is a true fallacy here. Your statement: there is a fast Turing machine that recognizes tautologies

but that we cannot prove that this is what it does. Of course, there is no such machine in theory B. Just take a good look at

axiom 1, and definition 5, 13 and 14.

So much for what you call the main argument of the paper.

Third, unfortunately, you are plying a bit dirty for our taste.

You claim that

(i) : the paper appears to redefine SAT.

This is of course wrong, see definition 11 that defines SAT as usual.

(ii) : However, PFm which the paper tries to use the SAT solver on is not propositional. It is defined only informally here, but for it to have

any relation to Haken's theorem, it needs to contain non-Boolean variables and equality operators.

Sorry, you are wrong. PFm is not defined informally. It is not defined at all in the paper. It refers to the same pigeonhole formula of Haken as you

say is propositional for Haken, but not propositional for Tarnlund. Obviously, your argument collapses.

Fourth, there is more to correct, but we leave it for now and save our energy to scrutinise

Tarnlund's proof. After all the problem P vs NP is interesting enough to push on to the more sophisticated parts of the proof. You are welcome to join our reading club when you have catched up.

RCLP

Readings in complexity, logic and programming

You are right that PF_m can indeed be taken as propositional. My bad. Correction entered in posting.

ReplyDelete"First, take a good look at the formulas of theory B, then it should be clear why theorem 1 mentions the simply consistent extension B', introduced in definition 15."

Definition 15 does not introduce or even mention any B'. A few lines above Definition 15 theres an (incomplete) sentence that mentions B' but does not say anything to pinpoint B' among the infinity of consistent extensions of B, or even say how B' differs from B.

"Your statement: there is a fast Turing machine that recognizes tautologies but that we cannot prove that this is what it does. Of course, there is no such machine in theory B. Just take a good look at axiom 1, and definition 5, 13 and 14."

I believe you are misunderstanding my statement. For a given input, B can of course prove that the Turing machine computes whatever it computes. But I was talking about the meta-level statement that for ALL inputs "whatever the Turing machine computes" happens to be the correct answer to the SAT problem for that input.

"So much for what you call the main argument of the paper."

The main argument in the paper appears to be the step from equations (49) and (50) to (51) where you assume that a fast run of an *arbitrary* SAT-solving Turing machine corresponds to a short resolution proof of its input. Your response does not address that at all.

However, here is a counterexample to (49),(50)=>(51): Consider a SAT-solving machine which works by first checking if its argument is textually identical to not-PF_m (easily done in polynomial time) -- if so it answers 'unsatisfiable' immediately; otherwise it does a slow exhaustive search for a satisfying truth assignment. It is true that there is a (polynomially) short proof in B that the Turing machine answers 'unsatisfiable' on not-PF_m, but that is not the same as a short resolution proof of PF_m itself. (As it had better not be, because that would contradict Haken).

I'm aware that my machine does not satisfy (47), but it does satisfy (48)-(50), so it works as a counterexample for the purported inference from (49),(50) to (51).

Furthermore, the paper does not even attempt to justify the inference that leads to (51). Why, the very definition of the notation used in (51) is the last thing that happens before Theorem 1, and nowhere is there any sentence or argument that connects the length of Turing machine computations to the length of resolution proofs.

Let me try to clarify what RCLP tried to say. I can understand that they do not bother to reply on your last response, so let me do it on their behalf.

ReplyDeleteI am not claiming that Tärnlund's paper is correct, since I haven't gone through the details yet. However, it hurts my sense of justice when a paper gets debunked for the wrong reasons. Note that your blog is already being quoted on the internet as a negative indication of the papers correctness.

First of all, Tärnlund argues that there cannot exist a polynomial length deduction of some tautologies of the pigeon hole principle in Theory B (relating it

to a Hilbert system of propositional logic).

Second, you state that:

"I believe you are misunderstanding my statement. For a given input, B can of course prove that the Turing machine computes whatever it computes. But I was talking about the meta-level statement that for ALL inputs "whatever the Turing machine computes" happens to be the correct answer to the SAT problem for that input."

You don't need to be able to prove that your Turing Machine solves SAT for all possible inputs. It is sufficient to assume that you are in the possession of a Turing Machine that solves SAT. Tärnlund takes such a turing machine and adds a trail of deductions in Theory B starting from the axiom B.

Given such a Turing Machine, run the negation of a sufficiently large tautology of the pigeon hole principle (named F).

For this particular input there cannot exist a polynomial deduction of the fact that F is a tautology. But since we run -F and finds (in polynomial time) that

the clause is not satisfied, we can deduce that F is a tautology, and furthermore, the trail left by our turing machine constitutes a proof in theory B of this fact.

But in Theory B there cannot exist a polynomial proof

that F is a tautology. Thus, we get a contradiction.

What I want to say is that you do not need to prove that your Turing machine solves SAT for all possible inputs. The assumption is that it does.

"However, here is a counterexample to (49),(50)=>(51): Consider a SAT-solving machine which works by first checking if its argument is textually identical to not-PF_m (easily done in polynomial time) -- if so it answers 'unsatisfiable' immediately; otherwise it does a slow exhaustive search for a satisfying truth assignment. It is true that there is a (polynomially) short proof in B that the Turing machine answers 'unsatisfiable' on not-PF_m, but that is not the same as a short resolution proof of PF_m itself. (As it had better not be, because that would contradict Haken)."

I am not sure what you are saying here. What does "textually identical to not-PF_m" mean, and how is that easily done in polynomial time?

Note again that if we feed our SAT solving TM with -F and it returns in polynomial steps with an unsatisfying

result, we have (in theory B, starting from axiom B) proved that F is a tautology (because if -F is not satisfiable, there cannot be a non-truth assignment of F).

Consider the "short proof" definition of NP. It states that if there is a satisfying assignment then there should be a short proof of its correctness. But it does not say anything about unsatisfiability. This is what Tärnlund aims at. Use Theory B to get a proof even for unsatisfying assignments. This is sweet.

To debunk the paper I would focus on Theory B and its relation to the Hilbert systems of propositional logic (since personally, I'm not there yet).

Mikael Hammar

PhD Computer Science

Apptus Technologies AB

What has happened to this proof?

ReplyDeleteI attended a lecture by Sten-Ake Tarnlund yesterday, and despite his age he appears to still be working on this. I didn't understand everything, being a master student, but all in all it appeared that he has gotten more structure, clarifications and more support for his proof. I can't make any guarantees but I believe something might be published in a not so distant future.

Delete