A Constructive Formalization of the Weak Perfect Graph Theorem

TL;DR

This paper develops a formal, constructive proof of the Weak Perfect Graph Theorem within the Coq proof assistant, modeling finite graphs and their properties to facilitate rigorous formal reasoning.

Contribution

It introduces a formal framework for finite simple graphs in Coq and provides a constructive formalization of the Weak Perfect Graph Theorem using this framework.

Findings

Formal framework for finite graphs in Coq

Constructive proof of the Weak Perfect Graph Theorem

Modeling of graph expansions and Lovász Replication Lemma

Abstract

The Perfect Graph Theorems are important results in graph theory describing the relationship between clique number $\omega(G) $ and chromatic number $\chi(G) $ of a graph $G$. A graph $G$ is called \emph{perfect} if $\chi(H)=\omega(H)$ for every induced subgraph $H$ of $G$. The Strong Perfect Graph Theorem (SPGT) states that a graph is perfect if and only if it does not contain an odd hole (or an odd anti-hole) as its induced subgraph. The Weak Perfect Graph Theorem (WPGT) states that a graph is perfect if and only if its complement is perfect. In this paper, we present a formal framework for working with finite simple graphs. We model finite simple graphs in the Coq Proof Assistant by representing its vertices as a finite set over a countably infinite domain. We argue that this approach provides a formal framework in which it is convenient to work with different types of graph constructions (or expansions) involved in the proof of the Lov\'{a}sz Replication Lemma (LRL), which is also the key result used in the proof of Weak Perfect Graph Theorem. Finally, we use this setting to develop a constructive formalization of the Weak Perfect Graph Theorem.