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

The remaining scribe notes for the spring term lectures are currently on hold. Hopefully, they will appear sometime during the academic year 2012/13, but this remains to be seen.

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

Nathan Segerlind: The Complexity of Propositional Proofs. Perhaps the most recent general-purpose survey of proof complexity.
Jakob Nordström: Pebble Games, Proof Complexity, and Time-Space Trade-offs. An even more recent survey paper, but mostly focused on proof space lower bounds and time-space trade-offs for resolution-based proof systems.
Jakob Nordström: Proof Complexity and Resolution. Chapter 4 of the lecturer's PhD thesis with a brief overview of proof complexity in general and resolution in particular.
Paul Beame and Toniann Pitassi: Propositional Proof Complexity: Past, Present and Future. This survey is somewhat of a classic. Perhaps a bit dated now but still a very good read.
Paul Beame: Proof Complexity. Lecture notes from an IAS summer school with very good coverage of proof complexity. Note that some of the "if pigs can fly" style of results appear to be slightly misstated, but corrected versions can be found in the PhD thesis above.
Samuel R. Buss: Towards NP–P via Proof Complexity and Search. A fairly recent survey of proof complexity and proof search, as motivated by the P versus NP problem.

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.

[ABRW02] Michael Alekhnovich, Eli Ben-Sasson, Alexander A. Razborov, and Avi Wigderson: Space Complexity in Propositional Calculus.
[AD08] Albert Atserias and Victor Dalmau: A Combinatorial Characterization of Resolution Width.
[AFT11] Albert Atserias, Johannes Klaus Fichte, and Marc Thurley: Clause-Learning Algorithms with Many Restarts and Bounded-Width Resolution.
[AR03] Michael Alekhnovich and Alexander A. Razborov: Lower Bounds for Polynomial Calculus: Non-Binomial Case.
[BBI12] Paul Beame, Chris Beck, and Russell Impagliazzo: Time-Space Tradeoffs in Resolution: Superpolynomial Lower Bounds for Superlinear Space.
[Ben09] Eli Ben-Sasson: Size-Space Tradeoffs for Resolution.
[BG01] Maria Luisa Bonet and Nicola Galesi: Optimality of Size-Width Tradeoffs for Resolution.
[BN08] Eli Ben-Sasson and Jakob Nordström: Short Proofs May Be Spacious: An Optimal Separation of Space and Length in Resolution.
[BN11] Eli Ben-Sasson and Jakob Nordström: Understanding Space in Proof Complexity: Separations and Trade-offs via Substitutions.
[BNT12] Chris Beck, Jakob Nordström, and Bangsheng Tang: Some Trade-off Results for Polynomial Calculus. [Unfortunately, no public full-length version available yet.]
[BW01] Eli Ben-Sasson and Avi Wigderson: Short Proofs Are Narrow—Resolution Made Simple.
[CEI96] Matthew Clegg, Jeffery Edmonds, and Russell Impagliazzo: Using the Groebner Basis Algorithm to Find Proofs of Unsatisfiability.
[FLNTZ12] Yuval Filmus, Massimo Lauria, Jakob Nordström, Neil Thapen, and Noga Ron-Zewi: Space Complexity in Polynomial Calculus.
[IPS99] Russell Impagliazzo, Pavel Pudlák, and Jiří Sgall: Lower Bounds for the Polynomial Calculus and the Gröbner Basis Algorithm.
[PD11] Knot Pipatsrisawat and Adnan Darwiche: On the Power of Clause-Learning SAT Solvers as Resolution Engines.
[Pud97] Pavel Pudlák: Lower Bounds for Resolution and Cutting Plane Proofs and Monotone Computations.
[Stå96] Gunnar Stålmarck: Short Resolution Proofs for a Sequence of Tricky Formulas.

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.

Scribe notes for lecture 1 might take a while to get written, but note that there are slides that cover in quite some detail what was said during the lecture.
Scribe notes for lecture 2 (last revised January 9, 2012)
Scribe notes for lecture 3 (last revised January 9, 2012)
Scribe notes for lecture 4 (last revised January 9, 2012)
Scribe notes for "lecture 4½" on pebble games and pebbling contradictions complementing what was said during lecture 4 (last revised January 7, 2012)
Scribe notes for lecture 5 (last revised November 30, 2011)
Scribe notes for lecture 6 (last revised February 11, 2012)
Scribe notes for lecture 7 (last revised February 29, 2012)
Scribe notes for lecture 8 (last revised February 11, 2012)
Scribe notes for lecture 9 (last revised February 28, 2012)
We will try to produce scribe notes for the guest lecture on SAT solving (lecture 10) but this might take a while.
Scribe notes for lecture 11 (last revised March 25, 2012)
Scribe notes for lecture 12 (last revised March 26, 2012)
Scribe notes for lecture 13 (last revised March 28, 2012)
Scribe notes for lecture 14 are in production. Unfortunately, there are no handwritten notes for this lecture. Sorry. You might try to have a look at the slides at Chris Beck's homepage, however. They cover the same material, although we saw a (much) simpler proof in Chris' guest lectures here.
The same goes for lecture 15. Scribe notes are in production; there are no handwritten notes, but you can look at Chris' slides.
Scribe notes for lecture 16 are being written. There might be handwritten notes a bit later, but they have not been cleaned up well enough yet to actually be posted on a public webpage.
Scribe notes for lecture 17 are in production, but there are handwritten notes.
Scribe notes for lecture 18 are in production, but again there are handwritten notes that you can look at.
We will try to produce scribe notes for the guest lecture on Gröbner bases and SAT solving.
Scribe notes for lecture 20 are in production; look at the handwritten notes for now.
Scribe notes for lecture 21 are in production; look at the handwritten notes for now.
Scribe notes for lecture 22 are in production; look at the handwritten notes for now.

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

Problem set 1 (last revised January 9, 2012, to harmonize notation with the scribed lecture notes): Deadline Sunday December 4, 2011. See also the webpage www.csc.kth.se/~jakobn/teaching/proofcplx11/minisat.php with some information about MiniSAT and the directory www.csc.kth.se/~jakobn/teaching/proofcplx11/files with some Sudoku instances.
Problem set 2 (last revised February 2, 2012, to correct typos): Deadline Sunday January 8, 2012.
Problem set 3 (last revised February 6, 2012, to clarify some fine points): Deadline Monday February 6, 2012. See also the webpage www.csc.kth.se/~jakobn/teaching/proofcplx11/minisat.php with some information about MiniSAT and the directory www.csc.kth.se/~jakobn/teaching/proofcplx11/files with some Kakuro instances.
Problem set 4 (last revised January 26, 2012): Deadline Monday March 5, 2012.
Problem set 5 (last revised May 5, 2012): Deadline Tuesday June 19, 2012. See also the webpage www.csc.kth.se/~jakobn/teaching/proofcplx11/minisat.php with some information about MiniSAT and the directory www.csc.kth.se/~jakobn/teaching/proofcplx11/files with some Slitherlink instances.