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.
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.
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.
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).
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 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.
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.
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.
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.
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.
[BNT12]
Chris Beck, Jakob Nordström, and Bangsheng Tang:
Some Trade-off Results for Polynomial Calculus.
[Unfortunately, no public full-length version available yet.]
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 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.
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.
(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.)
In English
