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 |