Autumn 2007

Propositional proof complexity studies the lengths of proofs in propositional logic. It is an area that is related to major open questions of computational complexity theory and to practical properties of automated theorem provers such as satisfiability checkers. Moreover, connections between proof complexity and circuit complexity have been discovered and concepts and techniques in proof complexity have contributed to several other areas of computer science, including cryptography, automated reasoning and AI, complexity of search classes within NP, the analysis of heuristics and algorithms for NP-hard problems, and bounded arithmetic.

In the course we cover fundamentals of propositional proof complexity and some interesting connections with the other areas.

General Information

• Lectures and seminars: Prof. Ilkka Niemelä, Mondays, 16-20, room TB353
• The course starts on Mon Sep 17 at 16.30 o'clock in TB353.
• Material:
  Clote, Peter and Kranakis, Evangelos: Boolean Functions and Computation Models. Springer 2002, ISBN: 978-3-540-59436-9. Link to Springer page
  Articles.
• The course is taken by giving seminar talks.
• Brochure for the course.
• Slides for introduction to the course (including practical arrangements and grading).
• Assessment form for seminar talks [pdf]
  An ASCII version of the assessment form that can be used for email submissions of the assessments [txt]
• Tentative seminar program

Course Feedback

We welcome feedback which is collected centrally in Finnish, Swedish, and English. The questionnaire is open from December 10 to January 7, 2008.

Seminar Presentations

• 08.10.2007
  Sections 5.1-5.3 (pp. 247-257) Petri Savola [PDF]
  Sections 5.3.1-5.3.3 (pp. 257-268) Antti Hyvärinen [PDF]
  
• 15.10.2007
  Sections 5.4-5.4.2 (pp. 268-279) Matti Järvisalo
  Sections 5.4.2-5.4.3 (pp. 279-291) Leo Bhebhe [PDF]
• 22.10.2007
  Sections 5.4.4-5.4.5 (pp. 291-300) Jori Dubrovin [PDF]
  Sections 5.4.6-5.5 (pp. 300-308) Siert Wieringa [PDF]
  
• 5.11.2007
  Sections 5.5.1 (pp. 308-316) Siert Wieringa [PDF]
  Sections 5.5.2-5.5.3 (pp. 316-326) Leo Bhebhe [PDF]
  
• 12.11.2007
  Sections 5.5.4-5.5.5 (pp. 326-337) Jori Dubrovin [PDF]
  Sections 5.5.6-5.6.1 (pp. 337-348) Emilia Oikarinen
• 19.11.2007
  Sections 5.6.2-5.6.4 (pp. 348-359) Petri Savola [PDF]
  Sections 5.6.5-5.6.6 (pp. 359-370) Antti Hyvärinen [PDF]
  

Related Material

• Paul Beame's Proof Complexity Lecture Notes [ps]
• Jan Krajicek's Lecture Notes: Propositional proof complexity I. [ps]
• Toniann Pitassi's Proof Complexity course home page [Link]
• Nicola Galesi's Proof Complexity course home page [Link]
• Proof Complexity Survey by Nathan Segerlind [pdf]
• Paul Beame: Satisfiability and Unsatisfiability: Proof Complexity and Algorithms, Invited talk at SAT 05, St. Andrews, June 2005. [ppt]