Abstract
A pseudorandom generator $G_n:\{0,1\}^n\to \{0,1\}^m$ is hard for a propositional proof system $P$ if (roughly speaking) $P$ cannot efficiently prove the statement $G_n(x_1,\ldots,x_n)\neq b$ for any string $b\in\{0,1\}^m$. We present a function ($m\geq 2^{n^{\Omega(1)}}$) generator which is hard for $\mathrm{Res}(\epsilon\log n)$; here $\mathrm{Res}(k)$ is the propositional proof system that extends Resolution by allowing $k$-DNFs instead of clauses.
As a direct consequence of this result, we show that whenever $t\geq n^2$, every $\mathrm{Res}(\epsilon\log t)$ proof of the principle $\neg \mathrm{Circuit}_t(f_n)$ (asserting that the circuit size of a Boolean function $f_n$ in $n$ variables is greater than $t$) must have size $\exp(t^{\Omega(1)})$. In particular, $\mathrm{Res}(\log \log N)$ ($N\sim 2^n$ is the overall number of propositional variables) does not possess efficient proofs of ${\bf NP}\not\subseteq {\bf P}/\mathrm{poly}$. Similar results hold also for the system PCR (the natural common extension of Polynomial Calculus and Resolution) when the characteristic of the ground field is different from 2.
As a byproduct, we also improve on the small restriction switching lemma due to Segerlind, Buss and Impagliazzo by removing a square root from the final bound. This in particular implies that the (moderately) weak pigeonhole principle $\mathrm{PHP}^{2n}_n$ is hard for $\mathrm{Res}(\epsilon\log n/\log\log n)$.
Full Article