Superpolynomial Length Lower Bounds for Tree-Like Semantic Proof Systems with Bounded Line Size

Abstract

We prove superpolynomial length lower bounds for the semantic tree-like Frege refutation system with bounded line size. Concretely, for any function $n^{2-\epsilon }\le s(n)\le 2^{n^{1-\epsilon }}$ we exhibit an explicit family $\mathcal{A}$ of $n$-variate CNF formulas $A$, each of size $|A|\le s(n{)}^{1+\epsilon }$, such that if $A$ is chosen uniformly from $\mathcal{A}$, then asymptotically almost surely any tree-like Frege refutation of $A$ in line-size $s(n)$ is of length super-polynomial in $|A|$. Our lower bounds apply also to tree-like degree-$d$ threshold systems, for $d\approx \log (s(n))$, that is, for $d$ up to $n^{1-\epsilon }$. More generally, our lower bounds apply to the semantic version of these systems and to any semantic tree-like proof system where the number of distinct lines is bounded by $\exp (s(n))$.