Title
A Framework for Space Complexity in Algebraic Proof Systems
Abstract
Algebraic proof systems, such as Polynomial Calculus (PC) and Polynomial Calculus with Resolution (PCR), refute contradictions using polynomials. Space complexity for such systems measures the number of distinct monomials to be kept in memory while verifying a proof. We introduce a new combinatorial framework for proving space lower bounds in algebraic proof systems. As an immediate application, we obtain the space lower bounds previously provided for PC/PCR [Alekhnovich et al. 2002; Filmus et al. 2012]. More importantly, using our approach in its full potential, we prove Ω(n) space lower bounds in PC/PCR for random k-CNFs (k≥ 4) in n variables, thus solving an open problem posed in Alekhnovich et al. [2002] and Filmus et al. [2012]. Our method also applies to the Graph Pigeonhole Principle, which is a variant of the Pigeonhole Principle defined over a constant (left) degree expander graph.
Year
DOI
Venue
2015
10.1145/2699438
Journal of the ACM
Keywords
Field
DocType
Theory,Proof complexity,space complexity,algebraic proof systems,polynomial calculus,resolution,random formulae
Discrete mathematics,Combinatorics,Open problem,Algebraic number,Expander graph,Polynomial,Proof complexity,Monomial,Polynomial calculus,Mathematics,Pigeonhole principle
Journal
Volume
Issue
ISSN
62
3
0004-5411
Citations 
PageRank 
References 
6
0.42
24
Authors
2
Name
Order
Citations
PageRank
Ilario Bonacina1586.49
Nicola Galesi236728.05