Verified Approximation Algorithms

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

January 16, 2020

Abstract

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. A detailed description of our work (excluding center selection) has been published in the proceedings of IJCAR 2020.
BSD License

Change history

June 29, 2021

added theory Center_Selection by Ujkan Sulejmani

February 8, 2021

added theory Approx_SC_Hoare (Set Cover) by Robin Eßmann

Topics

Theories of Approximation_Algorithms