Kernels and Small Quasi-Kernels in Digraphs

TL;DR

This paper proves that source-free directed graphs with kernels have small quasi-kernels, and verifies the proofs using the Coq proof assistant, contributing to the understanding of kernels and quasi-kernels in digraphs.

Contribution

It establishes that such graphs possess quasi-kernels of size at most half the vertices, and formalizes the proofs in Coq, advancing the theoretical understanding and verification of digraph properties.

Findings

Source-free directed graphs with kernels have small quasi-kernels.

All proofs are formally verified using Coq.

The result supports the conjecture on quasi-kernels in source-free digraphs.

Abstract

A directed graph $D=(V(D),A(D))$ has a kernel if there exists an independent set $K\subseteq V(D)$ such that every vertex $v\in V(D)-K$ has an ingoing arc $u\mathbin{\longrightarrow}v$ for some $u\in 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\H{o}s and L.A. Sz\'ekely (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.