Hi all,

Anders Forsgren suggested that I post this announcement here, so here goes.

I just wanted to let you know, with somewhat short forward notice, about a course in theoretical computer science with some fun math titled "Current Research in Proof Complexity". This course will start in late October/early November and run through the winter.

A brief summary of the course follows below. More info can be found at the course webpage www.csc.kth.se/~jakobn/teaching/proofcplx11.

Please drop a line to jakobn at kth dot se if you are interested in taking the course (and to vote on the schedule, which is currently being determined by a Doodle poll). Also, feel free to contact me (by e-mail, phone or in person — see below) if you have any questions.

The course will be given in periods 2 and 3. There will probably be an average of one two-hour lecture a week, but some weeks will have two lectures and some weeks none due to travelling.

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. Although there are no real formal prerequisites, it should be noted that this will probably be 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 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 to understand the potential and limitations of algorithms for the satisfiability problem (SAT solvers), which typically use some proof system to deduce whether the formula is satisfiable or unsatisfiable. The course will have a slight bias towards this second reason, and will therefore focus on proof systems that are especially interesting from a SAT solving perspective.

With best regards,
Jakob Nordström

Jakob Nordström, KTH Royal Institute of Technology
Address: KTH CSC, Osquars backe 2, office 4420, 100 44 Stockholm, Sweden
Phone: +46 8 790 62 42 (office), +46 70 742 21 98 (cell)
Webpage: http://www.csc.kth.se/~jakobn/