A human-checkable proof of the 112-vertex counterexample to the Petersen coloring conjecture

Abstract

The Petersen coloring conjecture of Jaeger asserts that every bridgeless cubic graph admits a Petersen coloring. Recently, Putman presented an explicit counterexample on $112$ vertices and verified its non-colorability by showing, using a SAT solver, that an instance with $3640$ variables and $68324$ clauses is unsatisfiable. We give a short human-checkable proof that this graph is indeed a counterexample. Our proof determines the coloring behavior of the multipoles used in the construction by means of small explicit finite case analyses and reduces the final contradiction to a simple structural property of the line graph of the Petersen graph. Besides providing a proof that does not rely on a large SAT computation, our approach gives further insight into the gadgets underlying the construction.