Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Polynomial Calculus sizes over the Boolean and Fourier bases are incomparable

Sasank Mouli

TL;DR

The paper resolves an open question by showing that Polynomial Calculus (PC) sizes over the Boolean basis and the Fourier basis are incomparable. It constructs an $O(n^2)$-variable CNF tautology with width $O(\log n)$ that admits PCR refutations of size $O(n^3\,\mathrm{polylog}(n))$ over $\{0,1\}$ but requires PC refutations of size $2^{\Omega(n)}$ over $\{+1,-1\}$, thereby separating the two bases. The construction relies on an OR-lifted version of the Linear/Ordering Principle via $LOP_n$ and $BOP_n$, augmented with gadget lifts and the Split operation, to enable small PCR proofs while forcing high PC complexity in the Fourier basis. A central technical contribution is a special-degree lower bound for PC proofs of the lifted $BOP^{\vee}_{\ell,n}$ tautologies, established through a linear-operator framework and a probabilistic gadget-clustering argument. Together, these results answer Sokolov’s open problem and illuminate fundamental limits of base-change arguments in PC/PCR proof systems.

Abstract

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.

Polynomial Calculus sizes over the Boolean and Fourier bases are incomparable

TL;DR

The paper resolves an open question by showing that Polynomial Calculus (PC) sizes over the Boolean basis and the Fourier basis are incomparable. It constructs an -variable CNF tautology with width that admits PCR refutations of size over but requires PC refutations of size over , thereby separating the two bases. The construction relies on an OR-lifted version of the Linear/Ordering Principle via and , augmented with gadget lifts and the Split operation, to enable small PCR proofs while forcing high PC complexity in the Fourier basis. A central technical contribution is a special-degree lower bound for PC proofs of the lifted tautologies, established through a linear-operator framework and a probabilistic gadget-clustering argument. Together, these results answer Sokolov’s open problem and illuminate fundamental limits of base-change arguments in PC/PCR proof systems.

Abstract

For every , we show the existence of a CNF tautology over variables of width such that it has a Polynomial Calculus Resolution refutation over variables of size but any Polynomial Calculus refutation over variables requires size . This shows that Polynomial Calculus sizes over the and bases are incomparable (since Tseitin tautologies show a separation in the other direction) and answers an open problem posed by Sokolov [Sok20] and Razborov.
Paper Structure (11 sections, 16 theorems, 13 equations)

This paper contains 11 sections, 16 theorems, 13 equations.

Table of Contents

  1. Introduction
  2. Preliminaries
  3. Proof of the main theorem
  4. The tautology
  5. Proof of the special degree lower bound
  6. Preliminaries
  7. Proof of the special degree lower bound
  8. 1.
  9. 2.
  10. 3.
  11. Proof of Sokolov's low Quadratic degree to low degree lemma

Key Result

Theorem 1

For any $n >0$, there exists a CNF tautology over $O(n^2)$ variables of width $O(\log n)$ which has PCR proofs of size $O(n^3\polylog(n))$ over $\{0,1\}$ but requires PC proofs of size $2^{\Omega(n)}$ over $\{+1,-1\}$.

Theorems & Definitions (37)

  • Theorem 1
  • Definition 1: Polynomial Calculus/Polynomial Calculus Resolution
  • Definition 2: Quadratic set, Quadratic degree, Quadratic terms over $\pm 1$; taken from sok20, Section 3.2
  • Definition 3: $\textrm{Split}$ operation over $x$ sok20, Section 5.4
  • Lemma 1: sok20
  • proof
  • Lemma 2: sok20
  • proof
  • Lemma 3: sok20, Lemma 3.6
  • Definition 4: Linear Ordering Principle, $LOP_n$
  • ...and 27 more