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

<p>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?)</p>

<p>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.</p>

<ol>
<li><p>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.</p></li>
<li><p>The example incorrectly calculates S_F(z). It would be {x1, x2, x3, ~x3, x4, ~x4}, not {x1, x2, ~x3}.</p></li>
<li><p>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.</p></li>
</ol>

<p>The rest of the proof kind of falls apart after that.</p>

CC BY-SA 4.0
2018-08-08T00:38:36.920Z
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
CC BY-SA 4.0
2018-08-06T23:50:03.890Z
2018-08-06T23:50:03.890Z
Christoph Burschka
<p>There are now several versions of G. V. Bokov's paper "Complexity of the CNF-satisfiability problem", cf. <a href="https://arxiv.org/abs/1804.02478" rel="nofollow noreferrer">https://arxiv.org/abs/1804.02478</a></p>

<p>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.</p>

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

CC BY-SA 4.0
2018-08-06T23:03:21.173Z
https://cstheory.meta.stackexchange.com/q/274/5038
D.W.
<time-complexity><sat>
What do you think of Bokov's "CNF-SAT is in P" proof?
Christoph Kögl
# What do you think of Bokov's "CNF-SAT is in P" proof?

(Asked by: username_0 on 2018-08-06)

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.

**Tags:** time-complexity, sat
> **Comments:**
> **username_1**: https://cstheory.meta.stackexchange.com/q/274/5038  

---

## 1 answers

### Answer by username_2 on 2018-08-06. Score: 7

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.

> **Comments:**
> **username_0**: 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.  

---

