Pseudorandom Generators in Propositional Proof Complexity

We call a pseudorandom generator G/sub n/: {0, 1}/sup n//spl rarr/{0, 1}/sup m/ hard for a propositional proof system P if P can not efficiently prove the (properly encoded) statement G/sub n/(x/sub 1/, .. ., x/sub n/)/spl ne/b for any string b/spl epsiv/{0, 1}/sup m/. We consider a variety of "combinatorial" pseudorandom generators inspired by the Nisan-Wigderson generator on 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).

Authors

• Michael Alekhnovich
• Eli Ben-Sasson
• Alexander A. Razborov
• Avi Wigderson

Keywords

• Circuits
• Polynomials
• Calculus
• Computer science
• Computational complexity
• Proof Of Proposition
• Proof Complexity
• Propositional Proof Complexity
• Lower Bound
• Structure Of Matrix
• Inference Rules
• Function Generator
• Curing Conditions
• Complex Framework
• String Length
• Computational Point Of View
• Hypergraph
• Boolean Function
• Linear Encoder
• Classical Circuit
• Function Gi