On simplified NP-complete variants of Not-All-Equal 3-Sat and 3-Sat

Andreas Darmann; Janosch D\"ocker

REVIEW 4 major objections 4 minor 24 references

On simplified NP-complete variants of Not-All-Equal 3-Sat and 3-Sat

T0 review · 4 major / 4 minor · reviewed 2026-08-14 · deepseek-v4-flash

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗ Review JSON

Pith's one-line read Monotone 3-Sat is NP-complete when each variable appears exactly k times unnegated and exactly once negated for every fixed k≥5; NAE-3-Sat is likewise NP-complete for linear, monotone, four-appearance formulas.

desk verdict The NAE-3-Sat and balanced (k,k) sections look solid, but the paper's headline Monotone 3-Sat-(k,1) hardness and the six-appearance dichotomy rest on a gadget that provably does not work. read the letter →

arxiv 1908.04198 v2 pith:MN5DMJFW submitted 2019-08-12 cs.CC

Andreas Darmann , Janosch Döcker This is my paper · ORCID

classification cs.CC MSC 68Q1768Q2503B05

keywords Not-All-Equal3-SatMonotoneNP-completenessvariableappearanceslinearformulasSATgadgetssatisfiabilitycomplexitydichotomy

verification ladder T0 review T1 audit T2 compute T3 formal

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The reading

The paper sets out to show that two well-known satisfiability problems stay intractable under extremely tight structural restrictions. For Not-All-Equal 3-Sat, it claims NP-completeness already when every variable appears exactly four times, no negations are present, and the formula is linear. For Monotone 3-Sat, where each clause is entirely positive or entirely negative, it claims NP-completeness when each variable appears $k$ times unnegated and $k$ times negated for every $k\ge 3$, and when each variable appears exactly $k$ times unnegated and exactly once negated for every $k\ge 5$. If these claims are right, the six-appearance-per-variable case is completely classified and the four-appearance case of ordinary 3-Sat is hard at a three-to-one split of negated and unnegated appearances. The intended payoff is a sharp map of the appearance budgets that separate trivial satisfiability from NP-completeness.

What carries the argument

The load-bearing objects are small sets of clauses over auxiliary variables, each designed to simulate one constraint. The equality and non-equality gadgets $EQ$ and $NE$ force two variables to receive the same or opposite truth values, and a four-argument version $EQ(x,y,z,u)$ makes the linearity-preserving reduction work. For the Monotone 3-Sat results, the central gadget is $D(X)$, a 20-clause construction over six argument positions and nine auxiliaries in which a satisfying assignment exists exactly when at least one argument is true; the proof then stacks three copies of $D(X)$ into $F(y)$, a gadget it relies on to force a variable $y$ to be true. The $G$, $H$, $B$, and $\bar{B}$ gadgets play analogous forcing roles for small-appearance monotone formulas. The work these gadgets do is to transfer a local constraint, such as at least one true, all equal, or opposite values, into the global appearance-count budget while keeping every clause monotone and of size three.

What would settle it

Set $y$ false and $u_1,u_2,u_3$ true in $F(y)$ as defined in the remark after Lemma 9; Lemma 9's own at-least-one-true-argument condition then extends this partial assignment to a satisfying assignment of each $D(X_i)$, so the full gadget is satisfied with $y$ false. That assignment is a direct counterexample to the forcing property on which Theorem 6 depends.

Watch

Extended reading notes

Core claim

The paper's central claim is a pair of completeness thresholds. First, Not-All-Equal 3-Sat remains NP-complete even when the input is simultaneously monotone, linear, and every variable appears in exactly four clauses. Second, Monotone 3-Sat remains NP-complete with every variable appearing equally often negated and unnegated for any common count $k\ge 3$, and with exactly one negated appearance plus $k\ge 5$ unnegated appearances. From these results the paper derives a complete classification for exactly six appearances per variable and a strengthening of the four-appearance case of ordinary 3-Sat to a $(3,1)$ or $(1,3)$ split of negated and unnegated appearances. The proof strategy is a chain of gadget reductions that replace each variable occurrence by a fresh variable and then wire the copies together with equality, non-equality, or forcing gadgets.

Load-bearing premise

The whole $(k,1)$ chain for $k\ge 5$ rests on the assertion that the gadget $F(y)$, built from three copies of $D(X)$ and the clause $\{u_1,u_2,u_3\}$, cannot be satisfied with $y$ false; if that assertion fails, the reduction in Theorem 6 that enforces complementary truth values for $x_{i,1}$ and $x_{i,2}$ collapses.

Editorial extensions

If this is right

If the reductions hold, Monotone NAE-3-Sat-E4 is NP-complete even for linear formulas, meaning no negations, exactly four appearances per variable, and any two clauses sharing at most one variable.
If the reductions hold, Monotone 3-Sat-$(k,k)$ is NP-complete for every $k\ge 3$, and the six-appearance case has a complete dichotomy: $(p,6-p)$ is hard for $p=1,\ldots,5$ and trivial only at the endpoints.
If the reductions hold, ordinary 3-Sat with exactly four appearances per variable is NP-complete under a 3-and-1 split of negated and unnegated appearances, not just the balanced 2-and-2 split previously known.
If the reductions hold, the remaining open small-appearance cases are Monotone 3-Sat-$(3,1)$ and $(4,1)$, along with Monotone 3-Sat-$(2,2)$, which is either all-satisfiable or NP-complete.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

This reader's inference: because the forcing property of $F(y)$ is in doubt, the NAE-3-Sat results, whose $EQ$ and $NE$ gadgets are verified with separate case analyses, may remain valid even if the $(k,1)$ chain for $k\ge 5$ does not.
This reader's inference: a repair of the $(k,1)$ chain would need a forcing gadget that stays unsatisfiable with $y$ false while preserving the exact appearance counts; the paper as written gives no such gadget.
This reader's inference: the $(2,2)$ 'trivial or NP-complete' dichotomy is a concrete experimental junction, since exhibiting a single unsatisfiable instance of Monotone 3-Sat-$(2,2)$ would immediately establish NP-completeness.

Share X Bluesky LinkedIn Reddit HN

Signed reviews

No signed human review yet.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, and a circularity audit.

Desk Editor's Note

read the letter

Two things to know. First, the monotone NAE-3-Sat-E4 result, including the linear version, looks real and is a genuine strengthening of Porschen et al. and Karpinski-Piecuch. Second, the paper's central 3-Sat results — Monotone 3-Sat-(k,1) for k >= 5 and the p+q=6 dichotomy — are not established: Theorem 6's reduction is broken, and the error is visible inside the text itself.

What is good: Section 3's gadget lemmas are carefully argued, and the linear NAE-4 construction (Lemma 3, Theorem 2) checks out; the auxiliary variable counts work. The balanced (k,k) chain (Lemmas 4–6, Theorem 3, Lemma 7) also holds up as far as I can see, giving NP-completeness for all k >= 3.

Where it falls apart: The Remark after Lemma 9 asserts that F(y) forces y true. It doesn't. Setting y=false and u1=u2=u3=true satisfies each D(Xi) because every Xi has at least one true argument (Lemma 9), and the final clause {u1,u2,u3} is satisfied. So y is not forced. Worse, even if y were true, {xi,1,xi,2,yi} is automatically satisfied and D(...) only demands that at least one of xi,1,xi,2 be true; nothing enforces they be different. The reduction from 3-Sat-(2,2) therefore does not preserve satisfiability. Corollary 3, Proposition 3, and the (5,1) leg of Theorem 8 all inherit the failure. I also found a second count problem: in Proposition 4, after replacing the 2-clause with a 3-clause, each xi,1/xi,2 has 4 unnegated and 1 negated appearance, not (3,2), so the (4,2) leg of the dichotomy is also not an instance of the stated class. The same paragraph in Theorem 6 has inconsistent appearance counts (xi,1 and xi,2 each get six unnegated occurrences before padding).

Bottom line: the NAE section and the (k,k) material are solid, and the paper is aimed at the right audience, but the advertised Monotone 3-Sat results are unsupported as written. This deserves a serious referee because the sound parts are nontrivial and the failures are concrete and instructive. I would not accept the current version, and the abstract needs to be rewritten if Theorem 6 and Proposition 4 cannot be repaired.

Referee Report

4 major / 4 minor

Summary. The paper studies restricted variants of NAE-3-Sat and Monotone 3-Sat with bounded variable appearances. It claims NP-completeness of Monotone NAE-3-Sat-E4, including for linear formulas; NP-completeness of Monotone 3-Sat-(k,k) for all k >= 3; NP-completeness of Monotone 3-Sat-(k,1) for all k >= 5; a complete dichotomy for Monotone 3-Sat with exactly six appearances per variable; and a four-appearance result in which each variable appears either three times unnegated and once negated or three times negated and once unnegated. The NAE part is developed through dedicated equality and non-equality gadgets, while the Monotone 3-Sat results use enforcer gadgets and reductions from 3-Sat-(2,2).

Significance. If correct, the results would strengthen known bounds by Berman et al., Darmann et al., and others, and would resolve the exact-six-appearance dichotomy for Monotone 3-Sat. The NAE-3-Sat section and the balanced (k,k) section are the strongest parts: their gadgets are explicit, the case analyses are detailed, and the reductions start from independent NP-complete source problems. The central (k,1) result, however, rests on a gadget claim that is false, and the appearance counts in the same construction are inconsistent; the six-appearance dichotomy also relies on a further construction whose auxiliary variables violate the required appearance bounds. Because these are load-bearing errors in the main new claims, the paper as it stands does not establish its headline results.

major comments (4)

[Section 4.2.1, Remark after Lemma 9] The Remark asserts that F(y) forces y to true, but this is false. Take y = false and u1 = u2 = u3 = true, and for each D(Xi) with Xi = (y, ui, ui, ui, ui, ui) use the extension supplied by Lemma 9, for example a = c = d = f = g = h = true and b = e = i = false. Each D(Xi) has at least one true argument, namely ui, so Lemma 9 gives a satisfying extension, and the final clause {u1,u2,u3} is also satisfied. Hence F(y) is satisfiable with y false, and the claimed forcing property is not established.
[Section 4.2.1, Theorem 6] The reduction from 3-Sat-(2,2) does not enforce that xi,1 and xi,2 receive opposite truth values. Even if yi were forced true, the clause {xi,1,xi,2,yi} is always satisfied regardless of xi,1 and xi,2, while the gadget D(xi,1,xi,1,xi,1,xi,2,xi,2,xi,2) only requires at least one of xi,1,xi,2 to be true, by Lemma 9. After all negations are removed, every original 3-Sat-(2,2) clause becomes a positive clause over the variables xi,j; setting every xi,1, xi,2, and yi to true and then extending each D and F gadget using Lemma 9 satisfies the entire constructed formula. The reduction therefore maps every instance to a satisfiable instance and cannot establish NP-hardness.
[Section 4.2.1, appearance counts in Theorem 6] The claimed appearance counts do not match the construction. Each xi,1 and xi,2 appears three times as an argument in D, twice in the original clauses after removing negations, and once in {xi,1,xi,2,yi}, for a total of six unnegated appearances and zero negated appearances before any padding; yi appears three times in F(yi) and once in {xi,1,xi,2,yi}, for four unnegated appearances and zero negated appearances. Thus the formula constructed in Theorem 6 is not an instance of Monotone 3-Sat-(5,1), and the statement that all variables except yi appear exactly five times unnegated and once negated is contradicted by the displayed construction.
[Section 4.3, Proposition 4 and Lemma 12] The construction for Monotone 3-Sat-(3,2) is not a valid instance of the target problem. The gadget G(x,y,z) in Lemma 12 consists entirely of positive clauses, so its auxiliary variables a,...,f have zero negated occurrences in any formula that uses G as described. Since Monotone 3-Sat-(3,2) requires every variable to appear exactly twice negated, the formula built in Proposition 4 cannot satisfy the degree condition. In addition, Lemma 12 lists clauses 5-8 as exact duplicates of clauses 1-4; if the formula is treated as a set, those duplicates collapse and the counts change, while if it is treated as a multiset, the paper does not state that duplicate clauses are permitted in Monotone 3-Sat-(3,2). This affects Corollary 8 and the (4,2) branch of Theorem 8.

minor comments (4)

[Section 4.2.1, before Proposition 3] The text reads 'We can construct on unsatisﬁable instance'; this should be 'an unsatisﬁable instance'.
[Section 4.2.1, Remark after Lemma 9] The forcing property of F(y) is asserted without proof. Since it is load-bearing for Theorem 6, it should either be proved as a separate lemma with a full case analysis or replaced by a gadget whose forcing behavior is verified.
[Section 4.3, Lemma 12] The duplicated clauses in Lemma 12 should be clarified: if they are intentional for appearance counting, the paper must state whether the problem instances allow duplicate clauses; if they are not intentional, they should be removed and all counts in Proposition 4 recomputed.
[Section 4.2.1, Theorem 6] The sentence 'Recall that 4n = 3|C| holds in the given instance of 3-Sat-(2,2), and hence the number of variables n is a multiple of 3' is correct, but it would be clearer to write 3m = 4n and then derive 3 | n before using n = 3q in the padding step.

Circularity Check

0 steps flagged · score 0.0 of 10

No circularity: all central reductions start from external NP-complete problems; the only self-citation is not load-bearing.

full rationale

The derivation chain is self-contained in the circularity sense. Theorem 1 reduces from Monotone NAE-3-Sat and NAE-3-Sat*, citing external hardness results [PSSW14] and [Sch78], and the equality/non-equality gadgets are new constructions verified by explicit case analysis rather than fitted to the target result. Theorem 2 reduces from Theorem 1 using the EQ gadget of Lemma 3. The Monotone 3-Sat results reduce from 3-Sat-(2,2) of Berman et al. [BKS03] in Theorems 3, 6, 9 and Proposition 4, with the padding steps in Lemmas 7 and 10 being explicit and independent. The paper's only self-citation, [DDD18], appears in the abstract and introduction as a baseline that the authors improve upon, not as an input to any reduction; it is therefore not load-bearing and does not make the argument circular. The skeptical observation that the Remark after Lemma 9 may be false, so that F(y) does not force y true and Theorem 6 may fail, is a correctness issue rather than a circularity issue: the claimed gadget behavior is not obtained by defining the gadget in terms of the target result, nor by fitting parameters to the data, nor by importing a uniqueness theorem from the authors' prior work. No equation in the paper reduces to its own input by construction, and no fitted parameter is renamed as a prediction.

Assumptions & free parameters 0 free parameters · 4 assumptions · 0 invented entities

The paper introduces no fitted parameters and no physical or mathematical entities beyond standard auxiliary gadget variables. It relies on prior NP-completeness results as source problems. The self-cited [DDD18] is used as a baseline, not as a load-bearing input.

assumptions (4)

domain assumption 3-Sat-(2,2) is NP-complete (Berman et al. [BKS03, Theorem 1])
Used as the source problem for several reductions, including Theorems 3, 6, 9 and Proposition 4.
domain assumption NAE-3-Sat* is NP-complete (Schaefer [Sch78])
Used in Proof 2 of Theorem 1.
domain assumption Monotone NAE-3-Sat is NP-complete (Porschen et al. [PSSW14, Theorem 3])
Used in Proof 1 of Theorem 1.
standard math In any 3-Sat-(2,2) instance, the number of variables is divisible by 3
Because 4n = 3m, this count is used for padding arguments in Theorems 3, 6, and Proposition 4.

how reviews work

0 comments

Cite this review

Pith. "Pith review of On simplified NP-complete variants of Not-All-Equal 3-Sat and 3-Sat." pith.science (2026). https://pith.science/paper/MN5DMJFW

@misc{pith2026190804198,
  author       = {Pith},
  title        = {Pith review of: On simplified NP-complete variants of Not-All-Equal 3-Sat and 3-Sat},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/MN5DMJFW}},
  note         = {Machine review of arXiv:1908.04198}
}

abstract

We consider simplified, monotone versions of Not-All-Equal 3-Sat and 3-Sat, variants of the famous Satisfiability Problem where each clause is made up of exactly three distinct literals. We show that Not-All-Equal 3-Sat remains NP-complete even if (1) each variable appears exactly four times, (2) there are no negations in the formula, and (3) the formula is linear, i.e., each pair of distinct clauses shares at most one variable. Concerning 3-Sat we prove several hardness results for monotone formulas with respect to a variety of restrictions imposed on the variable appearances. Monotone 3-Sat is the restriction of 3-Sat to monotone formulas, i.e. to formulas in which each clause contains only unnegated variables or only negated variables, respectively. In particular, we show that, for any $k\geq 5$, Monotone 3-Sat is NP-complete even if each variable appears exactly $k$ times unnegated and exactly once negated. In addition, we show that Monotone 3-Sat is NP-complete even if each variable appears exactly three times unnegated and three times negated, respectively. In fact, we provide a complete analysis of Monotone 3-Sat with exactly six appearances per variable. Further, we prove that the problem remains NP-complete when restricted to instances in which each variable appears either exactly once unnegated and three times negated or the other way around. Thereby, we improve on a result by Darmann et al. [DDD18] showing NP-completeness for four appearances per variable. Our stronger result also implies that 3-Sat remains NP-complete even if each variable appears exactly three times unnegated and once negated, therewith complementing a result by Berman et al. [BKS03].

Figures

Figures reproduced from arXiv: 1908.04198 by the authors.

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

24 extracted references · 23 canonical work pages

[1]

Berman, M

P. Berman, M. Karpinski, and A. D. Scott. Approximation hardness of short symmetric instances of MAX-3SAT . Electronic Colloquium on Computational Complexity , 2003. Report No. 49

work page 2003
[2]

S.A. Cook. The complexity of theorem-proving procedures. In Proceedings of the 3rd annual ACM symposium on Theory of Computing , pages 151--158. ACM, 1971

work page 1971
[3]

De Berg and A

M. De Berg and A. Khosravi. Optimal binary space partitions for segments in the plane. International Journal of Computational Geometry & Applications , 22(03):187--205, 2012

work page 2012
[4]

Darmann, J

A. Darmann, J. D \"o cker, and B. Dorn. The monotone satisfiability problem with bounded variable appearances. International Journal of Foundations of Computer Science , 29(06):979--993, 2018

work page 2018
[5]

Devlin and B

D. Devlin and B. O'Sullivan. Satisfiability as a classification problem. In Proceedings of the 19th Irish Conference on Artificial Intelligence and Cognitive Science , 2008

work page 2008
[6]

Dehghan, M

A. Dehghan, M. Sadeghi, and A. Ahadi. On the complexity of deciding whether the regular number is at most two. Graphs and Combinatorics , 31(5):1359--1365, Sep 2015

work page 2015
[7]

Garey and D.S

M.R. Garey and D.S. Johnson. Computers and intractability: a guide to the theory of NP -completeness. 1979

work page 1979
[8]

M.E. Gold. Complexity of automaton identification from given data. Information and Control , 37(3):302--320, 1978

work page 1978

Show all 24 references

[9]

Horbach, T

A. Horbach, T. Bartsch, and D. Briskorn. Using a SAT -solver to schedule sports leagues. Journal of Scheduling , 15(1):117--125, 2012

2012
[10]

Karpinski and K

M. Karpinski and K. Piecuch. On vertex coloring without monochromatic triangles. In F.V. Fomin and V.V. Podolskii, editors, Computer Science - Theory and Applications - Proceedings of the 13th International Computer Science Symposium in Russia ( CSR '18) , volume 10846 of Lect...

2018
[11]

Kratochv \' l

J. Kratochv \' l. A special planar satisfiability problem and a consequence of its NP -completeness. Discrete Applied Mathematics , 52(3):233--252, 1994

1994
[12]

Kautz and B

H. Kautz and B. Selman. Pushing the envelope: Planning, propositional logic, and stochastic search. In Proceedings of the 13th National Conference on Artificial Intelligence (AAAI'96) , pages 1194--1201. AAAI Press, 1996

1996
[13]

W.N. Li. Two-segmented channel routing is strong NP -complete. Discrete Applied Mathematics , 78(1-3):291--298, 1997

1997
[14]

Lichtenstein

D. Lichtenstein. Planar formulae and their uses. SIAM Journal on Computing , 11(2):329--343, 1982

1982
[15]

B. Moret. Planar NAE3SAT is in P . ACM SIGACT News , 19(2):51--54, 1988

1988
[16]

Nam, K.A

G. Nam, K.A. Sakallah, and R.A. Rutenbar. Satisfiability-based layout revisited: Detailed routing of complex FPGAs via search-based boolean SAT . In Proceedings of the ACM/SIGDA 7th International Symposium on Field Programmable Gate Arrays (FPGA '99) , pages 167--175, New York...

1999
[17]

A. Pilz. Planar 3-SAT with a clause/variable cycle. Discrete Mathematics & Theoretical Computer Science , 21(3), 2019

2019
[18]

Porschen

S. Porschen. On some weighted satisfiability and graph problems. In International Conference on Current Trends in Theory and Practice of Computer Science , pages 278--287. Springer, 2005

2005
[19]

Porschen, B

S. Porschen, B. Randerath, and E. Speckenmeyer. Linear time algorithms for some not-all-equal satisfiability problems. In Theory and Applications of Satisfiability Testing -- SAT 2004 , pages 256--257. Springer, 2004

2004
[20]

Porschen and T

S. Porschen and T. Schmidt. On some SAT -variants over linear formulas. In International Conference on Current Trends in Theory and Practice of Computer Science , pages 449--460. Springer, 2009

2009
[21]

Paulusma and S

D. Paulusma and S. Szeider. On the parameterized complexity of (k,s)- SAT . Information Processing Letters , 143:34 -- 36, 2019

2019
[22]

Porschen, T

S. Porschen, T. Schmidt, E. Speckenmeyer, and A. Wotzlaw. XSAT and NAE-SAT of linear CNF classes. Discrete Applied Mathematics , 167:1--14, 2014

2014
[23]

Schaefer

T.J. Schaefer. The complexity of satisfiability problems. In Proceedings of the 10th annual ACM symposium on Theory of Computing , pages 216--226. ACM, 1978

1978
[24]

C.A. Tovey. A simplified NP -complete satisfiability problem. Discrete Applied Mathematics , 8(1):85--89, 1984

1984

Pith tools

Reviewed August 14, 2026 · model on record in the stance chip above.

[1] [1]

Berman, M

P. Berman, M. Karpinski, and A. D. Scott. Approximation hardness of short symmetric instances of MAX-3SAT . Electronic Colloquium on Computational Complexity , 2003. Report No. 49

work page 2003

[2] [2]

S.A. Cook. The complexity of theorem-proving procedures. In Proceedings of the 3rd annual ACM symposium on Theory of Computing , pages 151--158. ACM, 1971

work page 1971

[3] [3]

De Berg and A

M. De Berg and A. Khosravi. Optimal binary space partitions for segments in the plane. International Journal of Computational Geometry & Applications , 22(03):187--205, 2012

work page 2012

[4] [4]

Darmann, J

A. Darmann, J. D \"o cker, and B. Dorn. The monotone satisfiability problem with bounded variable appearances. International Journal of Foundations of Computer Science , 29(06):979--993, 2018

work page 2018

[5] [5]

Devlin and B

D. Devlin and B. O'Sullivan. Satisfiability as a classification problem. In Proceedings of the 19th Irish Conference on Artificial Intelligence and Cognitive Science , 2008

work page 2008

[6] [6]

Dehghan, M

A. Dehghan, M. Sadeghi, and A. Ahadi. On the complexity of deciding whether the regular number is at most two. Graphs and Combinatorics , 31(5):1359--1365, Sep 2015

work page 2015

[7] [7]

Garey and D.S

M.R. Garey and D.S. Johnson. Computers and intractability: a guide to the theory of NP -completeness. 1979

work page 1979

[8] [8]

M.E. Gold. Complexity of automaton identification from given data. Information and Control , 37(3):302--320, 1978

work page 1978