There are finitely many $5$-vertex-critical $(P_6,\text{bull})$-free graphs
Yiao Ju, Jorik Jooken, Jan Goedgebeur, Shenwei Huang
TL;DR
The paper addresses certifying $4$-colourability in $(P_6, ext{bull})$-free graphs by proving there are only finitely many $5$-vertex-critical graphs in this class. It combines a computer-assisted generation framework for $k$-vertex-critical $ ext{H}$-free graphs with a detailed structural analysis centered on homogeneous $C_5$ to bound the graph size and classify the base cases. The main contribution is establishing finiteness of the target family, which implies a polynomial-time certifying algorithm that returns either a $4$-colouring or a small induced subgraph serving as a certificate of non-$4$-colourability. This certifying approach enhances reliability of $4$-colouring decision procedures in this graph class and provides a constructive proof via finite witnesses and substitutions.
Abstract
In this paper, we are interested in $4$-colouring algorithms for graphs that do not contain an induced path on $6$ vertices nor an induced bull, i.e., the graph with vertex set $\{v_1,v_2,v_3,v_4,v_5\}$ and edge set $\{v_1v_2,v_2v_3,v_3v_4,v_2v_5,v_3v_5\}$. Such graphs are referred to as $(P_6,\text{bull})$-free graphs. A graph $G$ is \emph{$k$-vertex-critical} if $χ(G)=k$, and every proper induced subgraph $H$ of $G$ has $χ(H)<k$. In the current paper, we investigate the structure of $5$-vertex-critical $(P_6,\text{bull})$-free graphs and show that there are only finitely many such graphs, thereby answering a question of Maffray and Pastor. A direct corollary of this is that there exists a polynomial-time algorithm to decide if a $(P_6,\text{bull})$-free graph is $4$-colourable such that this algorithm can also provide a certificate that can be verified in polynomial time and serves as a proof of 4-colourability or non-4-colourability.
