2021/10/02 by van Hulst, Allan
#05C20 #Combinatorics (math.CO) #FOS: Mathematics
paper · doi:10.48550/arxiv.2110.00789
A directed graph D=(V(D),A(D)) has a kernel if there exists an independent set K⊆ V(D) such that every vertex v∈ V(D)-K has an ingoing arc u\mathbin\longrightarrowv for some u∈ K. There are directed graphs that do not have a kernel (e.g. a 3-cycle). A quasi-kernel is an independent set Q such that every vertex can be reached in at most two steps from Q. Every directed graph has a quasi-kernel. A conjecture by P.L. Erdős and L.A. Székely (cf. A. Kostochka, R. Luo, and, S. Shan, arxiv:2001.04003v1, 2020) postulates that every source-free directed graph has a quasi-kernel of size at most |V(D)|/2, where source-free refers to every vertex having in-degree at least one. In this note it is shown that every source-free directed graph that has a kernel also has a quasi-kernel of size at most |V(D)|/2, by means of an induction proof. In addition, all definitions and proofs in this note are formally verified by means of the Coq proof assistant.