What do you think of Bokov's “CNF-SAT is in P” proof? [closed]

There are now several versions of G. V. Bokov's paper "Complexity of the CNF-satisfiability problem", cf. https://arxiv.org/abs/1804.02478

In the most recent version of his paper, the proof is only two pages long. I did not find any mention of Bokov's proof (whether it is obviously wrong or not etc.) anywhere. Bokov seems to be a serious researcher in this field.

Has anybody reviewed or analyzed his alleged proof? It has been submitted to FOCS 2018 (but not accepted) and computational complexity journal.

closed as off-topic by D.W., Aryeh, Gamow, Emil Jeřábek, Hsien-Chih Chang 張顯之Aug 13 '18 at 2:11

This question appears to be off-topic. The users who voted to close gave this specific reason:

• "Your question does not appear to be a research-level question in theoretical computer science. For more information about the scope, please see help center. Your question might be suitable for Computer Science which has a broader scope." – Aryeh, Gamow, Emil Jeřábek, Hsien-Chih Chang 張顯之
If this question can be reworded to fit the rules in the help center, please edit the question.

CNFSAT is NP-complete [Cook-Levin] (see https://en.m.wikipedia.org/wiki/Boolean_satisfiability_problem); in fact even 3CNFSAT captures NP, and is one of the standard problems used for reduction in proving NP-hardness.

Any proof it's in P in barely a page should be viewed with some skepticism. (The author doesn't even seem to conclude that NP = P, so they may have missed that implication?)

I'm not sure I fully the approach here, but the recursive definition doesn't seem to make sense, and the example already contains an error.

1. The set S_F(z) is recursively defined as "{z}, and all literals except ~z which occur in a clause that doesn't contain any of the literals already in the set". However, the recursion collapses after the first step: The literals fulfilling that criterion for any set containing z must already fulfill it for {z}, so only the first step does anything.

2. The example incorrectly calculates S_F(z). It would be {x1, x2, x3, ~x3, x4, ~x4}, not {x1, x2, ~x3}.

3. The actual example value makes it clear that the condition labeled (1) in the proof is incorrect. There is nothing stopping S_F(x) from containing both a literal and its negation.

The rest of the proof kind of falls apart after that.

• I don't think that reasoning is correct. Each step in constructing S_F(z) adds those literals that occur in a clause not containing any of the already present literals but whose negation only occurs in such clauses. This e.g. adds x2 in step 1 (starting step is 0) in Bokov's example. Continuing in this way you get exactly his shown value for S_F(x1). I think the error is in the proof of Lemma 3.2. – Christoph Kögl Aug 8 '18 at 0:38