On the weak pigeonhole principle
By J. Krajícek. 2001
115 citations recorded by the source corpus.
We investigate the proof complexity, in (extensions of) resolution and in bounded arithmetic, of the weak pigeonhole principle and of the Ramsey theorem. In particular, we link the proof complexities of these two principles. Further we give lower bounds to the width of resolution proofs and to the size of (extensions of) tree-like resolution proofs of the Ramsey theorem. We establish a connection between provability of WPHP in fragments of bounded arithmetic and cryptographic assumptions (the existence of one-way functions). In particular, we show that functions violating WPHP2n n are one-way and, on the other hand, one-way permutations give rise to functions violating PHPn+1 n , and strongly collision-free families of hash functions give rise to functions violating WPHP2n n (all in suitable models of bounded arithmetic). Further we formulate a few problems and conjectures; in particular, on the structured PHP (introduced here) and on the unrelativised WPHP. The symbol WPHPn (with any n < m ≤ ∞) will denote both propositional and arithmetic formalisations of the weak pigeonhole principle; in the latter case I write WPHPn (R), where R is a binary relation symbol. The qualification weak means m ≥ 2n and that is the case studied here. The propositional formalisation is a set of clauses in atoms pi,j for i < m and j < n: {pi,0, . . . , pi,n−1} (1)
Subfields: Computational Theory and Mathematics, Geometry and Topology
View Paper: https://www.semanticscholar.org/paper/32911c891545b6ef944ba526d52a2f2e5b2f4dde
How researchers see this paper
The researchers whose trusted networks rank it highest, strongest advocate first. Every researcher gets a different order.
In Computational Theory and Mathematics
In Geometry and Topology
Citations in the corpus
- The provably total search problems of bounded arithmetic (2011, methodology): “In general, depth k+ 12 corresponds to T k+2 2 (α) [17, 19]; we come back to this in Section 4.”
- Towards Understanding and Harnessing the Potential of Clause Learning (2004, methodology): “Here RES(k) denotes the extension of RES that allows resolving, instead of clauses, disjunctions of conjunctions of up to k literals (Kraj́ıček, 2001).”