pith. sign in

arxiv: 2605.19055 · v1 · pith:FUOUTK5Tnew · submitted 2026-05-18 · 💻 cs.DM · cs.LO· math.CO

Super-linear Lower Bounds for CSP Non-Redundancy via Shrinking Instances

Joshua Brakensiek , Venkatesan Guruswami , Bart M. P. Jansen , Victor Lagerkvist , Magnus Wahlstr\"om This is my paper

Pith reviewed 2026-05-20 08:13 UTC · model grok-4.3

classification 💻 cs.DM cs.LOmath.CO
keywords constraint satisfaction problemsnon-redundancyhypergraph projectionsshrinking factorgadget reductionslower boundsCSP predicatesSAT solvers
0
0 comments X

The pith

Studying shrinking factors of hypergraph projections lets gadget reductions prove super-linear non-redundancy lower bounds for CSP predicates where earlier methods failed.

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

The paper recontextualizes gadget reductions between CSP predicates as hypergraph projections. By measuring the shrinking factor of these projections, it predicts more precisely which reductions transfer super-linear lower bounds on non-redundancy. This refines prior analyses and produces new lower bounds for specific predicates whose behavior was previously out of reach. The work further shows that SAT solvers can automatically discover useful reductions, creating a computational route to map relationships among more CSPs.

Core claim

Recontextualizing gadget reductions as hypergraph projections and introducing their shrinking factor shows that this quantity controls whether the reduction yields a super-linear NRD lower bound, allowing such bounds for concrete CSP predicates that previous gadget-reduction techniques could not establish.

What carries the argument

Hypergraph projections of CSP instances together with their shrinking factor, which quantifies size reduction under projection and thereby governs the super-linearity of the non-redundancy lower bound obtained via the corresponding gadget reduction.

If this is right

  • Super-linear NRD lower bounds become provable for additional concrete CSP predicates.
  • The success of a gadget reduction can be forecasted from the shrinking factor before the reduction is fully constructed.
  • Reductions between predicates can be discovered automatically by SAT solvers.
  • Analyses from earlier gadget-reduction papers are refined to give tighter predictions.

Where Pith is reading between the lines

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

  • The same shrinking-factor test may extend to related measures such as sparsification or kernelization size.
  • Systematic search could eventually classify which predicates have near-linear NRD.
  • The approach may generalize to higher-arity predicates or different hypergraph families.

Load-bearing premise

The shrinking factor of a hypergraph projection directly determines whether the associated gadget reduction produces a super-linear NRD lower bound rather than merely correlating with it in the examined cases.

What would settle it

An explicit gadget reduction between two predicates whose measured shrinking factor predicts a super-linear bound but for which the actual NRD lower bound remains only linear, or the converse case.

read the original abstract

The non-redundancy (NRD) of a constraint satisfaction problem (CSP) is a combinatorial quantity closely tied to the behavior of CSPs in various computational models including their sparsification, kernelization, and streaming complexity. A primary open question in the study of non-redundancy is the identification of which CSP predicates have near-linear NRD. Recent works by Carbonnel [CP 2022], Khanna, Putterman and Sudan [STOC 2025], Brakensiek and Guruswami [STOC 2025] and Brakensiek, Guruswami, Jansen, Lagerkvist, and Wahlstr\"om [2025] have introduced various forms of gadget reductions between CSPs to relate their non-redundancy. The primary contribution of this work is to recontextualize many of these gadget reductions in a framework which we call hypergraph projections. By studying a quantity we call the shrinking factor of these hypergraph projections, we can more precisely predict when a gadget reduction between predicates can yield a super-linear NRD lower bound, greatly improving on the analysis of previous works. To illustrate the power of our framework, we identify some concrete CSP predicates whose non-redundancy is at the cusp of our understanding and show how our methods give lower bounds that could not have been achieved with these previous methods. We also demonstrate how these gadget reductions can be automatically deduced using SAT solvers, thereby opening up novel computational avenues for discovering further relationships between the non-redundancy of various CSPs.

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

2 major / 2 minor

Summary. The manuscript recontextualizes gadget reductions for CSP non-redundancy (NRD) as hypergraph projections and introduces the shrinking factor of these projections as a quantity that predicts when a reduction yields a super-linear NRD lower bound. The authors apply the framework to concrete predicates whose NRD was previously out of reach, obtain improved lower bounds, and demonstrate that the underlying reductions can be discovered automatically via SAT solvers.

Significance. If the central claims hold, the work would meaningfully advance the study of NRD by supplying a more precise analytic tool than prior gadget-reduction analyses and by opening a computational route to discovering new relationships. The explicit use of SAT solvers to enumerate reductions is a reproducible strength that the paper correctly highlights.

major comments (2)
  1. [§3] §3 (Framework and main theorem): The manuscript defines the shrinking factor from the projection construction and then uses it to forecast super-linear NRD lower bounds, yet provides no general theorem establishing that a shrinking factor below a fixed threshold is a sufficient condition (as opposed to an observed correlation in the examined cases). The predictive claim for new predicates therefore rests on the unproven generality noted in the stress-test.
  2. [§5] §5 (Concrete predicates): The reported lower bounds for the new predicates are presented as improvements over prior methods, but the text does not include explicit shrinking-factor calculations or a verification that the predicted bounds match the actual NRD values obtained from the reductions; this gap prevents direct confirmation of the framework's accuracy.
minor comments (2)
  1. [§2] Notation for the hypergraph projection operator is introduced without a compact summary table relating it to the earlier gadget-reduction terminology; a small comparison table would improve readability.
  2. [Introduction] The abstract claims the framework 'greatly improving on the analysis of previous works,' but the introduction does not quantify the improvement (e.g., by citing the exact prior bounds that are now superseded).

Simulated Author's Rebuttal

2 responses · 0 unresolved

We thank the referee for their thoughtful review and constructive suggestions. We address the major comments point by point below and outline the revisions we plan to make.

read point-by-point responses

  1. Referee: [§3] §3 (Framework and main theorem): The manuscript defines the shrinking factor from the projection construction and then uses it to forecast super-linear NRD lower bounds, yet provides no general theorem establishing that a shrinking factor below a fixed threshold is a sufficient condition (as opposed to an observed correlation in the examined cases). The predictive claim for new predicates therefore rests on the unproven generality noted in the stress-test.

    Authors: We appreciate this point. The main theorem in Section 3 derives the super-linear lower bound directly from the shrinking factor being less than one in the hypergraph projection framework. This provides a sufficient condition within the context of the gadget reductions considered. However, we acknowledge that the generality for arbitrary new predicates relies on the specific constructions, as noted in the stress-test. To strengthen the presentation, we will include a clearer statement of the theorem's applicability and perhaps a corollary making the sufficient condition explicit. revision: partial

  2. Referee: [§5] §5 (Concrete predicates): The reported lower bounds for the new predicates are presented as improvements over prior methods, but the text does not include explicit shrinking-factor calculations or a verification that the predicted bounds match the actual NRD values obtained from the reductions; this gap prevents direct confirmation of the framework's accuracy.

    Authors: We agree that providing these explicit calculations would enhance the clarity and verifiability of our results. In the revised manuscript, we will add the computations of the shrinking factors for the predicates discussed in Section 5 and include a verification step showing how the predicted super-linear bounds align with the NRD lower bounds derived from the reductions. revision: yes

Circularity Check

0 steps flagged

No significant circularity; shrinking factor derived independently from projection construction

full rationale

The paper defines the shrinking factor directly from the hypergraph projection construction and applies it to analyze gadget reductions for NRD bounds. No step reduces a claimed prediction or lower bound to a fitted parameter or self-citation by construction. Self-citations to prior gadget work exist but are not load-bearing for the new framework's internal definitions or predictions, which remain self-contained against the combinatorial objects introduced. The derivation chain does not equate outputs to inputs via renaming or ansatz smuggling.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 2 invented entities

The framework rests on standard combinatorial definitions of hypergraphs and projections plus the modeling choice that NRD lower bounds can be read off from shrinking factors. No free parameters or invented physical entities are mentioned; the main new objects are the projection construction and the shrinking factor itself.

axioms (1)
  • domain assumption Hypergraph projections preserve the combinatorial structure needed to translate gadget reductions into NRD bounds
    Invoked when the authors recontextualize prior gadget reductions inside the new framework.
invented entities (2)
  • hypergraph projection no independent evidence
    purpose: A geometric view that organizes gadget reductions between CSP predicates
    New abstraction introduced to unify earlier reductions and enable shrinking-factor analysis
  • shrinking factor no independent evidence
    purpose: A numeric quantity that predicts whether a projection yields a super-linear NRD lower bound
    Central new quantity whose value determines the quality of the lower bound

pith-pipeline@v0.9.0 · 5838 in / 1567 out tokens · 47089 ms · 2026-05-20T08:13:36.854217+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

14 extracted references · 14 canonical work pages · 3 internal anchors

  1. [1]

    Chain Length and CSPs Learnable with Few Queries , booktitle =

    [BCK20] Christian Bessiere, Cl´ ement Carbonnel, and George Katsirelos. Chain Length and CSPs Learnable with Few Queries.Proceedings of the AAAI Conference on Artificial Intelli- gence, 34(02):1420–1427, April 2020.doi:10.1609/aaai.v34i02.5499. [BG25] Joshua Brakensiek and Venkatesan Guruswami. Redundancy is all you need. In Michal Kouck´ y and Nikhil Ban...

    work page doi:10.1609/aaai.v34i02.5499 2020

  2. [2]

    Redundancy Is All You Need , booktitle =

    ACM, 2025.doi:10.1145/3717823.3718212. [BGJ+25] Joshua Brakensiek, Venkatesan Guruswami, Bart M. P. Jansen, Victor Lagerkvist, and Magnus Wahlstr¨ om. The Richness of CSP Non-redundancy. (arXiv:2507.07942), July 2025.arXiv:2507.07942,doi:10.48550/arXiv.2507.07942. [BGP26] Joshua Brakensiek, Venkatesan Guruswami, and Aaron Putterman. Classification of non-...

    work page doi:10.1145/3717823.3718212 2025

  3. [3]

    In Gary L

    time. In Gary L. Miller, editor,Proceedings of the Twenty-Eighth Annual ACM Sympo- sium on the Theory of Computing, Philadelphia, Pennsylvania, USA, May 22-24, 1996, pages 47–55. ACM, 1996.doi:10.1145/237814.237827. [Bul17] Andrei A. Bulatov. A dichotomy theorem for nonuniform csps. In Chris Umans, edi- tor,58th IEEE Annual Symposium on Foundations of Com...

    work page doi:10.1145/237814.237827 1996

  4. [4]

    [BˇZ20] Silvia Butti and Stanislav ˇZivn´ y

    doi:10.1109/FOCS.2017.37. [BˇZ20] Silvia Butti and Stanislav ˇZivn´ y. Sparsification of Binary CSPs.SIAM Journal on Discrete Mathematics, 34(1):825–842, January 2020.doi:10.1137/19M1242446. [Car22] Cl´ ement Carbonnel. On Redundancy in Constraint Satisfaction Problems. In28th International Conference on Principles and Practice of Constraint Programming (...

    work page doi:10.1109/focs.2017.37 2017

  5. [5]

    Springer, 2008.doi:10.1007/978-3-540-78800-3\_24

    Proceedings, Lecture Notes in Computer Science, pages 337–340. Springer, 2008.doi:10.1007/978-3-540-78800-3\_24. [EHM64] Paul Erd˝ os, Andr´ as Hajnal, and John W. Moon. A problem in graph theory.The American Mathematical Monthly, 71(10):1107–1110,

    work page doi:10.1007/978-3-540-78800-3 2008

  6. [6]

    Sparsification of Two-Variable Valued Con- straint Satisfaction Problems.SIAM Journal on Discrete Mathematics, 31(2):1263–1276, January 2017.doi:10.1137/15M1046186

    [FK17] Arnold Filtser and Robert Krauthgamer. Sparsification of Two-Variable Valued Con- straint Satisfaction Problems.SIAM Journal on Discrete Mathematics, 31(2):1263–1276, January 2017.doi:10.1137/15M1046186. [Hav26] Ishay Haviv. Kernelization bounds for constrained coloring,

    work page doi:10.1137/15m1046186 2017

  7. [7]

    Kernelization Bounds for Constrained Coloring

    URL:https:// arxiv.org/abs/2604.21531,arXiv:2604.21531. [Kar93] David R. Karger. Global min-cuts in RNC, and other ramifications of a simple min- cut algorithm. In Vijaya Ramachandran, editor,Proceedings of the Fourth Annual ACM/SIGACT-SIAM Symposium on Discrete Algorithms, 25-27 January 1993, Austin, Texas, USA, pages 21–30. ACM/SIAM,

    work page internal anchor Pith review Pith/arXiv arXiv 1993

  8. [8]

    Sketching Cuts in Graphs and Hypergraphs

    [KK15] Dmitry Kogan and Robert Krauthgamer. Sketching Cuts in Graphs and Hypergraphs. InProceedings of the 2015 Conference on Innovations in Theoretical Computer Science, ITCS ’15, pages 367–376, New York, NY, USA, January

    work page 2015

  9. [9]

    [KPS24] Sanjeev Khanna, Aaron L

    Association for Computing Machinery.doi:10.1145/2688073.2688093. [KPS24] Sanjeev Khanna, Aaron L. Putterman, and Madhu Sudan. Code Sparsification and its Applications. InProceedings of the 2024 Annual ACM-SIAM Symposium on Discrete Algorithms (SODA), Proceedings, pages 5145–5168. Society for Industrial and Applied Mathematics, January 2024.doi:10.1137/1.9...

    work page doi:10.1145/2688073.2688093 2024

  10. [10]

    62,doi:10.4230/LIPICS.APPROX/RANDOM.2025.62

    URL:https://doi.org/10.4230/LIPIcs.APPROX/RANDOM.2025. 62,doi:10.4230/LIPICS.APPROX/RANDOM.2025.62. [LGE26] Victor Lagerkvist, Johanna Groven, and Leif Eriksson. Towards single exponential time for temporal and spatial reasoning: A study via redundancy and dynamic pro- gramming. In Sven Koenig, Chad Jenkins, and Matthew E. Taylor, editors,Fortieth AAAI Co...

    work page doi:10.4230/lipics.approx/random.2025 2025

  11. [11]

    [LW20] Victor Lagerkvist and Magnus Wahlstr¨ om

    URL:https://doi.org/10.1609/aaai.v40i17.38443, doi:10.1609/AAAI.V40I17.38443. [LW20] Victor Lagerkvist and Magnus Wahlstr¨ om. Sparsification of SAT and CSP Problems via Tractable Extensions.ACM Transactions on Computation Theory, 12(2):1–29, June 2020.doi:10.1145/3389411. [SV26a] Amatya Sharma and Santhoshini Velusamy. Characterizing streaming decidabili...

    work page doi:10.1609/aaai.v40i17.38443 2020

  12. [12]

    Characterizing Streaming Decidability of CSPs via Non-Redundancy

    URL:https://arxiv.org/abs/2604.21922,arXiv: 2604.21922. [SV26b] Amatya Sharma and Santhoshini Velusamy. Non-redundancy of low-arity symmetric boolean csps,

    work page internal anchor Pith review Pith/arXiv arXiv

  13. [13]

    Non-Redundancy of Low-Arity Symmetric Boolean CSPs

    URL:https://arxiv.org/abs/2605.14007,arXiv:2605.14007. [Zhu20] Dmitriy Zhuk. A Proof of the CSP Dichotomy Conjecture.J. ACM, 67(5):30:1–30:78, August 2020.doi:10.1145/3402029. A FindingI-substructures using a SAT-solver Given predicatesP 1 ⊊Q 1 ⊆D r1 1 andP 2 ⊊Q 2 ⊆D r2 2 as well as a familyI= (I 1, . . . , Ir2) of subsets of [r1] a natural question is ho...

    work page internal anchor Pith review Pith/arXiv arXiv doi:10.1145/3402029 2020

  14. [14]

    More precisely, consider the following predicates

    Cat+ 5 , we also give stronger lower bounds for some arity 3 projections. More precisely, consider the following predicates. For ease of discussion, we give each succinct names. P1 :=π {1,3,4} Cat5 ={001,111,120,222,212} Q1 :=π {1,3,4} Cat+ 5 =P 1 ∪ {000} P2 :=π {1,2,4} Cat5 ={011,111,120,222,202} Q2 :=π {1,2,4} Cat+ 5 =P 2 ∪ {000} P3 :=π {1,2,3,4} Cat5 =...

    work page 2012