Verified Approximation Algorithms

Robin Eßmann 📧, Tobias Nipkow 🌐, Simon Robillard 🌐 and Ujkan Sulejmani

January 16, 2020

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


We present the first formal verification of approximation algorithms for NP-complete optimization problems: vertex cover, set cover, independent set, center selection, load balancing, and bin packing. The proofs correct incompletenesses in existing proofs and improve the approximation ratio in one case.
BSD License


Theories of Approximation_Algorithms