Pseudorandom Generators, Resolution and Heavy Width

Following the paper of Alekhnovich, Ben-Sasson, Razborov, Wigderson [Michael Alekhnovich et al., 2004] we call a pseudorandom generator ℱ:{0, 1}ⁿ → {0, 1}^m hard for a propositional proof system P if P cannot efficiently prove the (properly encoded) statement b ∉ Im(ℱ) for any string b ∈ {0, 1}^m. In [Michael Alekhnovich et al., 2004] the authors suggested the "functional encoding" of the considered statement for Nisan-Wigderson generator that allows the introduction of "local" extension variables. These extension variables may potentially significantly increase the power of the proof system. In [Michael Alekhnovich et al., 2004] authors gave a lower bound of exp[Ω(n²/{m⋅2^{2^Δ}})] on the length of Resolution proofs where Δ is the degree of the dependency graph of the generator. This lower bound meets the barrier for the restriction technique. In this paper, we introduce a "heavy width" measure for Resolution that allows us to show a lower bound of exp[n²/{m 2^𝒪(εΔ)}] on the length of Resolution proofs of the considered statement for the Nisan-Wigderson generator. This gives an exponential lower bound up to Δ := log^{2 - δ} n (the bigger degree the more extension variables we can use). In [Michael Alekhnovich et al., 2004] authors left an open problem to get rid of scaling factor 2^{2^Δ}, it is a solution to this open problem.