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 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 this second reason, and will therefore focus on proof systems that are especially interesting from a SAT solving perspective. A list of subjects that the course is intended to cover (which is very likely overly optimistic) is as follows:
- General proof complexity
- Some proof complexity fundamentals
- Connections to complexity theory (P vs. NP) and SAT solving
- Resolution
- Proof length and proof space: upper bounds, lower bounds and trade-offs
- Proof width and its connection to length and space
- Automatizability: can one search for resolution proofs efficiently?
- k-DNF resolution
- Proof length and proof space: upper bounds, lower bounds and trade-offs
- Hiearchy of proof systems for increasing k
- Polynomial calculus
- Upper and lower bounds on proof size
- Proof degree and its connection to size
- Proof space
- Cutting planes
- Upper and lower bounds on proof size
- Interpolation
- SAT solving
- Basics of SAT solvers based on resolution (DPLL, clause learning)
- Depending on time, participant interest, and calendar constraints, possibly also some more in-depth coverage of how state-of-the-art SAT solvers work
When discussing the above subjects, we might also need to make excursions into other areas such as communication complexity, circuit complexity, and pebble games (depending on exactly which results we will study and in what depth).