Kruskal's Algorithm for Minimum Spanning Forest

Maximilian P. L. Haslbeck 🌐, Peter Lammich 🌐 and Julian Biendarra

February 14, 2019

This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.

Abstract

This Isabelle/HOL formalization defines a greedy algorithm for finding a minimum weight basis on a weighted matroid and proves its correctness. This algorithm is an abstract version of Kruskal's algorithm. We interpret the abstract algorithm for the cycle matroid (i.e. forests in a graph) and refine it to imperative executable code using an efficient union-find data structure. Our formalization can be instantiated for different graph representations. We provide instantiations for undirected graphs and symmetric directed graphs.

License

BSD License

Topics

Session Kruskal

Depends on

Cite

× 
@article{Kruskal-AFP,
  author  = {Maximilian P. L. Haslbeck and Peter Lammich and Julian Biendarra},
  title   = {Kruskal's Algorithm for Minimum Spanning Forest},
  journal = {Archive of Formal Proofs},
  month   = {February},
  year    = {2019},
  note    = {\url{https://isa-afp.org/entries/Kruskal.html},
             Formal proof development},
  ISSN    = {2150-914x},
}
Download

Download

× Download latest

Older releases: