Jakob Nordström
School of Computer Science and Communication
KTH Royal Institute of Technology, Stockholm
Sweden
Time-space trade-offs in proof complexity
Abstract
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
- J. Nordström. Time-space trade-offs in proof complexity. Lecture slides for EWSCS '12, 2012. part 1 [pdf], part 2 [pdf], part 3 [pdf], part 4 [pdf]
- J. Nordström. Pebble games, proof complexity, and time-space trade-offs. Logical Methods in Computer Science, to appear. [pdf]
Last changed
March 3, 2012 22:25 EET
by
local organizers, ewscs12(at)cs.ioc.ee
EWSCS'12 page:
//cs.ioc.ee/ewscs/2012/