Proofs by Transformation in Extremal Graph Theory

A graph is a mathematical model representing binary relationships between
elements of a set. It is composed of two sets: the set of the elements called
the vertices and a set of pairs of vertices called the edges. Graphs appear in
many fields from computer networks to chemistry and even scheduling.

Often, problems about graphs consist in finding the best possible structure to
reduce costs or optimize performance. The best structure is the one that
maximizes or minimizes some measure called a graph invariant. These problems
are usually solved using heuristics that will try to find a good enough
solution because finding the best solution is time-consuming. Extremal graph
theory, instead of using heuristics, uses formal proofs to show that specific
structures, called extremal graphs, are indeed the ones that reach the
extremum value for an invariant given some constraints.

The process of finding those extremal graphs can benefit from computer software
that produce candidates in order to help researchers. Those candidates then
need to be studied, and a formal proof has to be written to show that they are
indeed extremal graphs. However, there are no software that aim to help
researchers with the writing of a proof.

In this work, we focus on a type of proof called the proof by transformation.
It consists in showing that, any graph that is not an extremal graph can be
transformed, using a chosen set of transformations, into a graph whose
invariant value is closer to that of the extremum.

We study the possibility of using computers to generate transformations for
huge amount of small graphs in order to provide insight about these
transformations and their impact on graph invariants. This method, combined
with theoretical and technical optimizations, led to the implementation of a
tool that has been successfully used in actual research, helping in the writing
of proofs by transformation for actual problems in extremal graph theory as
well as producing conjectures about the impact of some transformations on the
value of graph invariants.