Complexity Theory Program
Coxeter Lecture Series
Lectures by Alexander A. Razborov (Steklov Mathematical
Institute)
February 23, 25 and 27, 1998
Complexity of Proofs and Computations
Natural Proofs and Feasible Proofs of Circuit Lower Bounds
Read-once Branching Programs and Regular Resolution (Tentative)
Complexity of Proofs and Computations
February 23, 1998
In discussions of computing issues, the very word ''Complexity'' is
often (and involuntarily) associated with the complexity of computations.
There are, however, other things behind computational algorithms (and
human beings) that might be complex and whose complexity is worth studying.
What, for example, makes a mathematical proof complex? A working mathematician
would probably say that a complex proof is either an extremely lengthy
one, or a proof using extremely heavy mathematics, or a proof involving
very intricate constructions. These questions are addressed and rigorously
studied by the theory of feasible (as opposed to complex) proofs, and,
quite amazingly, these three seemingly different aspects of a proof's
complexity are captured by very similar and related formal concepts.
Moreover, in every imaginable way these concepts interlace with their
counterparts in computational complexity, and it is this unique (and
complex) blend of proofs, computations and their complexities that this
lecture is devoted to. Keywords: theories of Bounded Arithmetic, propositional
proof systems.
Participants are welcome to attend a reception immediately following
this lecture ____________________________________________________________________________
Natural Proofs and Feasible Proofs of Circuit Lower Bounds
February 25, 1998
Proof-theoretical studies are usually motivated by two general properties.
First, there should be sufficiently many interesting statements that
are provable in the studied framework. Secondly, there should be at
least one very interesting statement of a similar nature whose provability
(and preferably the truth itself) is unknown and thus presents a challenge.
In this lecture we are interested in feasible proofs of circuit lower
bounds in computational complexity. We also introduce the matching combinatorial
framework of so-called natural proofs. Both these models are powerful
enough to formulate and easily prove all (to the best of our knowledge)
known theorems of the form ''an explicit Boolean function is complex
in some (weak) non-uniform computational model'', and the challenge
is whether they can prove that SAT is complex for a strong model. This
adds a new and somewhat unexpected dimension to the rich interrelations
between (the complexity of) proofs and computations addressed by lecture
#1. In the context of natural proofs the challenge has already been
more or less satisfactorily answered, and in the context of feasible
formal proofs there are some partial results toward this goal. They
are surveyed in this lecture. ____________________________________________________________________________
Read-once Branching Programs and Regular Resolution (Tentative)
February 27, 1998
The material in the two previous lectures might be somewhat too elusive
and philosophical for that part of the audience which favours concrete
results about plain things. The third lecture is designed as a sort
of a proof (hopefully, feasible) to this category of listeners that
logicians and complexity theorists also prefer simple structures whenever
permitted by the nature of their world. We consider a concrete and popular
model in Boolean complexity (read-once branching programs), and a concrete
model in propositional proof complexity (regular resolution). Firstly,
we review some properties of read-once branching programs, recalling
that they are more powerful than certain other common models (used in
circuit design) such as ordered binary decision diagrams. We then show
that regular resolution is equivalent (in a very straightforward sense
without any IFs and BUTs) to read-once branching programs for some specific
class of search problems. We give a survey of (unconditional) lower
bounds for these models attained by the good old combinatorial machinery,
and conclude with some directions for future research.
Presented in conjunction with the Workshop on Complexity Lower
Bounds, February 23 - 27, 1998
