A note on propositional proof complexity of some Ramsey-type statements
type: Item
instance of: scholarly article
title: A note on propositional proof complexity of some Ramsey-type statements
zbMATH Open document ID: 1231.03050
author: Jan Krajíček
published in: Archive for Mathematical Logic
publication date: 2011-03-02T00:00:00Z
review text: 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\)).
reviewed by: Emil Jeřábek
Mathematics Subject Classification ID: 03F20
Mathematics Subject Classification ID: 68Q15
zbMATH DE Number: 5859293
zbMATH Keywords: proof complexity
zbMATH Keywords: Ramsey theorem
zbMATH Keywords: resolution
zbMATH Keywords: exponential lower bounds
MaRDI profile type: Publication
full work available at URL: s00153-010-0212-9
OpenAlex ID: W2043904987
cites work: The relative complexity of NP search problems
cites work: Lifting independence results in bounded arithmetic
cites work: Computer Science Logic
cites work: Some remarks on the theory of graphs
cites work: Herbrandizing search problems in Bounded Arithmetic
cites work: Lower bounds to the size of constant-depth propositional proofs
cites work: Q4856172
cites work: On the weak pigeonhole principle
cites work: Combinatorics of first order structures and propositional proof systems
cites work: An exponential lower bound to the size of bounded depth frege proofs of the pigeonhole principle
cites work: NP search problems in low fragments of bounded arithmetic
cites work: A new proof of the weak pigeonhole principle
cites work: Exponential lower bounds for the pigeonhole principle
cites work: Q4281694
cites work: The provably total search problems of bounded arithmetic
DOI: 10.1007/S00153-010-0212-9
description: scientific article; zbMATH DE number 5859293