:: Home
:: What is EACSL
:: Organization
:: Membership
:: CSL Conferences
:: Ackermann Award
:: Alonzo Church Award
:: CSL Bibliography
:: Constitutions
:: Minutes
:: Contact

Ackermann Award 2005: Nathan Segerlind


Citation

Nathan Segerlind recieves the 2005 Ackermann Award of the European Association of Computer Science Logic (EACSL) for his thesis

New Separations in Propositional Proof Complexity

.
His thesis extends switching lemmas, one of the most primary tools in the area, in a very unexpected way. This has allowed Segerlind to solve a host of difficult open problems in propositional proof complexity and, in particular, to take in a single step the proof system Res(k) from an almost complete mystery to being almost completely understood.

Background of the thesis

The central question of propositional proof complexity can be formulated in a deceivingly simple way. Given a (sound and complete) proof system P for propositional logic and a tautology φ, what is the ``simplest'' (in most cases meaning the shortest) P-proof of φ? Partly due to the universal nature of the notion of a propositional tautology, this is an interdisciplinary area on the border between (and with motivations from) mathematical logic, theory of computing, automated theorem proving, cryptography, algebra and combinatorics among other.

Largely influenced by the automated theorem proving (Davis, Putnam (1960), Davis, Longemann, Loveland (1962), Robinson (1965)), the most widely studied proof system in the area is (propositional) Resolution. After considerable efforts by many researchers beginning with the seminal paper by Tseitin (1968), the resolution proof system is by now fairly well understood. We have rather general, industrial methods to analyze the complexity of resolution proofs (like the width-size relation by Ben-Sasson, Wigderson (1999)), as well as concrete results concerning virtually all combinatorial principles normally used as ``benchmarks'' in the whole area (Haken (1985), Urquhart (1987), Chvátal, Szemerédi (1988), Raz (2001), Razborov (2001)).

Until the work represented by Segerlind's thesis, however, everything looked very different (meaning much more obscure) beyond Resolution. As a typical example, take one of the most influential results in the whole area, exponential lower bounds on the complexity of the pigeon-hole principle in the constant-depth Frege proof system (Beame, Impagliazzo, Krajíček, Pitassi, Pudlák, Woods (1992)) based on one of the most powerful tools in the area, switching lemmas for random restrictions. We do not know how to apply this method to many tautologies where it should have been applicable, and even when successful (like e.g. Beame, Riis (1998)), the switching lemmas and other techniques, already extremely complicated, have to be re-done almost from the scratch. The situation is very similar for the intermediate proof system Res(k) that operates like Resolution but allows in clauses conjunctions of size ≤ k rather than just literals. This system is of great potential interest for automated proving (perhaps, of better interest than constant-depth Frege) since it is structured almost as well as Resolution but surprisingly can do more interesting things than the latter (Maciel, Pitassi, Woods (2000)).

Just to give an idea of the state of the art in the area, random 3-CNF is one of the most popular benchmark models both in theoretical and practical communities. They had been shown to be hard for Resolution by Chvátal and Szemerédi in 1988, but the same question was widely open for any reasonable extension of Resolution, including Res(2).

Another important subject addressed in the thesis is algebraic proof systems (like Nullstellensatz and Polynomial Calculus) and hybrid systems combining logical and algebraic reasoning (constant-depth Frege with counting axioms or modular gates). By the time of Segerlind's work, purely algebraic proof systems and relations between them were in general understood much better than purely logical systems, but several important questions remained open.


Segerlind's thesis

In his thesis Segerlind proved important and nice results about the relative power of algebraic and mixed proof systems, both positive and negative, that had been open for a while. Among other things he showed that counting gates are more powerful than counting axioms (Chapter VI), but the counting axioms can efficiently simulate any Nullstellensatz proof (Chapter V). The most striking part of the thesis, however, concerns the systems Res(k) for small values of k (Chapters III and IV).

The upshot of these latter results is very simple: we now understand the systems Res(k) almost as well as Resolution itself. In his thesis Segerlind analyzed the complexity of the weak pigeon-hole principle and random w-CNFs (both are standard ``tests for maturity'') in these proof systems, and he also gave separation results between the systems Res(k) and Res(w) for some w>k. His techniques were already used in different situations by Razborov and Alekhnovich. So, it really looks like what he has found is a general, powerful and flexible method rather than ad hoc argument. All in all, Segerlind's work changed the situation with these prominent systems from a few scattered and weak results to a few important problems left open. And two features of this development look particularly striking.

The first is its speed. For Resolution it took decades to have reached the level of understanding that was reached here in a single step. Of course, this comparison is not quite fair since the general methodology gathered during these decades also played very essential role in Segerlind's work. But even with this disclaimer the speed with which it all happened was quite remarkable and totally unexpected.

The second surprise came in the form of proof methods. The novelty essentially consists in a new version of switching lemmas called in the thesis switching with small restrictions. And, in order to appreciate this, one should be fully aware to which extent this tool is basic in both computational complexity and proof complexity. Many researchers have been looking at these lemmas since the seminal work by Håstad (1986). They have been scrutinized and analyzed from every possible perspective and in all fine and technical details. The fact that Segerlind was able to say a substantially new word in an area so often re-visited by strongest researchers is also quite remarkable.


Biographic Sketch

Nathan Segerlind was born on December 31, 1973 in Marlette, Michigan. In 1992-1998 he studied Computer Science and Mathematics at Carnegie Mellon University, Pittsburg. Between 1998 and 2003 he was a PhD student at the University of California at San Diego, under joint supervision by Samuel Bass and Russell Impagliazzo. He spent the next year 2003-2004 as a postdoctoral member at the Institute for Advanced Study, Princeton. Currently he is continuing his post-doc research at the University of Washington, Seattle.