2021 36th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)
Download PDF

Abstract

In this paper we consider the relationship between monomial-size and bit-complexity in Sums-of-Squares (SOS) in Polynomial Calculus Resolution over rationals (PCR/ℚ). We show that there is a set of polynomial constraints Qnover Boolean variables that has both SOS and PCR/ℚ refutations of degree 2 and thus with only polynomially many monomials, but for which any SOS or PCR/ℚ refutation must have exponential bit-complexity, when the rational coefficients are represented with their reduced fractions written in binary.
Like what you’re reading?
Already a member?
Get this article FREE with a new membership!

Related Articles