Fatal Flaws in Deolalikar’s Proof?

Possible fatal flaws in the finite model part of Deolalikar’s proof

Neil Immerman is one of the world’s experts on Finite Model Theory. He used insights from this area to co-discover the great result that is closed under complement.

Today I had planned not to discuss the proof, but I just received a note from Neil on Vinay Deolalikar “proof” that PNP. Neil points out two flaws in the finite model part that sound extremely damaging to me. He has already shared them with Vinay, and suggested that I highlight them here. The comments from Neil are in the next section—I have only edited it slightly to make it “compile.”

Two Flaws?

Dear Vinay Deolalikar,

Thank you very much for sharing your paper with me. I find your approach and your ideas fascinating, but I am afraid that there is currently a serious hole in your paper as I now describe. For page numbers, I refer to the 102 page, 12 pt. version of your paper.

Your main idea for the lower bound is to show that FO(LFP) is not powerful enough to express SAT, by using Hanf-Gaifman locality to limit the connectivity of the graphs you consider at successive stages of the fixed point computation. As you point out, if a total ordering is given as part of the input structure, then the Gaifman graph has diameter one, so locality is meaningless. Thus you restrict to a successor relation and as you point out, it is still true that FO(LFP) is equal to P in the presence of a successor relation. However, you make two assertions that are not true.

You use the relation as your successor relation. On page 67 you write, “The reason for the relation that creates the chain is that on such structures, polynomial time queries are captured by FO(LFP) [EF06, S11.2].” This is a technicality. Recall that an order on the structure enables the LFP computation (or the Turing machine the runs this computation) to represent tuples in a lexicographical ordering. In our problem -SAT, it plays no further role. Specifically, the assignments to the variables that are computed by the LFP have nothing to do with their order. They depend only on the relation which encodes the clauses and the relation that holds the initial partial assignment that we are going to ask the LFP to extend. In other words, each stage of the LFP is order invariant. It is known that the class of order invariant queries is also Gaifman local [GS00].

Unfortunately, it is not true that each stage of the fixed point must be order invariant. In particular, consider the definition of ordering from successor, easily defined by a least fixed point and thus the reason that successor suffices to capture P. The ordering is defined by taking the transitive closure of the successor relation. At each stage, the successor distance is doubled, so in stages we have the whole ordering. Note that all these stages contain the order dependent information that is part of the original successor relation. It is true that the final aim of your computation is the SAT property which is order independent. But that definitely does not imply that each stage of the induction is order independent.

The other problem is that you restrict your attention to monadic fixed points. You write,

“Remark 7.4. The relation being constructed is monadic, and so it does not introduce new edges into the Gaifman graph at each stage of the LFP computation. When we compute a -ary LFP, we can encode it into a monadic LFP over a polynomially () larger product space, as is done in the canonical structure, for instance, but with the linear order replaced by a weaker successor type relation. Therefore, we can always chose to deal with monadic LFP. This is really a restatement of the transitivity principle for inductive definitions that says that if one can write an inductive definition in terms of other inductively defined relations over a structure, then one can write it directly in terms of the original relations that existed in the structure [Mos74, p. 16].”

It is not the case that you can freely assume that your fixed points are monadic. If you actually work on the canonical structure, then you require the multiple arity relations that can take us from a tuple to its individual elements and back again. These would again make the diameter of the whole graph bounded. However, in your proof you do not include these relations. Thus, your restriction to only have successor and to restrict to monadic fixed points is fundamental. In this domain—only monadic fixed points and successor—FO(LFP) does not express all of P!

Currently, as I see it, the strongest tool we have in descriptive complexity — rather than the locality theorems — is the Håstad Switching Lemma. Paul Beame and Johan Håstad used this to shown that Mike Sipser’s hierarchy theorem extends all the way to FO[]. As you know, FO(LFP) is the same thing as FO[]—properties expressible by the polynomial iteration of a fixed block of restricted quantifiers. We know that is contained in FO[] and this is tight. Furthermore, L and NL are contained in , and it remains open whether is equal to NP. A state of the art paper that I very much recommend is Ben Rossman’s result that expressing the existence of a clique requires variables in FO, and even in FO[] for appropriate . (In Rossman’s result, as in all results that use the switching lemma, the lower bound is true in the presence not just of order, but of any numeric relations including addition and multiplication.)

—Neil

Open Problems

Is Neil right? It seems that the most damaging statement of Neil is:

Thus, your restriction to only have successor and to restrict to monadic fixed points is fundamental. In this domain—only monadic fixed points and successor—FO(LFP) does not express all of P!

Most of us have focused on the issues of 2-SAT and XOR-SAT compared to -SAT, but Neil’s comment points out serious flaws in the finite model part. It was the connection of this work with the random structure of -SAT that excited many of us in the first place. Unless Neil is wrong, it seems that his points are very serious.