Verified Approximation Algorithms

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

January 16, 2020


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


June 29, 2021
added theory Center_Selection by Ujkan Sulejmani
February 8, 2021
added theory Approx_SC_Hoare (Set Cover) by Robin Eßmann


Session Approximation_Algorithms