pith. sign in

arxiv: 2606.25895 · v1 · pith:R3BZIATDnew · submitted 2026-06-24 · 💻 cs.CC

The Power of Small Symmetries

Nikita Gaevoy This is my paper

Pith reviewed 2026-06-25 19:09 UTC · model grok-4.3

classification 💻 cs.CC
keywords proof complexityresolutionsymmetriessmall symmetriesexponential separationsSRCISRIIFrege systems
0
0 comments X

The pith

Resolution systems with symmetries limited to a bounded number of variables form strict exponential hierarchies.

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

The paper shows that adding small symmetries—symmetries acting on only a fixed number of variables at once—to resolution creates a hierarchy ordered by that bound. For both global symmetries applied to the whole formula and local symmetries applied to subformulas, increasing the bound yields systems that are exponentially stronger than those with smaller bounds. Even the lowest levels in these hierarchies are exponentially stronger than plain resolution and separate from constant-depth Frege systems. The same constructions give the first exponential separation between the classical SRCI and SRII systems.

Core claim

We show that proof systems with both local and global small symmetries form strict hierarchies w.r.t. the size of symmetries. We prove exponential separations between proof systems with symmetries of different sizes and types. It turns out that even lower levels of these hierarchies are exponentially separated from Resolution and stronger proof systems, such as constant-depth Frege. As a byproduct of our constructions, we obtain an exponential separation between the classical systems SRCI and SRII that was not known before.

What carries the argument

Small symmetries: symmetries that operate on a limited number of variables at the same time and are used to shorten resolution derivations.

If this is right

  • Increasing the bound on symmetry size produces exponentially shorter proofs than any smaller bound allows.
  • Even the smallest fixed bound on symmetry size yields exponential savings over plain resolution.
  • Lower levels of the small-symmetry hierarchy remain exponentially stronger than constant-depth Frege.
  • Global and local versions of small symmetries produce distinct hierarchy levels with their own exponential separations.
  • The constructions separate SRCI from SRII by an exponential factor.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • Practical SAT solvers could exploit small symmetries without needing to detect arbitrary large ones.
  • Approximating dynamic symmetries by small ones might make lower-bound techniques for dynamic systems more tractable.
  • Similar bounded-resource hierarchies could appear in other proof systems that incorporate limited forms of symmetry or automorphism.

Load-bearing premise

Specific families of formulas exist where symmetries of one bounded size cannot be simulated by symmetries of any smaller size without an exponential increase in proof length.

What would settle it

A concrete formula family on which the shortest proof in the system with symmetry size k is not exponentially longer than the shortest proof in the system with symmetry size k+1.

read the original abstract

Resolution with symmetries is a natural extension of the Resolution proof system that allows to use symmetries of the formula to simplify the proof. Symmetries can be global (applied to the whole input formula), local (applied to a subformula), or dynamic (applied to newly derived clauses as well). The framework of Resolution with (global) symmetries was introduced by Krishnamurthy (1985) and further extended by Arai and Urquhart (2000) to local symmetries. Later, Szeider (2005) generalized this approach to homomorphisms and introduced the notion of Resolution with dynamic symmetries. While proving superpolynomial proof-size lower bounds for Resolution with dynamic symmetries remains an open problem already for two decades, the power of proof systems with global and local symmetries is well studied: exponential lower bounds have been proven for these proof systems, as well as exponential separations between all of them. However, these systems are too general to reflect practical applications since it is computationally too hard to find and efficiently exploit arbitrary symmetries. In this work, we introduce the notion of small symmetries: symmetries that can operate on a limited number of variables at the same time. Resolution with small symmetries gives hopes both for practical applications and for theoretical study of dynamic symmetries. We show that proof systems with both local and global small symmetries form strict hierarchies w.r.t. the size of symmetries. We prove exponential separations between proof systems with symmetries of different sizes and types. It turns out that even lower levels of these hierarchies are exponentially separated from Resolution and stronger proof systems, such as constant-depth Frege. As a byproduct of our constructions, we obtain an exponential separation between the classical systems SRCI and SRII that was not known before.

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 / 3 minor

Summary. The paper introduces 'small symmetries' (symmetries acting on at most k variables simultaneously) as a restriction on global, local, and dynamic symmetry exploitation in Resolution. It defines corresponding proof systems (global/local small-symmetry resolution) and proves that both form strict hierarchies with respect to k. Exponential separations are shown between systems with different k and between global vs. local variants; the lowest non-trivial levels are exponentially stronger than Resolution and constant-depth Frege. The same constructions yield a new exponential separation between the classical systems SRCI and SRII.

Significance. If the explicit formula-family constructions hold, the work supplies a parameterized, potentially practical bridge between full-symmetry systems (computationally intractable) and ordinary Resolution, while delivering the first strict hierarchies and the indicated exponential separations from stronger systems. The byproduct SRCI/SRII separation is a concrete advance. The provision of concrete witnessing formulas (rather than existence proofs alone) is a methodological strength that supports reproducibility of the lower-bound arguments.

minor comments (3)
  1. [§2.2] §2.2: the formal definition of a k-small symmetry (as a permutation acting on at most k variables while fixing the rest) should explicitly state whether the permutation must preserve the entire clause set or only a subformula; the current wording leaves the scope ambiguous for local symmetries.
  2. [Theorem 4.3] Theorem 4.3 (hierarchy for global small symmetries): the base case k=1 is stated to coincide with ordinary Resolution, but the proof sketch does not address whether the size measure counts the symmetry applications themselves; a short clarifying sentence would prevent misreading.
  3. [Figure 3] Figure 3 (separation diagram): the arrow labels for exponential vs. superpolynomial separations are not visually distinguished; adding a legend or different line styles would improve readability.

Simulated Author's Rebuttal

0 responses · 0 unresolved

We thank the referee for the positive and encouraging report, which highlights the contributions of our work on small symmetries in resolution. The recommendation for minor revision is noted, and we will address any editorial or presentational suggestions in the revised manuscript.

Circularity Check

0 steps flagged

No significant circularity

full rationale

The paper defines new notions of small symmetries (global and local) and supplies explicit formula-family constructions to witness strict size-based hierarchies and exponential separations from Resolution and constant-depth Frege. These constructions are presented directly rather than derived from fitted parameters or prior self-citations; the cited earlier systems (Krishnamurthy 1985, Arai-Urquhart 2000, Szeider 2005) are external and the byproduct SRCI/SRII separation follows from the same families without reduction to a self-citation chain or definitional equivalence. The derivation chain is therefore self-contained against external benchmarks.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 1 invented entities

The central claims rest on the newly introduced definition of small symmetries and on the existence of separating formula families; the work inherits standard axioms of propositional logic and resolution from the cited literature.

axioms (1)
  • domain assumption Standard axioms and inference rules of the Resolution proof system and its extensions with global, local, and dynamic symmetries as defined in Krishnamurthy (1985), Arai and Urquhart (2000), and Szeider (2005).
    The paper explicitly builds its new systems on these established definitions.
invented entities (1)
  • small symmetries no independent evidence
    purpose: Symmetries restricted to a bounded number of variables to enable both practical exploitation and theoretical hierarchy results.
    Newly defined in the paper as the central technical device.

pith-pipeline@v0.9.1-grok · 5834 in / 1476 out tokens · 36281 ms · 2026-06-25T19:09:52.204006+00:00 · methodology

discussion (0)

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

Reference graph

Works this paper leans on

35 extracted references · 18 canonical work pages

  1. [1]

    Arai and Alasdair Urquhart

    Noriko H. Arai and Alasdair Urquhart. Local symmetries in propositional logic. In Roy Dyckhoff, editor, Automated Reasoning with Analytic Tableaux and Related Methods , pages 40--51, Berlin, Heidelberg, 2000. Springer Berlin Heidelberg

    2000

  2. [5]

    Symmetric explanation learning: Effective dynamic symmetry handling for SAT

    Jo Devriendt, Bart Bogaerts, and Maurice Bruynooghe. Symmetric explanation learning: Effective dynamic symmetry handling for SAT . In Serge Gaspers and Toby Walsh, editors, Theory and Applications of Satisfiability Testing -- SAT 2017 , pages 83--100, Cham, 2017. Springer International Publishing

    2017

  3. [8]

    Marijn J. H. Heule, Oliver Kullmann, and Victor W. Marek. Solving and verifying the boolean pythagorean triples problem via cube-and-conquer. In Nadia Creignou and Daniel Le Berre, editors, Theory and Applications of Satisfiability Testing -- SAT 2016 , pages 228--245, Cham, 2016. Springer International Publishing

    2016

  4. [10]

    Stephan, Y

    Johan Håstad and Kilian Risse. On bounded depth proofs for Tseitin formulas on the grid; revisited. In 2022 IEEE 63rd Annual Symposium on Foundations of Computer Science (FOCS) , pages 1138--1149, 2022. https://doi.org/10.1109/FOCS54457.2022.00110 doi:10.1109/FOCS54457.2022.00110

    work page doi:10.1109/focs54457.2022.00110 2022

  5. [11]

    Exploiting isomorphic subgraphs in SAT

    Alexander Ivrii and Ofer Strichman. Exploiting isomorphic subgraphs in SAT . Proceedings of the 21st Formal Methods in Computer-Aided Design, FMCAD 2021 , pages 204--211, 2021. https://arxiv.org/abs/2103.10267 arXiv:2103.10267 , https://doi.org/10.34727/2021/isbn.978-3-85448-046-4_29 doi:10.34727/2021/isbn.978-3-85448-046-4_29

    work page doi:10.34727/2021/isbn.978-3-85448-046-4_29 2021

  6. [13]

    Michal Kouril and Jerome L. Paul. The van der Waerden number W(2, 6) is 1132. Experimental Mathematics , 17(1):53--61, 2008. https://doi.org/10.1080/10586458.2008.10129025 doi:10.1080/10586458.2008.10129025

    work page doi:10.1080/10586458.2008.10129025 2008

  7. [15]

    Short proofs for tricky formulas

    Balakrishnan Krishnamurthy. Short proofs for tricky formulas. Acta Inf. , 22(3):253–275, August 1985

    1985

  8. [18]

    The complexity of resolution with generalized symmetry rules

    Stefan Szeider. The complexity of resolution with generalized symmetry rules. Theory of Computing Systems , 38:171--188, February 2005. https://doi.org/10.1007/s00224-004-1192-0 doi:10.1007/s00224-004-1192-0

    work page doi:10.1007/s00224-004-1192-0 2005

  9. [21]

    Journal of Symbolic Logic , author =

    The relative efficiency of propositional proof systems , volume =. Journal of Symbolic Logic , author =. 1979 , pages =. doi:10.2307/2273702 , number =

    work page doi:10.2307/2273702 1979

  10. [22]

    On Small-depth

    H. On Small-depth. J. ACM , month = nov, articleno =. 2020 , issue_date =. doi:10.1145/3425606 , abstract =

    work page doi:10.1145/3425606 2020

  11. [23]

    On Bounded Depth Proofs for

    Håstad, Johan and Risse, Kilian , booktitle =. On Bounded Depth Proofs for. 2022 , volume =

    2022

  12. [24]

    On the Decision Trees with Symmetries , booktitle =

    Riazanov, Artur , editor =. On the Decision Trees with Symmetries , booktitle =. 2018 , publisher =

    2018

  13. [25]

    SIAM Journal on Computing , volume =

    Segerlind, Nathan and Buss, Sam and Impagliazzo, Russell , title =. SIAM Journal on Computing , volume =. 2004 , doi =. https://doi.org/10.1137/S0097539703428555 , abstract =

    work page doi:10.1137/s0097539703428555 2004

  14. [26]

    Ben-Sasson, Eli and Wigderson, Avi , title =. J. ACM , month = mar, pages =. 2001 , issue_date =. doi:10.1145/375827.375835 , abstract =

    work page doi:10.1145/375827.375835 2001

  15. [27]

    Acta Inf

    Krishnamurthy, Balakrishnan , title =. Acta Inf. , month = aug, pages =. 1985 , issue_date =

    1985

  16. [28]

    The Complexity of Resolution with Generalized Symmetry Rules , volume =

    Szeider, Stefan , year =. The Complexity of Resolution with Generalized Symmetry Rules , volume =. Theory of Computing Systems , doi =

  17. [29]

    38th International Symposium on Theoretical Aspects of Computer Science (STACS 2021) , pages =

    Schweitzer, Pascal and Seebach, Constantin , title =. 38th International Symposium on Theoretical Aspects of Computer Science (STACS 2021) , pages =. 2021 , volume =. doi:10.4230/LIPIcs.STACS.2021.58 , annote =

    work page doi:10.4230/lipics.stacs.2021.58 2021

  18. [30]

    Exploiting Isomorphic Subgraphs in

    Ivrii, Alexander and Strichman, Ofer , doi =. Exploiting Isomorphic Subgraphs in. Proceedings of the 21st Formal Methods in Computer-Aided Design, FMCAD 2021 , pages =. arXiv , arxivid =:2103.10267 , isbn =

    arXiv 2021

  19. [31]

    1999 , issn =

    The symmetry rule in propositional logic , journal =. 1999 , issn =. doi:https://doi.org/10.1016/S0166-218X(99)00039-6 , author =

    work page doi:10.1016/s0166-218x(99)00039-6 1999

  20. [32]

    Urquhart, Alasdair , title =. J. ACM , month = jan, pages =. 1987 , issue_date =. doi:10.1145/7531.8928 , abstract =

    work page doi:10.1145/7531.8928 1987

  21. [33]

    1985 , note =

    The intractability of resolution , journal =. 1985 , note =. doi:https://doi.org/10.1016/0304-3975(85)90144-6 , author =

    work page doi:10.1016/0304-3975(85)90144-6 1985

  22. [34]

    Symmetric Explanation Learning: Effective Dynamic Symmetry Handling for

    Devriendt, Jo and Bogaerts, Bart and Bruynooghe, Maurice , editor =. Symmetric Explanation Learning: Effective Dynamic Symmetry Handling for. Theory and Applications of Satisfiability Testing -- SAT 2017 , year =

    2017

  23. [35]

    and Urquhart, Alasdair , editor =

    Arai, Noriko H. and Urquhart, Alasdair , editor =. Local Symmetries in Propositional Logic , booktitle =. 2000 , publisher =

    2000

  24. [36]

    On the weak pigeonhole principle , volume =

    Jan Krajíček , journal =. On the weak pigeonhole principle , volume =

  25. [37]

    , title =

    Sakallah, Karem A. , title =. Handbook of Satisfiability , editor =. 2009 , doi =

    2009

  26. [38]

    On the satisfiability of symmetrical constrained satisfaction problems , booktitle =

    Puget, Jean-Francois , editor =. On the satisfiability of symmetrical constrained satisfaction problems , booktitle =. 1993 , publisher =

    1993

  27. [39]

    SIAM Journal on Computing , volume =

    Dantchev, Stefan and Galesi, Nicola and Ghani, Abdul and Martin, Barnaby , title =. SIAM Journal on Computing , volume =. 2024 , doi =

    2024

  28. [40]

    Lower bounds for resolution and cutting plane proofs and monotone computations , volume =

    Pudlák, Pavel , date =. Lower bounds for resolution and cutting plane proofs and monotone computations , volume =. doi:10.2307/2275583 , abstract =

    work page doi:10.2307/2275583

  29. [41]

    Journal of Artificial Intelligence Research , author =

    Certified Symmetry and Dominance Breaking for Combinatorial Optimisation , volume =. Journal of Artificial Intelligence Research , author =. 2022 , month = mar, day =. doi:10.1613/jair.1.14296 , abstract =

    work page doi:10.1613/jair.1.14296 2022

  30. [42]

    Exponential lower bounds for the pigeonhole principle , volume =

    Pitassi, Toniann and Beame, Paul and Impagliazzo, Russell , urldate =. Exponential lower bounds for the pigeonhole principle , volume =. doi:10.1007/BF01200117 , pages =

    work page doi:10.1007/bf01200117

  31. [43]

    An Exponenetioal Lower Bound to the Size of Bounded Depth Frege Proofs of the Pigeonhole Principle , journal =

    Krajíček, Jan and Pudlák, Pavel and Woods, Alan , urldate =. An exponential lower bound to the size of bounded depth frege proofs of the pigeonhole principle , volume =. doi:10.1002/rsa.3240070103 , abstract =

    work page doi:10.1002/rsa.3240070103

  32. [44]

    2018 , month =

    Proceedings of the AAAI Conference on Artificial Intelligence , author =. 2018 , month =. doi:10.1609/aaai.v32i1.12209 , number =

    work page doi:10.1609/aaai.v32i1.12209 2018

  33. [45]

    Paul , title =

    Michal Kouril and Jerome L. Paul , title =. Experimental Mathematics , volume =. 2008 , publisher =

    2008

  34. [46]

    Artificial Intelligence , volume =

    Computer-aided proof of. Artificial Intelligence , volume =. 2015 , issn =. doi:https://doi.org/10.1016/j.artint.2015.03.004 , author =

    work page doi:10.1016/j.artint.2015.03.004 2015

  35. [47]

    Heule, Marijn J. H. and Kullmann, Oliver and Marek, Victor W. , editor =. Solving and Verifying the Boolean Pythagorean Triples Problem via Cube-and-Conquer , booktitle =. 2016 , publisher =

    2016