FDD3501 Current Research in Proof Complexity 9.0 credits

Aktuell forskning inom beviskomplexitet

Offering and execution

Course offering missing for current semester as well as for previous and coming semesters

Course information

Content and learning outcomes

Course contents *

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

Intended learning outcomes *

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

Course Disposition

No information inserted

Literature and preparations

Specific prerequisites *

No information inserted

Recommended prerequisites

No information inserted

Equipment

No information inserted

Literature

No information inserted

Examination and completion

If the course is discontinued, students may request to be examined during the following two academic years.

Grading scale *

P, F

Examination *

    Based on recommendation from KTH’s coordinator for disabilities, the examiner will decide how to adapt an examination for students with documented disability.

    The examiner may apply another examination format when re-examining individual students.

    Opportunity to complete the requirements via supplementary examination

    No information inserted

    Opportunity to raise an approved grade via renewed examination

    No information inserted

    Examiner

    Jakob Nordström

    Ethical approach *

    • All members of a group are responsible for the group's work.
    • In any assessment, every student shall honestly disclose any help received and sources used.
    • In an oral assessment, every student shall be able to present and answer questions about the entire assignment and solution.

    Further information

    Course web

    No information inserted

    Offered by

    EECS/Theoretical Computer Science

    Main field of study *

    No information inserted

    Education cycle *

    Third cycle

    Add-on studies

    No information inserted

    Contact

    Jakob Nordström, e-post: jakobn@kth.se

    Supplementary information

    The course is given during period 2-3 2011/2012.

    Postgraduate course

    Postgraduate courses at EECS/Theoretical Computer Science