Proof complexity generators hidden inside demi-bits generators revealed
Many Proof Complexity Generators Inside One Demi-Bits Generator
Computational ComplexityLogic in Computer Science
Summary
This paper explores special mathematical functions called generators that produce complicated outputs related to logical proofs. The authors show that a weaker type of generator, called a demi-bits generator, actually contains many stronger generators known as proof complexity generators within it. They prove this surprising fact using an existing combinatorial lemma, Pajor's Lemma. Their findings help demonstrate new challenges involved in certain problems about avoiding outputs of these functions in restricted settings.
What this means in practice
- •For proof system designers: Assess new hardness results for avoiding outputs in restricted logical proof systems using embedded proof complexity generators.
- •For circuit complexity engineers: Use zero-error disperser families computable by projections to develop complexity-theoretic tools with minimal circuit overhead.
A theory result. No direct application yet.
Authors
Xin Li, Hanlin Ren, Yan Zhong
Abstract
For a propositional proof system $\mathcal{P}$ and a polynomial-time function $G: \{0, 1\}^n \to \{0, 1\}^N$ ($N > 10n$), we say that $G$ is a *proof complexity generator* against $\mathcal{P}$ if $\mathcal{P}$ cannot efficiently prove the (suitably encoded) statement "$y\not\in\mathrm{Range}(G)$" for every $y \in \{0, 1\}^N$, and $G$ is a *demi-bits generator* against $\mathcal{P}$ if $\mathcal{P}$ cannot efficiently prove the statement "$y \not\in\mathrm{Range}(G)$" for a noticeable fraction of $y \in \{0, 1\}^N$. As can be seen from the definitions, proof complexity generators are qualitatively stronger objects than demi-bits generators. Our main result is that, perhaps counter-intuitively, every demi-bits generator "contains" exponentially many proof complexity generators. In fact, a random subset of output bits of a demi-bits generator forms a proof complexity generator with constant probability. This result is an extremely simple corollary of Pajor's Lemma (a strengthening of the well-known Sauer--Shelah Lemma). This result allows us to exhibit the hardness of the Range Avoidance problem ($\text{Avoid}$) in several new, restricted settings of interest. Along the way, we introduce the notion of *zero-error disperser families* that can transform demi-bits generators into proof complexity generators, and show that this family can be computed by projections (i.e., without any circuit complexity overhead). Using a different instantiation of this family, we construct proof complexity generators from *barely non-trivial* demi-bits generators $G: \{0, 1\}^n \to \{0, 1\}^N$, where the number of hard-to-prove statements of the form "$y \not \in \mathrm{Range}(G)$" just slightly exceeds $2^n$ (which is the number of *false* statements of this form).