A Framework for Space Complexity in Algebraic Proof Systems

作者：Bonacina Ilario^*; Galesi Nicola

来源：Journal of the ACM, 2015, 62(3): 23.

DOI：10.1145/2699438

• Theory
• Proof complexity
• space complexity
• algebraic proof systems
• polynomial calculus
• resolution
• random formulae

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 Omega(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.

• 出版日期2015-6