{"id":"fb1504e3-5902-4a93-a8d0-8e584483f0f1","arxiv_id":"1908.04198","paper_version":2,"verdict":"REJECT","confidence":"MODERATE","novelty_score":6.0,"correctness_risk":"high","formal_verification":"none","parameter_count":0,"one_line_summary":"The paper asserts NP-completeness for several bounded-appearance SAT variants, but a central gadget for the (k,1) monotone results fails to enforce the required constraints.","lead":"This paper claims new NP-completeness results for Not-All-Equal 3-Sat and Monotone 3-Sat when each variable appears a fixed number of times, sometimes with no negations or with linear structure. A load-bearing reduction for the Monotone 3-Sat-(k,1) results contains a gadget that does not do what the proof says, so those claims are not supported as written.","discovery_kind":"extension","skeptic_critique":{"model":"deepseek-v4-flash","headline":"Theorem 6's reduction fails: F(y) from the Remark is satisfiable with y=false, and even with y true the clause {xi,1,xi,2,yi} is vacuous, so the claimed enforcement of xi,1≠xi,2 is absent and the (k,1) hardness result is unproven.","rationale":"The reader's verdict is REJECT with moderate confidence, and my reading supports that assessment. The paper's central advertised result, Monotone 3-Sat-(k,1) NP-completeness for every k≥5, rests entirely on Theorem 6. The reduction's key sentence, 'Since these clauses can be satisfied if and only if we assign different truth values to xi,1 and xi,2,' is incorrect. The Remark's F(y) does not force y true: a direct satisfying assignment with y=false exists. Even if that remark were corrected so that y were forced true, the added clause {xi,1,xi,2,yi} would be automatically satisfied and D(...) provides only a lower-bound (at-least-one-true) constraint, not the required exactly-one-true constraint. Thus the reduction does not enforce the complementarity that the encoding of 3-Sat-(2,2) needs. The appearance counts in the same construction are also internally inconsistent, so the constructed instance is not even a valid Monotone 3-Sat-(5,1) instance as written. Consequently, Corollary 3 and the six-appearance dichotomy in Theorem 8, both of which depend on Theorem 6, are not established. This is an internal inconsistency in the proof as printed, not a disagreement with the surrounding literature. The NAE-3-Sat-E4 section and the balanced (k,k) results may well be salvageable, but the paper's headline claim and its dependent dichotomy are unsupported. I would not accept the paper in this form; rejection, with an opportunity for the authors to supply a corrected gadget and verified reduction, is the appropriate verdict.","tokens_in":29567,"tokens_out":18747,"duration_ms":183905,"concrete_test":"Run a SAT solver on the exact formula F(y)∧¬y from the Remark. The assignment y=false, u1=u2=u3=true, and, for each of the three D(X_i) blocks, a,c,d,f,g,h=true and b,e,i=false on fresh auxiliary variables satisfies every clause, so the solver should return SAT. This directly refutes the Remark's forcing claim and removes the only mechanism by which Theorem 6 claims to enforce xi,1≠xi,2. A useful follow-up within the same check is to run the full Theorem 6 reduction on a small unsatisfiable 3-Sat-(2,2) instance; if the resulting formula is satisfiable, the reduction is invalid.","verdict_should_be":"REJECT","load_bearing_attack":"The Remark after Lemma 9 asserts that F(y) forces y to true, and Theorem 6 relies on this to make the clause {xi,1,xi,2,yi} enforce complementarity. That assertion is false: set y=false and u1=u2=u3=true. Each D(X_i) then has at least one true argument, so by Lemma 9 it admits a satisfying extension (for fresh auxiliaries, take a,c,d,f,g,h=true and b,e,i=false), and the final positive clause {u1,u2,u3} is also satisfied. Hence F(y)∧¬y is satisfiable, so y is not forced at all. Moreover, the alleged consequence does not follow even if y were forced true: {xi,1,xi,2,yi} is then satisfied regardless of xi,1 and xi,2, while Lemma 9's D(...) only demands that at least one of xi,1,xi,2 be true. The construction therefore never enforces xi,1≠xi,2, and the reduction from 3-Sat-(2,2) in Theorem 6 does not preserve satisfiability. Corollary 3 (all k≥5) and the six-appearance dichotomy in Theorem 8 depend on Theorem 6 and are unsupported as written. The appearance counts in the same paragraph are also inconsistent (xi,1 and xi,2 each receive six unnegated occurrences, and yi receives four before padding), corroborating that the construction is not a valid (5,1) instance.","agreement_with_reader":"agree"},"referee_report":{"model":"deepseek-v4-flash","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).","tokens_in":29823,"tokens_out":13054,"duration_ms":131617,"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":[{"comment":"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":"Section 4.2.1, Remark after Lemma 9"},{"comment":"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":"Section 4.2.1, Theorem 6"},{"comment":"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":"Section 4.2.1, appearance counts in Theorem 6"},{"comment":"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.","section":"Section 4.3, Proposition 4 and Lemma 12"}],"minor_comments":[{"comment":"The text reads 'We can construct on unsatisfiable instance'; this should be 'an unsatisfiable instance'.","section":"Section 4.2.1, before Proposition 3"},{"comment":"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":"Section 4.2.1, Remark after Lemma 9"},{"comment":"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":"Section 4.3, Lemma 12"},{"comment":"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.","section":"Section 4.2.1, Theorem 6"}],"recommendation":"reject","confidential_remarks":"The NAE-3-Sat part and the balanced (k,k) part appear technically sound and may be publishable in revised form, but the headline (k,1) hardness result and the exact-six-appearance dichotomy depend on constructions that fail as written. In particular, the F(y) forcing gadget in Theorem 6 is satisfiable with y false and does not enforce complementarity, so Corollary 3 and Theorem 8 are unproven. The additional degree-count problem in Proposition 4 further undermines the six-appearance dichotomy. These are not merely presentation issues, and I recommend rejection of the current manuscript."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","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.\n\nWhat 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.\n\nWhere 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).\n\nBottom 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.","headline":"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.","tokens_in":30487,"tokens_out":18105,"would_cite":false,"duration_ms":148976,"reading_group":"maybe","serious_thinker":"no","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":["68Q17","68Q25","03B05"],"pacs":[],"model":"deepseek-v4-flash","headline":"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.","keywords":["Not-All-Equal 3-Sat","Monotone 3-Sat","NP-completeness","variable appearances","linear formulas","SAT gadgets","satisfiability","complexity dichotomy"],"falsifier":"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.","tokens_in":29278,"feed_emoji":"🧩","tokens_out":14926,"duration_ms":130047,"temperature":0.7,"pith_summary":"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.","feed_headline":"Monotone 3-Sat stays hard at one negated appearance per variable","feed_subtitle":"Gadget reductions also settle the six-appearance case and tighten NAE-3-Sat to linear monotone formulas with four appearances.","key_machinery":"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.","core_discovery":"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.","pith_inferences":["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."],"forward_implications":["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."],"supporting_citations":[{"why":"Supplies the source problem 3-Sat-(2,2) from which the main Monotone 3-Sat reductions start.","marker":"[BKS03]"},{"why":"Establishes NP-completeness of NAE-3-Sat*, the starting point of the second NAE-3-Sat-E4 proof.","marker":"[Sch78]"},{"why":"Shows Monotone NAE-3-Sat is NP-complete, the starting point of the first NAE proof and the result the linearity strengthening improves.","marker":"[PSSW14]"},{"why":"Gives the earlier four-appearance Monotone 3-Sat hardness that Theorem 9 strengthens to a 3-and-1 split.","marker":"[DDD18]"},{"why":"Supplies the known boundary that at most three appearances per variable is trivial, against which the new hardness thresholds are measured.","marker":"[Tov84]"},{"why":"Proves NAE-3-Sat* hard with at most four appearances; the paper improves this to exactly four distinct appearances and linearity.","marker":"[KP18]"},{"why":"Provides polynomial-time solvability of monotone NAE-3-Sat with at most three appearances per variable, marking the boundary the four-appearance result crosses.","marker":"[PRS04]"}],"fun_headline_variants":["Linear monotone NAE-3-Sat hard with 4 appearances per variable","Monotone 3-Sat hard at one negated, any k≥5 unnegated appearances","Six-appearance Monotone 3-Sat fully classified","Monotone 3-Sat NP-complete with any k≥3 balanced signs","Tightened NP-completeness for monotone satisfiability"],"cache_read_input_tokens":3200,"weakest_assumption_plain":"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.","fun_headline_variants_meta":{"raw":{"variants":["Linear monotone NAE-3-Sat hard with 4 appearances per variable","Monotone 3-Sat hard at one negated, any k≥5 unnegated appearances","Six-appearance Monotone 3-Sat fully classified","Monotone 3-Sat NP-complete with any k≥3 balanced signs","Tightened NP-completeness for monotone satisfiability"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.000625,"raw_usage":{"total_tokens":2978,"prompt_tokens":1115,"completion_tokens":1863,"prompt_tokens_details":{"cached_tokens":384},"prompt_cache_hit_tokens":384,"prompt_cache_miss_tokens":731,"completion_tokens_details":{"reasoning_tokens":1759}},"tokens_in":731,"tokens_out":1863,"duration_ms":13935,"temperature":1.0,"reasoning_tokens":1759,"cache_read_input_tokens":384,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-14T13:50:57.703379+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"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.","supporting_citations":[],"review_version":1}