1. Introduction
2. Background
1. Proof Complexity
2. Derandomization and pseudo-randomness
3. Contributions
1. Proof Complexity
2. Derandomization and pseudo-randomness
4. Literature
 

I. Introduction

P=NP, or more generally, are there natural computationally difficult problems?

 

NP=co-NP, or more generally, what constitutes a difficult theorem to prove?

 

P=BPP, or more generally, does randomization help computation?

 

BPP=QP, or more generally, can quantum mechanics be efficiently simulated classically?

The work done during the Special Year advanced every one of these four goals in the directions varying from quantum computation to the complexity of testing knots to PCPs and optimization (see our paper page ).  Still in retrospective one can say that most educational and research effort was concentrated on #2 (Proof Complexity) and #3 (Derandomization and Pseudo-Randomness) in which there was special strength and interest among the residents. For this reason, in the next section we give a very brief and extremely informal introduction into these particular subjects. It is accompanied with recommendations for further reading.

Section 3 essentially consists of annotations to some of the papers related to these two themes and linked or referenced at our paper page . We give there an (also very brief) account of some of the contributions made by the participants of the Special Year to both intrinsic studies within Computational Complexity and interdisciplinary areas where it meets classical mathematics.
 
 

For the reasons sketched above, we do not attempt to give here a general background on Computational Complexity (not to say that the discipline is already vast enough to make the task hopeless, at least within a limited space). To get started, the reader is recommended the standard sources [GJ79, Weg87, Han90, Pap94].
 
 

Proof Complexity does not restrict itself to propositional proof systems, and in fact it took its origins in classical proof-theoretical studies of the so-called Bounded arithmetic [Bus86, Kra95]. It soon turned out, however, that propositional proof systems provide a very convenient and elegant framework greatly unifying many things unrelated heretofore, and at the same time providing considerable simplifications by attaching to them a clean combinatorial meaning [Kra95, Raz96, BP98, Raz99]. In any case, the proof complexity part of the Special Year's activities to a large extent concentrated on propositional proof systems, and we also confine ourselves to them here.

The central theme of propositional proof complexity is to prove strong lower bounds on the bit size (or other complexity measures like degree, width or space) of interesting propositional proof systems. There is a natural correspondence between circuit classes and proof systems: simply allow only formulae from the given circuit class as lines in the corresponding proof system (and add reasonable deduction rules). In some sense, the reasoning in this system is restricted to functions computable in the circuit class. See [Raz99] for more detailed by still informal account or [Kra95] for exact mathematical statements.

Given these relations, it is no wonder that the most important (and most well-known) propositional proof systems are Frege systems and Extended Frege systems as they correspond to the complexity (circuit) classes NC^1 and P respectively. These systems are represented in the form of a  logical calculus, i.e., a proof is given by a sequence of formulas, where each formula is either an axiom (from some set of axioms), or derived from previous formulas by an inference rule (from some set of inference rules). In Frege, we allow arbitrary Boolean formulas, and the size of the proof is the sum of the sizes of all the formulas in the sequence (whence the relation with NC^1 ). In Extended Frege, we allow arbitrary Boolean circuits, and the size of the proof is the sum of the sizes of all circuits in the sequence (so that we get the proof-theoretical analogue of P ).

Most propositional proof systems studied today follow the same pattern of a logical calculus, and it is the set of admissible formulas that varies from one system to another. The notable examples are bounded-depth Frege proofs, where each formula is restricted to be of constant depth (the corresponding circuit class is AC^0) and Resolution in which admissible formulas are just clauses, i.e., disjunctions of variable and their negations.

Algebraic proof systems originally appeared as a tool for obtaining lower bounds for certain extensions of bounded-depth Frege, although they stand somewhat apart in this hierarchy. In these proof systems the formula to be proven is represented as a set of polynomial equations over a field, and our eventual goal is to infer the contradiction 1=0. There are two major systems of this kind: Nullstellensatz proof system whose proofs are just instances of Hilbert's Nullstellensatz, and its dynamical version presented in the form of a logical calculus, Polynomial Calculus . In most cases, complexity of an algebraic proof is traditionally measured by the maximal degree of polynomials appearing in it.

If lower bounds for a circuit class exist, one may hope to use the techniques in proving lower bounds for the corresponding proof system. Indeed, many known lower bounds for proof systems somehow use a related circuit lower bound. However, there are hardly any ``black box'' reductions, and usually applying the circuit techniques in the context of propositional proof complexity is a hard and non-trivial task. Reversing this empirical observation, we also get a (somewhat pessimistic) message: if we currently do not know how to prove lower bounds for circuits, then we do not know how to handle the corresponding proof system. As of today, there is not a single exception to this rule.

The above suggests the following classification (very rough and subject to change as we are gaining new knowledge): a propositional proof system is weak if we currently know how to prove lower bounds for the corresponding circuit class and strong if we do not. Of the systems mentioned in this section, bounded-depth Frege, Resolution and all algebraic proof systems are weak, whereas Frege and Extended Frege are strong. The state of art and the current goals differ rather drastically for weak and strong propositional proof systems.

For weak proof systems there is a steady progress, in many cases started by the above-mentioned transfer of ideas from the circuit complexity [ Kra95, Urq95, BP98, Pud98]. Lower bounds for the most important and natural tautologies (incidentally, quite often accompanied by rather unexpected upper bounds) like the Pigeonhole principle are followed by the general understanding of what is and what is not efficiently provable in the given system, as well as by structural results, separations between various proof systems and complexity mesaures etc. All this highly parallels similar development in the computational complexity. There are, however, a few examples of weak proof systems which we still can not handle, the most notable is bounded-depth Frege with modular connectives.

Very little is known about the power of strong proof systems. It seems, the best we can currently hope for is to prove conditional  results saying that efficient proofs in such systems can be sometimes transformed into efficient computations (cf. witnessing theorems in Bounded Arithemtic [Bus86, Kra95]). Then, by contraposition, computational lower bounds would  transfer to lower bounds for propositional proof systems. This scheme works perfectly well for some weak propositional proof systems in the form of the so-called feasible interpolation theorem [Raz96, BP98]. Unfortunately, there are strong reasons to believe that feasible interpolation does not hold for strong proof systems. As to a possible substitute, apparently the only suggestion that still looks reasonable is to use for the purpose Nisan-Wigderson generators [ABRW00].

The last issue which we discuss in this brief introduction is automatization [BP98]. So far we were interested only in the existence of efficient propositional proofs for various tautologies. But what is equally (if not more) important from the perspective of automated theorem proving, is how to find a good proof provided one exists. A propositional proof system is called fully automatizable if this search does not make new essential contributions to the inherent complexity of the tautology, i.e., there exists a determinsitic algorithm that finds its proof within time which is polynomial in the length of the shortest proof. As a general phenomenon, it turns out that the more powerful is a proof system, the less likely it is automatizable. Still, there are non-trivial examples of automatizable proof systems; for example, Polynomial Calculus is so.
 
 

The P=BPP question and related questions about the power of randomness  in computation have given rise to the notion of pseudo-random generator, a deterministic process that in some sense looks random to the computational model at hand.  The fundamental insight here is that a hard function for that computational model can (sometimes) be efficiently converted into a pseudo-random number generator for the same model.

This insight, that hardness can be turned into randomness, has led to some surprising and deep connections between the complexity of randomness, cryptography, circuit complexity and combinatorics. And once we have such a generator at hand, it results in a derandomization procedure for all probabilistic algorithms in that model - simply try out
all possible seeds of the generator (which are much fewer than all possible random strings the algorithm used).

The techniques for implementing this paradigm have improved tremendously in the two decades of its existence. For BPP (which is the class of algorithmic problems solvable by probabilistic polynomial time algorithms), such non-trivial derandomization is possible already if BPP is different from the class of problems solvable by deterministic exponential algorithms, EXP . Moreover, if EXP contains functions requiring exponential circuit size, then BPP=P (namely, randomness can be always eliminated from polynomial time computations). This brings up the problem of unconditionally separating BPP from EXP  as a natural "next step", which may be feasible even with the current technology. The extensive technical  progress of the last couple of years  on different ways of constructing pseudo-random generators still has to be fully understood, simplified and generalized to realize its potential impact on this and related problems.

The analogous techniques developed for fooling probabilistic logarithmic space computations (again, some only very recently) seem to put us quite close to deciding unconditionally that randomness is useless in that context as well, e.g that RL=L (L stands for "logarithmic space", and R stands for "randomized"). But "en-route", there are many seemingly simpler problems that still remain  challenges like derandomizing constant-width probabilistic computations or even combinatorial rectangles. Interestingly, the connection between pseudo-randomness and lower bounds is not as explicit in space bounded models as in time bounded models, and has yet to be clarified.

Finally, it seems that we have precious few ways of generating randomness from hardness. It will be extremely interesting to find drastically different pseudo-random generators, (even if these will not improve current results), or find that current constructions (like Nisan-Wigderson generators mentioned in the previous section ) are somehow universal.

Another line of research in the area is more combinatorial in nature and is aimed at improving sources of imperfect randomness so that after this improvement the outcome can be used for derandomizing various classes of algorithms.  Combinatorial constructions like expanders , extractors and condensers were identified for the purpose, and the ultimate goal here is to be able to build explicit constructions of such objects that match the performance of  randomly chosen objects. There has been a constant progress in this direction over several last years, but much still remains to be done.
 
 

As we already mentioned in Introduction, this section can be viewed as annotations to some of the papers linked or referenced at our paper page , and for a more complete picture the latter should be consulted . We confine ourselves here only to the two topics somewhat elucidated in the previous section. But many good results were proved in other branches of Computational Complexity, as well as in Combinatorics, Algebra and Topology, and more information about them can be gained from the abstracts of the respective papers.
 
 

One of the long-standing open problems in propositional proof complexity was to decide whether the weak Pigeonhole principle is hard for Resolution or not (here "weak" refers to the fact that the number of pigeons is much larger than the number of holes, potentially infinite). This problem was completely solved in the papers  Resolution Lower Bounds for the Weak Pigeonhole Principle by R. Raz and Improved Resolution Lower Bounds for the Weak Pigeonhole Principle by A. A. Razborov (very recently this result was extended to the functional version of the Pigeonhole principle, see Resolution Lower Bounds for the Weak Functional Pigeonhole Principle).

In the paper Resolution is Not Automatizable Unless W[P] is Tractable, M. V. Alekhnovich and A. A. Razborov studied the question whether Resolution is automatizable or not. Under a rather strong hardness assumption from the theory of parameterized complexity they were able to completely answer this question in negative.

Another important contribution to understanding the power of Resolution was made by Eli Ben-Sasson and Nicola Galesi in Space Complexity of Random Formulae in Resolution . The behaviour of a proof system on random tautologies is traditionally considered as a good indicator of its strength. Ben-Sasson and Galesi were able to show that Resolution performs rather badly on such formulas in terms of space consumed by the proof (a similar result for the ordinary bit size measure was known for a long time).

Among the papers devoted to stronger proof systems, we can mention Monotone simulations of nonmonotone propositional proof by Albert Atserias, Nicola Galesi and Pavel Pudlak that contains the following  (rather surprising) result. An interesting fragment of the Frege proof system called monotone sequent calculus was introduced several years ago and was long believed to be substantially weaker than (non-monotone) Frege. This paper showed that, contrary to this belief, the monotone sequent calculus can in fact efficiently simulate every Frege proof.
 
 

The paper In Search of an Easy Witness: Exponential Time vs. Probabilistic Polynomial Time by R. Impagliazzo , V. Kabanets and  A. Wigderson (awarded the Best Paper Award at the 16th IEEE Conference on Computational Complexity) makes very important contributions to the goal of extracting randomness from hardness described above . It proves (in a sense, and in an intermediate form) the universality of this approach: no derandomization of the complexity class MA (that stands for "Arthur-Merlin games") is possible unless there are hard functions in NEXPTIME. As another application of this technique, they showed a number of the so-called downward closure results (that are very rare in Complexity Theory).
The paper Entropy Waves, The Zig-Zag Graph Product, and New Constant-Degree  Expanders and Extractors by O. Reingold, S. Vadhan and A. Wigderson introduces one elegant combinatorial construction,  zig-zag product of graphs. Iterating this construction, one in particular gets simple explicit expander graphs of every size, starting from one constant-size expander. The subsequent paper Semi-direct Products in Groups and Zig-Zag products in graphs: Connections and Applications by N. Alon , A. Lubotsky and  A. Wigderson reveals deep connections between this zig-zag product and basic group-theoretical primitives. As an important application, they give an example showing that the expansion property of the Cayley graph of a group may be not invariant under the choice of generators.

Extracting Randomness via Repeated Condensing by O. Reingold, R. Saltiel and A. Wigderson constructs efficient explicit condensers and extractors that give significant qualitative improvements over previously known constructions  for sources of arbitrary min-entropy.
 
 

[GW96] O. Goldreich, A. Wigderson. Theory of Computation: A Scientific Perspective, an essay.
 

[Raz00] A. Razborov. Theoretical Computer Science: a mathematician's look (Russian), full version of an essay written for Computerra.
 
 

[GJ79] M. R. Garey, D. S. Johnson. Computers and Intractability. A guide to the theory of NP-completeness, W. H. Freeman, 1979.

[Weg87]  I. Wegener. The Complexity of Boolean Functions. John Wiley & Sons, 1987.

[Han90]  Handbook of Theoretical Computer Science, vol. A  (Algorithms and Complexity). Elsevier Science Publishers B.V. and The MIT Press, 1990.

[Pap94]  C. Papadimitriou. Computational Complexity, Addison-Wesley, 1994.
 
 

[Bus86]  S. R. Buss. Bounded arithmetic, Bibliopolis, Napoli, 1986.

[Kra95] J. Krajicek. Bounded arithmetic, propositional logic and complexity theory, Cambridge University Press, 1995.

[Urq95] A. Urquhart. The complexity of propositional proofs, Bulletin of Symbolic Logic, 1:425-467, 1995.

[Raz96] A. Razborov.  Lower bounds for propositional proofs and independence results in Bounded Arithmetic, in  Proceedings of the 23rd ICALP, Lecture Notes in Computer Science, vol. 1099, 1996, 48-62.

[BP98] P. Beame, T. Pitassi. Propositional Proof Complexity: Past, Present, and Future, Bulletin of the European  Association for Theoretical Computer Science, 65:66-89, June 1998. The Computational Complexity Column (ed. E. Allender).

[Pud98] P. Pudlak. The lengths of proofs, Handbook of Proof Theory, pages 547-637. Elsevier, 1998.

[Raz99] A. Razborov. Reviewon the book Proof Complexity and Feasible Arithmetics,  Journal of Symbolic Logic.

[ABRW00] M. Alekhnovich, E. Ben-Sasson, A. Razborov, A. Wigderson. Pseudorandom generators in propositional complexity, Proceedings of the 41st IEEE FOCS, 43-53.