Proof complexity and the P vs. NP problem
Course code: NMAG536.
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
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
offer a related material and references.
There is a number of topics in this area suitable for
MSc. and especially PhD. Thesis work.
To paraphrase the classics: "Let no one ignorant of
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).
Part 1: Basic concepts and examples
Cook-Reckhow proof systems, (p)-simulation,
links to NP vs. coNP problem, three 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
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
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.
Proof complexity generators.
. . .
I will make available to the course participants
a draft of my forthcoming book on "Proof complexity"
for the Cambridge University Press.
original bibliography page
for the course (including links, where available).