Exact Formulations for the AVD-Total Coloring Problem on Fullerene Graphs

This paper studies the Adjacent-Vertex-Distinguishing Total Coloring (AVD) problem on fullerene graphs. We propose two exact integer programming formulations: a \textit{Diff} model, which compares incident color sets componentwise, and a \textit{Big-\(M\)} model, which represents each incident color set by an auxiliary integer and linearizes the resulting disjunction.
The formulations are evaluated under pure branch-and-bound and strengthened branch-and-cut settings, combining callback cuts with theoretical lower bound.
Computational experiments on the complete benchmark of \(22{,}430\) fullerene instances up to \(68\) vertices show that the strengthened Big-\(M\) formulation certifies optimality for all instances within a 60-second time limit.
Since fullerenes are cubic and the lower bound is five, every five-color solution proves optimality. 
Consequently, the experiments provide an exhaustive computational verification, over the tested universe, that Hulgan's conjecture holds for all considered fullerene graphs.