Strong Sparsification for 1-in-3-SAT via Polynomial Freiman-Ruzsa
Pith reviewed 2026-05-19 03:14 UTC · model grok-4.3
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.
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
- 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.
Referee Report
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)
- [§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.
- [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)
- [Definition 1.2] The formal definition of strong sparsification (Definition 1.2) would benefit from an immediate comparison table contrasting it with ordinary sparsification.
- [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
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
-
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
-
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
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
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.
Lean theorems connected to this paper
-
IndisputableMonolith/Foundation/RealityFromDistinction.leanreality_from_one_distinction unclear?
unclearRelation between the paper passage and the cited Recognition theorem.
Theorem 3. Fix n, d. Consider V = {v1, …, vn} ⊆ F_2^d and let N1, …, Nn ⊆ V satisfy (i) for all i, v_i + N_i = N_i, and (ii) for all i, v1 … v_{i-1} ∉ <N_i + N_i>. Then ∑ |N_i| = O(n^{2-ε}) … using Polynomial Freiman-Ruzsa Theorem
-
IndisputableMonolith/Cost/FunctionalEquation.leanwashburn_uniqueness_aczel unclear?
unclearRelation between the paper passage and the cited Recognition theorem.
Proof of Theorem 7 … Balog-Szemerédi-Gowers … Polynomial Freiman-Ruzsa … E_4(V) … doubling |B+B| ≤ K|B| … subspace G …
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
-
[1]
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]
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]
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]
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]
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]
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]
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]
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
work page internal anchor Pith review arXiv 2025
-
[9]
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]
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]
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]
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]
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
work page internal anchor Pith review Pith/arXiv arXiv doi:10.1109/focs.2019.00059 2019
-
[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]
Fomin and Lukasz Kowalik and Daniel Lokshtanov and D
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]
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
work page internal anchor Pith review Pith/arXiv arXiv doi:10.1007/s00453-019-00660-y 2020
-
[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
work page internal anchor Pith review Pith/arXiv arXiv doi:10.1137/120880471 2013
-
[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]
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]
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]
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]
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
work page internal anchor Pith review Pith/arXiv arXiv doi:10.1137/15m1046186 2017
-
[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]
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]
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]
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]
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]
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]
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]
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
work page internal anchor Pith review Pith/arXiv arXiv doi:10.1145/3349618 2019
-
[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]
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]
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]
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]
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]
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]
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]
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
discussion (0)
Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.