A Lower Bound for Polynomial Calculus with Extension Rule
Computational Complexity
2020-10-13 v1
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.
Keywords
Cite
@article{arxiv.2010.05660,
title = {A Lower Bound for Polynomial Calculus with Extension Rule},
author = {Yaroslav Alekseev},
journal= {arXiv preprint arXiv:2010.05660},
year = {2020}
}