pith. sign in

arxiv: 2104.00406 · v3 · pith:TGX5AAE7new · submitted 2021-04-01 · 💻 cs.CC · cs.LO· math.LO

The complete classification for quantified equality constraints

Dmitriy Zhuk , Barnaby Martin , Michal Wrona This is my paper

Pith reviewed 2026-05-24 13:25 UTC · model grok-4.3

classification 💻 cs.CC cs.LOmath.LO
keywords quantified constraint satisfactionequality languagescomplexity classificationPSPACE-completeQCSPtrichotomyLogspaceNP-complete
0
0 comments X

The pith

QCSP over natural numbers with the relation x=y implies y=z is PSPACE-complete.

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

The paper proves that QCSP(N; x=y→y=z) is PSPACE-complete. This settles an open question from more than ten years ago. The result finishes the full classification of QCSP problems over all equality languages into a trichotomy of Logspace, NP-complete, or PSPACE-complete. It also classifies the bounded-alternation versions of these problems into Logspace, NP-complete, coNP-complete, or levels inside the polynomial hierarchy.

Core claim

We prove that QCSP(ℕ; x=y→y=z) is PSPACE-complete, settling a question open for more than ten years. This completes the complexity classification for the QCSP over equality languages as a trichotomy between Logspace, NP-complete and PSPACE-complete. We additionally settle the classification for bounded alternation QCSP(Γ), for Γ an equality language. Such problems are either in Logspace, NP-complete, co-NP-complete or rise in complexity in the Polynomial Hierarchy.

What carries the argument

The ternary relation x=y→y=z on the natural numbers, which serves as the template that reduces from a known PSPACE-complete problem to establish hardness in the QCSP setting for equality languages.

Load-bearing premise

The specific relation x=y→y=z produces PSPACE-completeness through a correct reduction from a known hard problem and that all cases in the equality-language classification have been covered without gaps.

What would settle it

A demonstration that QCSP(N; x=y→y=z) lies in NP or that some equality language falls outside the three claimed classes.

Figures

Figures reproduced from arXiv: 2104.00406 by Barnaby Martin, Dmitriy Zhuk, Michal Wrona.

Figure 2
Figure 2. Figure 2: Set of constraints C0. 2. variables x 0 i and x 1 i encode the variable xi ; x 0 i = t means that xi = 0, x 1 i = t means that xi = 1; 3. variables y 0 i and y 1 i encode the variable yi ; y 0 i = t means that yi = 0, y 1 i = t means that yi = 1. x y z t z [PITH_FULL_IMAGE:figures/full_fig_p006_2.png] view at source ↗
Figure 1
Figure 1. Figure 1: An example of a graph defining constraints. [PITH_FULL_IMAGE:figures/full_fig_p006_1.png] view at source ↗
Figure 3
Figure 3. Figure 3: Set of constraints Ci . x 0 n−1 y 1 n−1 y 0 n−1 y 1 n y 0 n x 1 n t x 0 n z [PITH_FULL_IMAGE:figures/full_fig_p007_3.png] view at source ↗
Figure 4
Figure 4. Figure 4: Set of constraints Cn−1. x 0 n y 1 n y 0 n t z [PITH_FULL_IMAGE:figures/full_fig_p007_4.png] view at source ↗
Figure 5
Figure 5. Figure 5: Set of constraints Cn. 7 [PITH_FULL_IMAGE:figures/full_fig_p007_5.png] view at source ↗
Figure 6
Figure 6. Figure 6: Set of constraints F. Theorem 3. Formulas Φ and Ψ are equivalent. Lemma 4. Φ → Ψ. Proof. In the following, we make no assumption that t 6= f, though the more interesting cases arise when this is true. Suppose we have a strategy for the existential player (EP) in Φ. Let us define a strategy for the existential player (EP) in Ψ. First, we want at most one of the two values x 0 i and x 1 i to be equal to t, a… view at source ↗
read the original abstract

We prove that QCSP$(\mathbb{N};x=y\rightarrow y=z)$ is PSpace-complete, settling a question open for more than ten years. This completes the complexity classification for the QCSP over equality languages as a trichotomy between Logspace, NP-complete and PSpace-complete. We additionally settle the classification for bounded alternation QCSP$(\Gamma)$, for $\Gamma$ an equality language. Such problems are either in Logspace, NP-complete, co-NP-complete or rise in complexity in the Polynomial Hierarchy.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

0 major / 2 minor

Summary. The paper proves that QCSP(ℕ; x=y→y=z) is PSPACE-complete, completing the complexity classification of QCSP over equality languages as a trichotomy (Logspace, NP-complete, PSPACE-complete). It further classifies bounded-alternation QCSP(Γ) for equality languages Γ into Logspace, NP-complete, coNP-complete, or polynomial-hierarchy levels.

Significance. The result settles a question open for over ten years and supplies the first full trichotomy for quantified equality constraints, including the bounded-alternation case. The argument rests on case analysis over equality languages, an explicit reduction establishing PSPACE-hardness, and placement within the polynomial hierarchy; these elements are presented without hidden finiteness assumptions or unaccounted quantifier configurations on the infinite domain ℕ.

minor comments (2)
  1. The reduction construction in the main theorem would benefit from an explicit statement of the quantifier prefix used in the target instance of QCSP(ℕ; x=y→y=z).
  2. Notation for the bounded-alternation classes (e.g., Σ_k^P vs. Π_k^P) should be introduced once in a preliminary section rather than repeated inline.

Simulated Author's Rebuttal

0 responses · 0 unresolved

We thank the referee for their positive assessment and recommendation to accept the manuscript. The report accurately captures the contribution in completing the trichotomy for QCSPs over equality languages and the bounded-alternation classification.

Circularity Check

0 steps flagged

No significant circularity in the derivation chain

full rationale

The paper establishes its central result—a direct proof that QCSP(ℕ; x=y→y=z) is PSPACE-complete via explicit reduction from a known hard problem, completing the trichotomy for equality languages—through case analysis over equality languages, reduction construction, and placement in the polynomial hierarchy. No load-bearing step reduces by construction to self-definition, a fitted parameter renamed as prediction, or a self-citation chain whose justification is internal to the present work; the argument is self-contained against external benchmarks and does not invoke uniqueness theorems or ansatzes from prior author work as the sole support for the classification.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 0 invented entities

No free parameters, invented entities, or ad-hoc axioms are visible in the abstract; the result rests on standard definitions of complexity classes.

axioms (1)
  • standard math Standard definitions and properties of the complexity classes Logspace, NP, PSPACE, and the polynomial hierarchy.
    The trichotomy and bounded-alternation classification are stated in terms of these established classes.

pith-pipeline@v0.9.0 · 5605 in / 1230 out tokens · 29819 ms · 2026-05-24T13:25:00.732220+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Lean theorems connected to this paper

Citations machine-checked in the Pith Canon. Every link opens the source theorem in the public Lean library.

What do these tags mean?
matches
The paper's claim is directly supported by a theorem in the formal canon.
supports
The theorem supports part of the paper's argument, but the paper may add assumptions or extra steps.
extends
The paper goes beyond the formal theorem; the theorem is a base layer rather than the whole result.
uses
The paper appears to rely on the theorem as machinery.
contradicts
The paper's claim conflicts with a theorem or certificate in the canon.
unclear
Pith found a possible connection, but the passage is too broad, indirect, or ambiguous to say the theorem truly supports the claim.

Reference graph

Works this paper leans on

27 extracted references · 27 canonical work pages

  1. [1]

    V., and Pinsker, M

    Barto, L., Kompatscher, M., Ols ´ak, M., Pham, T. V., and Pinsker, M. The equivalence of two dichotomy conjectures for infinite domain constraint satisfaction problems. In 32nd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2017, Reykjavik, Ice - land, June 20-23, 2017 (2017), IEEE Computer Society, pp. 1–12

    work page 2017

  2. [2]

    Topology is irrelevant (in a dichotomy conjecture for infinite domain constraint satisfaction pro blems)

    Barto, L., and Pinsker, M. Topology is irrelevant (in a dichotomy conjecture for infinite domain constraint satisfaction pro blems). SIAM J. Comput. 49 , 2 (2020), 365–393

    work page 2020

  3. [3]

    Quantified equality constraints

    Bodirsky, M., and Chen, H. Quantified equality constraints. In 22nd IEEE Symposium on Logic in Computer Science (LICS 2007), 10- 12 July 2007, Wroclaw, Poland, Proceedings (2007), IEEE Computer Society, pp. 203–212

    work page 2007

  4. [4]

    Quantified equality constraints

    Bodirsky, M., and Chen, H. Quantified equality constraints. SIAM J. Comput. 39 , 8 (2010), 3682–3699

    work page 2010

  5. [5]

    The reducts of equality up to primitive positive interdefinability

    Bodirsky, M., Chen, H., and Pinsker, M. The reducts of equality up to primitive positive interdefinability. J. Symb. Log. 75 , 4 (2010), 1249–1292

    work page 2010

  6. [6]

    The complexity of equality constraint languages

    Bodirsky, M., and K ´ara, J. The complexity of equality constraint languages. Theory Comput. Syst. 43 , 2 (2008), 136–158

    work page 2008

  7. [7]

    The complexity of temporal constraint satisfaction problems

    Bodirsky, M., and K ´ara, J. The complexity of temporal constraint satisfaction problems. J. ACM 57 , 2 (2010), 9:1–9:41

    work page 2010

  8. [8]

    Discrete temporal constraint satisfaction problems

    Bodirsky, M., Martin, B., and Mottet, A. Discrete temporal constraint satisfaction problems. J. ACM 65 , 2 (2018), 9:1–9:41

    work page 2018

  9. [9]

    A dichotomy for first-order reducts of unary structures

    Bodirsky, M., and Mottet, A. A dichotomy for first-order reducts of unary structures. Log. Methods Comput. Sci. 14 , 2 (2018)

    work page 2018

  10. [10]

    Constraint satisfaction with count- able homogeneous templates

    Bodirsky, M., and Nesetril, J. Constraint satisfaction with count- able homogeneous templates. J. Log. Comput. 16 , 3 (2006), 359–373

    work page 2006

  11. [11]

    Schaefer’s theorem for graphs

    Bodirsky, M., and Pinsker, M. Schaefer’s theorem for graphs. J. ACM 62 , 3 (2015), 19:1–19:52

    work page 2015

  12. [12]

    Bulatov, A. A. A dichotomy theorem for nonuniform CSPs. In 2017 IEEE 58th Annual Symposium on Foundations of Computer Science (FOCS) (2017), pp. 319–330

    work page 2017

  13. [13]

    Quantified positive temporal constraints

    Charatonik, W., and Wrona, M. Quantified positive temporal constraints. In Computer Science Logic, 22nd International Workshop, 21 CSL 2008, 17th Annual Conference of the EACSL, Bertinoro, Italy, September 16-19, 2008. Proceedings (2008), M. Kaminski and S. Mar- tini, Eds., vol. 5213 of Lecture Notes in Computer Science , Springer, pp. 94–108

    work page 2008

  14. [14]

    Tractable quantified constraint satisfaction problems over positive temporal templates

    Charatonik, W., and Wrona, M. Tractable quantified constraint satisfaction problems over positive temporal templates. I n Logic for Programming, Artificial Intelligence, and Reasoning, 15th In ternational Conference, LPAR 2008, Doha, Qatar, November 22-27, 2008. Pro ceed- ings (2008), I. Cervesato, H. Veith, and A. Voronkov, Eds., vol. 5 330 of Lecture Note...

    work page 2008

  15. [15]

    A rendezvous of logic, complexity, and algebra

    Chen, H. A rendezvous of logic, complexity, and algebra. SIGACT News 37 , 4 (2006), 85–114

    work page 2006

  16. [16]

    Existentially restricted quantified constraint satisfact ion

    Chen, H. Existentially restricted quantified constraint satisfact ion. Inf. Comput. 207 , 3 (2009), 369–388

    work page 2009

  17. [17]

    Three concrete complexity questions about constraints, in search of theories

    Chen, H. Three concrete complexity questions about constraints, in search of theories. Invited talk at Arbeitstagung Allgemei ne Alge- bra (Workshop on General Algebra), AAA98, Dresden, Germany , July 2019

    work page 2019

  18. [18]

    An algebraic preservation theorem for aleph-zero categorical quantified constraint satisfactio n

    Chen, H., and M ¨uller, M. An algebraic preservation theorem for aleph-zero categorical quantified constraint satisfactio n. Log. Methods Comput. Sci. 9 , 1 (2012)

    work page 2012

  19. [19]

    Guarded ord-horn: A tractable fragment of quantified constraint satisfaction

    Chen, H., and Wrona, M. Guarded ord-horn: A tractable fragment of quantified constraint satisfaction. In 19th International Symposium on Temporal Representation and Reasoning, TIME 2012, Leicest er, United Kingdom, September 12-14, 2012 (2012), B. C. Moszkowski, M. Reynolds, and P. Terenziani, Eds., IEEE Computer Society , pp. 99– 106

    work page 2012

  20. [20]

    The complexity of logic-based abduc- tion

    Eiter, T., and Gottlob, G. The complexity of logic-based abduc- tion. J. ACM 42 , 1 (1995), 3–42

    work page 1995

  21. [21]

    Model Theory

    Hodges, W. Model Theory . Encyclopedia of Mathematics and its Applications. Cambridge University Press, 1993

    work page 1993

  22. [22]

    A., Jeavons, P., and Jonsson, P

    Krokhin, A. A., Jeavons, P., and Jonsson, P. Reasoning about temporal relations: The tractable subalgebras of allen’s i nterval algebra. J. ACM 50 , 5 (2003), 591–640

    work page 2003

  23. [23]

    Tractability frontier for dually-closed ord-horn quanti- fied constraint satisfaction problems

    Wrona, M. Tractability frontier for dually-closed ord-horn quanti- fied constraint satisfaction problems. In Mathematical Foundations of Computer Science 2014 - 39th International Symposium, MFCS 201 4, 22 Budapest, Hungary, August 25-29, 2014. Proceedings, Part I (2014), E. Csuhaj-Varj´ u, M. Dietzfelbinger, and Z. ´Esik, Eds., vol. 8634 of Lecture Notes ...

    work page 2014

  24. [24]

    A proof of CSP dichotomy conjecture

    Zhuk, D. A proof of CSP dichotomy conjecture. In 2017 IEEE 58th Annual Symposium on Foundations of Computer Science (FOCS) (Oct 2017), pp. 331–342

    work page 2017

  25. [25]

    A proof of the CSP dichotomy conjecture

    Zhuk, D. A proof of the CSP dichotomy conjecture. J. ACM 67 , 5 (2020), 30:1–30:78

    work page 2020

  26. [26]

    The complexity of the quantified CSP having the polynomi- ally generated powers property

    Zhuk, D. The complexity of the quantified CSP having the polynomi- ally generated powers property. CoRR abs/2110.09504 (2021)

    work page arXiv 2021

  27. [27]

    QCSP monsters and the demise of the chen conjecture

    Zhuk, D., and Martin, B. QCSP monsters and the demise of the chen conjecture. In Proceedings of the 52nd Annual ACM SIGACT Symposium on Theory of Computing (2020), pp. 91–104. 23

    work page 2020