Email Gateway (Jun 29 2026 at 11:45): Email Gateway (Jun 29 2026 at 11:45):From: Tobias Nipkow <nipkow@in.tum.de>
Subject: [isabelle] New in the AFP: Greedy Algorithms for Cardinality-Constrained Submodular Maximization
Greedy Algorithms for Cardinality-Constrained Submodular Maximization
Feier Lyu
This entry formalizes greedy algorithms for monotone non-negative submodular
maximization under a cardinality constraint on a finite ground set in
Isabelle/HOL. The main result is the classical Nemhauser--Wolsey--Fisher
approximation guarantee for deterministic greedy: after k-steps, the greedy
solution satisfies the finite-step bound ..., and hence the standard ...
approximation ratio. The development separates the executable greedy
construction, an abstract step-specification interface, and the approximation
proof. The entry also includes a verified stateful lazy greedy variant based on
cached upper bounds for marginal gains. The formalization proves that the lazy
implementation selects a valid greedy element at each iteration and therefore
inherits the same approximation guarantee. The result is intended as reusable
Isabelle infrastructure for later formal developments on submodular maximization
algorithms.
https://isa-afp.org/entries/Submodular_Greedy.html
Enjoy!
Last updated: Jul 02 2026 at 07:34 UTC