On the existence of strong proof complexity generators
share
The working conjecture from K'04 that there is a proof complexity generator hard for all proof systems can be equivalently formulated (for p-time generators) without a reference to proof complexity notions as follows: * There exist a p-time function g stretching each input by one bit such that its range rng(g) intersects all infinite NP sets. We consider several facets of this conjecture, including its links to bounded arithmetic (witnessing and independence results) and the range avoidance problem, to time-bounded Kolmogorov complexity, to feasible disjunction property of propositional proof systems and to complexity of proof search. We argue that a specific gadget generator from K'09 is a good candidate for g.
READ FULL TEXT