We prove that every cyclically 4-edge-connected cubic graph that can be embedded in the torus, with the exception of two specific infinite families of “Petersen-like” graphs, is 3-edge-colorable. This shows that every toroidal snark can be obtained from several copies of the Petersen graph using the dot product operation. The first two snarks in this family are the Petersen graph and one of the Blanuša snarks; the rest were exposed by Belcastro and Kaminski and by Vodopivec. This proves a strengthening of the well-known, long-standing conjecture of Grünbaum from 1968.

Abstract. We show that any planar graph [Formula: see text] has a 5-coloring such that one color class contains at most [Formula: see text] vertices. In other words, there exists a partition of [Formula: see text] into five independent sets [Formula: see text] such that [Formula: see text]. Our proof yields an [Formula: see text]-time algorithm to find such a partition, and unlike the Four Color Theorem, our proof is fully verifiable without computer assistance.

We prove that every cyclically 4-edge-connected cubic graph that can be embedded in the projective plane, with the single exception of the Petersen graph, is 3-edge-colorable. In other words, the only (nontrivial) snark that can be embedded in the projective plane is the Petersen graph. This implies that a 2-connected cubic (multi)graph that can be embedded in the projective plane is not 3-edge-colorable if and only if it can be obtained from the Petersen graph by replacing each vertex by a 2-edge-connected planar cubic (multi)graph. Here, a replacement of a vertex$v$in a cubic graph$G$is the operation that takes a 2-connected planar (cubic) multigraph$H$containing some vertex$u$of degree 3, unifying$G-v$and$H-u$, and connecting the vertices in$N_{G}[v]$in$G-v$with the three neighbors of$u$in$H-u$with 3 edges. Any graph obtained in such a way is said to be Petersen-like. This result is a nontrivial generalization of the Four Color Theorem, and its proof requires a combination of extensive computer verification and computer-free extension of existing proofs on colorability. Using this result, we obtain the following algorithmic consequence. Input: A cubic graph$G$. Output: Either a 3-edge-coloring of$G$, an obstruction showing that$G$is not 3-edge-colorable, or the conclusion that$G$cannot be embedded in the projective plane (certified by exposing a forbidden minor for the projective plane contained in$G$). Time complexity:$O(n^{2})$, where$n=\vert V(G)\vert$. An unexpected consequence of this result is a coloring-flow duality statement for the projective plane: A cubic graph embedded in the projective plane is 3-edge-colorable if and only if its dual multigraph is 5-vertex-colorable. Moreover, we show that a 2-edge connected graph embedded in the projective plane admits a nowhere-zero 4-flow unless it is Petersen-like (in which case it does not admit nowhere-zero 4-flows). This proves a strengthening of the Tutte 4-flow conjecture for graphs on the projective plane. Some of our proofs require extensive computer verification. The necessary source codes, together with the input and output files and the complete set of more than 5000 reducible configurations, are available on Github11https://github.com/edge-coloring. Refer to the “README.md” file in each directory for instructions on how to run each program. which can be considered as an addendum to this paper. Moreover, we provide pseudocodes for all our computer verifications.