pith. sign in

arxiv: 2507.17878 · v4 · pith:JM5S3NM7new · submitted 2025-07-23 · 💻 cs.DS · cs.CC· cs.DM· math.CO

Strong Sparsification for 1-in-3-SAT via Polynomial Freiman-Ruzsa

Pith reviewed 2026-05-19 03:14 UTC · model grok-4.3

classification 💻 cs.DS cs.CCcs.DMmath.CO
keywords strong sparsification1-in-3-SATPolynomial Freiman-Ruzsa Theoremvariable merginghypergraph colouringconstraint satisfaction problems
0
0 comments X

The pith

1-in-3-SAT admits strong sparsification by merging variables, with the algorithm's correctness following from a sub-quadratic bound on vector sets in F_2^d obtained via the Polynomial Freiman-Ruzsa Theorem.

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

The paper defines strong sparsification as a reduction that merges variables rather than deleting constraints. It constructs such an algorithm for 1-in-3-SAT whose safety rests on proving that certain collections of vectors over GF(2) cannot be too large. The size bound is derived from the Polynomial Freiman-Ruzsa Theorem and is the key step that lets the merging procedure preserve satisfiability. A reader would care because the sparsified instances immediately yield an improved approximation algorithm for linearly-ordered 3-uniform hypergraph colouring and open the question of which other constraint problems allow the same treatment.

Core claim

The central claim is that a strong sparsification algorithm exists for 1-in-3-SAT. The algorithm merges variables; its correctness is guaranteed once one establishes a sub-quadratic upper bound on the size of certain sets of vectors in F_2^d. That bound is proved by direct application of the Polynomial Freiman-Ruzsa Theorem.

What carries the argument

The sub-quadratic bound on the cardinality of certain subsets of vectors in F_2^d, obtained from the Polynomial Freiman-Ruzsa Theorem, which limits linear dependencies sufficiently to certify that variable merging preserves the 1-in-3 property.

If this is right

  • The approximation ratio for linearly-ordered colourings of 3-uniform hypergraphs improves over the previous best algorithm.
  • Strong sparsification algorithms may exist for selected other constraint satisfaction problems.
  • The Polynomial Freiman-Ruzsa Theorem supplies a new tool for designing polynomial-time preprocessing routines for SAT-type problems.

Where Pith is reading between the lines

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

  • The same vector-set bound may apply to other problems whose constraints can be encoded as linear equations over GF(2).
  • If the bound is tight only for certain algebraic structures, strong sparsification will succeed precisely on those CSPs whose constraint language respects the same linear geometry.
  • Derandomising the merging procedure or making the bound constructive would turn the existence result into an explicit polynomial-time algorithm.

Load-bearing premise

The sub-quadratic bound on the size of the relevant vector sets in F_2^d holds for every set that arises from a 1-in-3-SAT instance and can be used directly in the variable-merging step.

What would settle it

An explicit 1-in-3-SAT instance whose associated vector set in F_2^d has size larger than quadratic in the dimension, or a small instance on which every possible variable merge changes the satisfiability status in a way forbidden by the sparsification definition.

read the original abstract

We introduce a new notion of sparsification, called \emph{strong sparsification}, in which constraints are not removed but variables can be merged. As our main result, we present a strong sparsification algorithm for 1-in-3-SAT. The correctness of the algorithm relies on establishing a sub-quadratic bound on the size of certain sets of vectors in $\mathbb{F}_2^d$. This result, obtained using the recent \emph{Polynomial Freiman-Ruzsa Theorem} (Gowers, Green, Manners and Tao, Ann. Math. 2025), could be of independent interest. As an application, we improve the state-of-the-art algorithm for approximating linearly-ordered colourings of 3-uniform hypergraphs (H{\aa}stad, Martinsson, Nakajima and{\v{Z}}ivn{\'{y}}, APPROX 2024). We also investigate the existence of strong sparsification algorithms for other constraint satisfaction problems.

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 introduces the notion of strong sparsification for constraint satisfaction problems, in which variables may be merged (rather than constraints removed) while exactly preserving satisfiability. The central result is a strong sparsification algorithm for 1-in-3-SAT whose correctness rests on establishing a sub-quadratic upper bound on the size of certain vector sets in F_2^d; this bound is obtained by applying the Polynomial Freiman-Ruzsa Theorem of Gowers, Green, Manners and Tao (2025). The algorithm is then used to improve the approximation guarantee for linearly-ordered 3-uniform hypergraph colorings, and the paper briefly investigates the existence of analogous strong sparsification procedures for other CSPs.

Significance. If the vector-set bound applies directly and without hidden restrictions on the input formulas, the work supplies a concrete algorithmic application of the recent Polynomial Freiman-Ruzsa Theorem and yields a measurable improvement over the prior approximation result of Håstad et al. (APPROX 2024). The combinatorial statement itself may be of independent interest to additive combinatorics. The paper does not claim machine-checked proofs or fully parameter-free derivations, but the explicit reduction from 1-in-3-SAT clauses to vector sets in F_2^d is a falsifiable step that can be checked.

major comments (2)
  1. [§3] §3 (Application of PFR): the claim that the sets A constructed from the 1-in-3-SAT clauses satisfy the small-doubling (or equivalent) hypothesis required by the Polynomial Freiman-Ruzsa Theorem is stated but not verified in detail; without an explicit argument that |A+A| ≤ K|A| for K independent of the instance, it is unclear whether the resulting bound is genuinely sub-quadratic in d rather than quadratic.
  2. [Theorem 1.1] Theorem 1.1 and §4.1 (variable-merging procedure): the translation from the sub-quadratic vector-set bound to a concrete reduction in the number of variables must be shown to preserve satisfiability exactly; the current sketch leaves open whether the merging step introduces new solutions or requires additional restrictions on the input formula.
minor comments (2)
  1. [Definition 1.2] The formal definition of strong sparsification (Definition 1.2) would benefit from an immediate comparison table contrasting it with ordinary sparsification.
  2. [References] The bibliographic entry for Gowers et al. (Ann. Math. 2025) should be completed with page numbers or DOI once available.

Simulated Author's Rebuttal

2 responses · 0 unresolved

We thank the referee for the careful reading and constructive comments on our manuscript. We address each major comment below and will revise the paper accordingly to strengthen the presentation.

read point-by-point responses
  1. Referee: [§3] §3 (Application of PFR): the claim that the sets A constructed from the 1-in-3-SAT clauses satisfy the small-doubling (or equivalent) hypothesis required by the Polynomial Freiman-Ruzsa Theorem is stated but not verified in detail; without an explicit argument that |A+A| ≤ K|A| for K independent of the instance, it is unclear whether the resulting bound is genuinely sub-quadratic in d rather than quadratic.

    Authors: We agree that an explicit verification of the small-doubling condition is needed for clarity. In the revised manuscript we will add a self-contained lemma in §3 showing that the set A of vectors arising from the 1-in-3-SAT clauses satisfies |A+A| ≤ 2^{O(1)}|A| with the implied constant independent of both d and the input formula. The argument relies on the fact that each clause imposes a linear dependence over F_2 that limits the number of distinct sums; this is a direct consequence of the clause structure and does not require any additional assumptions on the instance. revision: yes

  2. Referee: [Theorem 1.1] Theorem 1.1 and §4.1 (variable-merging procedure): the translation from the sub-quadratic vector-set bound to a concrete reduction in the number of variables must be shown to preserve satisfiability exactly; the current sketch leaves open whether the merging step introduces new solutions or requires additional restrictions on the input formula.

    Authors: We will expand the proof of Theorem 1.1 and the description in §4.1 with a formal argument that the variable-merging step preserves satisfiability exactly. Specifically, we will prove that (i) every satisfying assignment to the original formula induces a satisfying assignment to the merged formula by identifying merged variables, and (ii) conversely, any satisfying assignment to the merged formula extends to a satisfying assignment of the original formula by assigning the same value to all variables that were merged. The construction uses only the vector-set bound and introduces no new solutions or extra restrictions on the input beyond the standard definition of 1-in-3-SAT. revision: yes

Circularity Check

0 steps flagged

No circularity: central bound derived from external PFR theorem applied to clause-derived vector sets

full rationale

The paper's main result establishes a sub-quadratic bound on vector sets in F_2^d arising from 1-in-3-SAT clauses and invokes the Polynomial Freiman-Ruzsa Theorem of Gowers, Green, Manners and Tao (Ann. Math. 2025) to obtain it. This theorem is external, with no author overlap and no reduction of the claimed bound to a fitted parameter or self-defined quantity inside the paper. The variable-merging procedure is then justified by that bound, without the bound itself being presupposed by the merging step or by any self-citation chain. The cited prior work on hypergraph colouring is used only for an application, not for the correctness of the sparsification algorithm itself. No equation or step reduces by construction to its own input.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 0 invented entities

The result depends on the Polynomial Freiman-Ruzsa Theorem as an external black-box result; no free parameters or new invented entities are introduced in the abstract.

axioms (1)
  • domain assumption The Polynomial Freiman-Ruzsa Theorem provides a sub-quadratic bound on the size of certain sets of vectors in F_2^d that is sufficient for the variable-merging procedure.
    Invoked in the abstract as the source of the key combinatorial bound.

pith-pipeline@v0.9.0 · 5726 in / 1301 out tokens · 21609 ms · 2026-05-19T03:14:31.653998+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

38 extracted references · 38 canonical work pages · 6 internal anchors

  1. [1]

    Energy-Efficient Algorithms,

    Alexandr Andoni, Jiecao Chen, Robert Krauthgamer, Bo Qin, David P. Woodruff, and Qin Zhang. On sketching quadratic forms. In Proc. 7th ACM Conference on Innovations in Theoretical Computer Science (ITCS'16) , pages 311--–319. ACM, 2016. https://doi.org/10.1145/2840728.2840753 doi:10.1145/2840728.2840753

  2. [2]

    (2+ ) - S at is NP -hard

    Per Austrin, Venkatesan Guruswami, and Johan H stad. (2+ )- S at is NP -hard. SIAM J. Comput. , 46(5):1554--1573, 2017. https://doi.org/10.1137/15M1006507 doi:10.1137/15M1006507

  3. [3]

    Proof verification and the hardness of approximation problems

    Sanjeev Arora, Carsten Lund, Rajeev Motwani, Madhu Sudan, and Mario Szegedy. Proof verification and the hardness of approximation problems. J. ACM , 45(3):501--555, 1998. https://doi.org/10.1145/278298.278306 doi:10.1145/278298.278306

  4. [4]

    Probabilistic checking of proofs: A new characterization of NP

    Sanjeev Arora and Shmuel Safra. Probabilistic checking of proofs: A new characterization of NP . J. ACM , 45(1):70--122, 1998. https://doi.org/10.1145/273865.273901 doi:10.1145/273865.273901

  5. [5]

    Libor Barto, Diego Battistelli, and Kevin M. Berg. Symmetric Promise Constraint Satisfaction Problems: Beyond the Boolean Case . In Proc. 38th International Symposium on Theoretical Aspects of Computer Science (STACS'21) , volume 187 of LIPIcs , pages 10:1--10:16. Schloss Dagstuhl -- Leibniz-Zentrum f \"u r Informatik, 2021. http://arxiv.org/abs/2010.0462...

  6. [6]

    Algebraic approach to promise constraint satisfaction

    Libor Barto, Jakub Bul \' n, Andrei A. Krokhin, and Jakub Opr s al. Algebraic approach to promise constraint satisfaction. J. ACM , 68(4):28:1--28:66, 2021. http://arxiv.org/abs/1811.00970 arXiv:1811.00970 , https://doi.org/10.1145/3457606 doi:10.1145/3457606

  7. [7]

    Promise constraint satisfaction: algebraic structure and a symmetric B oolean dichotomy

    Joshua Brakensiek and Venkatesan Guruswami. Promise constraint satisfaction: A lgebraic structure and a symmetric B oolean dichotomy. SIAM J. Comput. , 50(6):1663--1700, 2021. http://arxiv.org/abs/1704.01937 arXiv:1704.01937 , https://doi.org/10.1137/19M128212X doi:10.1137/19M128212X

  8. [8]

    Redundancy is all you need

    Joshua Brakensiek and Venkatesan Guruswami. Redundancy is all you need. In Proc. 57th Annual ACM Symposium on Theory of Computing (STOC'25) . ACM , 2025. http://arxiv.org/abs/2411.03451 arXiv:2411.03451

  9. [9]

    In Gary L

    Andr\' a s A. Bencz\' u r and David R. Karger. Approximating s-t Minimum Cuts in O (n^2) Time . In Proc. 28th Annual ACM Symposium on Theory of Computing (STOC'96) , pages 47--55. ACM, 1996. https://doi.org/10.1145/237814.237827 doi:10.1145/237814.237827

  10. [10]

    New approximation algorithms for graph coloring

    Avrim Blum. New approximation algorithms for graph coloring. J. ACM , 41(3):470--516, 1994. https://doi.org/10.1145/176584.176586 doi:10.1145/176584.176586

  11. [11]

    A statistical theorem of set addition

    Antal Balog and Endre Szemer \'e di. A statistical theorem of set addition. Comb. , 14(3):263--268, 1994. https://doi.org/10.1007/BF01212974 doi:10.1007/BF01212974

  12. [12]

    Spielman, and Nikhil Srivastava

    Joshua Batson, Daniel A. Spielman, and Nikhil Srivastava. Twice- R amanujan sparsifiers. SIAM Review , 56(2):315--334, 2014. http://arxiv.org/abs/0808.0163 arXiv:0808.0163 , https://doi.org/10.1137/130949117 doi:10.1137/130949117

  13. [13]

    New Notions and Constructions of Sparsification for Graphs and Hypergraphs

    Nikhil Bansal, Ola Svensson, and Luca Trevisan. New notions and constructions of sparsification for graphs and hypergraphs. Proc. 60th IEEE Annual Symposium on Foundations of Computer Science (FOCS'19) , pages 910--928, 2019. http://arxiv.org/abs/1905.01495 arXiv:1905.01495 , https://doi.org/10.1109/FOCS.2019.00059 doi:10.1109/FOCS.2019.00059

  14. [14]

    Sparsification of binary C S P s

    Silvia Butti and Stanislav Z ivn \' y . Sparsification of binary C S P s. SIAM J. Discret. Math. , 34(1):825--842, 2020. http://arxiv.org/abs/1901.00754 arXiv:1901.00754 , https://doi.org/10.1137/19M1242446 doi:10.1137/19M1242446

  15. [15]

    Fomin, Lukasz Kowalik, Daniel Lokshtanov, Dániel Marx, Marcin Pilipczuk, Michal Pilipczuk, and Saket Saurabh.Parameterized Algorithms

    Marek Cygan, Fedor V Fomin, ukasz Kowalik, Daniel Lokshtanov, D \'a niel Marx, Marcin Pilipczuk, Micha Pilipczuk, and Saket Saurabh. Parameterized algorithms . Springer, 2015. https://doi.org/10.1007/978-3-319-21275-3 doi:10.1007/978-3-319-21275-3

  16. [16]

    Hubie Chen, Bart M. P. Jansen, and Astrid Pieterse. Best-case and worst-case sparsifiability of B oolean csps. Algorithmica , 82(8):2200--2242, 2020. http://arxiv.org/abs/1809.06171 arXiv:1809.06171 , https://doi.org/10.1007/S00453-019-00660-Y doi:10.1007/S00453-019-00660-Y

  17. [17]

    Unique-maximum and conflict-free colorings for hypergraphs and tree graphs

    Panagiotis Cheilaris, Balázs Keszegh, and Dömötör Pálvölgyi. Unique-maximum and conflict-free coloring for hypergraphs and tree graphs. SIAM J. Discret. Math. , 27(4):1775--1787, 2013. http://arxiv.org/abs/1002.4210 arXiv:1002.4210 , https://doi.org/10.1137/120880471 doi:10.1137/120880471

  18. [18]

    The PCP theorem by gap amplification

    Irit Dinur. The PCP theorem by gap amplification. J. ACM , 54(3):12, 2007. https://doi.org/10.1145/1236457.1236459 doi:10.1145/1236457.1236459

  19. [19]

    Faster exact solutions for some np-hard problems

    Limor Drori and David Peleg. Faster exact solutions for some np-hard problems. Theor. Comput. Sci. , 287(2):473--499, 2002. https://doi.org/10.1016/S0304-3975(01)00257-2 doi:10.1016/S0304-3975(01)00257-2

  20. [20]

    Smyth , title =

    Irit Dinur, Oded Regev, and Clifford Smyth. The Hardness of 3-Uniform Hypergraph Coloring . Comb. , 25(5):519--535, 2005. https://doi.org/10.1007/s00493-005-0032-4 doi:10.1007/s00493-005-0032-4

  21. [21]

    Satisfiability allows no nontrivial sparsification unless the polynomial-time hierarchy collapses

    Holger Dell and Dieter van Melkebeek. Satisfiability allows no nontrivial sparsification unless the polynomial-time hierarchy collapses. J. ACM , 61(4):23:1--23:27, 2014. https://doi.org/10.1145/2629620 doi:10.1145/2629620

  22. [22]

    Sparsification of Two-Variable Valued CSPs

    Arnold Filtser and Robert Krauthgamer. Sparsification of two-variable valued constraint satisfaction problems. SIAM J. Discret. Math. , 31(2):1263--1276, 2017. http://arxiv.org/abs/1509.01844 arXiv:1509.01844 , https://doi.org/10.1137/15M1046186 doi:10.1137/15M1046186

  23. [23]

    Kernelization: theory of parameterized preprocessing

    Fedor V Fomin, Daniel Lokshtanov, Saket Saurabh, and Meirav Zehavi. Kernelization: theory of parameterized preprocessing . Cambridge University Press, 2019. https://doi.org/10.1017/9781107415157 doi:10.1017/9781107415157

  24. [24]

    On a conjecture of M arton

    William Timothy Gowers, Ben Green, Freddie Manners, and Terence Tao. On a conjecture of M arton. Ann. Math. , 201(2):515--549, 2025. http://arxiv.org/abs/2311.05762 arXiv:2311.05762 , https://doi.org/10.4007/annals.2025.201.2.5 doi:10.4007/annals.2025.201.2.5

  25. [25]

    Garey and David S

    Michael R. Garey and David S. Johnson. The complexity of near-optimal graph coloring. J. ACM , 23(1):43--49, 1976. https://doi.org/10.1145/321921.321926 doi:10.1145/321921.321926

  26. [26]

    A new proof of szemer \'e di's theorem for arithmetic progressions of length four

    William Timothy Gowers. A new proof of szemer \'e di's theorem for arithmetic progressions of length four. Geom. Funct. Anal. , 8(3):529--551, 1998. https://doi.org/10.1007/s000390050065 doi:10.1007/s000390050065

  27. [27]

    Goemans and David P

    Michel X. Goemans and David P. Williamson. Improved approximation algorithms for maximum cut and satisfiability problems using semidefinite programming. J. ACM , 42(6):1115--1145, 1995. https://doi.org/10.1145/227683.227684 doi:10.1145/227683.227684

  28. [28]

    A Logarithmic Approximation of Linearly-Ordered Colourings

    Johan H a stad, Bj\" o rn Martinsson, Tamio-Vesa Nakajima, and Stanislav Z ivn\' y . A Logarithmic Approximation of Linearly-Ordered Colourings . In Proc. Approximation, Randomization, and Combinatorial Optimization. Algorithms and Techniques (APPROX/RANDOM 2024) , pages 7:1--7:6. Schloss Dagstuhl -- Leibniz-Zentrum f \"u r Informatik, 2024. http://arxiv....

  29. [29]

    Which problems have strongly exponential complexity? J

    Russell Impagliazzo, Ramamohan Paturi, and Francis Zane. Which problems have strongly exponential complexity? J. Comput. Syst. Sci. , 63(4):512--530, 2001. https://doi.org/10.1006/JCSS.2001.1774 doi:10.1006/JCSS.2001.1774

  30. [30]

    Bart M. P. Jansen and Astrid Pieterse. Optimal Sparsification for Some Binary CSPs Using Low-Degree Polynomials . ACM Trans. Comput. Theory , 11(4):28:1--28:26, 2019. http://arxiv.org/abs/1606.03233 arXiv:1606.03233 , https://doi.org/10.1145/3349618 doi:10.1145/3349618

  31. [31]

    [KPS24] Sanjeev Khanna, Aaron L

    Dmitry Kogan and Robert Krauthgamer. Sketching cuts in graphs and hypergraphs. In Proc. 6th ACM Conference on Innovations in Theoretical Computer Science (ITCS'15) , pages 367--376. ACM, 2015. https://doi.org/10.1145/2688073.2688093 doi:10.1145/2688073.2688093

  32. [32]

    doi:10.1109/focs61266.2024.00070 , booktitle=

    Sanjeev Khanna, Aaron Putterman, and Madhu Sudan. Near-optimal size linear sketches for hypergraph cut sparsifiers. In Proc. 65th IEEE Annual Symposium on Foundations of Computer Science (FOCS'24) , pages 1669--1706. IEEE , 2024. http://arxiv.org/abs/2407.03934 arXiv:2407.03934 , https://doi.org/10.1109/FOCS61266.2024.00105 doi:10.1109/FOCS61266.2024.00105

  33. [33]

    Code sparsification and its applications

    Sanjeev Khanna, Aaron (Louie) Putterman, and Madhu Sudan. Code sparsification and its applications. In Proc. 2024 ACM-SIAM Symposium on Discrete Algorithms (SODA'24) , pages 5145--5168. SIAM , 2024. http://arxiv.org/abs/2311.00788 arXiv:2311.00788 , https://doi.org/10.1137/1.9781611977912.185 doi:10.1137/1.9781611977912.185

  34. [34]

    Efficient algorithms and new characterizations for csp sparsification

    Sanjeev Khanna, Aaron (Louie) Putterman, and Madhu Sudan. Efficient algorithms and new characterizations for csp sparsification. In Proc. 57th Annual ACM Symposium on Theory of Computing (STOC'25) , pages 407--416. ACM , 2025. http://arxiv.org/abs/2404.06327 arXiv:2404.06327 , https://doi.org/10.1145/3717823.3718205 doi:10.1145/3717823.3718205

  35. [35]

    Sparsification of SAT and CSP problems via tractable extensions

    Victor Lagerkvist and Magnus Wahlstr \" o m. Sparsification of SAT and CSP problems via tractable extensions. ACM Trans. Comput. Theory , 12(2):13:1--13:29, 2020. https://doi.org/10.1145/3389411 doi:10.1145/3389411

  36. [36]

    Linearly Ordered Colourings of Hypergraphs , journal =

    Tamio-Vesa Nakajima and Stanislav Z ivn\' y . Linearly ordered colourings of hypergraphs. ACM Trans. Comput. Theory , 13(3--4), 2022. http://arxiv.org/abs/2204.05628 arXiv:2204.05628 , https://doi.org/10.1145/3570909 doi:10.1145/3570909

  37. [37]

    Additive sparsification of csps

    Eden Pelleg and Stanislav Z ivn \' y . Additive sparsification of csps. ACM Trans. Algorithms , 20(1):1:1--1:18, 2024. http://arxiv.org/abs/2106.14757 arXiv:2106.14757 , https://doi.org/10.1145/3625824 doi:10.1145/3625824

  38. [38]

    Note on the Theorem of Balog, Szemer \'e di, and Gowers

    Christian Reiher and Tomasz Schoen. Note on the Theorem of Balog, Szemer \'e di, and Gowers . Comb. , 44(3):691--698, 2024. http://arxiv.org/abs/2308.10245 arXiv:2308.10245 , https://doi.org/10.1007/s00493-024-00092-5 doi:10.1007/s00493-024-00092-5