Verification of the Total Coloring Conjecture for small graphs

One of the most famous open problem in Graph Theory is the Total Coloring Conjecture. For a total coloring we color all vertices and edges of a graph, such that no adjacent vertices, no adjacent edges and no edge and one of its endpoints have the same color. The conjecture claims that any graph $G$ has a total coloring using $\Delta(G) + 2$ differen colors, where $\Delta(G)$ is the maximum degree of a vertex in $G$. Despite being more than 60 years old, it has only been proven in some restricted cases, for example in (Kostochka, 1996) for graphs with $\Delta(G) \leq 5$.

Recently Markus Kirchweger, Tomáš Peitl and Stefan Szeider sucessfully used their SAT Modulo Symmetry solver smsg to disprove the existence of small counter-examples for similar conjectures as this publication list demonstrates. As described in this paper, the solver directly integrates symmetry breaking into a custom state of the art QBF solver to efficiently deal with any coNP complete constraints. This allows the easy encoding of properties like being an unsatisfiable SAT instance or not having a total coloring with $k$ colors, which unless $NP = coNP$ would require exponentially many constraints in standard CNF. While this could also be done using general QBF solvers like caqe, their SAT Modulo Symmetry solver drastically outperforms standard QBF solvers in its domain of problems.

Here we use the smsg solver via the PySMS API to search for small counter examples for the Total Coloring Conjecture. In qbf.py a straight forward encoding of the problem is implemented, allowing the user with python3 qbf.py [n] to search for counter examples with $n$ vertices. Since the graph is not required to be connected, if the solver finds no counter example with $n$ vertices, there can't also be one with $< n$ vertices. Using a AMD Ryzen 7735HS, we can prove the Total Coloring conjecture for all graphs with $n \leq 13$ in $3$ minutes and for $n \leq 14$ in $68$ minutes.

(c) Mia Müßig