June 21, 2024

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