Proceedings 41st Annual Symposium on Foundations of Computer Science (2000)

Redondo Beach, California

Nov. 12, 2000 to Nov. 14, 2000

ISSN: 0272-5428

ISBN: 0-7695-0850-2

pp: 43

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

ABSTRACT

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

CITATION

A. Razborov, E. Ben-Sasson, A. Wigderson and M. Alekhnovich, "Pseudorandom generators in propositional proof complexity,"

*Proceedings 41st Annual Symposium on Foundations of Computer Science(FOCS)*, Redondo Beach, California, 2000, pp. 43.

doi:10.1109/SFCS.2000.892064

CITATIONS

SEARCH