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.

License

BSD License

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

Related publications

Session Approximation_Algorithms

Cite

× 
@article{Approximation_Algorithms-AFP,
  author  = {Robin Eßmann and Tobias Nipkow and Simon Robillard and Ujkan Sulejmani},
  title   = {Verified Approximation Algorithms},
  journal = {Archive of Formal Proofs},
  month   = {January},
  year    = {2020},
  note    = {\url{https://isa-afp.org/entries/Approximation_Algorithms.html},
             Formal proof development},
  ISSN    = {2150-914x},
}
Download

Download

× Download latest

Older releases: