English

Polynomial Calculus sizes over the Boolean and Fourier bases are incomparable

Computational Complexity 2024-07-02 v3 Logic

Abstract

For every n>0n >0, we show the existence of a CNF tautology over O(n2)O(n^2) variables of width O(logn)O(\log n) such that it has a Polynomial Calculus Resolution refutation over {0,1}\{0,1\} variables of size O(n3polylog(n))O(n^3polylog(n)) but any Polynomial Calculus refutation over {+1,1}\{+1,-1\} variables requires size 2Ω(n)2^{\Omega(n)}. This shows that Polynomial Calculus sizes over the {0,1}\{0,1\} and {+1,1}\{+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.

Keywords

Cite

@article{arxiv.2403.03933,
  title  = {Polynomial Calculus sizes over the Boolean and Fourier bases are incomparable},
  author = {Sasank Mouli},
  journal= {arXiv preprint arXiv:2403.03933},
  year   = {2024}
}