加载中…
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 over 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.

生成讲解博客的中文版本

生成AI智能校验的中文版本