A note on propositional proof complexity of some Ramsey-type statements (Q627444)

As observed by \textit{B. Krishnamurthy} and \textit{R. N. Moll} [``Examples of hard tautologies in the propositional calculus'', in: Proceedings of the 13th ACM symposium on the theory of computing, 28--37 (1981)], the Ramsey-type statement \(n\to(k)^2_2\) (any graph on \(n\) vertices contains a clique or an independent set of size \(k\)) can be expressed as a propositional formula \(\mathsf{RAM}(n,k)\), which is a DNF formula of size \(O(n^k)\). This paper studies the proof complexity of \(\mathsf{RAM}(n,k)\) and related tautologies for some settings of the parameter \(n\). The first result is that the formulas \(\mathsf{RAM}(r_k,k)\) require exponential-size proofs in constant-depth Frege systems, where \(r_k\) is the smallest \(n\) such that \(n\to(k)^2_2\) (it is known that \(2^{k/2}<r_k<4^k\)). The other results concern the tautologies \(\mathsf{RAM}(4^k,k)\). It follows from the results of \textit{P. Pudlák} [``Ramsey's theorem in bounded arithmetic'', Lect. Notes Comput. Sci. 533, 308--317 (1991; Zbl 0795.03081)] that \(\mathsf{RAM}(4^k,k)\) has quasipolynomial-size constant-depth Frege proofs, whereas it is conjectured to require exponential-size \(R(\log)\) proofs. In the paper under review, the author proves exponential lower bounds on the lengths of resolution proofs of two relativized variants of the Ramsey statements \(\mathsf{RAM}^U(4^k,k)\) (where \(U\) is a subset of vertices, and the principle claims that one of the induced subgraphs with vertex set \(U\) or \([n]\setminus U\) contains a homogeneous set of size \(k\)) and \(\mathsf{RAM}^f(4^k,k)\) (where \(f:[n/4]\to[n]\) is an injective function, and the statement asserts that the image of \(f\) contains a homogeneous set of size \(k-1\)).