The complexity of proving that a graph is Ramsey

TL;DR

This paper investigates the complexity of proving that a graph is Ramsey, establishing superpolynomial lower bounds on proof length for certain properties, and linking Ramsey graphs to properties of random graphs.

Contribution

It introduces a CNF formulation for the Ramsey property and proves superpolynomial lower bounds on resolution proof lengths for this property.

Findings

Superpolynomial lower bounds on resolution proofs for Ramsey graphs.

Every Ramsey graph contains a large subgraph with properties similar to random graphs.

The proof connects combinatorial properties of Ramsey graphs to proof complexity.

Abstract

We say that a graph with $n$ vertices is $c$-Ramsey if it does not contain either a clique or an independent set of size $c \log n$. We define a CNF formula which expresses this property for a graph $G$. We show a superpolynomial lower bound on the length of resolution proofs that $G$ is $c$-Ramsey, for every graph $G$. Our proof makes use of the fact that every Ramsey graph must contain a large subgraph with some of the statistical properties of the random graph.