拟阵与贪婪体算法的形式化分析
计算机科学中的逻辑
2025-07-01 v2 数据结构与算法
最优化与控制
摘要
我们在 Isabelle/HOL 中对拟阵和贪婪体的优化算法进行了形式化分析。拟阵是优化中出现的组合结构的有用推广，而贪婪体是拟阵的推广。尽管早期已有一些关于拟阵的形式化工作，但我们在此的工作首次对贪婪体的结果进行了形式化，并且我们在本文中形式化的许多关于拟阵的结果也是首次被形式化。我们对拟阵和贪婪体的多种优化算法进行了形式化分析。我们还从这些算法中推导出了可执行的实现，包括用于最小生成树的 Kruskal 算法、用于二部图最大基数匹配的算法，以及用于计算最小权重生成树的 Prim 算法。
关键词
引用
@article{arxiv.2505.19816,
title = {A Formal Analysis of Algorithms for Matroids and Greedoids},
author = {Mohammad Abdulaziz and Thomas Ammer and Shriya Meenakshisundaram and Adem Rimpapa},
journal= {arXiv preprint arXiv:2505.19816},
year = {2025}
}