The complexity of the Hajos calculus

The Hajos construction is a simple, nondeterministic procedure for generating the class of graphs that are not 3-colorable. A.J. Mansfield and D.J.A. Welsh have posed the problem of proving whether or not there exists a polynomial-size Hajos construction for every non-3-colorable graph. The main result of this paper is a proof that the Hajos calculus is polynomially-bounded if and only if extended Frege proof systems are polynomially bounded. This result links an open problem in graph theory to an important open problem in the complexity of propositional proof systems. In addition, the authors establish an exponential lower bound for a strong subsystem of the Hajos calculus. Lastly, they discuss an interesting graph-theoretical consequence of this result.< >