bild
School of
Computer Science
and Communication
KTH / CSC / Courses / DD2442 / DD2442 Autumn 2016

DD2442/DD3343 Seminars on Theoretical Computer Science Autumn 2016: Proof Complexity

Follow these shortcut links to go directly to course news, short overview of course, schedule, course material (with scribe notes), list of problem sets, or links to other courses.

Go to the separate administrative information page to find information about instructors, prerequisites, registration, learning outcomes, examination, problem sets in general (with a description of the peer evaluation process), and scribing of lectures.

These webpages provide all documentation and information about the course, so there is no separate course memo ("kurs-PM") PDF file.

Course News

  • Solutions to problem set 3 have now been sent out for peer evaluation. The peer evaluations are due Friday February 10 at at 12 noon.
  • As usual, there will also be a discussion phase for pset 3 at Piazza, which will tentatively start sometime this coming Wednesday. So stay tuned…
  • The lectures are over.

Short Overview of Course

Very simply put, proof complexity can be said to be the study of how to provide a short and efficiently verifiable certificate of the fact that a given propositional logic formula (typically in conjunctive normal form, or CNF) is unsatisfiable. Note that for satisfiable formulas there are very succinct certificates—just list a satisfying assignment—but for unsatisfiable formulas it is not quite clear what to do.

It is widely believed that it is not possible in general to give short certificates for unsatisfiable formulas, which if proven would imply PNP. One important research direction in proof complexity is to approach this distant goal by establishing lower bounds for stronger and stronger proof systems.

Another reason to study proof complexity is that any algorithm for the satisfiability problem (a so-called SAT solver) uses some method of reasoning for deciding whether a formula is satisfiable or unsatisfiable. Studying the proof systems corresponding to these methods of reasoning and proving upper and lower bounds for them tells us something about the potential and limitations of such SAT solvers.

This course will have a bias towards the first reason above, and will therefore focus on the strongest proof systems for which it is currently known how to prove (at least some) lower bounds. After a brief introduction to proof complexity, we will survey some recent research in the area and present some of many problems that still remain open. While the intention is to give a fairly broad coverage, there will probably be a certain tilt towards topics which are of particular interest in the context of the research conducted at the Theory Group at KTH, which has one of the largest research groups in proof complexity in the world today.

Schedule and Course Contents

This course was given in periods 1-2 in the autumn of 2016. We had a total of 24 lectures, with 2 lectures per week on average. In accordance with the academic quarter tradition at KTH, 10 am in the schedule actually means 10:15 am et cetera. See the list of rooms at KTH to locate the different lecture rooms.

 Weekday Date Time Room Plan of lectures References
 Monday Sep 5 10-12 1537 1. Introduction to proof complexity slides
 Wednesday Sep 7 13-15 4523 2. Resolution: Pigeonhole principle lower bound [Hak85], [Pud00], notes
 Monday Sep 12 10-12 1537 3. Resolution: Tseitin lower bound [Urq87], notes
 Wednesday Sep 14 13-15 4423 4. Interpolation; resolution lower bound for clique-colouring formulas [Pud97], notes
 Monday Sep 19 10-12 1537 5. Marc Vinyals: Cutting planes: Clique-colouring lower bound [Pud97], notes
 Wednesday Sep 21 13-15 4523 6. Marc Vinyals: Real monotone circuit lower bound for clique [Pud97], notes
 Monday Sep 26 10-12 1537 7. Bounded-depth Frege, k-DNF resolution, and random restrictions [SBI04], notes
 Wednesday Sep 28 13-15 4523 8. k-DNF resolution: Switching lemma; from shallow trees to resolution [SBI04], notes
 Monday Oct 3 10-12 1537 9. k-DNF resolution: Switching lemma continued [SBI04], notes
 Wednesday Oct 5 13-15 4523 10. k-DNF resolution: Pigeonhole principle lower bound [SBI04], notes
 Monday Oct 10 10-12 1537 11. k-DNF resolution: Random 3-CNF lower bound I [Ale11], notes
 Wednesday Oct 12 13-15 4523 12. k-DNF resolution: Random 3-CNF lower bound II [Ale11], notes
 Monday Oct 31 10-12 1537 13. Bounded-depth Frege: Pigeonhole principle lower bound I [KPW95], [PBI93], notes
 Wednesday Nov 2 13-15 4523 14. Bounded-depth Frege: Pigeonhole principle lower bound II [UF96], notes
 Monday Nov 7 10-12 1537 15. Bounded-depth Frege: Pigeonhole principle lower bound III [UF96], notes
 Wednesday Nov 9 14-16 4523 16. Bounded-depth Frege: Pigeonhole principle lower bound IV [UF96], notes
 Monday Nov 14 10-12 1537 17. Johan Håstad: Switching lemmas I notes for Johan's lectures
 Wednesday Nov 16 13-15 4523 18. Johan Håstad: Switching lemmas II
 Monday Nov 21 10-12 1537 19. Johan Håstad: Switching lemmas III
 Wednesday Nov 23 13-15 4523 20. Pavel Pudlák: Open problems and challenges in proof complexity
 Monday Nov 28 10-12 1537 21. Bounded-depth Frege: Overview of Tseitin lower bound [PRST16], notes
 Wednesday Nov 30 13-15 4523 22. Non-automatizability I [AR08], notes
 Monday Dec 5 9:45-11:30 1537 23. Non-automatizability II [AR08], notes
 Wednesday Dec 7 13-15 4523 24. Non-automatizability III; wrap-up of course [AR08], notes

Course Material

Textbook(s)

Unfortunately, there is no textbook that gets even close to covering the material in this course. Some of the material that we will discuss can also be found in the book Boolean Functions and Computation Models by Peter Clote and Evangelos Kranakis, but there will not be enough overlap to make it an officially recommended textbook for the course.

Surveys

Some survey papers on proof complexity, listed in roughly reverse chronological order, are:

Research Articles

Most of the course will be based on research articles. Below follows a list of links to these articles.

The intention is that the lectures will cover the material in the papers that we need, so students are not required to read these papers—the references are provided for completeness and for students interested in further reading. However, for students interested in learning more, it should be noted that many of the proofs given in class are actually not those found in the papers, and more recent survey papers of an area are likely to be better reads than the original research articles. Please do not hesitate to contact the instructors if you are interested in specific references for some specific area.

Note that if you are not at KTH, or if you are connected to the KTH network via wireless, then you might not be able to access the PDF files with the articles linked to below. One way around this problem is to search for the titles of the papers in your favourite search engine—this should hopefully help you find free versions of the same papers on the webpages of the authors or similar. Another, often better, solution to this problem (courtesy of Lars Arvestad) is to invoke the KTH library proxy server directly in the address field of the browser. You do this by adding .focus.lib.kth.se to the domain of the web address where you found the paper in question, which will work if the KTH library has a subscription (this is usually the case). For instance, if you want to look at http://www.journal.com/somepaper.html but this paper is behind a pay-wall, you try to change the URL to http://www.journal.com.focus.lib.kth.se/somepaper.html. Supposing that the KTH library is paying for the journal in question, this should take you to the paper via a login page for your KTH account.

Scribe Notes for the Lectures

Links to scribe notes will be added below as they become available.

Please see also the instructions for scribing and the sign-up sheet.

Please note that these scribe notes are provided "as is" without warranty of any kind, either expressed or implied, including, but not limited to, the implied warranties of merchantability and fitness for a particular purpose. Having said that, the notes are of course intended to be as useful and correct as possible, so if you notice any errors or have any other suggestions for improvements (regardless of whether you are taking the course or just happen to visit this webpage), please do not hesitate to send a message to jakobn at kth dot se.

List of Problem Sets

Please note that dates for future problem sets are not completely, irrevocably, 100% fixed. The actual deadlines are somewhat configurable, and can be discussed in class. The important thing is that we all agree on the deadlines beforehand, and that once they are set we stick to them without exceptions.

  • Problem set 1 (last updated on September 21, 2016): Deadline Wednesday September 28. Peer evaluation due Friday October 7 at 12 noon.
  • Problem set 2 (last updated on October 30, 2016): Deadline Monday October 31. Peer evaluation due Friday November 11 at 12 noon.
  • Problem set 3 (last updated on January 9, 2017): Deadline Monday January 23. Peer evaluation due Friday February 10 at 12 noon.

Links to Other Courses

Some other courses in proof complexity as taught by

There are other proof complexity courses out there as well that Google can find for you, but the ones listed above are probably those that are closest to our interests. Perhaps it should be pointed out explicitly that there will intentionally be as little overlap as possible with the courses DD3501 Current Research in Proof Complexity and DD3013 Sum of Squares and Integer Programming Relaxations taught previously at KTH.

Copyright © Published by: Jakob Nordström <jakobn~at-sign~kth~dot~se>
Updated 2017-06-01