Lower Bounds for Subset Sum in Resolution with Modular Counting

TL;DR

The paper addresses exponential lower bounds for refutations of unsatisfiable linear-system instances $A\cdot x = b$ over $\mathbb{F}_q$ in the proof system $\mathsf{Res(lin_{\mathbb{F}_q})}$ with $\operatorname{char}(\mathbb{F}_q) \ge 5$. It introduces the hardness criterion of $(s,r)$-robustness tied to the distance of the code generated by $A$, and analyzes dag-like and tree-like fragments (notably $\mathsf{BinRegDags}_{\mathbb{F}_q}$, $\mathsf{BinDags}_{\mathbb{F}_q}$, and $\mathsf{LinDags}_{\mathbb{F}_q}$) through dynamic-programming techniques and code-based constructions. The main results show a $2^{\Omega(r)}$ lower bound for dag-like refutations on $(s,r)$-robust instances, with random matrices achieving robustness and explicit constructions via algebraic-geometry codes; a tree-like lower bound of $2^{\Omega(((q+1)\ln q)^{-1/3}\, d^{1/5})}$ in terms of the minimal distance $d$ of $C_A$; and a framework connecting proof complexity bounds to coding theory criteria. These findings broaden understanding of Res(lin) fragments and establish concrete hardness criteria for linear-system refutations, linking combinatorial linear-algebraic properties with proof-size lower bounds.

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^{Ω(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, Ω\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^{Ω({((q+1)\ln q)^{-1/3}}d^{1/5})}$ for any Subset Sum instance where $d$ is the minimal distance of $C_{A}$.

Theorems & Definitions (1)

• Definition : Definition \ref{['binDagsDef']}