FDD3501 Aktuell forskning inom beviskomplexitet 9,0 hp

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).

This course is intended to

• give an introduction to proof complexity (partly with a view towards connections to SAT solving),
• survey some of the most recent exciting results in this area, and
• present a number of open problems right at the frontier of current research,

so that that students after having completed the course

• will have a good grasp of modern proof complexity,
• will be able to reconstruct the proofs, at least in principle, of some of the major results during the last decade, and
• will be well equipped to attack open problems in the area (or will potentially already successfully have done so).

När kurs inte längre ges har student möjlighet att examineras under ytterligare två läsår.

Examinator beslutar, baserat på rekommendation från KTH:s handläggare av stöd till studenter med funktionsnedsättning, om eventuell anpassad examination för studenter med dokumenterad, varaktig funktionsnedsättning.

Examinator får medge annan examinationsform vid omexamination av enstaka studenter.

Jakob Nordström

• Vid grupparbete har alla i gruppen ansvar för gruppens arbete.
• Vid examination ska varje student ärligt redovisa hjälp som erhållits och källor som använts.
• Vid muntlig examination ska varje student kunna redogöra för hela uppgiften och hela lösningen.

Kursen ges i period 2-3 läsåret 2011/2012.