NEWS
2001/2002
Issue No 11
2001 SCIENTIFIC PROGRAMME
Workshop on Circuit and Proof Complexity
1–6 October 2001
Scientific Organising Committee:
Jan Krajicek (Prague),
Alexander Razborov (Princeton/Moscow),
Alex Wilkie (Oxford)
Supported by:
The Engineering and Physical Sciences Research Council
The area of circuit and proof complexity is central to many important topics in computational complexity as well as to parts of mathematical logic. The main open problem addressed at this meeting, the so-called ‘P/NP problem’, is now universally recognised as a major open problem in mathematics.
Informally, the problem can be stated as follows: ‘Is it harder to find proofs than to verify them?’ The concept of a proof is formalised using the notions of non-deterministic Turing machine (this subsumes all usual formalisms of logic). The qualification ‘harder’ is formalised by the time complexity of algorithms. Of course, everybody would agree that finding proofs is harder than verifying them. However, the corresponding formal conjecture that the computational class NP is strictly bigger than class P is open.
Circuit complexity represents a combinatorial approach to time lower bounds in computational complexity theory. It has developed over some fifty years from an early work of Shannon to a series of strong lower bounds for restricted circuit classes (work done from the 1980s on). The conjecture about P/NP will follow if one succeeds in proving sufficiently strong lower bounds for general boolean circuits.
In the same way in which circuit complexity is an attempt on the P/NP question, proof complexity relates to the NP/coNP question: ‘How hard it is to prove that a theorem has no short proof?’ (This was actually asked 1956 by K Gödel in a letter to J von Neumann.) The name ‘proof complexity’ reflects the fact that the research into logical calculi is developed mainly for various classes of proof systems. This topic is closely related to formal arithmetic theories (the so-called bounded arithmetic).
These areas are very active and interesting new relations to both logic and complexity theory are being developed. In the same way as the P/NP problem connects to various parts of mathematics and theoretical computer science, the research itself uses methods from different fields and uncovers new connections.
The Scientific Organising Committee succeeded in securing participation of many of key researchers in the field. The meeting took place three weeks after the September 11 terrorist attacks in the USA. Fortunately, only three people cancelled their participation because of this and the meeting was certainly a success; new results were reported in lectures and the very friendly atmosphere at the ICMS encouraged many informal discussions and exchange of ideas.
We heard many stimulating talks addressing central issues in the field. The complexity of arithmetic operations was addressed by Ran Raz and Alan Woods, who outlined lower bounds for circuits (of a particular form) computing the matrix product and primality respectively. We are hopeful that such results will mover us closer towards understanding the inherent complexity of arithmetic constructs (e.g. it is unproved at present that multiplication is harder than addition). Stephen Cook considered an empirical parallel between proof systems, circuit classes and first-order theories, which seems to appear always in naturally associated triples. He discussed a particular technical concept that attempts to formalise a part of this connection.
Nathan Segerlind reported an interesting result that is a step towards resolving a well-known problem, the proof complexity of the constant-depth Frege system with modular counting gates. He presented a combinatorial principle that separates the proof systems from some of its subsystems.
Albert Atserias gave an improved upper bound on the proof complexity of the weak pigeonhole principle, utilising Nepomnajscij’s theorem. The weak pigeonhole principle is related to approximate counting whose exact complexity is unknown. Pavel Pudlak described a framework that allows one to extend a part of the feasible interpolation method to some non-classical logics. That is interesting because limitations of non-classical proofs come from their global properties and not from the expressive power of formulas, as it is the case in many standard proof systems.
Mikhail Alekhnovich presented an optimal lower bound on the speed-up between regular and general resolution. Regular resolution was the first non-trivial proof system for which some lower bounds have been proved (by Tseitin) and its exact relation to general resolution has been open.
Return to Contents List
Participants:
Alekhnovitch, Mikhail – Massachusetts Institute of Technology
Atserias, Albert – Universidad Politecnica de Catalunya
Beame, Paul – University of Washington
Beckmann, Arnold – Technical University of Vienna
Bonet, Maria Luisa – Universidad Politecnica de Catalunya
Buss, Sam – University of California at San Diego
Cook, Stephen – University of Toronto
Dantchev, Stefan – BRICS, University of Aarhus and Queen Mary
Galesi, Nicola – Universidad Politecnica de Catalunya
Grohe, Martin – University of Edinburgh
Hanika, Jiri – Charles University
Hastad, Johan – Royal Institute of Technology in Stockholm
Jerabek, Emil – Academy of Sciences at Prague
Jerrum, Mark – University of Edinburgh
Krajicek, Jan – Academy of Sciences at Prague
Macintyre, Angus – University of Edinburgh
Morioka, Tsuyoshi – University of Toronto
Pudlak, Pavel – Academy of Sciences at Prague
Raz, Ran – Weizmann Institute
Riis, Soren – Queen Mary College
Segerlind, Nathan – University of California San Diego
Takeuti, Gaisi – University of Pennsylvania
Thapen, Neil – University of Oxford
Wilkie, Alex – University of Oxford
Woods, Alan – University of Western Australia
Xirotiri, Olga – Universities of Crete and Edinburgh
Return to Contents List