Proof complexity and the P vs. NP problem
Jan Krajicek

Course code: NMAG536.

Spring 2021 special page.
Exam questions.

Student logic seminar.


The course is concerned with S.Cook's approach to the P vs. NP problem, considering it as a special case of a more general task to prove super-polynomial lengths-of-proofs lower bounds for all propositional proof systems. This was not achieved yet but we have lower bounds for a number of particular proof systems, and already these have various interesting consequences (e.g. for automated theorem proving and SAT solving, for linear programing or optimization algorithms, or independence results in mathematical logic).

A variety of formal systems for proving propositional tautologies fall under a general definition of a propositional proof system by Cook and Reckhow. The main problem is whether there exists such a proof system in which any tautology admits a proof of the length bounded above by a polynomial in the length of the tautology. This problem is equivalent to the question whether the computational complexity class NP is closed under complementation. The negative answer would imply that P and NP differ (because P is clearly closed under complementation).

We shall put most emphasis on lengths-of-proofs lower bounds and their consequences. However, we will also look at some important upper bounds and, more importantly, on ways how to establish them via bounded arithmetic.

The syllabus below will, of course, not be fully covered; rather it charts the ambient area in which we shall work. Some past courses: in 1996 (proof complexity survey), 1997a (interpolation - still called "effective" then) and 1997b (my Oxford course), 1999 (on the P vs. NP problem), 2003 and 2005 (old proof complexity courses), and 2011 (on automatizability of proof search) offer a related material.

Note:

There is a number of topics in this area suitable for MSc. and especially PhD. Thesis work.

Prerequisites:

To paraphrase the classics: "Let no one ignorant of logic enter."
I shall expect that the participants of the course are familiar with basic concepts of mathematical logic and of computational complexity theory on an undergraduate level (e.g.: first-order logic, theories and structures, p-time computations, NP-completeness, Boolean circuits).

Ambient syllabus:

Part 1: Basic concepts and examples

  • Cook-Reckhow proof systems, (p)-simulation, links to NP vs. coNP problem, main problems.

  • Examples of proof systems: logical (Frege systems F, resolution R, ER, EF, SF, G), algebraic (polynomial calculus PC, NS), geometric (cutting planes CP, Lovasz-Schrijver system LS), and other.

    Part 2: Upper bounds

  • Pi^1_1 properties of finite structures, coNP properties and their translations into propositional logic.

  • Bounded arithmetic and translations of arithmetic proofs into sequences of short propositional proofs. Examples of theories and proofs.

  • From proofs of the soundness of a SAT algorithm or a proof systems to its p-simulation.

    Part 3: Lower bound methods

  • Basic lengths-of-proofs lower bounds and shortcomings of the methods used.

  • Feasible interpolation, its links to automatizability and possible generalizations.

  • Consequences of lengths-of-proof lower bounds:
    - time lower bounds for classes of SAT (or other) algorithms,
    - the consistency of P \neq NP with various theories,
    - explicit examples of hard instances, both satisfiable as well as unsatisfiable.

    Part 4: Beyond bounds

  • Optimality of proof systems (links to structural complexity theory, finite model theory, finitistic Godel's thm, total NP search problems, ... ).

  • Proof search (successes and limits).

  • Proof complexity of computational complexity theory and provability of circuit lower bounds.

  • Methods of mathematical logic: diagonalization and model theory in proof complexity.

  • Hard tautologies. Proof complexity generators.

  • . . .

    References:

    We will use sections from my 2019 book "Proof Complexity" that appeared in the Cambridge University Press. The complete manuscript is freely available online.

    You can also consult the original bibliography page for the course (including links, where available).