Pseudorandom Generators in Propositional Proof Complexity
Michael Alekhnovich, Eli Ben‐Sasson, Alexander Alexandrovich Razborov, Avi Wigderson · SIAM Journal on Computing · 2004
We call a pseudorandom generator $G_n:\{0,1\}^n\to \{0,1\}^m$ hard for a propositional proof system P if P cannot efficiently prove the (properly encoded) statement $G_n(x_1,\ldots,x_n) eq b$ for any string $b\in\{0,1\}^m$. We consider a variety of "combinatorial" pseudorandom generators inspired by the Nisan--Wigderson generator on the one hand, and by the construction of Tseitin tautologies on the other. We prove that under certain circumstances these generators are hard for such proof systems as resolution, polynomial calculus, and polynomial calculus with resolution (PCR).