17th Estonian Winter School in Computer Science (EWSCS)
XVII Eesti Arvutiteaduse Talvekool

Palmse, Estonia, February 26 -March 2, 2012

Jakob Nordström

School of Computer Science and Communication
KTH Royal Institute of Technology, Stockholm

Time-space trade-offs in proof complexity


During the last decade, an active line of research in proof complexity has been to study space complexity and time-space trade-offs for proofs. Besides being a natural complexity measure of intrinsic interest, space is also an important issue in SAT solving (i.e., the problem of deciding whether propositional logic formulas are satisfiable or not). Therefore, research has mostly focused on relatively weak proof systems that are used by SAT solvers, such as resolution, polynomial calculus and cutting planes.

All SAT solvers use 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 can hopefully tell us something about the potential and limitations of such SAT solvers. Typically, one wants to optimize both time and memory consumption, and it is therefore interesting to study complexity measures corresponding to time and space and see how they are related to one another in different proof systems. (For instance: can time and space be optimized simultaneously, or must minimizing one of the measures lead to a dramatic increase in the other?)

In this course, we hope to give a (by necessity very selective and subjective) survey of the area, cover a couple of the most recent results, and discuss some of the many open problems that remain.

Course materials

See also material for the course "Current Research in Proof Complexity" at KTH [link]

Valid CSS! Valid XHTML 1.0 Strict Last changed March 3, 2012 22:25 EET by local organizers, ewscs12(at)cs.ioc.ee
EWSCS'12 page: http://cs.ioc.ee/ewscs/2012/