pith. sign in

arxiv: 2202.08214 · v3 · submitted 2022-02-16 · 💻 cs.CC

Lower Bounds for Subset Sum in Resolution with Modular Counting

Fedor Part This is my paper

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

classification 💻 cs.CC
keywords subset sumresolution proof systemslinear equations over finite fieldserror-correcting codesproof complexity lower boundsdag-like refutationstree-like refutationsfinite fields
0
0 comments X

The pith

Certain Subset Sum instances require exponential-size refutations in Res(lin) over finite fields of characteristic at least 5.

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

The paper proves lower bounds on refutation sizes for unsatisfiable vector Subset Sum instances in the Res(lin_F_q) proof system. Hardness follows from the coefficient matrix generating a good error-correcting code. For (s,r)-robust instances, which guarantee minimum code distance at least r, dag-like refutations in a fragment of the system require size 2^Omega(r). Random instances and algebraic-geometry-code constructions achieve robustness parameters yielding superpolynomial bounds. Tree-like refutations of any such instance require size 2^Omega(((q+1)ln q)^{-1/3} d^{1/5}), where d is the code distance.

Core claim

For (s,r)-robust Subset Sum instances we prove 2^Omega(r) lower bound for sizes of refutations in a dag-like fragment of Res(lin_F_q). For tree-like Res(lin_F_q) refutations we show the size lower bound 2^Omega(((q+1)ln q)^{-1/3} d^{1/5}) for any Subset Sum instance where d is the minimal distance of C_A.

What carries the argument

The (s,r)-robustness property of Subset Sum instances, which ensures the coefficient matrix A generates an error-correcting code C_A with minimal distance s >= r and serves as the basis for the size lower bounds.

If this is right

  • Random instances are (n/3, Omega((n/(q+1)ln q)^{1/3}))-robust and therefore require dag-like refutations of size 2^Omega((n/(q+1)ln q)^{1/3}).
  • Algebraic geometry codes yield explicit constructions of instances achieving the same robustness parameters.
  • Every Subset Sum instance whose matrix generates a code of distance d has tree-like refutation size at least 2^Omega(((q+1)ln q)^{-1/3} d^{1/5}).
  • All stated bounds hold when the characteristic of F_q is at least 5.

Where Pith is reading between the lines

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

  • The robustness criterion directly imports distance properties of linear codes into proof-size lower bounds.
  • The same linking technique may apply to other systems of linear equations over finite fields.
  • Tighter analysis of the robustness-to-distance translation could improve the exponents in both the dag-like and tree-like bounds.

Load-bearing premise

The Subset Sum instances must satisfy the (s,r)-robustness property, which in particular implies that A defines an error-correcting code with minimal distance s >= r.

What would settle it

Exhibit one (s,r)-robust Subset Sum instance together with a dag-like Res(lin_F_q) refutation whose size is o(2^r).

read the original abstract

In this paper we prove lower bounds for sizes of refutations of unsatisfiable vector Subset Sum instances $\overrightarrow{a}_1 x_1 + \dots + \overrightarrow{a}_n x_n = \overrightarrow{b}$ in the proof system Res(lin$_{\mathbb{F}_q}$) where $char(\mathbb{F}_{q})\geq 5$. As a basis for the hardness criterion for such instances we choose the property of the matrix $A$ with columns $(\overrightarrow{a}_1, \ldots, \overrightarrow{a}_n)$ to be (the transpose of) the generating matrix for a good error-correcting code $C_{A} := \{x\cdot A\, |\, x \in \mathbb{F}_{q}^k\}\subset \mathbb{F}_{q}^n$ and prove the following lower bounds: 1) For a dag-like fragment of Res(lin$_{\mathbb{F}_q}$). We introduce the notion of $(s,r)$-robustness for Subset Sum instances, which in particular implies that $A$ defines an error-correcting code with the minimal distance $s\geq r$. For $(s,r)$-robust instances we prove $2^{\Omega(r)}$ lower bound for sizes of refutations in a dag-like fragment of Res(lin$_{\mathbb{F}_q}$). We show that random instances are $(n / 3, \Omega\left((n/(q + 1)\ln q))^{1/3}\right))$-robust and that specific examples achieving these bounds can be constructed using algebraic geometry codes. 2) For tree-like Res(lin$_{\mathbb{F}_q}$) refutations we show the size lower bound $2^{\Omega({((q+1)\ln q)^{-1/3}}d^{1/5})}$ for any Subset Sum instance where $d$ is the minimal distance of $C_{A}$.

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 lower bounds on refutation sizes for unsatisfiable vector Subset Sum instances in Res(lin_{F_q}) (char(F_q) >= 5). It introduces the (s,r)-robustness property for the matrix A (implying C_A is an error-correcting code with min distance s >= r), establishes a 2^Ω(r) size lower bound in a dag-like fragment of the system for (s,r)-robust instances, shows that random instances achieve (n/3, Ω((n/(q+1) ln q)^{1/3}))-robustness with matching algebraic-geometry code constructions, and derives a 2^Ω(((q+1) ln q)^{-1/3} d^{1/5}) lower bound for tree-like refutations in terms of the code distance d.

Significance. If the derivations hold, the work is significant for proof complexity: it supplies an explicit hardness criterion via robustness and coding parameters, yields exponential lower bounds with concrete dependence on r and d, and separates dag-like from tree-like fragments. The probabilistic argument for random instances and the AG-code constructions are notable strengths, as is the uniform derivation of the tree-like bound from distance alone.

minor comments (2)
  1. The definition of the dag-like fragment of Res(lin_{F_q}) (used for the 2^Ω(r) bound) should be stated explicitly in the main body with a comparison to the full system, as this is central to interpreting the result.
  2. Notation for the vector Subset Sum equation and the matrix A could be clarified with a running example early in the paper to aid readability of the robustness property.

Simulated Author's Rebuttal

0 responses · 0 unresolved

We thank the referee for the positive assessment and the recommendation of minor revision. The summary accurately captures the main contributions of the paper.

Circularity Check

0 steps flagged

No significant circularity; derivation self-contained

full rationale

The paper defines the (s,r)-robustness property for Subset Sum instances (which implies minimum distance s ≥ r for the associated code C_A) and derives the 2^Ω(r) dag-like lower bound and the tree-like bound in terms of d directly from this definition via explicit combinatorial and algebraic arguments on the proof system. Random instances are shown to satisfy the property with the stated parameters, and algebraic-geometry codes provide explicit constructions; neither the robustness definition nor the distance parameter is fitted inside the paper or reduced to a self-citation chain. All load-bearing steps rely on externally verifiable coding-theory notions and standard resolution lower-bound techniques rather than any of the enumerated circular patterns.

Axiom & Free-Parameter Ledger

0 free parameters · 2 axioms · 0 invented entities

The central claim rests on standard linear algebra over finite fields, the definition of error-correcting codes, and the newly introduced robustness property; no free parameters or invented entities are apparent from the abstract.

axioms (2)
  • domain assumption Finite fields F_q with char(F_q) >= 5 support the modular counting operations in the Res(lin) system.
    Explicitly stated as the setting for the proof system in the abstract.
  • domain assumption The matrix A generates a linear code C_A with the stated minimum distance properties when the instance is (s,r)-robust.
    Invoked as the basis for the hardness criterion.

pith-pipeline@v0.9.0 · 5877 in / 1396 out tokens · 29745 ms · 2026-05-24T12:05:25.379234+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

17 extracted references · 17 canonical work pages

  1. [1]

    The complexity of the pigeonhole princip le

    Mikl´ os Ajtai. The complexity of the pigeonhole princip le. In Proceedings of the IEEE 29th Annual Symposium on Foundations of Computer Science , pages 346–355, 1988

    work page 1988

  2. [2]

    Razborov

    Michael Alekhnovich and Alexander A. Razborov. Lower bo unds for polynomial calculus: Non-binomial case. In Proceedings of the 42nd Annual IEEE Symposium on Foundations of Computer Science (FOCS 2001) , pages 190–199, 2001

    work page 2001

  3. [3]

    A Lower Bound for Polynomial Calculu s with Extension Rule

    Yaroslav Alekseev. A Lower Bound for Polynomial Calculu s with Extension Rule. In Valentine Kabanets, editor, 36th Computational Complexity Conference (CCC 2021) , volume 200 of Leib- niz International Proceedings in Informatics (LIPIcs) , pages 21:1–21:18, Dagstuhl, Germany,

    work page 2021

  4. [4]

    Schloss Dagstuhl – Leibniz-Zentrum f¨ ur Informatik. 19

    work page

  5. [5]

    Hirsch, an d Iddo Tzameret

    Yaroslav Alekseev, Dima Grigoriev, Edward A. Hirsch, an d Iddo Tzameret. Semi-algebraic proofs, IPS lower bounds, and the τ-conjecture: can a natural number be negative? In Proccedings of the 52nd Annual ACM SIGACT Symposium on Theory of Co mputing, STOC 2020, Chicago, IL, USA, June 22-26, 2020 , pages 54–67. ACM, 2020

    work page 2020

  6. [6]

    Hard examples for the bounded depth Freg e proof system

    Eli Ben-Sasson. Hard examples for the bounded depth Freg e proof system. Comput. Complex- ity, 11(3-4):109–136, 2002

    work page 2002

  7. [7]

    O n the lengths of proofs in the propositional calculus (preliminary version)

    Stephen A. Cook and Robert A. Reckhow. Corrections for “O n the lengths of proofs in the propositional calculus (preliminary version)”. SIGACT News , 6(3):15–22, July 1974

    work page 1974

  8. [8]

    Cook and Robert A

    Stephen A. Cook and Robert A. Reckhow. On the lengths of pr oofs in the propositional calculus (preliminary version). In Proceedings of the 6th Annual ACM Symposium on Theory of Computing (STOC 1974) , pages 135–148, 1974. For corrections see Cook-Reckhow [6]

    work page 1974

  9. [9]

    Cook and Robert A

    Stephen A. Cook and Robert A. Reckhow. The relative efficie ncy of propositional proof sys- tems. J. Symb. Log. , 44(1):36–50, 1979. This is a journal-version of Cook-Reck how [7] and Reckhow [16]

    work page 1979

  10. [10]

    J. Hastad. On Small-Depth Frege Proofs for Tseitin for Gr ids. In 2017 IEEE 58th Annual Symposium on Foundations of Computer Science (FOCS) , pages 97–108, Los Alamitos, CA, USA, oct 2017. IEEE Computer Society

    work page 2017

  11. [11]

    Resolution over li near equations modulo two

    Dmitry Itsykson and Dmitry Sokolov. Resolution over li near equations modulo two. Ann. Pure Appl. Log., 171(1), 2020. Extended abstract appeared initially in MFC S 2014

    work page 2020

  12. [12]

    On proof complexity of resolution over p olynomial calculus

    Erfan Khaniki. On proof complexity of resolution over p olynomial calculus. manuscript, January 2021

    work page 2021

  13. [13]

    An expon ential lower bound to the size of bounded depth Frege proofs of the pigeonhole principle

    Jan Kraj ´ ıˇ cek, Pavel Pudl´ ak, and Alan Woods. An expon ential lower bound to the size of bounded depth Frege proofs of the pigeonhole principle. Random Structures Algorithms , 7(1):15–39, 1995

    work page 1995

  14. [14]

    Resolution with counting : Dag-like lower bounds and different moduli

    Fedor Part and Iddo Tzameret. Resolution with counting : Dag-like lower bounds and different moduli. To appear in 11th Innovations in Theoretical Computer Science Co nference (ITCS) 2020, January, 2020, Seattle, WA, USA , 2020

    work page 2020

  15. [15]

    Exponential lower bounds for the pigeonhole principle

    Toniann Pitassi, Paul Beame, and Russell Impagliazzo. Exponential lower bounds for the pigeonhole principle. Comput. Complexity , 3(2):97–140, 1993

    work page 1993

  16. [16]

    Resolution over linear equat ions and multilinear proofs

    Ran Raz and Iddo Tzameret. Resolution over linear equat ions and multilinear proofs. Ann. Pure Appl. Logic , 155(3):194–224, 2008

    work page 2008

  17. [17]

    Robert A. Reckhow. On the lengths of proofs in the propositional calculus . PhD thesis, Uni- versity of Toronto, 1976. 20

    work page 1976