The P≠NP “Proof” Is One Week Old
Another update on progress understanding the proof of Deolalikar
Terence Tao is leading, as often is the case, with some very insightful comments on the status of Vinay Deolalikar’s proof.
Today Ken Regan and I want to try to summarize the main issues with Deolalikar’s proof of PNP raised by Tao and many many others.
We intend to give a short summary of where the proof stands and outline what will happen next. A side-effect is this will help “refresh” a comment thread growing past 250 entries on our last post. We hope that a constructive discussion can continue here and on other blogs, as the proof strategy is finally understood by the community. We do believe that beyond the claimed proof there has been much interesting discussion on a host of topics, and we think this discussion has been informative.
We are still hopeful that the promised final release of the “journal paper” by Deolalikar for peer review will be able to answer all the questions raised here and elsewhere. We wish Deolalikar good luck—we hope in a small way we have been able to help him, if indeed he is successful in either releasing a correct proof or deriving some rigorous lesser results from it.
The Two Main Issues
In our opinion there are two parts of the proof, each of which contains difficult issues. Perhaps these issues can be resolved, but the consensus right now seems to be these issues will be hard to avoid.
The first issue is the proof’s use of FO(LFP) as a way to characterize .
The second issue is the proof’s use of the structure of the solution space of -SAT. Both of these have problems which will now discuss.
The First Order Issue
This issue seems to us to be potentially fatal. Recall Neil Immerman pointed out that the proof mis-uses FO(LFP)—and the consequence of this mis-use is that the complexity class studied is not . It is a much weaker complexity class. The class may or may not be interesting, but this is a pretty major issue. How can the proof separate polynomial time from anything if the class called is not ?
To our knowledge no one has disputed Neil’s claim. It is unfair to argue from authority, but Neil is one of the best in the world in this area of logic. The proof is using Neil’s theorem—who better to point out a flaw in this part of the proof. Since this was communicated Thursday evening there has been ample time for, or someone else, to respond. An answer to this needs to affirm that the class being captured by the first-order part of the paper really equals . We are disappointed that Neil’s communication has not been engaged.
Perhaps the pith of the issue is that FO(LFP) is a somewhat exotic way to define . If the proof had used polynomial time Turing machines, then there would be no issue here. But, the use of first order formulas has allowed Deolalikar to claim properties of polynomial time computations that seem plausible in the logic framework. In a classic machine model it seems to us that the claims might be transparently false when reflected in the other issue.
The Solution Space Structure Issue
Here on Saturday Tao posted evidence to have “isolated the fundamental problem with Deolalikar’s argument” on the -SAT solution space side. This followed constructions by Ryan Williams and others showing the inherent difficulty of deriving lower bounds from arguments on solution-space structure.
The particular problem found by Tao is that Deolalikar’s concept of “polylog parameterizability” of a distribution on a solution space may not carry over to the induced distributions when certain variables are projected out. This is not merely analogous to how can be regarded as a projection of . Further discussion has ranged from whether this is a conceptual flaw in Deolalikar’s constructions, or is rescued by the for-contradiction assumption of in the proof. This is reflected on the weblog of Timothy Gowers, the other Fields Medalist actively taking part in these discussions—see also previous items on his weblog. Many others have contributed valuable insights and critiques as this investigation goes deeper.
Tao has also created a separate wiki page on polylog parametrizability, as beginning the rigorous delineation and evaluation of the physics-derived tools in Deolalikar’s paper. The master wiki page continues to be updated.
Some Technical Details on The Solution Space Issue
Here is a more detailed version of this last issue. For -CNFSAT the clauses are disjunctions of -many literals, where each literal is a variable or its negation , Then not only is the existence of a solution -complete, but so is the following extensibility problem even when limited to formulas that are satisfiable. The extensibility problem EXT asks whether a given assignment to some of the variables in can be extended to a satisfying assignment. This is the problem attacked by Deolalikar’s paper. However, one can also make formulas with clauses using the XOR operator between literals, such as:
These formulas are equivalent to systems of linear equations over the finite field , for which these problems can be solved in polynomial time. Hence any proof based on the structure of solution spaces must show an essential distinction between the -CNFSAT and -XORSAT cases. The paper promises this, but not only is no convincing answer evident, commenters have demonstrated what may be an exhaustive net of correspondences by which the cases have indistinguishable solution spaces.
Ryan Williams has also demonstrated such a correspondence within the -CNFSAT spaces themselves. Here is the high level view of his insight: Suppose you are trying to argue that for a certain class of Boolean formulas has an intractable extensibility problem, based solely on features of the solution spaces of . Let , a partial assignment , and a satisfying assignment extending be given. Note that is a yes-instance of EXT. Now create a formula by flipping the sign of each literal or that is not assigned by , and for which .
Then is also a yes-instance of EXT, for the trivial reason that extending by the all-zero assignment on the other variables satisfies it. The point is that the solution spaces of and are isomorphic in a way that preserves every distance and clustering detail perceived in Deolalikar’s paper. For no-instances of EXT, we can extend the mapping from to arbitrarily to preserve a “no” answer for , and the same isomorphism remark applies because the solution spaces are empty. The upshot is that supposedly all algorithms fail on the instances by the claimed proof. The same proof, however, must work on the transformed instances because the employed statistics are identical. The latter, however, have the trivial polynomial-time algorithm that tries extending by the all-zero assignment, and answers yes if and only if that satisfies . With that conclusion, deducing from the proof is a self-contradiction.
It needs to be noted that Deolalikar’s argument takes solution spaces not just as point-sets but as supports of distributions . There has been some doubt about how the EXT case differs from the case where the given is empty, which gives Ryan’s original mapping into the space SAT0 of formulas satisfied by the all-0 assignment. However, the argument appears to be modifiable by taking a distribution on extensions that respects .
“The 3 issues that were raised were (a) the use of locality and the techniques used to deal with complex fixed points (b) the difference between 9-SAT and XORSAT/2-SAT and (c) clarification on the method of parametrization. I will address all these in the version being prepared, which will be sent for peer and journal review.”
The “version being prepared” evidently refers to an earlier promise of a fully technical paper, which many evaluating his work have found wanting. The original paper’s latest version is dated 11 August, while his papers web folder includes all previous versions.
The synposis contains a key footnote:
“In earlier versions of the paper we used locality. We later realized that locality is not the fundamental property of first order logic that we require. What we require is that the first order formula based its decision at each stage only on the presence of fixed formulae in a fixed number of element types, as described by the Gaifman and Schwentick-Barthelmann Normal Forms. Both monadic and complex LFP have this property at each stage, since it characterizes all first-order formulae. It simplifies our proof and resolves the issues raised about the finite model theory portion of the proof.”
The last sentence aims to answer Neil’s objection, but does it? Recall Neil’s contention is that the class whose power is quantified by the finite-model theory section of the paper is not , but rather a class already known to be properly contained in . No one has disputed Immerman’s counter-claim. We are, as we stated earlier, disappointed that this essence of Neil’s communication has not been engaged.
Is It Over?
Yogi Berra said, “It ain’t over til it’s over.” To judge from the discussions reported above, it ain’t over. This is so even with the passing of some days since the community has determined that the answers to the first two of Tao’s three questions which we headlined on Wednesday is “No”, and most probably likewise the third. It is hard to believe that this all started just one week ago this Sunday. It seems longer than that.
There has been lively give and take with numerous researchers, and several distinguished academics including Harvey Friedman, Robert Solovay, and Barkley Rosser Jr. have contributed numerous observations. Take away all of these, and there are still math+CS background comments, even ranging to ones by Tao on the Borel-Cantelli Lemma, that are recommended reading. It is not possible to acknowledge everyone’s contributions in this short space, but we are grateful for all.
What solid research can emerge from the discussion? New barriers? More tools for working with distributions? How is this affecting the perception of theoretical computer science as a profession, and the dynamics of the community?