Structured pigeonhole principle, search problems and hard tautologies
Jan Krajı́ček · Journal of Symbolic Logic · 2005
Abstract We consider exponentially large finite relational structures (with the universe {0, 1}n) whose basic relations are computed by polynomial size (nO(1)) circuits. We study behaviour of such structures when pulled back by P/poly maps to a bigger or to a smaller universe. In particular, we prove that: 1. If there exists a P/poly map g: {0, 1}n → {0, 1}m, n < m, iterable for a proof system then a tautology (independent of g) expressing that a particular size n set is dominating in a size 2n tournament is hard for the proof system. 2. The search problem WPHP. decoding RSA or finding a collision in a hashing function can be reduced to finding a size m homogeneous subgraph in a size 22m graph. Further we reduce the proof complexity of a concrete tautology (expressing a Ramsey property of a graph) in strong systems to the complexity of implicit proofs of implicit formulas in weak proof systems.