For every n > 0, we show the existence of a CNF tautology over O(n^2) variables of width O(log n) such that it has a Polynomial Calculus Resolution refutation over {0, 1} variables of size O(n^3polylog(n)) but any Polynomial Calculus refutation over {+1, −1} variables requires size 2^Ω(n). This shows that Polynomial Calculus sizes over the {0, 1} and {+1, −1} bases are incomparable (since Tseitin tautologies show a separation in the other direction) and answers an open problem posed by Sokolov [Sok20] and Razborov.

 

Short Bio: Sasank Mouli is an Assistant Professor at IIT Indore. He completed his PhD at UC San Diego under the guidance of Russell Impagliazzo. He was briefly a postdoc at IDSIA, Lugano, Switzerland.