Proof complexity generators: conjectures
Jan Krajı́ček · Cambridge University Press eBooks · 2010
All three generators that we have discussed in Chapter 29 are determined by some kind of data that can vary: an NW generator is determined by a matrix A and a function f , a gadget generator by its gadget, and the truth-table function tt s,k by its size function s = s(k) . A generator with specific data may be hard for one proof system and easy for another one. For example, if f is the parity function then EF can prove all valid τ-formulas for the NW generator by following Gaussian elimination. Or the PHP-gadget is hard for F d while easy for CP. With the current sorry state of circuit complexity lower bounds one has to take s very slow indeed to have a similar example (but s(k) = 2 k will do). It is an interesting question whether one can choose these data in some particular way so that the resulting generator would be hard for all proof systems. In this chapter we present various informal speculations as well as formal conjectures related to the hardness of these generators. Theorem 29.3.2 makes in a sense the truth-table function the most prominent among proof complexity generators. We will thus start our speculations in the first section with this function. On provability of circuit lower bounds Assume that a lower bound s = s(k) (maybe even with an exponential s ) is valid for SAT. Then the truth-table function tt s,k will not be hard for all proof systems.