Joint Advanced Student School - JASS'2009

Propositional Proof  Complexity

St. Petersburg, 29.3 - 7.4. 2009


Within the scope of the "Joint Advanced Student School -  JASS'2009" in St. Petersburg (March 29 - April 7), we offer the course  "Propositional Proof Complexity".

Directors:


Prof. Dr. E. Hirsch (Steklov Institute, St. Petersburg)

Prof. Dr. E. W. Mayr (TU München)

 

Assistants:


D. Chibisov
D. Itsykson



Application:


The course addresses highly motivated and interested students. Active preparation and contribution of the participants will be required. The course language is English. Expenses for travel, board and lodging of german participants are covered by the school.

 

Application deadline for GERMAN applicants: February 10, 2009 (extended). 

Application form: PDF .

 

German applicants should send their applications to D. Chibisov.
Russian applicants should send their applications to Prof. Dr. E. Hirsch

 

Course Description:


Proof complexity studies the length of proofs in propositional logic and  is closely related to open questions in the computational complexity theory as well as to practical applications of automated theorem proving. The course is devoted, besides the fundamentals of  proof theory, to complexity theoretic considerations of different proof calculi (like resolution, cutting planes,  and algebraic proofs). Additionally, the connections between proof complexity and communication complexity will be considered as well as applications of  proof complexity in areas like pseudorandom number generators or crpytography will be discussed.

Organization:


Every participant is expected to give a talk and to prepare a paper on the topic of his/her talk. Some help is provided on the organizational stuff page



Talks
 german

russian



Stefan Kunkel

Introduction: P, NP, coNP, NP-completeness, propositional proof systems, simulations and separations.  Examples: Frege, resolution, Nullstellensatz, polynomial calculus.  

Literature: [Bu,AB/Pap,Pu1,Pu2]


Michael Herrmann

Equivalence of Frege systems; treelike Frege systems; Gentzen calculus.Extended Frege, equivalence to extended resolution. Upper bound for PHP in Extended Frege and Frege.

Literature: [Bu]



Maximilian Schlund, Mykola Protsenko

Width-based lower bounds for resolution and polynomial calculus: PHP, Tseytin formulas.

Literature: [BSW,BIKP,CEI]


Alisa Knizel

Razborov's theorem, interpolation method, and lower bounds for Resolution and Cutting Planes.

Literature:[Pap, Pu3, AB]


Sergey Nurk

Lower bounds for Res-k.

Literature: [A, ABE, AB2]


Alexander Glazman

Switching lemma.

Literature: ...

Ivan Monakhov

Lower bounds for bounded depth Frege systems.


Literature:[BS, BSH]


Tobias Lieber

Automatisation (Grobner bases and width-based) and non-automatisability.

Literature: [BSW,AR,CEI,AB2]




Dmitry Antipov

Optimal proof systems and disjoint NP pairs.

Literature: ...

Markus Latte

Pseudorandom generators hard for propositional proof systems.

Literature: [ABR,Raz]




Grigory Yaroslavtsev

Lower bounds using communication complexity.

Literature: [BP, ... ]



Literature:

[A] Alekhnovich, M.: Lower bounds for k-DNF resolution on random 3-CNFs. In: STOC'05: Proceedings of the thirty-seventh annual ACM symposium on
Theory of computing, New York, NY, USA, ACM Press (2005) 251-256


[AB] S. Arora and B. Barak [draft of their new book]
Atserias, A., Bonet, M.L., Esteban, J.L.: Lower bounds for the weak pigeonhole principle and random formulas beyond resolution. Information and Computation 176(2) (2002) 136-152

[AB2] A. Atserias and M. L. Bonet. On the Automatizability of Resolution and Related Propositional Proof Systems, Information and Computation, 189(2), pages 182-201, 2004.

[ABE] Atserias, A., Bonet, M.L., Esteban, J.L.: Lower bounds for the weak pigeonhole principle and random formulas beyond resolution. Information and Computation 176(2) (2002) 136-152

[ABR] M. Alekhnovich, E. Ben-Sasson, A. Razborov. Pseudorandom Generators In Propositional Proof Complexity. FOCS-2000.

[AR] M. Alekhnovich, A.A. Razborov. Resolution is not automatizable unless W[P] is not tractable. Proceedings of the 42nd IEEE Symposium on Foundations of Computer Science.

[BIKP] P. Beame, R. Impagliazzo, J. Krajicek, T. Pitassi, Lower bounds on Hilbert's Nullstellensatz and propositional proofs. Foundations of Computer Science, 1994.

[BS] E. Ben-Sasson. Hard Examples for Bounded Depth Frege Proceedings of the 34th Annual {ACM} Symposium on Theory of Computing, STOC02, 563--572, 2002.

[BSH] E. Ben-Sasson, P. Harsha. Lower Bounds for Bounded Depth Frege Proofs via Buss-Pudlak Games ECCC Report TR03-004, 2003.

[BSW] E. Ben-Sasson and A. Wigderson. Short proofs are narrow - Resolution made simple. Journal of ACM, 48(2):149-169, 2001.

[Bu] S. Buss. An Introduction to Proof Theory.In Handbook of Proof Theory, Elsevier, 1--78, 1998.
*or*
Propositional Proof Complexity: An Introduction. NATO Summer School, Marktoberdorf, Germany, 1997.
ftp://euclid.ucsd.edu/pub/sbuss/research/marktoberdorf97.ps

[CEI] M. Clegg, J. Edmonds, R. Impagliazzo. Using the Groebner basis algorithm to find proofs of unsatisfiability. STOC 96, 174-183.

[Pap] C. Papadimitriou, Computational Complexity, Addison-Wesley, 1994.

[Pu1] P. Pudlak [draft of his new book]

[Pu2] P. Pudlak. On the complexity of the propositional calculus. Sets and Proofs: Invited papers from Logic Colloquium'97, Cambridge
University Press, 197--218, 1999

[Pu3] P. Pudlak. Lower bounds for resolution and cutting plane proofs and monotone computations. Journal of Symbolic Logic, 62(3):981-998, 1997.

[Raz] A. Razborov. Pseudorandom Generators hard for k-DNF Resolution and Polynomial Calculus. Manuscript. Availalble at the Author's web
page, 2003

[SBI] N. Segerlind, S. Buss, R. Impagliazzo: A Switching Lemma for Small Restrictions and Lower Bounds for k-DNF Resolution. SIAM
Journal on Computing 33(5) (2004) 1171-1200