In standard implementations of the Gröbner basis algorithm, the original polynomials are homogenized so that each term in a given polynomial has the same degree. In this paper, we study the effect of homogenization on the proof complexity of refutations of polynomials derived from Boolean formulas in both the Polynomial Calculus (PC) and Nullstellensatz systems. We show that the PC refutations of homogenized formulas give crucial information about the complexity of the original formulas. The minimum PC refutation degree of homogenized formulas is equal to the Nullstellensatz refutation degree of the original formulas, whereas the size of the homogenized PC refutation is equal to the size of the PC refutation for the originals. Using this relationship, we prove nearly linear (Ω(n/logn) vs. O(1)) separations between Nullstellensatz and PC degree, for a family of explicitly constructed contradictory 3CNF formulas. Previously, a Ω(n1/2) separation had been proved for equations that did not correspond to any CNF formulas, and a log n separation for equations derived from kCNF formulas.
CITATION STYLE
Buresh-Oppenheim, J., Pitassi, T., Clegg, M., & Impagliazzo, R. (2000). Homogenization and the polynomial calculus. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 1853, pp. 926–938). Springer Verlag. https://doi.org/10.1007/3-540-45022-x_78
Mendeley helps you to discover research relevant for your work.