swe flag På svenska
bild
School of
Computer Science
and Communication
KTH / CSC / Theory Group / Jakob Nordström / Teaching / DD3501 Current Research in Proof Complexity 2011/12

DD3501 Current Research in Proof Complexity, 9 ECTS Credits

Follow these shortcut links to go directly to news, schedule (for period 2 and period 3), lecturer, prerequisites, course goals, short overview, course requirements, course material (with scribe notes), problem sets, or links.

News

  • There is now a course analysis available.
  • The remaining scribe notes for the spring term lectures never made it into a polished enough state to publish. Hopefully there will be time to go over them sometime in the future, but when this will be remains to be seen.

Schedule

This course was given during periods 2 and 3 of the academic year 2011/12. The intention was to have on average one two-hour lecture per week, but some weeks had two lectures and some weeks none due to travelling or other constraints.

Schedule for Period 2

 Weekday Date Time Room Plan of lectures References
 Monday Oct 24 10-12 1537 Introduction to proof complexity; course overview; practicalities slides
 Thursday Oct 27 10-12 4523 Connection between proof length and proof width in resolution [BW01], slides, notes
 Monday Oct 31 10-12 1537 Lower bounds on proof length in resolution [BW01], notes
 Thursday Nov 3 10-12 MDI-torget Connection between space and width in resolution; combinatorial characterization of width [AD08], [Ben09], slides
 Monday Nov 14 10-12 1537 Tightness of connection between proof length and proof width in resolution [BG01], [Stå96], notes
 Monday Nov 28 10-12 1537 Connections between proof size and proof degree in polynomial calculus [CEI96], [IPS99], notes
 Thursday Dec 1 10-12 1625 Size vs. degree continued; lower bounds on proof size in polynomial calculus [IPS99], [AR03], notes
 Monday Dec 5 10-12 1537 Lower bounds on proof size in polynomial calculus (cont.) [AR03], notes
 Monday Dec 12 10-12 4523 Lower bounds on proof space in polynomial calculus [ABRW02], [FLNTZ12], notes
 Thursday Dec 15 10-12 1537 Guest lecture by Matti Järvisalo: Modern SAT Solving: CDCL and Inprocessing
 Monday Dec 19 10-12 4523 Lower bounds on proof space in polynomial calculus (cont.) [FLNTZ12], notes

Schedule for Period 3

In addition to the lectures below, we also had a TCS seminar related to proof complexity and SAT solving by Bangsheng Tang from Tsinghua University on Monday January 30.

 Weekday Date Time Room Plan of lectures References
 Tuesday Jan 17 10-12 1537 Size-space trade-offs for resolution in sublinear space [BN08], [BN11], notes
 Wednesday Jan 18 13-15 1537 Size-space trade-offs for resolution in sublinear space (cont.) [BN08], [BN11], no notes
 Tuesday Jan 24 10-12 1537 Guest lecture by Chris Beck: Size-space trade-offs for resolution in superlinear space [BBI12], no notes
 Wednesday Jan 25 13-15 1537 Guest lecture by Chris Beck: Size-space trade-offs for resolution in superlinear space (cont.) [BBI12], no notes
 Tuesday Jan 31 10-12 4523 Lower bounds on proof length in cutting planes [Pud97], no notes (yet)
 Tuesday Feb 7 10-12 1537 Size-space trade-offs for polynomial calculus and PCR [BNT12], notes
 Wednesday Feb 8 13-15 1537 Upper bounds on resolution width imply upper bounds on CDCL running time [AFT11], notes
 Monday Feb 13 13-15 1537 Guest lecture by Samuel Lundqvist: The SAT Problem and Boolean Gröbner Bases
 Tuesday Feb 14 10-12 1537 Upper bounds on resolution width imply upper bounds on CDCL running time (cont.) [AFT11], notes
 Tuesday Feb 21 10-12 1537 CDCL as a proof system polynomially simulates resolution [PD11], notes
 Wednesday Feb 22 13-15 1537 CDCL polynomially simulates resolution (cont.); final remarks [PD11], notes

Lecturer

Jakob Nordström, jakobn at kth dot se, office 4420 (currently office 4517). Office hours are by appointment only—send an e-mail to agree about a time to meet.

Prerequisites

This course is open to anyone, but the main target audience are grad students and advanced undergrads. Some background in computational complexity theory and/or discrete mathematics will probably be helpful, but all that should really be needed is "mathematical maturity" and a willingness to learn new stuff. The lectures are given in English. The course code is DD3501, or FDD3501 if you are a PhD student.

Although there are no real formal prerequisites, it should be noted that this is a somewhat demanding course (but hopefully even more fun).

Course Goals

This course is intended to

  • give an introduction to proof complexity (partly with a view towards connections to SAT solving),
  • survey some of the most recent exciting results in this area, and
  • present a number of open problems right at the frontier of current research,
so that that students after having completed the course
  • will have a good grasp of modern proof complexity,
  • will be able to reconstruct the proofs, at least in principle, of some of the major results during the last decade, and
  • will be well equipped to attack open problems in the area (or will potentially already successfully have done so).

Short Overview

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 this second reason, and will therefore focus on proof systems that are especially interesting from a SAT solving perspective. A list of subjects that the course is intended to cover (which is very likely overly optimistic) is as follows:

  • General proof complexity
    • Some proof complexity fundamentals
    • Connections to complexity theory (P vs. NP) and SAT solving
  • Resolution
    • Proof length and proof space: upper bounds, lower bounds and trade-offs
    • Proof width and its connection to length and space
    • Automatizability: can one search for resolution proofs efficiently?
  • k-DNF resolution
    • Proof length and proof space: upper bounds, lower bounds and trade-offs
    • Hiearchy of proof systems for increasing k
  • Polynomial calculus
    • Upper and lower bounds on proof size
    • Proof degree and its connection to size
    • Proof space
  • Cutting planes
    • Upper and lower bounds on proof size
    • Interpolation
  • SAT solving
    • Basics of SAT solvers based on resolution (DPLL, clause learning)
    • Depending on time, participant interest, and calendar constraints, possibly also some more in-depth coverage of how state-of-the-art SAT solvers work
When discussing the above subjects, we might also need to make excursions into other areas such as communication complexity, circuit complexity, and pebble games (depending on exactly which results we will study and in what depth).

Update 1: Complementing and elaborating on the list above, in late January we had a vote in class on possible themes for the remaining lectures. Just for the record, there is a webpage with the list of topics we were choosing from.

Update 2: While the list above was indeed (as expected) a bit too ambitious, we did manage to cover most of the items listed there. The most important omissions, perhaps, are that we did not do much k-DNF resolution (except for very briefly sketching space lower bounds and time-space trade-offs) and we did not go into any details about why resolution probably is not automatizable.

Course Requirements

There is a total of 5 problem sets on the course. In principle, students should pass all 5 sets to get a pass on the course.

Another course requirement is to scribe one lecture (in LaTeX). There are template files and instructions for this that the scribes get by e-mail from the lecturer, and there is a scribing schedule on which you can sign up by e-mailing the lecturer. Update: As it has turned out, pretty much all students will have to scribe two lectures, but we agreed that the second scribed lecture should count towards half a problem set of the student's choosing.

Given that this is a course that is intended to bring us right up to the state-of-the-art in proof complexity research, there will also be a possibility to substitute a reading or research project for parts of the other requirements. The details here will be determined on a case-by-case basis by mutual agreement by the student and lecturer.

Please note the code of honour that applies to all courses at KTH CSC.

Course Material

Surveys

Some general surveys of proof complexity which might be useful are:

Some of the material that we covered can also be found in Chapter 5 of the book Boolean Functions and Computation Models by Peter Clote and Evangelos Kranakis, but there was not enough overlap to make it an officially recommended textbook for the course.

Research Articles

Below follows a list of the research articles on which the lectures have been based. Note that some of this material is also covered in the surveys above (possibly even in more readable form) but the links below are to the original papers. Whenever available, the link is to the journal version (or full-length technical report), which means that the date of the paper can be several years later than that of the original conference publication.

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 download some of the the article PDF files. If so, just googling for the title should help you find free preliminary versions of the same papers on the webpages of the authors or similar.

Another 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. 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

We have had a schedule for scribing lecture notes in LaTeX, which are being posted below as they become available.

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 an e-mail to jakobn at kth dot se.

Problem Sets

General Information

Problems sets should be submitted as PDF-files by e-mail to jakobn at kth dot se. Please use the subject line Problem set <N>: <your name>. Solutions should be typeset in some math-aware system (read: LaTeX or such like; MS Word with Equation Editor is borderline but might pass).

For most of the problems, it will be possible to purchase "hints" for a certain deduction from the max score of the problem. In this way, you can configure yourself whether you want the problems to be more creative and open-ended, where sometimes a lot can depend on finding the right idea, or whether you want them to be more of guided exercises providing a useful work-out on the concepts of proof complexity. Please feel free to use (or not use) this possibility to make the course more interesting and rewarding for you.

When you are working on the problem sets, discussions of ideas in groups of two to three people are allowed—and indeed, encouraged—but you should always write down your own solution individually and understand all aspects of it fully. You should also acknowledge in your solutions with whom you have been collaborating.

Some of the problems will be "classic" and hence their solutions can probably be found on the Internet or in research papers. It is not allowed to use such solutions in any way unless explicitly stated otherwise. Anything said during the lectures on in the lecture notes should be fair game, though, unless you are specifically asked to show something that we claimed without proof in class.

List of Problem Sets

Links

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.)

Published by: Jakob Nordström <jakobn~at-sign~kth~dot~se>
Updated 2015-01-29