DD2442 Seminars on Theoretical Computer Science, 7.5 ECTS Credits

First two lectures on Monday Sep 5 at 10:15-12:00 in 1537 and Wednesday Sep 7 at 13:15-15:00 in 4523 at Lindstedtsvägen 3/5.

This is an advanced course at MSc and PhD level which is intended to be interesting and challenging for PhD students in both computer science and mathematics. If you love both mathematics and computers, then here you will get the best of both worlds!

More information at www.csc.kth.se/DD2442/semteo16/

BRIEF COURSE DESCRIPTION

Deciding whether a propositional logic formula is satisfiable (the SAT problem) is believed to be hard, but if a formula is satisfiable, then there is a short, easily verifiable proof of this fact (namely a satisfying assignment). What if a formula is *not* satisfiable, though? Is there a way to give a short, easily verifiable proof that all of the exponentially many truth value assignments fail to satisfy the formula? This is the question addressed by proof complexity.

 

Proof complexity studies formal methods of reasoning about formulas (so-called proof systems) and the power and limitation of such methods. This is connected to deep problems in computational complexity, such as whether NP and coNP are equal or not. It is also related to algorithmic questions in SAT solving, where one wants to understand not only whether short proofs exist but whether they can also be *found* efficiently. These questions turn out to have surprising connections with areas such as circuit complexity, cryptography, and combinatorial optimization.

 

In this course, we hope to cover some of the exciting developments in proof complexity during the last two decades and to see what challenges lie ahead (some of which we are working hard on in the TCS group at KTH).