Verified Approximation Algorithms
Robin E{\ss}mann, Tobias Nipkow, Simon Robillard, Ujkan Sulejmani
TL;DR
This paper provides the first formal verification of approximation algorithms for several NP-complete problems, identifying proof gaps and improving ratios through invariant-based proofs.
Contribution
It introduces a formal verification framework for approximation algorithms and corrects and enhances existing proofs for multiple NP-complete problems.
Findings
Identified incompleteness in previous proofs
Verified approximation ratios for several problems
Improved approximation ratio for one problem
Abstract
We present the first formal verification of approximation algorithms for NP-complete optimization problems: vertex cover, independent set, set cover, center selection, load balancing, and bin packing. We uncover incompletenesses in existing proofs and improve the approximation ratio in one case. All proofs are uniformly invariant based.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.