This Article 
 Bibliographic References 
 Add to: 
41st Annual Symposium on Foundations of Computer Science
Pseudorandom generators in propositional proof complexity
Redondo Beach, California
November 12-November 14
ISBN: 0-7695-0850-2
M. Alekhnovich, Moscow State Univ., Russia
E. Ben-Sasson, Moscow State Univ., Russia
A.A. Razborov, Moscow State Univ., Russia
A. Wigderson, Moscow State Univ., Russia
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).
Index Terms:
theorem proving; computational complexity; process algebra; random processes; pseudorandom generators; propositional proof complexity; combinatorial pseudorandom generators; Nisan-Wigderson generator; Tseitin tautologies; resolution; polynomial calculus with resolution; polynomial calculus
M. Alekhnovich, E. Ben-Sasson, A.A. Razborov, A. Wigderson, "Pseudorandom generators in propositional proof complexity," focs, pp.43, 41st Annual Symposium on Foundations of Computer Science, 2000
Usage of this product signifies your acceptance of the Terms of Use.