DD2442 Autumn 2016

DD2442/DD3343
Seminars on Theoretical Computer Science Autumn 2016:
Proof Complexity
Follow these shortcut links to go directly to
course news,
short overview of course,
schedule,
course material
(with
scribe notes),
list of problem sets,
or
links to other courses.
Go to the separate
administrative information page
to find information about
instructors,
prerequisites,
registration,
learning outcomes,
examination,
problem sets in general
(with a description of the
peer evaluation process),
and
scribing of lectures.
These webpages provide all documentation and information
about the course, so there is no separate course memo ("kursPM") PDF
file.

Solutions to problem set 3 have now been sent out for peer evaluation.
The peer evaluations are due
Friday February 10 at at 12 noon.

As usual, there will also be a discussion phase for pset 3 at Piazza,
which will tentatively start
sometime this coming Wednesday. So stay tuned…

The lectures are over.
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 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.
This course
was
given in periods 12 in the autumn of 2016.
We had a total of
24 lectures,
with 2 lectures per week on average.
In accordance with the
academic
quarter
tradition at KTH, 10 am
in the schedule
actually means 10:15 am et cetera.
See the
list of rooms at KTH
to locate the different lecture rooms.
Weekday 
Date 
Time 
Room 
# 
Plan of lectures 
References 
Monday 
Sep 5 
1012 
1537 
1. 
Introduction to proof complexity 
slides 
Wednesday 
Sep 7 
1315 
4523 
2. 
Resolution: Pigeonhole principle lower bound 
[Hak85], [Pud00], notes 
Monday 
Sep 12 
1012 
1537 
3. 
Resolution: Tseitin lower bound 
[Urq87], notes 
Wednesday 
Sep 14 
1315 
4423 
4. 
Interpolation; resolution lower bound for cliquecolouring formulas 
[Pud97], notes 
Monday 
Sep 19 
1012 
1537 
5. 
Marc Vinyals: Cutting planes: Cliquecolouring lower bound 
[Pud97], notes 
Wednesday 
Sep 21 
1315 
4523 
6. 
Marc Vinyals: Real monotone circuit lower bound for clique 
[Pud97], notes 
Monday 
Sep 26 
1012 
1537 
7. 
Boundeddepth Frege, kDNF resolution, and random restrictions 
[SBI04], notes 
Wednesday 
Sep 28 
1315 
4523 
8. 
kDNF resolution: Switching lemma; from shallow trees to resolution 
[SBI04], notes 
Monday 
Oct 3 
1012 
1537 
9. 
kDNF resolution: Switching lemma continued 
[SBI04], notes 
Wednesday 
Oct 5 
1315 
4523 
10. 
kDNF resolution: Pigeonhole principle lower bound 
[SBI04], notes 
Monday 
Oct 10 
1012 
1537 
11. 
kDNF resolution: Random 3CNF lower bound I 
[Ale11], notes 
Wednesday 
Oct 12 
1315 
4523 
12. 
kDNF resolution: Random 3CNF lower bound II 
[Ale11], notes 
Monday 
Oct 31 
1012 
1537 
13. 
Boundeddepth Frege: Pigeonhole principle lower bound I 
[KPW95], [PBI93], notes 
Wednesday 
Nov 2 
1315 
4523 
14. 
Boundeddepth Frege: Pigeonhole principle lower bound II 
[UF96], notes 
Monday 
Nov 7 
1012 
1537 
15. 
Boundeddepth Frege: Pigeonhole principle lower bound III 
[UF96], notes 
Wednesday 
Nov 9 
1416 
4523 
16. 
Boundeddepth Frege: Pigeonhole principle lower bound IV 
[UF96], notes 
Monday 
Nov 14 
1012 
1537 
17. 
Johan Håstad: Switching lemmas I 
notes for Johan's lectures 
Wednesday 
Nov 16 
1315 
4523 
18. 
Johan Håstad: Switching lemmas II 

Monday 
Nov 21 
1012 
1537 
19. 
Johan Håstad: Switching lemmas III 

Wednesday 
Nov 23 
1315 
4523 
20. 
Pavel Pudlák: Open problems and challenges in proof complexity 

Monday 
Nov 28 
1012 
1537 
21. 
Boundeddepth Frege: Overview of Tseitin lower bound 
[PRST16], notes 
Wednesday 
Nov 30 
1315 
4523 
22. 
Nonautomatizability I 
[AR08], notes 
Monday 
Dec 5 
9:4511:30 
1537 
23. 
Nonautomatizability II 
[AR08], notes 
Wednesday 
Dec 7 
1315 
4523 
24. 
Nonautomatizability III; wrapup of course 
[AR08], notes 
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
the instructors
if you are interested in specific references for some
specific area.
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
(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 (this is usually the case).
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.

[Ale11]
Michael Alekhnovich:
Lower Bounds
for kDNF Resolution on Random 3CNFs.
Computational Complexity,
volume 20, number 4, pages 597614, 2011.

[AR08]
Michael Alekhnovich and Alexander A. Razborov:
Resolution Is Not Automatizable Unless W[P] Is Tractable.
SIAM Journal on Computing,
volume 38, number 4, pages 13471363, 2008.

[Hak85]
Armin Haken:
The Intractability of Resolution.
Theoretical Computer Science,
volume 39, pages 297308, 1985.

[KPW95]
Jan Krajíček, Pavel Pudlák, and Alan R. Woods:
An Exponential
Lower Bound to the Size of Bounded Depth
Frege Proofs of the Pigeonhole Principle.
Random Structures and Algorithms,
volume 7, number 1, pages 1540, 1995.

[PBI93]
Toniann Pitassi, Paul Beame, and Russell Impagliazzo:
Exponential Lower Bounds for the Pigeonhole Principle.
Computational Complexity,
volume 3, pages 97140, 1993.

[PRST16]
Toniann Pitassi and Benjamin Rossman and
Rocco Servedio and LiYang Tan:
Polylogarithmic
Frege Depth Lower Bounds.
In Proceedings of the 48th Annual ACM Symposium on Theory
of Computing (STOC '16),
pages 644657, 2016.

[Pud97]
Pavel Pudlák:
Lower Bounds for Resolution and Cutting Plane Proofs and Monotone Computations.
Journal of Symbolic Logic,
volume 62, issue 3, pages 981998, 1997.

[Pud00]
Pavel Pudlák:
Proofs as Games.
The American Mathematical Monthly,
volume 107, number 6, pages 541550, 2000.

[SBI04]
Nathan Segerlind, Samuel R. Buss, and Russell Impagliazzo:
A Switching
Lemma for Small Restrictions and Lower Bounds
for kDNF Resolution.
SIAM Journal on Computing,
volume 33, number 5, pages 11711200, 2004.

[UF96]
Alasdair Urquhart and Xudong Fu:
Simplified Lower
Bounds for Propositional Proofs.
Notre Dame Journal of Formal Logic,
volume 37, number 4, pages 523544, 1996.

[Urq87]
Alasdair Urquhart:
Hard
Examples for Resolution.
Journal of the ACM,
volume 34, issue 1, pages 209219, 1987.
Links to scribe notes will be added below as they become available.
Please see also the
instructions for scribing
and the
signup
sheet.
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
in class.
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):
Deadline
Wednesday September 28.
Peer evaluation due
Friday October 7 at 12 noon.

Problem set 2
(last updated on October 30, 2016):
Deadline
Monday October 31.
Peer evaluation due
Friday November 11 at 12 noon.

Problem set 3
(last updated on January 9, 2017):
Deadline
Monday January 23.
Peer evaluation due
Friday February 10 at 12 noon.
Some other courses in proof complexity as taught by

Eli BenSasson
at the Technion in Haifa, Israel,

Nicola Galesi
at the
NoNA Summer School on Complexity Theory
(lecture 1,
lecture 2,
lecture 3,
and
lecture 4)
in St Petersburg, Russia,

Jan Krajíček
at Charles University in Prague, Czech Republic.

Massimo Lauria
at Tokyo Institute of Technology, Japan.

Toniann Pitassi
at the University of Toronto, Canada,

Alexander Razborov
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
DD3501
Current Research in Proof Complexity
and
DD3013
Sum of Squares and Integer Programming Relaxations
taught previously at KTH.
