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.
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 P ≠ NP. 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.
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.
Some survey papers on proof complexity, listed in roughly reverse chronological order, are:
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
is to invoke the KTH library proxy server directly in the address field of
the browser. You do this by adding
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
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.
Links to Other Courses
Some other courses in proof complexity as taught by