Commit 0fba3825 authored by nipkow's avatar nipkow
Browse files

added set cover by Robin Essman

parent 07ea995a6665
......@@ -7419,9 +7419,11 @@ date = 2020-01-16
notify = nipkow@in.tum.de
abstract =
We present the first formal verification of approximation algorithms
for NP-complete optimization problems: vertex cover, independent set,
for NP-complete optimization problems: vertex cover, set cover, independent set,
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 has been published in the proceedings of
<a href="https://doi.org/10.1007/978-3-030-51054-1_17">IJCAR 2020</a>.
 
[Diophantine_Eqns_Lin_Hom]
title = Homogeneous Linear Diophantine Equations
......
......@@ -4,7 +4,7 @@ theory Approx_LB_Hoare
imports Complex_Main "HOL-Hoare.Hoare_Logic"
begin
text \<open>This is formalization of the load balancing algorithms and proofs
text \<open>This is a formalization of the load balancing algorithms and proofs
in the book by Kleinberg and Tardos \cite{KleinbergT06}.\<close>
hide_const (open) sorted
......
......@@ -7,6 +7,7 @@ session Approximation_Algorithms (AFP) = HOL +
"HOL-Hoare"
theories
Approx_VC_Hoare
Approx_SC_Hoare
Approx_MIS_Hoare
Approx_LB_Hoare
Approx_BP_Hoare
......
@string{Springer="Springer"}
@string{LNCS="LNCS"}
@inproceedings{EssmannNR-IJCAR20,
author={Robin E{\ss}mann and Tobias Nipkow and Simon Robillard},
title={Verified Approximation Algorithms},
booktitle={Automated Reasoning (IJCAR 2020)},
editor={N. Peltier and V. Sofronie-Stokkermans},publisher={Springer},
series={LNCS},volume={12167},pages={12167},year=2020,
note={\url{https://doi.org/10.1007/978-3-030-51054-1_17}}}
@inproceedings{BerghammerM03,
author = {Rudolf Berghammer and Markus M{\"{u}}ller{-}Olm},
title = {Formal Development and Verification of Approximation Algorithms Using
......
......@@ -18,9 +18,11 @@
\begin{abstract}
We present the first formal verifications of approximation algorithms
for NP-complete optimization problems:
vertex cover, independent set, load balancing, and bin packing.
vertex cover, set cover, independent set, load balancing, and bin packing.
The proofs correct incompletnesses in existing proofs
and improve the approximation ratio in one case.
A detailed description of our work has been published in the proceedings of
\emph{IJCAR 2020} \cite{EssmannNR-IJCAR20}.
\end{abstract}
\tableofcontents
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment