Abstract
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 \(1 - (1 - 1/k)^k\), and hence the standard \(1 - 1/e\) 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.
License
Note
Generative AI tools, including ChatGPT, were used during the development process for brainstorming, proofreading, code-organization suggestions, and local Isabelle proof-engineering assistance. All definitions, theorem statements, proofs, and documentation were reviewed, edited, and mechanically checked by the author, who takes full responsibility for the content of the submission.
Topics
- Computer science/Algorithms/Approximation
- Computer science/Algorithms/Optimization
- Computer science/Algorithms/Mathematical
Related publications
- Nemhauser, G. L., Wolsey, L. A., & Fisher, M. L. (1978). An analysis of approximations for maximizing submodular set functions—I. Mathematical Programming, 14(1), 265–294. https://doi.org/10.1007/bf01588971
- Minoux, M. Accelerated greedy algorithms for maximizing submodular set functions. Optimization Techniques, 234–243. https://doi.org/10.1007/bfb0006528
Session Submodular_Greedy
- Submodular_Base
- Greedy_Submodular_Construct
- Lazy_Greedy_Oracle
- Lazy_Greedy_Stateful
- Greedy_Step_Spec
- Greedy_Submodular_Approx
- Lazy_Greedy_Stateful_StepSpec
- Lazy_Greedy_Stateful_Approx