Verified Approximation Algorithms
 1 Citations
 202 Downloads
Abstract
We present the first formal verification of approximation algorithms for NPcomplete optimization problems: vertex cover, independent set, load balancing, and bin packing. We uncover incompletenesses in existing proofs and improve the approximation ratio in one case.
1 Introduction
Approximation algorithms for NPcomplete problems [12] are a rich area of research untouched by automated verification. We present the first formal verifications of three classical and one lesser known approximation algorithm. Three of these algorithms had been verified on paper by program verification experts [3, 4]. We found that their claimed invariants need additional conjuncts before they are strong enough to be real invariants. That is, their proofs are incomplete. The fourth algorithm only comes with a sketchy informal proof.
the classic approximation algorithm for a minimal vertex cover is a kapproximation algorithm for rank k hypergraphs;
Wei’s algorithm for a maximal independent set [13] is a \(\Delta \)approximation algorithm for graphs with maximum degree \(\Delta \);
the greedy algorithm for the load balancing problem is a \(\frac{3}{2}\)approximation algorithm if job loads are sorted and a 2approximation algorithm if job loads are unsorted [8];
the bin packing algorithm by Berghammer and Reuter [4] is a \(\frac{3}{2}\)approximation algorithm.
Isabelle not only helped finding mistakes in penandpaper proofs but also encouraged proof refactoring that led to simpler proofs, and in one case, to a stronger result: The invariant given by Berghammer and Müller for Wei’s algorithm [3] is sufficient to show that the algorithm has an approximation ratio of \(\Delta + 1\). We managed to simplify their argument significantly which lead to an improved approximation ratio of \(\Delta \).
All algorithms are expressed in a simple imperative WHILElanguage. In each case we show that the approximation algorithm computes a valid solution that is at most a constant factor worse than an optimum solution. The polynomial running time of the approximation algorithm is easy to see in each case.
2 Isabelle/HOL and Imperative Programs
Isabelle/HOL is largely based on standard mathematical notation but with some differences and extensions.
Type variables are denoted by \({^\prime {a}}, {^\prime {b}}\), etc. The notation t :: \(\tau \) means that term t has type \(\tau \). Except for function types \({^\prime {a}} \Rightarrow {^\prime {b}}\), type constructors follow postfix syntax, e.g. \({^\prime {a}}\) set is the type of sets of elements of type \({^\prime {a}}\). Function some :: \({{^\prime {a}} \, set \Rightarrow {^\prime {a}}}\) picks an arbitrary element from a set; the result is unspecified if the set is empty.
The types nat and real represent the sets \(\mathbb {N}\) and \(\mathbb {R}\). In this paper we drop the coercion function real :: nat \(\Rightarrow \) real. The set \(\{m..n\}\) is the closed interval [m, n].
The box around the program means that it has been verified. All our proofs employ a VCG and essentially reduce to showing the preservation of the invariants.
3 Vertex Cover
\(vc\; {:}{:} \;{^\prime {a}} \; set \; set \Rightarrow {^\prime {a}} \; set \; \Rightarrow \;bool\)
\(vc\; E\; C\; = (\forall \; e\!\in \!{E}. \; e \cap C \ne \emptyset )\)
\(finite\ C\ \wedge \ matching\ M\ \wedge \ M\ \subseteq \ E \ \wedge \ vc\ E\ C\ \longrightarrow \ M \le C\)
We fix a rankk hypergraph \(E \;{:}{:} \; {^\prime {a}} \ set\ set\) assuming \(\emptyset \notin E\), \(finite\ E\) and \(e\ \in \ E\ {\longrightarrow }\ finite\ e\ \wedge \ e \le k\).
\(invar \;{:}{:}\;{^\prime {a}} \ set\ \Rightarrow \ {^\prime {a}} \ set \ set\ \Rightarrow \ bool\)
 \(invar \ C\ F\ =\)$${}(F \ \subseteq \ E\ \wedge \ vc\ (E\ \ F)\ C\ \wedge \ finite\ C\ \wedge \ (\exists \ M .\ {inv}\_{matching} \ C\ F\ M))$$
\({inv}\_{matching}\ C\ F\ M\ =\) \((matching\ M\ \wedge \ M\ \subseteq \ E\ \wedge \ C\ \le \ k\ *\ M\ \wedge \ (\forall \ e\!\in \!{M}.\ \forall {f}\!\in \!{F}.\ e\ \cap \ f\ =\ \emptyset ))\)
The key step in the program proof is that the invariant is invariant:
Lemma 1
\(F \ne \emptyset \ \wedge \ invar\ C\ F\ \longrightarrow \)
\(invar\ (C\ \cup \ some\ F)\ (F  \{e{^\prime } \in F\ \ some\ F \ \cap \ e{^\prime }\ \ne \ \emptyset \})\)
Our invariant is stronger than the one in [3] which lacks \(F \subseteq E\). But without \(F \subseteq E\) the claimed invariant is not invariant (as acknowledged by MüllerOlm).
4 Independent Set
As in the previous section, a graph is a set of edges. An independent set of a graph E is a subset of its vertices such that no two vertices are adjacent.

\(iv\ {:}{:}\ {^\prime {a}}\ set\ set\ \Rightarrow \ {^\prime {a}}\ set\ \Rightarrow \ bool\)

\(iv\ E\ S\ =\ (S\ \subseteq \ \bigcup \ E\ \wedge \ (\forall \ {v}_{1} \ {v}_{2}.\ {v}_{1} \ \in \ S\ \wedge \ {v}_{2} \ \in \ S\ \longrightarrow \ \{ {v}_{1},\ {v}_{2}\} \ \notin \ E))\)
\(inv\_{iv} \;{:}{:}\ {^\prime {a}}\ set\ \Rightarrow \ {^\prime {a}}\ set\ \Rightarrow \ bool\)
\(inv\_{iv}\ S\ X\ = \)
\((iv\ E\ S \wedge \ X \subseteq V \wedge \ (\forall {v}_{1}\!\in \!V\ \ X.\ \forall {v}_{2}\!\in \!S.\ \{{v}_{1},\ {v}_{2} \}\ \notin \ E)\ \wedge \ S\ \subseteq \ X)\)
This invariant is taken almost verbatim from [3], except that in [3] it says that S is an independent set of the subgraph generated by X. This is later used to show that the x picked at each iteration from \(V  X\) is not already in S. Defining subgraphs adds unnecessary complexity to the invariant. We simply state \(S \subseteq X\), together with the fact that S is an independent set of the whole graph.
We now extend the invariant with properties of the auxiliary variable P.

\(inv\_{partition}\ {:}{:}\ {^\prime {a}}\ set\ \Rightarrow \ {^\prime {a}}\ set\ \Rightarrow \ {^\prime {a}}\ set\ set\ \Rightarrow \ bool\)

\(inv\_{partition}\ S\ X\ P\ =\)
\((inv\_{iv}\ S\ X\ \wedge \)
\(\bigcup \; P = X \wedge \ (\forall \;{p}\!\in \!{P}.\; \exists \,{s}\!\in \!{V}.\; p = \{s\} \ \cup \ neighbors\ s) \ \wedge \ P\ =\ S\ \wedge \ finite\ P)\)
We can view the set P as an auxiliary program variable. In order to satisfy the invariant, P would be initially empty and the loop body would include the assignement \(P := P \cup \{neighbors \ x \ \cup \ \{x \}\}\). Intuitively, P contains the sets of vertices that are added to X at each iteration (or more precisely, an overapproximation, since some vertices in \(neighbors\ x\) may have been added to X in a previous iteration). Instead of adding an unnecessary variable to the program, we only use the existentially quantified invariant. The assignments described above correspond directly to instantiations of the quantifier that are needed to solve proof obligations. This is illustrated with the following lemma, which corresponds to the preservation of the invariant:
Lemma 2
\({(\exists \,{P}.\ inv\_{partition}\ S\ X\ P) \wedge x \in V  X \longrightarrow }\) \((\exists \,{P}{^\prime }.\ inv\_{partition}\ (S\ \cup \ \{x\})\ (X\ \cup \ neighbors \ x\ \cup \ \{x\})\ P{^\prime )}\)
The existential quantifier in the antecedent yields a witness P. After instantiating the quantifier in the succedent with \(P \cup \{neighbors\ x\ \cup \ \{x\}\}\), the goal can be solved straightforwardly. Finally, the following lemma combines the invariant and the negated postcondition to prove the approximation ratio:
Lemma 3
\(inv\_{partition}\ S\ V\ P\ \longrightarrow \ (\forall {S}{^\prime }.\ iv\ E\ S{^\prime }\ \longrightarrow \ S{^\prime }\ \le \ S\ *\ \Delta )\)
To prove it, we observe that any set \(p \in P\) consists of a vertex x and its neighbors, therefore an independent set \(S{^\prime }\) can contain at most \(\Delta \) of the vertices in p, thus \(S{^\prime } \le P *\Delta \). Furthermore, as indicated by the invariant, \(P\ =\ S\).
Compared to the proof in [3], our invariant describes the contents of the set P more precisely, and thus yields a better approximation ratio. In [3], the invariant merely indicates that \(X = \bigcup \; P\), together with two cardinality properties: \(\forall {p}\!\in \!{P}.\ p \le \Delta + {1}\) and \(P \le S\). Taken with the negated postcondition, this invariant can be used to show that for any independent set \(S{^\prime }\), we have \(S{^\prime } \le S *(\Delta \ +{1})\). The proof of this lemma makes use of the following (in)equalities: \(S{^\prime } \le V, V\ = \bigcup \; P\), \(\bigcup \; P \le P *(\Delta \ +{1})\) and finally \(P *(\Delta \ +{1}) \le S *(\Delta \ +{1})\). Note that this only relies on the trivial fact that an independent set cannot contain more vertices than the graph. By contrast, our own argument takes into account information regarding the edges of the graph.
Although this proof results in a weaker approximation ratio than our own, it yields a useful insight: an approximation ratio is given by the cardinality of the largest set \(p\!\in \!P\) (i.e., the largest number of vertices added to X during any given iteration). In the worst case, this is equal to \(\Delta \ +{1}\), but in practice the number may be smaller. This suggests a variant of the algorithm that stores that value in a variable r, as described in [3]. At every iteration, the variable r is assigned the value \(max\ r\ \{x\}\ \cup \ neighbors\ x\ \ X\). Ultimately, the algorithm returns both the independent set S and the value r, with the guarantee that \(S{^\prime }\ \le \ S\ *\ r\) for any independent set \(S{^\prime }\).
We also formalized this variant and proved the aforementioned property. The proof follows the idea outlined above, but does away with the variable P entirely: instead, the invariant simply maintains that \(inv\_{iv}\ S\ X \wedge X \le S *r\), and the proof of preservation is adapted accordingly. Indeed, this demonstrates that the argument used in [3] does not require an auxiliary variable nor an existentially quantified invariant. For the proof of the approximation ratio \(\Delta \), a similar simplification is not as easy to obtain, because the argument relies on a global property of the graph (a constraint that edges impose on independent sets) that is not easy to summarize in an inductive invariant.
So far, we have only considered an algorithm where the vertex x is picked nondeterministically. An obvious heuristic is to pick, at every iteration, the vertex with the smallest number of neighbors among \(V  X\). Halldórsson and Radhakrishnan [7] prove that this heuristic achieves an approximation ratio of \((\Delta \ +{2})\ / \ {3}\). However their proof is far more complex than the arguments presented here. It is also not given as an inductive invariant, instead relying on case analysis for different types of graphs. This is beyond the scope of our paper.
5 Load Balancing
\({lb\ {:}{:}\ (nat\ \Rightarrow \ nat)\ \Rightarrow \ (nat\ \Rightarrow \ nat\ set)\ \Rightarrow \ nat\ \Rightarrow \ bool}\)
\({lb\ T\ A\ j\ =}\)
\(((\forall {x}\!\in \{1..m\}.\ \forall {y}\in \{1..m\}.\ x \ne y\ \longrightarrow \ A\ x\ \cap \ A\ y\ =\ \emptyset )\ \wedge \)
\(\; {(\bigcup _{x\in \{1..m\}}\ A\ x)\ =\ \{1..j\}\ \wedge \ (\forall {x}\!\in \! \{1..m\}.\ (\sum {y}\!\in \!{A}\ x.\ t\ y)\ =\ T\ x))}\)
\(makespan \ {:}{:}\ (nat\ \Rightarrow \ nat)\ \Rightarrow \ nat\)
\(makespan\ T = Max\ (T\ `\{1..m\})\)
\(min_{k}\ {:}{:}\ (nat\ \Rightarrow \ nat)\ \Rightarrow \ nat\ \Rightarrow \ nat\)
\(min_{k}\ T\ 0 \ =\ 1\)
\(min_{k} \ T\ (x\ +1)\ =\)
\(({{\textsf {\textit{let}}}}\ k\ =\ min_{k}\ T\ x\ {{\textsf {\textit{in}}}}\ {{\textsf {\textit{if}}}}\ T\ (x + 1)\ <\ T\ k\ {{\textsf {\textit{then}}}}\ x\ + 1 \ {{\textsf {\textit{else}}}}\ k)\)
\(sorted\ {:}{:}\ nat\ \Rightarrow \ bool\)
\(sorted\ j\ =\ (\forall {x}\!\in \! \{1..j\}.\ \forall {y}\!\in \! \{1..x\}.\ t\ x \le t\ y)\)
Property \(sorted \ n\) is not part of the precondition because it is not influenced by the algorithm and thus there is no need to prove that it remains unchanged. Therefore we made \(sorted \ n\) an assumption of the whole Hoare triple. The notation \(f(a := b)\) denotes an updated version of function f that maps a to b and behaves like f otherwise. Thus an assignment \(f := f(i := b)\) is nothing but the conventional imperative array update notation \(f[i] := b\).
Functional correctness follows because each iteration extends a partial solution for j jobs to one for \(j +1\) jobs:
Lemma 4
\(lb\ T\ A\ j \wedge x \in \{1..m\} \longrightarrow \)
\(lb\ (T(x := T\ x + t\ (j\ +1 )))\ (A(x\ :=\ A\ x \cup \{j\ +1\}))\ (j\ +1)\)
Moreover, it is easy to see that the initialization establishes \(lb\ T\ A\ j\).
To prove the approximation factor in both the sorted and unsorted case, the following lower bound is important:
Lemma 5
\(lb\ T\ A\ j\ \longrightarrow \ (\sum _{x={1}}^{j}\ t\ x)\ / \ m \le makespan\ T\)
This is a result of \(\sum _{x = 1}^{m} T(x) = \sum _{x = 1}^{j} t(x)\) together with this general property of sums: \(finite\ A \wedge A \ne \emptyset \longrightarrow (\sum {a}\!\in \!{A}.\ f\ a) \le A *Max\ (f\ `\ A)\).
A similar observation applies to individual jobs. Any job must be a lower bound on some machine, as it is assigned to one and, by extension, it must also be a lower bound of the makespan:
Lemma 6
\(lb\ T\ A\ j \longrightarrow Max_{0}\ (t ` \{1..j\}) \le makespan\ T\)
As any job load is a lower bound on the makespan over the machines, the job with maximum load must also be such a lower bound. Note that \(Max_{0}\) returns 0 for the empty set.
When jobs are sorted in descending order, a stricter lower bound for an individual job can be established. We observe that an added job is at most as large as the jobs preceding it. Therefore, if a machine contains at least two jobs, this added job is only at most half as large as the makespan. We can use this observation by assuming the machines to be filled with more than m jobs, as this will ensure that some machine must contain at least two jobs.
Lemma 7
\(lb\ T\ A\ j \wedge m\ <\ j \wedge sorted\ j \longrightarrow {2} *t\ j \le makespan\ T\)
Note that this lower bound only holds if there are strictly more jobs than machines. One must, however, also consider how the algorithm behaves in the other case. One may intuitively see that the algorithm will be able to distribute the jobs such that every machine will only have at most one job assigned to it, making the algorithm trivially optimal. To prove this, we need to show the following behavior of \(min_k\):
Lemma 8
 1.
\(x \in \{1..m\} \wedge T\ x = 0 \longrightarrow T\ (min_{k}\ T\ m)\ =\ {0}\)
 2.
\(x \in \{1..m\} \wedge T\ x = 0 \longrightarrow min_k\ T\ m \le x\)
They can be shown by induction on the number of machines m.
\(inv_{2} \ {:}{:}\ (nat\ \Rightarrow \ nat)\ \Rightarrow \ (nat\ \Rightarrow \ nat\ set)\ \Rightarrow \ nat\ \Rightarrow \ bool\)
\(inv_{2}\ T\ A\ j =\)
\((lb\ T\ A\ j \wedge j \le n \ \wedge \)
\(\;(\forall {T}\; {^\prime }\ A^\prime .\ lb\ T{^\prime }\ A^\prime \ j\ \longrightarrow \ makespan\ T \le 3\ / \ 2 *\ makespan \ T{^\prime }) \wedge \)
\(\;(\forall {x} \; >\ j.\ T\ x = 0) \wedge (j \le m \longrightarrow \ makespan\ T\ =\ Max_0 \ (t\ `\ \{1..j\})))\)
The final two conjuncts relate to the trivially optimal behavior of the algorithm if \({j\ \le \ m}\). The penultimate conjunct shows that only as many machines can be occupied as there are available jobs. The final conjunct ensures that every job is distributed on its own machine, making the makespan equivalent to the job with maximum load.
It should be noted that if the makespan is sufficiently large, an added job may not increase the makespan at all, as the machine with minimum load combined with the job may not exceed the previous makespan. As such, we will also consider the possibility that an added job can simply be ignored without affecting the overall makespan.
Lemma 9
\(makespan\ (T(x := T\ x + y)) \ne T\ x + y \longrightarrow \)
\(makespan\ (T(x := T\ x + y)) = makespan\ T\)
To make use of this observation, we need to be able to relate the makespan of a solution with the added job to the makespan of a solution without it. One can easily show the following by removing \(j + 1\) from the solution:
Lemma 10
\(lb\ T\ A\ (j + 1) \longrightarrow \)
\((\exists \,{T}{^\prime }\ A{^\prime }.\ lb\ T{^\prime }\ A{^\prime }\ j \wedge makespan\ T{^\prime } \le makespan\ T)\)
\(inv_1 \ T\ A\ j =\)
\((lb\ T\ A\ j \wedge j \le n \wedge (\forall \ {T}{^\prime }\ A{^\prime }.\ lb\ T{^\prime }\ A{^\prime }\ j \longrightarrow \ makespan\ T \le {2} \ *\ makespan \ T{^\prime }))\)
The proof for this invariant is a simpler version of the proof above: We do not need the initial case distinction (case \(j + 1 \le m\) need not be considered separately) and to prove the approximation factor we use Lemma 6 instead of Lemma 7 to obtain a bound for \(t(j + 1)\).
6 Bin Packing
We finally consider the linear time \(\frac{3}{2}\)approximation algorithm for the bin packing problem proposed by Berghammer and Reuter [4]. The bin packing problem is similar to the load balancing problem described in the previous section. The main distinction is that in the load balancing problem, the number of machines is fixed, while the load a single machine can hold is unbounded. With the bin packing problem, this is essentially reversed. The maximum capacity a single bin can hold is limited by some fixed c. However, we are free to use as many bins as necessary to achieve a solution. The goal is now to minimize this number of bins used instead of the maximum capacity of a bin.
For the bin packing problem we are given a finite, nonempty set of objects \(U\ {:}{:} \;{^\prime {a}} \ set\), whose weights are given by a function \(w\ {:}{:} \; {^\prime {a}} \Rightarrow real\). Note that in this paper nats are implicitly converted to reals if needed. The weight of an object in U is strictly greater than zero, but bounded by a maximum capacity \(c\ {:}{:} \ nat\). The abbreviation \(W(B) \equiv \sum _{u\in B}w(u)\) denotes the weight of a bin \(B \subseteq U\). The set U can also be separated into small and large objects. An object u is considered small if \(w(u) \le \frac{c}{2}\). An object is large if the opposite is the case. We will begin by assuming that all small objects in U can be found in a set S, and large objects in U can be found in a set L, such that \(S \cup L\ =\ U\) and \(S \cap L\ =\ \emptyset \). Of course L and S can also be computed from U in linear time. Variables U, w, c, L, and S are fixed throughout this section.
\(bp\ {:}{:}\; {^\prime {a}}\ set\ set\ \Rightarrow \ bool\)
\(bp\ P\ =\ (partition\_{o}n\ U\ P\ \wedge \ (\forall \ B\!\in \!P.\ W\ B \le c))\)
\([\![{\cdot }]\!]\ {:}{:}\; {^\prime {a}}\ set\ \Rightarrow \ {^\prime {a}} \ set\ set\)
\([\![{B}]\!]= ({{\textsf {\textit{if}}}}\ B\ = \emptyset \ {{\textsf {\textit{then}}}}\ \emptyset \ {{\textsf {\textit{else}}}}\ \{B\})\)
 Case 1. The object fits into \(B_1\):
\(inv_ 1 \ P_ 1 \ P_ 2 \ B_ 1 \ B_ 2 \ V \wedge u \in V \wedge W\ B_ 1 + w\ u \le c\ \longrightarrow \)
\(inv_ 1 \ P_ 1 \ P_ 2 \ (B_ 1 \cup \{u\})\ B_ 2\ (V  \{u\})\)
 Case 2. The object fits into \(B_ 2\):
\(inv_ 1\ P_ 1\ P_ 2\ B_ 1\ B_ 2\ V \wedge u \in V \wedge W\ B_ 2 + w\ u \le c\ \longrightarrow \)
\(inv_ 1\ (P_ 1 \cup [\![{B}_ 1]\!])\ P_ 2\ \emptyset \ (B_ 2 \cup \{u\})\ (V  \{u\})\)
 Case 3. The object fits into neither bin:
\(inv_ 1\ P_ 1\ P_ 2\ B_ 1\ B_ 2\ V \wedge u \in V \longrightarrow \)
\(inv_ 1\ (P_ 1 \cup [\![{B}_ 1 ]\!]) \ (P_ 2 \cup [\![{B}_ 2 ]\!]) \ \emptyset \ \{u\}\ (V \{u\})\)
\(inv_ 1\ P_ 1 \ P_ 2 \ B_ 1 \ B_ 2 \ V\ =\ bp\ (P_ 1 \cup [\![{B}_ 1]\!]\cup P_ 2 \cup [\![{B}_ 2 ]\!]\cup \{\{v\}\ \ v \in V\})\)
\(inv_ 1\ {:}{:}\; {^\prime {a}}\ set\ set\ \Rightarrow \ {^\prime {a}}\ set\ set\ \Rightarrow \ {^\prime {a}}\ set\ \Rightarrow \ {^\prime {a}}\ set\ \Rightarrow \ {^\prime {a}}\ set\ \Rightarrow \ bool\)
\(inv_ 1 \ P_ 1 \ P_ 2 \ B_ 1 \ B_ 2 \ V\ =\)
\((bp\ (P_ 1 \cup [\![{B}_ 1]\!]\cup P_ 2 \cup [\![{B}_ 2]\!]\cup \{\{v\}\ \ v \in V\})\ \wedge \)
\(\,\,\bigcup \ (P_ 1 \cup [\![{B}_ 1]\!]\cup P_ 2 \cup [\![{B}_ 2]\!])\ =\ U  V\ \wedge \)
\(\,\,B_ 1 \notin P_ 1 \cup P_ 2 \cup [\![{B}_ 2]\!]\ \wedge \)
\(\,\,B_ 2 \notin P_ 1 \cup [\![{B}_ 1]\!]\cup \ P_ 2\ \wedge \)
\(\,\,(P_ 1 \cup [\![{B}_ 1]\!]) \cap (P_ 2 \cup [\![{B}_ 2]\!])\ =\ \emptyset )\)
There are different ways to strengthen the original \(inv_ 1\). We use the above additional conjuncts as they can be inserted in existing proofs with little modification, and their preservation in the invariant can be proved quite trivially. The first additional conjunct ensures that no element still in V is already in a bin or partial solution. The second and third additional conjuncts ensure distinctness of the bins \(B_ 1\) and \(B_ 2\) with the remaining solution. The final conjunct ensures that the partial solutions with their added bins are disjoint from each other. It should be noted that the last conjunct is not necessary to prove functional correctness. It will, however, be needed in later proofs, and as its preservation in this invariant for the simplified algorithm can be used in the proof of the full algorithm, one can save redundant case distinctions by proving it now. Another advantage of proving it now is that later invariants can remain identical to the invariants proposed in the paper.
\(bp\ (P_ 1 \cup [\![{B}_ 1 \cup \{u\}]\!]\cup P_ 2 \cup [\![{B}_ 2 ]\!]\cup \{\{v\}\ \ v \in V\ \ \{u\}\})\)
\(B_ 1 \cup \{u\} \notin P_ 1 \cup P_ 2 \cup \ [\![{B}_ 2 ]\!]\)
\(B_ 2 \notin P_ 1 \cup [\![{B}_ 1 \cup \{u\}]\!]\cup P_ 2\)
\((P_ 1 \cup [\![{B}_ 1 \cup \{u\}]\!]) \cap (P_ 2 \cup [\![{B}_ 2 ]\!])\ =\ \emptyset \)
To prove the approximation factor, we proceed as in [4] and establish suitable lower bounds. The first lower bound
Lemma 11
\(bp\ P\ \longrightarrow \ L\ \le \ P\)
holds because a bin can only contain at most one large object, and every large object needs to be in the solution. To prove this in Isabelle, we first make the observation that for every large object there exists a bin in P in which it is contained. Therefore, we may obtain a function f that returns this bin for every \(u \in L\). Using the fact that any bin can hold at most one large object, we can show that this function has to be injective, as every large object must map to a unique bin. Hence, the number of large objects is equal to the number of bins f maps to. Moreover, the image of f has to be a subset of P. Thus, the number of large objects has to be a lower bound on the number of bins in P.
Lemma 12
\(bp\ P \wedge inv_ 1\ P_ 1 \ P_ 2 \ B_ 1 \ B_ 2 \ V \wedge (\forall \,{B}\!\in \!{P}_ 1 \cup [\![{B}_ 1 ]\!].\ B \cap L \ne \emptyset )\ \longrightarrow \) \(P_ 1 \cup [\![{B}_ 1]\!]\cup \{\{v\}\ \ v \in V \cap L\}\ \le \ P\)
Another easy lower bound is this one:
Lemma 13
\(bp\ P\ \longrightarrow \ (\sum _{u \in U} w\,u) \le c \ *\ P\)
\(bij\_{exists}\ {:}{:}\; {^\prime {a}}\ set\ set\ \Rightarrow \ {^\prime {a}}\ set\ \Rightarrow \ bool\)
\(bij\_{exists}\ P\ V\ =\ (\exists \,{f}.\ bij\_{betw}\ f\ P\ V \wedge (\forall \;{B}\!\in \!{P}.\ c\ <\ W\ B\ +\ w\ (f\ B)))\)
From this, we can make the observation that the number of bins in \(P_ 1\) is a strict lower bound on the number of bins of any correct bin packing P:
Lemma 14
\(bp\ P \ \wedge \ inv_ 1 \ P_ 1 \ P_ 2 \ B_ 1 \ B_ 2 \ V \ \wedge \ bij\_{exists}\ P_ 1\ (\bigcup \ (P_ 2 \ \cup \ [\![{B}_ 2 ]\!]))\ \longrightarrow \ P_ 1 \ +\ 1 \ \le \ P\)
\(inv_ 2 \ P_ 1 \ P_ 2 \ B_ 1 \ B_ 2 \ V\ =\)
\((inv_ 1 \ P_ 1 \ P_ 2 \ B_ 1 \ B_ 2 \ V\ \wedge \)
\(\;(V \cap L \ne \emptyset \ \longrightarrow \ (\forall \;{B}\!\in \!P_ 1 \cup [\![{B}_ 1]\!].\ B \cap L \ne \emptyset ))\ \wedge \)
\(\; bij\_{exists}\ P_ 1 \ (\bigcup \; (P_ 2 \cup [\![{B}_ 2 ]\!])) \wedge 2 *P_ 2 \le \bigcup \; P_ 2)\)
\( inv_ 3 \ P_ 1 \ P_ 2 \ B_ 1 \ B_ 2 \ V\ =\ (inv_ 2 \ P_ 1 \ P_ 2 \ B_ 1 \ B_ 2 \ V\ \wedge \ B_ 2 \subseteq \ S)\)
The motivation for the last conjunct in \(inv_ 2\) is the following lower bound:
\(inv_ 1 \ P_ 1 \ P_ 2 \ B_ 1 \ B_ 2 \ V \ \wedge \ 2 \ *P_ 2 \le \bigcup \ P_ 2\ \wedge \ bij\_{exists}\ P_ 1\ (\bigcup \ (P_ 2 \ \cup \ [\![{B}_ 2]\!]))\ \longrightarrow \) \(\ 2 *P_ 2 \ \cup \ [\![{B}_ 2]\!] \le P_ 1\ +\ 1\).
The main lower bound lemma (Theorem 4.1 in [4]) is the following:
Lemma 15
\(V \cap S = \emptyset \wedge inv_ 2\ P_ 1 \ P_ 2\ B_ 1\ B_ 2\ V \wedge bp\ P\ \longrightarrow \)
\(P_ 1 \cup [\![{B}_ 1 ]\!]\cup \ P_ 2 \cup \ [\![{B}_ 2 ]\!]\cup \{\{v\}\ \ v \in V\}\ \le \ 3 \ /\ 2 \ *\ P\)
From this lower bound the postcondition of the algorithm follows easily under the assumption that \(inv_ 2\) holds at the end of the loop. This in turn follows because \(inv_ 3\) can be shown to be a loop invariant.
7 Conclusion
In the first application of theorem proving to approximation algorithms we have verified three classical and one less wellknown approximation algorithm for fundamental NPcomplete problems, have corrected purported invariants from the literature and could even strengthen the approximation ratio in one case. Although we have demonstrated the benefits of formal verification of approximation algorithms, we have only scratched the surface of this rich theory. The next step is to explore the subject more systematically. As a large fraction of the theory of approximation algorithms is based on linear programming, this is a promising and challenging direction to explore. Some linear programming theory has been formalized in Isabelle already [5, 11]. Approximation algorithms can also be formulated as relational programs, and verified accordingly. This approach was explored in [2], with some support from theorem provers, but has yet to be fully formalized.
Notes
Acknowledgement
Tobias Nipkow is supported by DFG grant NI 491/161.
References
 1.Bansal, N., Khot, S.: Inapproximability of hypergraph vertex cover and applications to scheduling problems. In: Abramsky, S., Gavoille, C., Kirchner, C., Meyer auf der Heide, F., Spirakis, P.G. (eds.) ICALP 2010. LNCS, vol. 6198, pp. 250–261. Springer, Heidelberg (2010). https://doi.org/10.1007/9783642141652_22CrossRefzbMATHGoogle Scholar
 2.Berghammer, R., Höfner, P., Stucke, I.: Cardinality of relations and relational approximation algorithms. J. Log. Algebraic Methods Program. 85(2), 269–286 (2016)MathSciNetCrossRefGoogle Scholar
 3.Berghammer, R., MüllerOlm, M.: Formal development and verification of approximation algorithms using auxiliary variables. In: Bruynooghe, M. (ed.) LOPSTR 2003. LNCS, vol. 3018, pp. 59–74. Springer, Heidelberg (2004). https://doi.org/10.1007/9783540259381_6CrossRefzbMATHGoogle Scholar
 4.Berghammer, R., Reuter, F.: A linear approximation algorithm for bin packing with absolute approximation factor 3/2. Sci. Comput. Program. 48(1), 67–80 (2003). https://doi.org/10.1016/S01676423(03)00011XMathSciNetCrossRefzbMATHGoogle Scholar
 5.Bottesch, R., Haslbeck, M.W., Thiemann, R.: Verifying an incremental theory solver for linear arithmetic in Isabelle/HOL. In: Herzig, A., Popescu, A. (eds.) FroCoS 2019. LNCS (LNAI), vol. 11715, pp. 223–239. Springer, Cham (2019). https://doi.org/10.1007/9783030290078_13CrossRefGoogle Scholar
 6.Eßmann, R., Nipkow, T., Robillard, S.: Verified approximation algorithms. Archive of Formal Proofs, Formal proof development, January 2020. http://isaafp.org/entries/Approximation_Algorithms.html
 7.Halldórsson, M.M., Radhakrishnan, J.: Greed is good: approximating independent sets in sparse and boundeddegree graphs. Algorithmica 18(1), 145–163 (1997)MathSciNetCrossRefGoogle Scholar
 8.Kleinberg, J.M., Tardos, É.: Algorithm Design. AddisonWesley (2006)Google Scholar
 9.Nipkow, T., Klein, G.: Concrete Semantics with Isabelle/HOL. Springer, Heidelberg (2014). http://concretesemantics.org
 10.Nipkow, T., Wenzel, M., Paulson, L.C. (eds.): Isabelle/HOL. LNCS, vol. 2283. Springer, Heidelberg (2002). https://doi.org/10.1007/3540459499
 11.Parsert, J., Kaliszyk, C.: Linear programming. Archive of Formal Proofs, Formal proof development, August 2019. http://isaafp.org/entries/Linear_Programming.html
 12.Vazirani, V.V.: Open problems. Approximation Algorithms, pp. 334–343. Springer, Heidelberg (2003). https://doi.org/10.1007/9783662045657_30CrossRefGoogle Scholar
 13.Wei, V.: A lower bound for the stability number of a simple graph. Technical Memorandum 81–112179, Bell Laboratories (1981)Google Scholar