DD2442 Autumn 2016
Seminars on Theoretical Computer Science Autumn 2016:
Follow these shortcut links to go directly to
short overview of course,
list of problem sets,
links to other courses.
Go to the separate
administrative information page
to find information about
problem sets in general
(with a description of the
peer evaluation process),
scribing of lectures.
These webpages provide all documentation and information
about the course, so there is no separate course memo ("kurs-PM") PDF
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.
given in periods 1-2 in the autumn of 2016.
We had a total of
with 2 lectures per week on average.
In accordance with the
tradition at KTH, 10 am
in the schedule
actually means 10:15 am et cetera.
list of rooms at KTH
to locate the different lecture rooms.
||Plan of lectures
||Introduction to proof complexity
||Resolution: Pigeonhole principle lower bound
||[Hak85], [Pud00], notes
||Resolution: Tseitin lower bound
||Interpolation; resolution lower bound for clique-colouring formulas
||Marc Vinyals: Cutting planes: Clique-colouring lower bound
||Marc Vinyals: Real monotone circuit lower bound for clique
||Bounded-depth Frege, k-DNF resolution, and random restrictions
||k-DNF resolution: Switching lemma; from shallow trees to resolution
||k-DNF resolution: Switching lemma continued
||k-DNF resolution: Pigeonhole principle lower bound
||k-DNF resolution: Random 3-CNF lower bound I
||k-DNF resolution: Random 3-CNF lower bound II
||Bounded-depth Frege: Pigeonhole principle lower bound I
||[KPW95], [PBI93], notes
||Bounded-depth Frege: Pigeonhole principle lower bound II
||Bounded-depth Frege: Pigeonhole principle lower bound III
||Bounded-depth Frege: Pigeonhole principle lower bound IV
||Johan Håstad: Switching lemmas I
||notes for Johan's lectures
||Johan Håstad: Switching lemmas II
||Johan Håstad: Switching lemmas III
||Pavel Pudlák: Open problems and challenges in proof complexity
||Bounded-depth Frege: Overview of Tseitin lower bound
||Non-automatizability III; wrap-up of course
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
if you are interested in specific references for some
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
to the domain of the web address where you found the paper in question,
which will work if the KTH library has a subscription (this is usually the case).
For instance, if you want to look at
but this paper is behind a pay-wall, you try to change the URL to
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.
for k-DNF Resolution on Random 3-CNFs.
volume 20, number 4, pages 597-614, 2011.
Michael Alekhnovich and Alexander A. Razborov:
Resolution Is Not Automatizable Unless W[P] Is Tractable.
SIAM Journal on Computing,
volume 38, number 4, pages 1347-1363, 2008.
The Intractability of Resolution.
Theoretical Computer Science,
volume 39, pages 297-308, 1985.
Jan Krajíček, Pavel Pudlák, and Alan R. Woods:
Lower Bound to the Size of Bounded Depth
Frege Proofs of the Pigeonhole Principle.
Random Structures and Algorithms,
volume 7, number 1, pages 15-40, 1995.
Toniann Pitassi, Paul Beame, and Russell Impagliazzo:
Exponential Lower Bounds for the Pigeonhole Principle.
volume 3, pages 97-140, 1993.
Toniann Pitassi and Benjamin Rossman and
Rocco Servedio and Li-Yang Tan:
Frege Depth Lower Bounds.
In Proceedings of the 48th Annual ACM Symposium on Theory
of Computing (STOC '16),
pages 644-657, 2016.
Lower Bounds for Resolution and Cutting Plane Proofs and Monotone Computations.
Journal of Symbolic Logic,
volume 62, issue 3, pages 981-998, 1997.
Proofs as Games.
The American Mathematical Monthly,
volume 107, number 6, pages 541-550, 2000.
Nathan Segerlind, Samuel R. Buss, and Russell Impagliazzo:
Lemma for Small Restrictions and Lower Bounds
for k-DNF Resolution.
SIAM Journal on Computing,
volume 33, number 5, pages 1171-1200, 2004.
Alasdair Urquhart and Xudong Fu:
Bounds for Propositional Proofs.
Notre Dame Journal of Formal Logic,
volume 37, number 4, pages 523-544, 1996.
Examples for Resolution.
Journal of the ACM,
volume 34, issue 1, pages 209-219, 1987.
Links to scribe notes will be added below as they become available.
Please see also the
instructions for scribing
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
jakobn at kth dot se.
Please note that dates for future problem sets are not completely,
irrevocably, 100% fixed.
The actual deadlines are somewhat configurable, and can be discussed
The important thing is that we all agree on the deadlines beforehand,
and that once they are set we stick to them without exceptions.
Problem set 1
(last updated on September 21, 2016):
Wednesday September 28.
Peer evaluation due
Friday October 7 at 12 noon.
Problem set 2
(last updated on October 30, 2016):
Monday October 31.
Peer evaluation due
Friday November 11 at 12 noon.
Problem set 3
(last updated on January 9, 2017):
Monday January 23.
Peer evaluation due
Friday February 10 at 12 noon.
Some other courses in proof complexity as taught by
at the Technion in Haifa, Israel,
NoNA Summer School on Complexity Theory
in St Petersburg, Russia,
at Charles University in Prague, Czech Republic.
at Tokyo Institute of Technology, Japan.
at the University of Toronto, Canada,
at the University of Chicago, USA.
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.
Perhaps it should be pointed out explicitly that
there will intentionally be as little overlap as possible with the courses
Current Research in Proof Complexity
Sum of Squares and Integer Programming Relaxations
taught previously at KTH.