{"id":"863b52a1-5be6-40c1-a8b1-c652fc1af6b3","arxiv_id":"1908.05361","paper_version":2,"verdict":"CONDITIONAL","confidence":"MODERATE","novelty_score":7.0,"correctness_risk":"medium","formal_verification":"none","parameter_count":0,"one_line_summary":"Quantified 3-SAT stays Π_2^P-complete when every variable appears exactly four times, and quantified Not-All-Equal 3-SAT stays Π_2^P-complete for linear monotone formulas with each universal variable appearing once, while some variants become NP-complete or polynomial-time solvable.","lead":"This paper shows exactly which restricted quantified versions of 3-SAT and Not-All-Equal 3-SAT stay hard for the second level of the polynomial hierarchy and which become easier. The results give sharp thresholds: some variants remain Π_2^P-complete with very few variable appearances, while others drop to NP-complete or polynomial time.","discovery_kind":"extension","skeptic_critique":{"model":"deepseek-v4-flash","headline":"The printed reductions lose negation bars in key gadgets: as rendered, Theorem 3.1's chain clauses do not force equality or give the claimed (2,2,2,2) counts, and Theorem 4.1's e-assignment fails when a universal is true; the proofs repair only if the original PDF restores the missing negations.","rationale":"The reader correctly identified missing negations in the enforcer formulas of Theorems 3.2 and 3.4 and conditioned acceptance on verifying them. My stress-test confirms that concern and extends it to two additional load-bearing locations that the reader did not flag. In Theorem 3.1, Step 3's chain clauses are the mechanism that both forces equality of the split variables and calibrates the (2,2,2,2) appearance counts; as rendered, they do neither, so the main 3-SAT completeness theorem is not proved by the extracted text. Similarly, in Theorem 4.1, the first direction of the equivalence assigns the e-variables the same value as the corresponding z-variable, but with a universal u set to true the new clause (z\\vee e\\vee u) becomes all-true and is not nae-satisfied; the intended assignment must use negated e-variables. These are not merely cosmetic: each is a yes-instance direction of a headline \\Pi_2^P-completeness proof. However, the pattern strongly suggests OCR/rendering loss of overline bars rather than a deliberate mathematical claim, and a corrected manuscript would likely restore all proofs. Therefore the appropriate verdict remains conditional, matching the reader's CONDITIONAL judgment: accept only after confirming the printed formulas contain the required negations. I therefore set verdict_should_be to UNCHANGED, since my analysis does not move the verdict away from CONDITIONAL.","tokens_in":26372,"tokens_out":30333,"duration_ms":276431,"concrete_test":"Inspect the original PDF or LaTeX source for negation bars at three locations: (1) Theorem 3.1, Step 3, the chain clauses should read (\\neg w_{i,1}\\vee w_{i,2}), (\\neg w_{i,2}\\vee w_{i,3}), \\ldots, (\\neg w_{i,a}\\vee w_{i,1}); (2) Theorem 3.2, the enforcer pair should be Su(\\neg c_i,y_i,y_i)\\wedge Su(c_i,\\neg y_i,\\neg y_i), and Theorem 3.4, E_\\forall(d_{i,k}) should be (d_{i,k}\\vee u_{i,k}\\vee v_{i,k})\\wedge(d_{i,k}\\vee\\neg u_{i,k}\\vee\\neg v_{i,k}); (3) Theorem 4.1, proof 4.1.1(iii), the e-assignment should be \\beta_2(e_{i,k})=\\neg\\beta_1(z_i).","verdict_should_be":"UNCHANGED","load_bearing_attack":"The most load-bearing concern is systemic loss of negation bars in the extracted text. In Theorem 3.1, Step 3 is rendered as the all-positive chain (w_{i,1}\\vee w_{i,2}) \\wedge (w_{i,2}\\vee w_{i,3}) \\wedge \\cdots \\wedge (w_{i,a}\\vee w_{i,1}). The proof of statement 3.1.2 uses these clauses to conclude w_{i,1}=\\cdots=w_{i,a}, but all-positive clauses do not force equality: for a=3, (T,T,F) satisfies every clause. They also break the appearance count: after Step 2 each variable w_{i,k} has one positive and one negative occurrence, and the all-positive chain adds two positive occurrences, yielding three positive and one negative appearances, not the two and two required for Balanced \\forall\\exists 3-SAT-(2,2,2,2). The intended chain is almost certainly a directed cycle of implications, (\\neg w_{i,1}\\vee w_{i,2}), (\\neg w_{i,2}\\vee w_{i,3}), \\ldots, (\\neg w_{i,a}\\vee w_{i,1}), which both forces all copies equal and restores the 2/2 counts. The same missing-negation pattern appears in Theorem 4.1: in the first direction of proof 4.1.1, the assignment sets \\beta_2(e_{i,k})=\\beta_1(z_i). If \\beta_1(z_i)=T and the universal u_{i,k}=T, the clause (z_{i,k}\\vee e_{i,k}\\vee u_{i,k}) is all-true and therefore not nae-satisfied; the existential e_{i,k} must be set to the negation of z_{i,k}. The reader's examples in Theorems 3.2 and 3.4, where the second enforcer copy must contain negated literals, are the same phenomenon. Since the yes-instance directions of two headline completeness theorems depend on these negations being present, the paper's central claim is not established by the extracted text as rendered.","agreement_with_reader":"partial"},"referee_report":{"model":"deepseek-v4-flash","summary":"The paper investigates quantified variants of 3-SAT and NAE-3-SAT with bounded variable appearances. Its main claims are that Balanced ∀∃ 3-SAT-(2,2,2,2) and Balanced ∀∃ 3-SAT-(1,1,2,2) are Π_2^P-complete, that Monotone ∀∃ NAE-3-SAT-(1,3) is Π_2^P-complete for linear formulas with at most one universal variable per clause, and that certain other variants are NP-complete, co-NP-complete, or polynomial-time solvable. The proofs use standard reductions from ∀∃ 3-SAT and ∀∃ NAE-3-SAT, along with enforcer gadgets, several of which are adapted from Berman et al. and from Darmann and Döcker.","tokens_in":26774,"tokens_out":28704,"duration_ms":241907,"significance":"If the results are correct, they provide tight bounded-appearance thresholds for quantified 3-SAT and quantified NAE-3-SAT, and the enforcer constructions could be useful for further work in the polynomial hierarchy. The positive results for Monotone ∀∃ NAE-3-SAT-(s,2) are also valuable. However, the version of the manuscript supplied for review has a systemic loss of negation bars in key formulas; as printed, several enforcers are identical to their complements or are otherwise not the gadgets the proofs require. The central claims are plausible and appear repairable, but the submitted text does not currently support them.","major_comments":[{"comment":"The S-enforcer is printed as (ℓ1∨a∨b) ∧ (ℓ2∨b∨c) ∧ (ℓ3∨a∨c) ∧ (a∨b∨c) ∧ (a∨b∨c), so the fourth and fifth clauses are identical. With this formula, Observation 2.1 is false: for ℓ1=ℓ2=ℓ3=F, the assignment a=T, b=F, c=F satisfies all five clauses. The proof text says the first three clauses form a cyclic implication chain and that the fourth or fifth clause fails, which only works if the fifth clause is (¬a∨¬b∨¬c). Since x(2), E(x), Su, Q1, Q3, and E∀ are all built on this enforcer, the missing negation propagates into Theorems 3.1, 3.2, 3.4, and 4.1. As supplied, this is a load-bearing gap in the formal basis of the paper.","section":"§2, Observation 2.1"},{"comment":"The chain clauses are printed as the all-positive cycle (w_{i,1}∨w_{i,2}) ∧ ... ∧ (w_{i,a}∨w_{i,1}). These clauses do not force w_{i,1}=...=w_{i,a}; for a=3, the assignment (T,T,F) satisfies every clause. The proof of statement 3.1.2 uses these clauses to conclude equality, so the intended clauses must be implications (¬w_{i,1}∨w_{i,2}), ..., (¬w_{i,a}∨w_{i,1}). The same issue affects the appearance counts: after Step 2 each w_{i,k} has one positive and one negative occurrence, and the chain must add exactly one positive and one negative occurrence to reach the claimed (2,2,2,2) counts. An analogous all-positive rendering occurs in Step 3 of Theorem 3.2, where the clauses must also be implications for the equality conclusion in statement 3.2.1.","section":"§3.2, Theorem 3.1, Step 3"},{"comment":"The replacement of a 2-clause is printed as (ℓ1∨ℓ2∨u) ∧ E(u). Since E(u) forces u=T, the 3-clause is automatically satisfied and does not preserve the constraint of the original 2-clause. The contradiction argument in statement 3.1.2 for a complemented 2-clause also requires the literal u in the 3-clause to be negated. In addition, the printed version gives u three unnegated and one negated appearance, contradicting the claimed (2,2,2,2) count; using (ℓ1∨ℓ2∨¬u) instead restores exactly two unnegated and two negated appearances. Thus Step 4 must use (ℓ1∨ℓ2∨¬u) rather than (ℓ1∨ℓ2∨u).","section":"§3.2, Theorem 3.1, Step 4"},{"comment":"Step 1 is printed with the duplicated pair Su(c_i,y_i,y_i) ∧ Su(c_i,y_i,y_i). The equality gadget needed for the equivalence in statement 3.2.1 must contain opposite polarities, for example Su(c_i,¬y_i,¬y_i) ∧ Su(¬c_i,y_i,y_i), in order to force y_i=c_i and to make the claimed counts come out: four unnegated and four negated appearances of y_i, and one unnegated and one negated appearance of c_i. As printed, the pair is either unsatisfiable for c_i=F (if the two copies are the same S(c,y,y) gadget) or does not give the stated counts. Consequently, the proof's assignment β4(y_i,k)=β4(c_i) is unsupported.","section":"§3.2, Theorem 3.2, Step 1"},{"comment":"In the forward direction of statement 4.1.1, the printed assignment sets β2(e_{i,k}) = β1(z_i). If β1(z_i)=T and the universal variable u_{i,k}=T, then the clause (z_{i,k}∨e_{i,k}∨u_{i,k}) is all true and hence not nae-satisfied, so the constructed formula Φ2 is not necessarily a yes-instance. The forward direction works only if e_{i,k} is assigned the negation of β1(z_i), or equivalently if the relevant clause contains a negated e-literal. This is a load-bearing gap in the proof of Theorem 4.1 as printed.","section":"§4.2, Theorem 4.1, proof of 4.1.1"}],"minor_comments":[{"comment":"The definition of a monotone Boolean formula is printed as \"no clause contains an element in {x1,x2,...,xn}\"; this should be the set of negated literals {¬x1,¬x2,...,¬xn}.","section":"§2, Preliminaries"},{"comment":"The sentence \"Let D be the clause obtained from C by applying Step 1\" should refer to the complement of C, since the subsequent argument concludes that all literals of D evaluate to F; otherwise the argument is incoherent.","section":"§3.2, Theorem 3.1, proof of 3.1.2"},{"comment":"The introduction attributes the Π_2^P-completeness of ∀∃ NAE-3-SAT to \"Dahlhaus et al. [6]\", but reference [6] is the Eiter-Gottlob report; the citation should be corrected.","section":"§1, Introduction"},{"comment":"The proof of Lemma 3.2 contains the typo \"Futhermore\" instead of \"Furthermore\".","section":"§3.1, Lemma 3.2"}],"recommendation":"major_revision","confidential_remarks":"The report is based on the supplied text. The systemic missing-negation issue makes it impossible to certify the proofs from the supplied version; the editor should ask the authors to confirm that the camera-ready text preserves all negation bars, especially in the S-enforcer, the chain clauses of Theorems 3.1 and 3.2, the Step 4 replacement clauses, the enforcer pair in Theorem 3.2, and the existential assignment in Theorem 4.1."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"The headline results are genuinely new: exact appearance-count thresholds for quantified 3-SAT and NAE-3-SAT that were not in Berman, Haviv, or Darmann-Döcker. The paper proves Balanced ∀∃ 3-SAT-(2,2,2,2) and (1,1,2,2) are Π_2^P-complete, pins down NP-completeness for the s1+s2=1 cases, and shows Monotone ∀∃ NAE-3-SAT-(1,3) is Π_2^P-complete for linear monotone formulas—plus matching positive results. The reduction strategy is standard enforcer work, but the gadgets are adapted to the quantified setting and the side results (co-NP, P) are correctly delimited. The authors re-derive the enforcer properties, so the circularity burden is low. For this subfield, it's a solid contribution.\n\nThe soft spot is the text I was given, not necessarily the PDF. The extracted formulas appear to lose negation bars in exactly the places where correctness depends on them. In Theorem 3.1 Step 3, the chain is rendered all-positive, which neither forces equality nor satisfies the (2,2,2,2) appearance counts; the intended implication chain with negated first literals repairs both. Theorem 3.2 Step 1 has Su(c_i,y_i,y_i) ∧ Su(c_i,y_i,y_i) duplicated, which would not enforce anything; the second copy needs negations. Theorem 3.4's E∀(d_i,k) is the same duplicated-clause issue. And in the first direction of Theorem 4.1's proof, setting e_i,k = β1(z_i) makes the clause (z_i,k ∨ e_i,k ∨ u_i,k) all-true when β1(z_i)=T and u_i,k=T; the existential should be ¬β1(z_i). These all look like typesetting or sign typos rather than flawed constructions—the intended gadgets are clear and the proofs otherwise hang together—but they are load-bearing enough that a referee needs the actual PDF to confirm.\n\nMinor: the introduction cites Stockmeyer and Dahlhaus for the base completeness, but the correct attribution for ∀∃ NAE-3-SAT is Eiter-Gottlob (as stated in the preliminaries). Not a big deal, but sloppy.\n\nIf the PDF restores the overlines and fixes the e_i,k assignment, I'd expect the theorems to hold. This deserves a serious referee; the results are new and the approach is sound. I'd bring it to reading group only after checking the PDF.","headline":"Genuinely new threshold results for quantified bounded-appearance SAT, but the extracted text hides negation bars in key gadgets—verify the PDF before trusting the completeness proofs.","tokens_in":27434,"tokens_out":6015,"would_cite":true,"duration_ms":54271,"reading_group":"maybe","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":["68Q17","68Q25","03D15"],"pacs":[],"model":"deepseek-v4-flash","headline":"Quantified 3-SAT stays $\\Pi_2^P$-complete under strict per-variable appearance limits, and quantified NAE-3-SAT stays complete in a linear monotone one-universal setting.","keywords":["quantified 3-SAT","quantified NAE-3-SAT","bounded variable appearances","polynomial hierarchy","Pi_2^P-completeness","enforcer gadgets","monotone linear formulas"],"falsifier":"Set the universal variable $c_i$ to false and the existential copy $y_i$ to true in the Step 1 gadget of Theorem 3.2. Taken literally, both copies of $S_u(c_i,y_i,y_i)$ are satisfiable by Observation 2.1, so the enforcer does not force $y_i=c_i$; this failure, if confirmed in the full construction, is enough to invalidate the equivalence in statement 3.2.1.","tokens_in":26141,"feed_emoji":"🧮","tokens_out":12404,"duration_ms":111863,"temperature":0.7,"pith_summary":"The paper draws a boundary for two quantified satisfiability problems inside the polynomial hierarchy. Its main results show that $\\forall\\exists$ 3-SAT remains $\\Pi_2^P$-complete when every variable appears exactly twice unnegated and exactly twice negated and when the number of universal and existential variables is equal; the same remains true when universal variables appear only once in each polarity and existential variables twice in each polarity. For Not-All-Equal 3-SAT, the paper proves $\\Pi_2^P$-completeness for linear monotone formulas in which each universal variable appears exactly once, each existential variable appears exactly three times, and no clause contains more than one universal variable. It also separates the easier territory: some one-literal universal variants are NP-complete, and certain NAE variants with existential variables appearing twice are in co-NP or polynomial time. The practical upshot is a near-complete map of where the quantified problems jump between the first and second levels of the hierarchy as variable appearances are restricted.","feed_headline":"Even four appearances per variable leave quantified 3-SAT hard","feed_subtitle":"The paper pins down the exact appearance limits where quantified 3-SAT and NAE-3-SAT lose second-level hardness.","key_machinery":"The arguments run through polynomial-time reductions that are carried by small Boolean gadgets called enforcers. The basic S-enforcer $S(\\ell_1,\\ell_2,\\ell_3)$ is a five-clause formula over three auxiliary variables that is satisfiable exactly when at least one of the three literals is true; from it the paper builds $x^{(2)}$ and $E(x)$, gadgets that force a designated variable to take the value true while respecting fixed appearance counts. Two quantified enforcers, $Q_1$ and $Q_3$, add blocks of universal variables in multiples that rebalance the universal and existential counts. The NAE half uses monotone gadgets: $NE_{\\mathrm{aux}}$ forces two variables to differ, $EQ$ forces equality, $NE$ combines them, and $P_1$ pads the appearance count of an existential variable without changing satisfiability. In the reductions, these gadgets are combined with a variable-splitting step, in which each appearance of a variable is replaced by a fresh variable linked by equality chains, and a clause-complement step, in which each clause is conjoined with its negated version; together these steps force all copies of a variable to agree and exactly control how many times each polarity appears.","core_discovery":"The central claim is that the quantified satisfiability problems $\\forall\\exists$ 3-SAT and $\\forall\\exists$ NAE-3-SAT keep their $\\Pi_2^P$-completeness under appearance bounds that are essentially the strictest possible without descending in the polynomial hierarchy. Theorem 3.1 proves Balanced $\\forall\\exists$ 3-SAT-(2,2,2,2) is $\\Pi_2^P$-complete: every variable, universal or existential, appears exactly twice unnegated and twice negated; every clause has exactly three distinct variables; and the universal and existential blocks have equal size. Theorem 3.2 strengthens this to Balanced $\\forall\\exists$ 3-SAT-(1,1,2,2), and Theorems 3.3 and 3.4 resolve the intermediate regimes, giving NP-completeness when each universal variable has exactly one appearance in total and $\\Pi_2^P$-completeness when each universal variable has one unnegated and one negated appearance. On the NAE side, Theorem 4.1 shows Monotone $\\forall\\exists$ NAE-3-SAT-(1,3) is $\\Pi_2^P$-complete even for linear formulas with at most one universal variable per clause, while the final section places Monotone $\\forall\\exists$ NAE-3-SAT-(s,2) in co-NP and its $(1,2)$ case in P. Quantified NAE-3-SAT can therefore tolerate a single universal appearance, a regime in which ordinary $\\forall\\exists$ 3-SAT is only NP-complete unless the polynomial hierarchy collapses.","pith_inferences":["The same enforcer-plus-variable-splitting recipe should transfer to other quantified constraint satisfaction problems whose unquantified versions are NP-complete under bounded appearances; a natural next case is 1-in-3 SAT, whose NAE-style symmetry may again absorb a single universal appearance.","The sharp contrast between the two problems suggests that the not-all-equal predicate, because it is invariant under flipping all truth values, neutralizes the extra power that a second universal appearance gives ordinary quantified 3-SAT.","One testable extension the authors leave open is whether optimization versions of these $\\Pi_2^P$-complete problems remain hard to approximate under the same appearance bounds."],"forward_implications":["Balanced $\\forall\\exists$ 3-SAT-(2,2,2,2) being $\\Pi_2^P$-complete means that a formula with four appearances per variable and equally many universal and existential variables already encodes the full difficulty of the second level of the polynomial hierarchy.","The (1,1,2,2) result shows that one universal appearance in each polarity is sufficient for $\\Pi_2^P$-completeness, so the universal variables can be almost as constrained as the existential ones.","Monotone $\\forall\\exists$ NAE-3-SAT-(1,3) being $\\Pi_2^P$-complete means linearity, monotonicity, one universal appearance, and three existential appearances do not weaken the quantified problem.","The NP-completeness of $\\forall\\exists$ 3-SAT-(s1,s2,t1,t2) with $s_1+s_2=1$ and $(t_1,t_2)\\in\\{(1,2),(2,1)\\}$ shows that at the first level of the hierarchy the existential variables carry the hardness, and the universal quantifier becomes eliminable.","Monotone $\\forall\\exists$ NAE-3-SAT-(1,2) being polynomial-time solvable and $(s,2)$ variants being in co-NP marks the $(1,3)$ theorem as a tight boundary rather than an artifact of the reduction."],"supporting_citations":[{"why":"Supplies the S-enforcer and $x^{(2)}$ gadgets and the variable-splitting reduction pattern used throughout Section 3.","marker":"[1]"},{"why":"Supplies the NP-complete restricted 3-SAT basis used for the $s_1+s_2=1$ NP-completeness theorem.","marker":"[4]"},{"why":"Supplies the monotone NAE enforcers and the unquantified linear monotone exact-4 result on which Proposition 4.1 builds.","marker":"[5]"},{"why":"Establishes the $\\Pi_2^P$-completeness of $\\forall\\exists$ NAE-3-SAT used as the starting problem in Section 4.","marker":"[6]"},{"why":"Gives the NP and co-NP membership bounds for small appearance counts that separate the easy from the hard cases.","marker":"[8]"},{"why":"Provides the linear-time NAE-SAT algorithm and clause-graph characterization used to prove MC-NAE-3-SAT-2 lies in P.","marker":"[11]"},{"why":"Supplies the transformation from NAE-3-SAT to a quantified formula with universals replaced by existentials, used in Theorem 3.1.","marker":"[13]"},{"why":"Establishes the $\\Pi_2^P$-completeness of $\\forall\\exists$ 3-SAT and supplies the polynomial-hierarchy background.","marker":"[16]"},{"why":"Provides the classical bounded-appearance 3-SAT results and the polynomial-time regime that mark the boundary.","marker":"[17]"}],"fun_headline_variants":["Quantified 3-SAT remains Π₂^P-complete with four appearances per variable","One universal appearance yields hard quantified NAE-3-SAT","Exact appearance limits decide where quantified SAT is hard","Tight appearance bounds don't soften quantified SAT hardness","Monotone linear NAE-3-SAT still hard with one universal appearance"],"cache_read_input_tokens":3200,"weakest_assumption_plain":"The load-bearing premise is that the printed enforcer gadgets force the values their names claim; in particular, the second copy of $S_u(c_i,y_i,y_i)$ and the second copy in $E_\\forall(d_{i,k})$ must contain negated literals as the surrounding proof assumes, since identical copies would not force equality or truth and the yes-instance equivalences in statements 3.2.1 and 3.4.1 would fail.","fun_headline_variants_meta":{"raw":{"variants":["Quantified 3-SAT remains Π₂^P-complete with four appearances per variable","One universal appearance yields hard quantified NAE-3-SAT","Exact appearance limits decide where quantified SAT is hard","Tight appearance bounds don't soften quantified SAT hardness","Monotone linear NAE-3-SAT still hard with one universal appearance"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.001643,"raw_usage":{"total_tokens":6662,"prompt_tokens":1214,"completion_tokens":5448,"prompt_tokens_details":{"cached_tokens":384},"prompt_cache_hit_tokens":384,"prompt_cache_miss_tokens":830,"completion_tokens_details":{"reasoning_tokens":5356}},"tokens_in":830,"tokens_out":5448,"duration_ms":43554,"temperature":1.0,"reasoning_tokens":5356,"cache_read_input_tokens":384,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-14T13:16:42.424340+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"Set the universal variable $c_i$ to false and the existential copy $y_i$ to true in the Step 1 gadget of Theorem 3.2. Taken literally, both copies of $S_u(c_i,y_i,y_i)$ are satisfiable by Observation 2.1, so the enforcer does not force $y_i=c_i$; this failure, if confirmed in the full construction, is enough to invalidate the equivalence in statement 3.2.1.","supporting_citations":[{"cited_title":"Berman, M","cited_arxiv_id":null,"evidence_quote":"Supplies the S-enforcer and $x^{(2)}$ gadgets and the variable-splitting reduction pattern used throughout Section 3."},{"cited_title":"Dahlhaus, D","cited_arxiv_id":null,"evidence_quote":"Supplies the NP-complete restricted 3-SAT basis used for the $s_1+s_2=1$ NP-completeness theorem."},{"cited_title":"Darmann and J","cited_arxiv_id":null,"evidence_quote":"Supplies the monotone NAE enforcers and the unquantified linear monotone exact-4 result on which Proposition 4.1 builds."},{"cited_title":"Eiter and G","cited_arxiv_id":null,"evidence_quote":"Establishes the $\\Pi_2^P$-completeness of $\\forall\\exists$ NAE-3-SAT used as the starting problem in Section 4."},{"cited_title":"Haviv, O","cited_arxiv_id":null,"evidence_quote":"Gives the NP and co-NP membership bounds for small appearance counts that separate the easy from the hard cases."},{"cited_title":"Porschen, B","cited_arxiv_id":null,"evidence_quote":"Provides the linear-time NAE-SAT algorithm and clause-graph characterization used to prove MC-NAE-3-SAT-2 lies in P."},{"cited_title":"Schaefer (2001)","cited_arxiv_id":null,"evidence_quote":"Supplies the transformation from NAE-3-SAT to a quantified formula with universals replaced by existentials, used in Theorem 3.1."},{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"Establishes the $\\Pi_2^P$-completeness of $\\forall\\exists$ 3-SAT and supplies the polynomial-hierarchy background."},{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"Provides the classical bounded-appearance 3-SAT results and the polynomial-time regime that mark the boundary."}],"review_version":1}