Logical Methods in Computer Science (Mar 2022)

Verified Approximation Algorithms

  • Robin Eßmann,
  • Tobias Nipkow,
  • Simon Robillard,
  • Ujkan Sulejmani

DOI
https://doi.org/10.46298/lmcs-18(1:36)2022
Journal volume & issue
Vol. Volume 18, Issue 1

Abstract

Read online

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.

Keywords