A Lower Bound for Polynomial Calculus with Extension Rule

2020/10/12 by Alekseev, Yaroslav · 1 citation
#Computational Complexity (cs.CC) #FOS: Computer and information sciences

paper · doi:10.48550/arxiv.2010.05660

Abstract

In this paper we study an extension of the Polynomial Calculus proof system where we can introduce new variables and take a square root. We prove that an instance of the subset-sum principle, the binary value principle, requires refutations of exponential bit size over rationals in this system. Part and Tzameret proved an exponential lower bound on the size of Res-Lin (Resolution over linear equations) refutations of the binary value principle. We show that our system p-simulates Res-Lin and thus we get an alternative exponential lower bound for the size of Res-Lin refutations of the binary value principle.

Cited by

• Lower Bounds against the Ideal Proof System in Finite Fields

Related

• The power of the Binary Value Principle
• Resolution with Counting: Dag-Like Lower Bounds and Different Moduli
• Monomial-size vs. Bit-complexity in Sums-of-Squares and Polynomial\n Calculus
• A Generalized Method for Proving Polynomial Calculus Degree Lower Bounds
• Exponential Separation Between Powers of Regular and General Resolution Over Parities