Nothing Special   »   [go: up one dir, main page]
Skip to main content
Springer Nature Link
Log in

Monotone Proofs of the Pigeon Hole Principle

  • Conference paper
  • First Online:
Automata, Languages and Programming (ICALP 2000)

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 1853))

Included in the following conference series:

Abstract

We study the complexity of proving the Pigeon Hole Principle (PHP) in a monotone variant of the Gentzen Calculus, also known as Geometric Logic. We show that the standard encoding of the PHP as a monotone sequent admits quasipolynomial-size proofs in this system. This result is a consequence of deriving the basic properties of certain quasipolynomial-size monotone formulas computing the boolean threshold functions. Since it is known that the shortest proofs of the PHP in systems such as Resolution or Bounded Depth Frege are exponentially long, it follows from our result that these systems are exponentially separated from the monotone Gentzen Calculus. We also consider the monotone sequent (CLIQUE) expressing the clique-coclique principle defined by Bonet, Pitassi and Raz (1997). We show that monotone proofs for this sequent can be easily reduced to monotone proofs of the one-to-one and onto PHP, and so CLIQUE also has quasipolynomial-size monotone proofs. As a consequence, Cutting Planes with polynomially bounded coefficients is also exponentially separated from the monotone Gentzen Calculus. Finally, a simple simulation argument implies that these results extend to the Intuitionistic Gentzen Calculus. Our results partially answer some questions left open by P. Pudlák.

Supported by the CUR, Generalitat de Catalunya, through grant 1999FI 00532.

Partially supported by ALCOM-FT, IST-99-14186, by FRESCO PB98-0937-C04-04 and by SGR CIRIT 1997SGR-00366.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution

Subscribe and save

Springer+ Basic
$34.99 /Month
  • Get 10 units per month
  • Download Article/Chapter or eBook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 84.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 109.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. M. Ajtai. The complexity of the pigeonhole principle. Combinatorica, 14, pp. 417–433, 1994.

    Article  MATH  MathSciNet  Google Scholar 

  2. M. Ajtai, J. Komlós, E. Szemer edi. An O(n log n) sorting network. Combinatorica, 3(1), pp. 1–19, 1983.

    Google Scholar 

  3. N. Alon, R. B. Boppana. The monotone circuit complexity of boolean functions. Combinatorica, 7, pp. 1–22, 1987.

    Article  MATH  MathSciNet  Google Scholar 

  4. P. Beame, R. Impagliazzo, J. KrajÍček, T. Pitassi, P. Pudlák, A. Woods. Exponential lower bounds for the Pigeon Hole Principle. STOC’92, pp. 200–220, 1992.

    Google Scholar 

  5. P. Beame, T. Pitassi. Propositional Proof Complexity: Past, Present and Future. Bulletin of the European Association for Theoretical Computer Science, 65, 1998.

    Google Scholar 

  6. P. Beame, T. Pitassi. Simplified and Improved Resolution Lower Bound. FOCS’96, pp. 274–282, 1996.

    Google Scholar 

  7. M. Bonet, C. Domingo, R. Gavaldá, A. Maciel, T. Pitassi. Non-automatizability of Bounded-Depth Frege Proofs. IEEE Conference on Computational Complexity, 1998.

    Google Scholar 

  8. M. Bonet, T. Pitassi, R. Raz. Lower Bounds for Cutting Planes Proofs with small Coefficients. Journal of Symbolic Logic, 62(3), pp. 708–728, 1997. A preliminary version appeared in STOC’95.

    Article  MATH  MathSciNet  Google Scholar 

  9. S. R. Buss. Polynomial size proofs of the propositional pigeon hole principle. Journal of Symbolic Logic, 52(4), pp. 916–927, 1987.

    Article  MATH  MathSciNet  Google Scholar 

  10. S. Buss. Some remarks on length of proofs. Archive for Mathematical Logic, 34, pp. 377–394, 1995.

    Article  MATH  MathSciNet  Google Scholar 

  11. S. Buss, G. Mints. The complexity of disjunction and existence properties in intuitionistc logic. Preprint, 1998.

    Google Scholar 

  12. S. Buss, T. Pitassi. Resolution and the weak Pigeonhole principle. Invited Talk to CSL 97. To appear in Selected Papers of the 11-th CSL, Lecture Notes in Computer Science, 1998.

    Google Scholar 

  13. S. R. Buss, G. Turan. Resolution proofs of generalized pigeonhole principles. Theoretical Computer Science, 62(3), pp. 311–317, 1988.

    Article  MATH  MathSciNet  Google Scholar 

  14. V. Chvátal E. Szemer edi. Many hard examples for resolution. Journal of the Association for Computer Machinery, 35, pp. 759–768, 1988.

    Google Scholar 

  15. P. Clote, A. Setzer. On PHP, st-connectivity and odd charged graphs. Proof Complexity and Feasible Arithmetics, 93–118, DIMACS Series in Discrete Mathematics and Theoretical Computer Science, Vol 39, eds. Paul W. Beame and Samuel R. Buss, 1998.

    Google Scholar 

  16. S. Cook, R. Reckhow. The relative efficiency of propositional proof systems. Journal of Symbolic Logic, 44, pp. 36–50, 1979.

    Article  MATH  MathSciNet  Google Scholar 

  17. W. Cook, C. R. Coullard, G. Turán. On the complexity of Cutting Plane proofs. Discrete Applied Mathematics, 18, pp. 25–38, 1987.

    Article  MATH  MathSciNet  Google Scholar 

  18. A. Haken. The intractability of resolution. Theoretical Computer Science, 39(2–3), pp. 297–305, 1985.

    Article  MATH  MathSciNet  Google Scholar 

  19. R. Impagliazzo, P. Pudlak, J. Sgall. Lower Bounds for the Polynomial Calculus and the Groebner basis Algorithm. ECCC TR97-042. To appear in Computational Complexity.

    Google Scholar 

  20. J. KrajÍček. Speed-up for propositional Frege systems via generalizations of proofs, Commentationes Mathematicae Universiatatis Carolinae, 30, 1989, pp. 137–140.

    MATH  Google Scholar 

  21. J. Krajíček. Interpolation theorems, lower bounds for proof systems and independence results for bounded arithmetic. Journal of Symbolic Logic, 62, pp. 457–486, 1997.

    Article  MathSciNet  MATH  Google Scholar 

  22. A. Maciel, T. Pitassi, and A. R. Woods. A New Proof of the Weak Pigeonhole Principle. To appear in STOC’00.

    Google Scholar 

  23. J. B. Paris, A. J. Wilkie, and A. R. Woods. Provability of the pigeonhole principle and the existence of infinitely many primes. Journal of Symbolic Logic, 53(4), pp. 1235–1244, 1988.

    Article  MATH  MathSciNet  Google Scholar 

  24. P. Pudlák. On the complexity of the propositional Calculus. Logic Colloquium’ 97. To appear.

    Google Scholar 

  25. P. Pudlák. Lower bounds for resolutions and cutting planes proofs and monotone computations. Journal of Symbolic Logic, 62(2), pp., 1997.

    Google Scholar 

  26. P. Pudlák, S. Buss. How to lie without being (easily) convicted and the lengths of proofs in propositional calculus. 8th Workshop on CSL, Kazimierz, Poland, September 1994, Springer Verlag LNCS n. 995, pp. 151–162, 1995.

    Google Scholar 

  27. A. Razborov. Lower bounds for the monotone complexity of some boolean functions. Soviet Math. Doklady, 31(2), pp. 354–357, 1985.

    MATH  Google Scholar 

  28. A. Razborov. Lower bounds for the Polynomial Calculus. Computational Complexity, 7(4), pp. 291–324, 1998.

    Article  MATH  MathSciNet  Google Scholar 

  29. A. A. Razborov, A. Wigderson, A. Yao. Read Once Branching Programs, Rectangular Proofs of the Pigeonhole Principle and the Transversal Calculus. STOC’97, pp. 739–748, 4–6 May 1997.

    Google Scholar 

  30. S. Riis. A Complexity Gap for Tree-Resolution. BRICS Report Series, RS-99-29, 1999.

    Google Scholar 

  31. G. Takeuti. Proof Theory. North-Holland, second edition, 1987.

    Google Scholar 

  32. A. Urquhart. Hard examples for Resolution. Journal of the Association for Computing Machinery, 34(1), pp. 209–219, 1987.

    MATH  MathSciNet  Google Scholar 

  33. L. Valiant. Short monotone formulae for the majority function. Journal of Algorithms, 5, pp. 363–366, 1984.

    Article  MATH  MathSciNet  Google Scholar 

  34. H. Vollmer. Introduction to Circuit Complexity. Springer, 1999.

    Google Scholar 

  35. I. Wegener. The Complexity of Boolean Functions. J. Wiley and Sons, 1987.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Departament de Llenguatges i Sistemes Informátics, Universitat Politécnica de Catalunya, Barcelona, Spain

    Albert Atserias, Nicola Galesi & Ricard Gavaldá

Authors
  1. Albert Atserias
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Nicola Galesi
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Ricard Gavaldá
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Department of Computer Sciences, University of Pisa, Corso Italia, 40, 56125, Pisa, Italy

    Ugo Montanari

  2. Center for Computer Sciences, University of Geneva, 24, Rue Général Dufour, 1211, Geneva 4, Switzerland

    José D. P. Rolim

  3. Department of Computer Sciences, ETH Zurich, 8092, Zurich, Switzerland

    Emo Welzl

Rights and permissions

Reprints and permissions

Copyright information

© 2000 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Atserias, A., Galesi, N., Gavaldá, R. (2000). Monotone Proofs of the Pigeon Hole Principle. In: Montanari, U., Rolim, J.D.P., Welzl, E. (eds) Automata, Languages and Programming. ICALP 2000. Lecture Notes in Computer Science, vol 1853. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-45022-X_13

Download citation

  • DOI: https://doi.org/10.1007/3-540-45022-X_13

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-67715-4

  • Online ISBN: 978-3-540-45022-1

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation