A Formal Analysis of Algorithms for Matroids and Greedoids

TL;DR

This paper provides a formal Isabelle/HOL analysis of algorithms for matroids and greedoids, including implementations of classical algorithms like Kruskal's and Prim's, advancing formal verification in combinatorial optimization.

Contribution

First formalisation of results on greedoids and extension of matroid formalisation, including verified implementations of key optimization algorithms.

Findings

Formalised analysis of algorithms for matroids and greedoids

Verified implementations of Kruskal's, Prim's, and maximum matching algorithms

First formalisation of results on greedoids in Isabelle/HOL

Abstract

We present a formal analysis, in Isabelle/HOL, of optimisation algorithms for matroids, which are useful generalisations of combinatorial structures that occur in optimisation, and greedoids, which are a generalisation of matroids. Although some formalisation work has been done earlier on matroids, our work here presents the first formalisation of results on greedoids, and many results we formalise in relation to matroids are also formalised for the first time in this work. We formalise the analysis of a number of optimisation algorithms for matroids and greedoids. We also derive from those algorithms executable implementations of Kruskal's algorithm for minimum spanning trees, an algorithm for maximum cardinality matching for bi-partite graphs, and Prim's algorithm for computing minimum weight spanning trees.