Till innehåll på sidan

Albert Atserias: Weak pigeonhole principles, circuits for approximate counting, and propositional proofs of bounded depth

Albert Atserias, Universitat Politècnica de Catalunya

Tid: Må 2013-08-26 kl 12.10 - 13.00

Plats: Room 1537, Osquars backe 2, 5th floor, KTH CSC

Exportera till kalender

Lunch is served at 12:00 noon (register at doodle.com/52n2v8ctrx69grwu by Thursday Aug 22 at 8 pm). The presentation starts at 12:10 pm and ends at 1 pm. Those of us who wish reconvene after a short break for ca two hours of more technical discussions.

Abstract

The pigeonhole principle (PHP) states that m pigeons cannot sit injectively into n holes if m is bigger than n. An often quoted result of the research in propositional proof complexity is that the PHP with m = n+1 does not have small proofs in proof systems that "lack the ability to count". These include resolution [Haken] and, more generally, proof systems that manipulate formulas with a bounded number of alternations between disjunctions and conjunctions (a.k.a. bounded-depth formulas) [Ajtai]. In contrast, for proof systems that manipulate arbitrary propositional formulas, or even bounded-depth formulas with "threshold gates", the PHP with m = n+1 admits small proofs [Buss]. For weaker PHPs where m is at least as large as a constant factor larger than n, the situation is much less understood. On one hand it looks clear that the ability to count approximately should be enough to establish these weaker PHPs. On the other, while bounded-depth circuits exist for approximate counting [Stockmeyer, Ajtai], their mere existence is not enough to get bounded-depth small proofs since one would also need elementary (i.e. comparably complex) proofs of their correctness.

In this talk we will survey the status of this classical problem in propositional proof complexity. Along the way we will discuss some new recent related results showing that a close variant of the weak PHP admits and requires quasipolynomial-size depth-2 proofs. To our knowledge, this is the first natural example that requires superpolynomial but not exponential proofs in a natural proof system. It also shows that the method of proof is in some sense "the right method"; a remarkable and rather unexpected fact by itself.