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