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.

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.
This course was given during periods 2 and 3 of the academic year 2011/12.
The intention was to have on average one twohour lecture per week,
but some weeks had two lectures and some weeks none due to
travelling or other constraints.
Weekday 
Date 
Time 
Room 
Plan of lectures 
References 
Monday 
Oct 24 
1012 
1537 
Introduction to proof complexity;
course overview; practicalities 
slides

Thursday 
Oct 27 
1012 
4523 
Connection between proof length and
proof width in resolution 
[BW01],
slides,
notes

Monday 
Oct 31 
1012 
1537 
Lower bounds on proof length in resolution 
[BW01],
notes

Thursday 
Nov 3 
1012 
MDItorget 
Connection between space and
width in resolution; combinatorial characterization of width 
[AD08], [Ben09],
slides

Monday 
Nov 14 
1012 
1537 
Tightness of connection between
proof length and proof width in resolution

[BG01],
[Stå96],
notes

Monday 
Nov 28 
1012 
1537 
Connections between proof size and proof degree in polynomial calculus

[CEI96],
[IPS99],
notes

Thursday 
Dec 1 
1012 
1625 
Size vs. degree continued; lower bounds on proof size in polynomial calculus

[IPS99],
[AR03],
notes

Monday 
Dec 5 
1012 
1537 
Lower bounds on proof size in polynomial calculus (cont.)

[AR03],
notes

Monday 
Dec 12 
1012 
4523 
Lower bounds on proof space in polynomial calculus

[ABRW02],
[FLNTZ12],
notes

Thursday 
Dec 15 
1012 
1537 
Guest lecture by
Matti Järvisalo:
Modern SAT Solving: CDCL and Inprocessing


Monday 
Dec 19 
1012 
4523 
Lower bounds on proof space in polynomial calculus (cont.)

[FLNTZ12],
notes

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 
1012 
1537 
Sizespace tradeoffs
for resolution in sublinear space 
[BN08],
[BN11],
notes

Wednesday 
Jan 18 
1315 
1537 
Sizespace tradeoffs
for resolution in sublinear space (cont.) 
[BN08],
[BN11],
no notes

Tuesday 
Jan 24 
1012 
1537 
Guest lecture by
Chris Beck:
Sizespace tradeoffs
for resolution in superlinear space 
[BBI12],
no notes

Wednesday 
Jan 25 
1315 
1537 
Guest lecture by
Chris Beck:
Sizespace tradeoffs
for resolution in superlinear space
(cont.) 
[BBI12],
no notes

Tuesday 
Jan 31 
1012 
4523 
Lower bounds on proof length
in cutting planes

[Pud97],
no notes (yet)

Tuesday 
Feb 7 
1012 
1537 
Sizespace tradeoffs
for polynomial calculus and PCR

[BNT12],
notes

Wednesday 
Feb 8 
1315 
1537 
Upper bounds on resolution width
imply upper bounds on CDCL running time

[AFT11],
notes

Monday 
Feb 13 
1315 
1537 
Guest lecture by
Samuel Lundqvist:
The SAT Problem and
Boolean Gröbner Bases


Tuesday 
Feb 14 
1012 
1537 
Upper bounds on resolution width
imply upper bounds on CDCL running time (cont.)

[AFT11],
notes

Tuesday 
Feb 21 
1012 
1537 
CDCL as a proof system
polynomially simulates resolution

[PD11],
notes

Wednesday 
Feb 22 
1315 
1537 
CDCL
polynomially simulates resolution (cont.);
final remarks

[PD11],
notes

Jakob Nordström,
jakobn at kth dot se,
office 4420
(currently office 4517).
Office hours are by appointment only—send an email 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).
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).
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 socalled 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
tradeoffs
 Proof width and its connection to length and space
 Automatizability: can one search for resolution proofs efficiently?
 kDNF resolution
 Proof length and proof space: upper bounds, lower bounds and
tradeoffs
 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 indepth coverage of how
stateoftheart 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
kDNF resolution (except for very briefly
sketching space lower bounds and timespace tradeoffs) 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 email from the lecturer,
and there is a
scribing schedule
on which you can sign up by emailing 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 stateoftheart 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
casebycase basis by mutual agreement by the student and lecturer.
Please note the
code of honour
that applies to all courses at KTH CSC.
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.
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 fulllength 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 paywall, 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 BenSasson, 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:
ClauseLearning Algorithms with Many Restarts and BoundedWidth
Resolution.

[AR03]
Michael Alekhnovich and Alexander A. Razborov:
Lower Bounds
for Polynomial Calculus: NonBinomial Case.

[BBI12]
Paul Beame, Chris Beck, and Russell Impagliazzo:
TimeSpace Tradeoffs in Resolution:
Superpolynomial Lower Bounds for Superlinear Space.

[Ben09]
Eli BenSasson:
SizeSpace
Tradeoffs for Resolution.

[BG01]
Maria Luisa Bonet and Nicola Galesi:
Optimality of
SizeWidth Tradeoffs for Resolution.

[BN08]
Eli BenSasson and Jakob Nordström:
Short Proofs
May Be Spacious: An Optimal Separation of Space and Length in Resolution.

[BN11]
Eli BenSasson and Jakob Nordström:
Understanding Space
in Proof Complexity: Separations and Tradeoffs via Substitutions.

[BNT12]
Chris Beck, Jakob Nordström, and Bangsheng Tang:
Some Tradeoff Results for Polynomial Calculus.
[Unfortunately, no public fulllength version available yet.]

[BW01]
Eli BenSasson 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 RonZewi:
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 ClauseLearning 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.
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 email 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 28, 2012)

Scribe notes for lecture 8
(last revised September 11, 2014)

Scribe notes for lecture 9
(last revised February 27, 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.
General Information
Problems sets should be submitted as PDFfiles by email to
jakobn at kth dot se.
Please use the subject line
Problem set <N>: <your name>
.
Solutions should be typeset in some mathaware 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 openended, 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 workout
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.
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.)