Polynomial Calculus sizes over the Boolean and Fourier bases are incomparable

2024/03/06 by Sasank Mouli, Mouli, Sasank
Computer Science · Engineering · #Advanced Numerical Analysis Techniques #Computational Complexity (cs.CC) #FOS: Computer and information sciences #FOS: Mathematics #Logic (math.LO) #Polynomial and algebraic computation

paper · pdf · doi:10.48550/arxiv.2403.03933

openalex publication_date 2024/03/06 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28

Abstract

For every n >0, we show the existence of a CNF tautology over O(n²) variables of width O(log n) such that it has a Polynomial Calculus Resolution refutation over \0,1\ variables of size O(n³polylog(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.

Related

• A Generalized Method for Proving Polynomial Calculus Degree Lower Bounds
• Narrow Proofs May Be Maximally Long
• A Lower Bound for Polynomial Calculus with Extension Rule
• From Small Space to Small Width in Resolution
• Characterizing Propositional Proofs as Non-Commutative Formulas