A lower bound for the pigeonhole principle in tree-like Resolution by asymmetric Prover-Delayer games

Article English OPEN
Beyersdorff, O ; Galesi, N ; Lauria, M (2010)
  • Publisher: Elsevier

In this note we show that the asymmetric Prover–Delayer game developed in Beyersdorff et al. (2010) [2] for Parameterized Resolution is also applicable to other tree-like proof systems. In particular, we use this asymmetric Prover–Delayer game to show a lower bound of the form 2Ω(nlogn) for the pigeonhole principle in tree-like Resolution. This gives a new and simpler proof of the same lower bound established by Iwama and Miyazaki (1999) [7] and Dantchev and Riis (2001) [5].
  • References (12)
    12 references, page 1 of 2

    [AD08] Albert Atserias and V´ıctor Dalmau. A combinatorial characterization of resolution width. Journal of Computer and System Sciences, 74(3):323-334, 2008.

    [BGL10] Olaf Beyersdorff, Nicola Galesi, and Massimo Lauria. Hardness of parameterized resolution. Technical Report TR10-059, Electronic Colloquium on Computational Complexity, 2010.

    [BSIW04] Eli Ben-Sasson, Russell Impagliazzo, and Avi Wigderson. Near optimal separation of tree-like and general resolution. Combinatorica, 24(4):585-603, 2004.

    [DMS07] Stefan S. Dantchev, Barnaby Martin, and Stefan Szeider. Parameterized proof complexity. In Proc. 48th IEEE Symposium on the Foundations of Computer Science, pages 150-160, 2007.

    [DR01] Stefan S. Dantchev and Søren Riis. Tree resolution proofs of the weak pigeon-hole principle. In Proc. 16th Annual IEEE Conference on Computational Complexity, pages 69-75, 2001.

    [EGM04] Juan Luis Esteban, Nicola Galesi, and Jochen Messner. On the complexity of resolution with bounded conjunctions. Theoretical Computer Science, 321(2-3):347-370, 2004.

    [IM99] Kazuo Iwama and Shuichi Miyazaki. Tree-like resolution is superpolynomially slower than dag-like resolution for the pigeonhole principle. In Proc. 10th International Symposium on Algorithms and Computation, volume 1741 of Lecture Notes in Computer Science, pages 133-142. Springer-Verlag, Berlin Heidelberg, 1999.

    [Kra95] Jan Kraj´ıˇcek. Bounded Arithmetic, Propositional Logic, and Complexity Theory, volume 60 of Encyclopedia of Mathematics and Its Applications. Cambridge University Press, Cambridge, 1995.

    [PB94] Pavel Pudla´k and Samuel R. Buss. How to lie without being (easily) convicted and the length of proofs in propositional calculus. In Proc. 8th Workshop on Computer Science Logic, volume 933 of Lecture Notes in Computer Science, pages 151-162. Springer-Verlag, Berlin Heidelberg, 1994.

    [PI00] Pavel Pudl´ak and Russell Impagliazzo. A lower bound for DLL algorithms for SAT. In Proc. 11th Symposium on Discrete Algorithms, pages 128-136, 2000.

  • Metrics
    views in OpenAIRE
    views in local repository
    downloads in local repository

    The information is available from the following content providers:

    From Number Of Views Number Of Downloads
    White Rose Research Online - IRUS-UK 0 32
Share - Bookmark