The Complexity of the Hajós Calculus
Toniann Pitassi, Alasdair Urquhart · SIAM Journal on Discrete Mathematics · 1995
The Hajós calculus is a simple, nondeterministic procedure that generates the class of non-3-colorable graphs. Mansfield and Welsch posed the question of whether there exist graphs that require exponential-sized Hajós constructions. Unless ${\text{NP}} e {\text{coNP}}$, there must exist graphs that require exponential-sized constructions, but to date, little progress has been made on this question, despite considerable effort. In this paper, we prove that the Hajós calculus generates polynomial-sized constructions for all non-3-colorable graphs if and only if extended Frege systems are polynomially bounded. Extended Frege systems are a very powerful family of proof systems for proving tautologies, and proving superpolynomial lower bounds for these systems is a long-standing, important problem in logic and complexity theory. We also establish a relationship between a complete subsystem of the Hajós calculus and bounded-depth Frege systems; this enables us to prove exponential lower bounds on this subsystem of the Hajós calculus.