Lower Bounds for Subset Sum in Resolution with Modular Counting
Fedor Part

TL;DR
This paper establishes exponential lower bounds on the size of refutations for unsatisfiable Subset Sum instances in a modular resolution proof system, linking complexity to error-correcting code properties.
Contribution
It introduces robustness-based criteria for Subset Sum instances and proves new exponential lower bounds for both dag-like and tree-like Res(lin) refutations.
Findings
Random instances are robust with high minimal distance
Lower bounds depend on the minimal distance of associated error-correcting codes
Specific algebraic geometry codes can achieve the robustness bounds
Abstract
In this paper we prove lower bounds for sizes of refutations of unsatisfiable vector Subset Sum instances in the proof system Res(lin) where . As a basis for the hardness criterion for such instances we choose the property of the matrix with columns to be (the transpose of) the generating matrix for a good error-correcting code and prove the following lower bounds: 1) For a dag-like fragment of Res(lin). We introduce the notion of -robustness for Subset Sum instances, which in particular implies that defines an error-correcting code with the minimal distance . For -robust instances…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
