A Formal Analysis of Algorithms for Matroids and Greedoids

Let $E:=\{e_1,e_2,\mathrm{\dots },e_n\}$, $c:E\to {ℝ}_{+}$, and $c(e_1)\ge c(e_2)\ge \mathrm{\dots }\ge c(e_n)$. Let $G_n$ be the final solution found by BestInGreedy assuming that the elements are sorted in the given order, and let $X_n$ be an arbitrary solution. Define $E_j:=\{e_1,\mathrm{\dots },e_j\}$, $G_j:=G_n\cap E_j$ and $X_j:=X_n\cap E_j$ for $j=0,\mathrm{\dots },n$. Set $d_n:=c(e_n)$ and $d_j:=c(e_j)-c(e_{j+1})$ for $j=1,\mathrm{\dots },n-1$.

Since $X_j\in ℱ$, we have $|X_j|\le r(E_j)$. Since $G_j$ is a basis of $E_j$, we have $|G_j|\ge \rho (E_j)$. Together with the definition of the rank quotient, we can conclude that

$◀$ Within the appropriate context in the locale Best_In_Greedy (which assumes the three axiom predicates described above and that c and order are valid), the lemma can be formulated as in Listing 6 in Isabelle/HOL. Here, c_set c S denotes the sum of the costs of the elements in a set S, where the cost function is c.

In our formalisation, the proof of this lemma followed the informal proof, with the main argument of the proof consisting of the chain of inequalities on sums. Since we do not explicitly store the current iteration number $j$ in the state, we provide the definition num_iter, which extracts the iteration number from a given state using the length of the carrier list. The definitions carrier_pref and pref are used to represent the prefix sets $E_j$, $G_j$ and $X_j$.

A main statement that is often given without further explanation in informal proofs is that for all $j\in \{1,\mathrm{\dots },n\}$, $G_j$ is a basis of $E_j$. Intuitively, $G_j$ can be seen to be a maximally independent subset of $E_j$ since it is independent by construction, and since no potential candidate elements are skipped during the algorithm. However, in the context of the formalisation, proving this statement requires some more work. In order to be able to use this fact in the proof, we formulate invariant invar_4, which expresses the desired property.

For the invariant preservation proofs for invar_4, defining some more auxiliary invariants and proving they are preserved across the algorithm is necessary. These are not part of the informal proof, since they are either fairly trivial (e.g. showing that result is always a subset of the current carrier prefix) or aspects specific to the formal proof (e.g. showing that result always satisfies the set ADT well-formedness invariant). Proving that invar_4 is preserved across the different execution paths of BestInGreedy then boils down to proving that if result is a basis of the current carrier prefix, the result set after one state update will still be a basis of the carrier prefix in the next step. We consider the two recursive cases of BestInGreedy, in which the current element is either added to result if it preserves independence, or left out otherwise. The two lemmas required for the invariant proofs in these two cases are formulated and proven in the context of the abstract indep_system locale. Through the theorems connecting the implementation of independence systems to the abstract theory of independence systems, we are able to use these theorems to complete the invariant preservation proofs of invar_4.

The second important correctness theorem on the Best-In-Greedy algorithm is Lemma 2, which states that there exists a nonnegative cost function $c$ and a valid solution $X$ for which the bound from Lemma 1 holds.

Choose $F\subseteq E$ and bases $B_1,B_2$ of $F$ such that $\frac{|B_1|}{|B_2|}=q(E,ℱ)$. Define $c(e):=1$ for $e\in F$, $c(e):=0$ for $e\in E\setminus F$ and sort $e_1,\mathrm{\dots },e_n$ such that $c(e_1)\ge c(e_2)\ge \mathrm{\dots }\ge c(e_n)$ and $B_1=\{e_1,\mathrm{\dots },e_{|B_1|}\}$. Then $c(G)=|B_1|$ and $c(X)=|B_2|$, which finishes the proof. $◀$ In our formalisation, this lemma is stated with an additional existential quantifier for the order parameter. The proof in our formalisation proceeds similarly to the informal proof we follow, except that we explicitly construct the initial order list and use the stability of the sorting function to show that the sorting of the elements produces the ordering necessary for the proof. Additionally, proving that the greedy result is $B_1$ requires defining some new loop invariants (for example that no element of $F-B_1$ is ever in the greedy result) and showing that they are preserved across the algorithm.

The final correctness theorem on the Best-In-Greedy algorithm concerns the relationship between the performance of the algorithm and matroids:

By Lemma 1 and Lemma 2 we have if and only if there exists a cost function $c:E\to {ℝ}_{+}$ for which BestInGreedy does not find an optimum solution. Using the fact that if and only if $(E,ℱ)$ is not a matroid completes the proof. $◀$

For an undirected graph $G$ with a set of edges $E$, a spanning tree $T$ is an acyclic subgraph connecting all vertices of $G$ to one another. A spanning forest is acyclic and connects all vertices that are connected via $E$.

The set of edges $E$ in undirected graphs forms a matroid under acyclicity, i.e. where those sets of edges that form acyclic subgraphs are independent. This is a so-called graphic matroid and it is a widely cited example of matroids [21, 33]. Acyclicity of sets $X\subseteq E$ indeed satisfies the matroid axioms and a circuit would be a cycle in the ordinary sense. We formalise this in Isabelle/HOL, including the equivalence of being a basis w.r.t. acyclicity and being a spanning forest, making the greedy algorithm suitable to solve the maximum spanning forest problem correctly. Note that minimum spanning trees can be easily computed using this algorithm by adapting the input.

The instantiation of the Best-In-Greedy algorithm for graph matroids is also known as Kruskal’s Algorithm [22]. An independence oracle could check for the absence of cycles by a modified Depth-First Search (DFS). Since the independence of the current solution $X$ is maintained as an invariant, it is enough to check that a new element $x$ does not lead to circuits in $X\cup \{x\}$, i.e. a new edge $e$ does not add a cycle in the case of the graphical matroid. We call this a weak oracle. It would be simpler to implement and to verify, and it might even allow for running time improvements e.g. if available, by using a union-find structure to store connected components of $X$.

We therefore have an extended locale that also specifies the behaviour of a weak oracle, which is that if (a) $X$ is independent and if (b) suitable data structure and auxiliary invariants are satisfied and (c) $x\notin X$, then the oracle determines whether $X\cup \{x\}$ is independent. Subsequently, we verify the greedy algorithm with a weak oracle by proving it equivalent to the first version when called on the empty set. As a result, correctness can be lifted. In the end, we obtain an executable algorithm for maximum spanning forests using a simple DFS as weak oracle. A simplified version of the correctness theorem for Kruskal’s Algorithm is stated in Listing 9. An informal analysis yields that this implementation has a running time of $𝒪(n^2\cdot {\log }^{2}n)$. $𝒪(|E|\cdot \iota )$ is the running time of the abstract algorithm where $\iota$ is the running time of the oracle.

We give an executable function that is equivalent to the one in Listing 10. However, candidate search is not performed on all $e\in E$ since anything in $X$ will never be a next best candidate. For the current solution $X$, it only checks those $e$ where $e\in E\setminus X$.

An arborescence $T$ around a vertex $r$ in a graph with edges $E$ is an acyclic, connected subgraph of $E$ that contains $r$. If an edge in $E$ is incident on $r$, the set of arborescences around $r$ forms a greedoid. Bases are spanning trees of the connected component of $r$ in $E$. The arborescence greedoid has strong exchange, making the instantiation of GreedoidGreedy, namely, the Jarnik-Prim Algorithm [31] optimal. We obtain a $𝒪(n\cdot |E|\cdot \log n)$ implementation to compute maximum weight bases where $n$ is the number of vertices in the component around $r$. Prim’s and Kruskal’s algorithm demonstrate that bounds tighter than what can be deduced from the running time of the abstract algorithm, which is $𝒪({|E|}^2\cdot \iota )$ and $𝒪(|E|\cdot \iota )$, respectively, is possible for concrete problems.

We show independence of $X_l:=(X\setminus \{x_1,\mathrm{\dots },x_l\})\cup \{y_1,\mathrm{\dots },y_l\}$ for $l\le s$ by induction. The theorem trivially holds for $l=0$. We assume the claim for $X_l$ where : It might be that $X_l\cup \{y_{l+1}\}$ is independent implying independence of $X_{l+1}$ because of (M2). If $X_l\cup \{y_{l+1}\}$ is dependent, however, it contains a unique circuit $𝒞(X_l,y_{l+1})$ containing $y_{l+1}$ due to $X_l$’s independence. All deleted $x_1,\mathrm{\dots },x_l$ cannot have been part of $𝒞(X,y_{l+1})$ because of (4) and neither any inserted $y_1,\mathrm{\dots },y_l$ because of (2), $y_{l+1}$ could, however. This implies $𝒞(X,y_{l+1})\subseteq X_{l+1}$. Therefore $𝒞(X_l,y_{l+1})=𝒞(X,y_{l+1})$. Due to (3), $x_{l+1}\in 𝒞(X,y_{l+1})$, implying independence of $(X_l\setminus \{x_{l+1}\})\cup \{y_{l+1}\}=X_{l+1}$. $◀$ The formalisation of the above lemma contains an inductive proof on $s$ within the context of the locale matroid. The $x_i$s and $y_i$s are formalised as a list of pairs.

From now on, we assume two matroids $(E,{ℱ}_1)$ and $(E,{ℱ}_2)$ over the same ground set $E$, or formally, we work in the double_matroid locale (Listing 11). Following Korte and Vygen [21], for a set $X\in {ℱ}_1\cap {ℱ}_2$, we define an auxiliary graph $G_X$ with vertices $E$ and edges $A_{X,1}\cup A_{X,2}$ where $A_{X,1}=\{(x,y).y\in E\setminus X\wedge x\in {𝒞}_1(X,y)\setminus \{y\}\}$ and $A_{X,2}=\{(y,x).y\in E\setminus X\wedge x\in {𝒞}_2(X,y)\setminus \{y\}\}$. $G_X$ is obviously bipartite between $X$ and $E\setminus X$. We define two sets $S_X=\{y.y\in E\setminus X\wedge X\cup \{y\}\in {ℱ}_1\}$ and $T_X=\{y.y\in E\setminus X\wedge X\cup \{y\}\in {ℱ}_2\}$. A path between a vertex from $S_X$ and another from $T_X$ indicates an alternating sequence of insertion and deletion. Due to bipartiteness, the length will be odd allowing for an augmentation. We make this precise as follows.

We apply Lemma 6 to $X\cup \{y_0\}$, $x_1,\mathrm{\dots },x_s$ and $y_1,\mathrm{\dots },y_s$ to show $X^{\prime }\in {ℱ}_1$: For all , $x_i$ is the second vertex of the $(2i-1)$th edge of $p$. Because the path alternates between $E\setminus X$ and $X$, the $(2i-1)$th is in $A_{X,2}$ and $x_i\in X\cup \{y_0\}$ for all $x_i$, yielding (1). For all , $y_i$ is the second vertex of the $(2i)$th edge in $p$. Because of alternation and pairwise distinctness of the $y$s ($p$ is shortest path), $y_i\in E\setminus (X\cup \{y_0\})$, implying (2). Also, for all , $x_i$ is the first vertex of the $(2i)$th edge, which is part of $A_{X,1}$ because of alternation. Therefore, $x_k\in {𝒞}_1(X\cup \{y_0\},y_k)$ for all $1\le k\le s$ (3). We assume an $x_i$ and $x_j$ where and $x_j\in {𝒞}_1(X\cup \{y_0\},y_i)$. $x_i$ or $x_j$ is the first vertex of the $2i$th of $2j$th edge of $p$, respectively. $y_j$ and $y_i$ are the second vertices. Both of those edges are part of $A_{X,1}$. As $y_i\in E\setminus X$, and therefore $x_j\ne y_i$, the edge $(x_j,y_i)\in A_{X,1}$. We could then delete $y_j,\mathrm{\dots },x_{i-1}$ giving a shorter $S_X$-$T_X$-path. Hence (4) is satisfied and Lemma 6 can be applied.

Analogously, we take $X\cup \{y_s\}$, $x_s,\mathrm{\dots },x_1$ and $y_{s-1},\mathrm{\dots },y_0$ to show $X^{\prime }\in {ℱ}_2$. $◀$ The statement is in Listing 11. We show that the edges of paths used by Lemma 7 alternate between $A_1$ and $A_2$ using an existing library on alternating lists for matchings [1]. From this we can easily deduce (1)-(3) to apply Lemma 6. The re-applicability of matching theory is no coincidence since bipartite matching is an instance of matroid intersection as we show later.

On top of improvement by augmentation, the absence of an augmenting path characterises maximality of $|X|$ for $X\in {ℱ}_1\cap {ℱ}_2$:

If there is an $S_X$-$T_X$ path, there is a shortest one as well, which could be used for an augmentation according to Lemma 7, leading to an increase in the cardinality.

Now assume, that there is no $S_X$-$T_X$ path. We define $R$ as the set of vertices in $G_X$ that are reachable from $S_X$. Obviously $S_X\subseteq R$ and $R\cap T_X=\mathrm{\varnothing }$. There are rank functions $r_1$ and $r_2$ w.r.t. ${ℱ}_1$ and ${ℱ}_2$, respectively.

We prove $r_2(R)=|X\cap R|$ by contradiction: Since $X\cap R$ has to be independent w.r.t. the second matroid and therefore $|X\cap R|=r_2(X\cap R)$, we would have since $r_2$ is monotone. Because of the strict inequality, there is $y\in R\setminus X$ where $(X\cap R)\cup \{y\}\in {ℱ}_2$. Otherwise, $X\cap R$ would be a basis of $R$ implying equal ranks. As $R\cap T_X=\mathrm{\varnothing }$, $X\cup \{y\}\notin {ℱ}_2$. There is $x\in X\setminus R$ with $x\in {𝒞}_2(X,y)$ (Otherwise $(X\cap R)\cup \{y\}\notin {ℱ}_2$). By definition, $(y,x)\in A_{X,2}$. That makes $x$ part of $R$, which is a contradiction.

We prove $r_1(E\setminus X)=|X\setminus R|$ by contradiction: Since $X\setminus R$ has to be independent w.r.t. the first matroid and therefore $|X\setminus R|=r_1(X\setminus R)$, we would have since $r_1$ is monotone. Because of the strict inequality, there is $y\in (E\setminus R)\setminus X$ where $(X\setminus R)\cup \{y\}\in {ℱ}_1$. Otherwise, $X\setminus R$ would be a basis of $E\setminus R$ implying equal ranks. As $S_X\subseteq R$, $X\cup \{y\}\notin {ℱ}_1$. There is $x\in X\cap R$ with $x\in {𝒞}_1(X,y)$ (Otherwise $(X\setminus R)\cup \{y\}\notin {ℱ}_1$). By definition, $(x,y)\in A_{X,1}$. That makes $y$ part of $R$, which is a contradiction.

Therefore, $|X|=r_1(E\setminus X)+r_2(X)$. Because of the rank criterion from Lemma 5, $X$ satisfies $|X|\le r_1(Q)+r_2(E\setminus Q)$ with equality. This gives the max-min equality and makes $X$ a set of maximum cardinality that is independent w.r.t. both matroids. $◀$

The formal proof of Theorem 8 is split in two directions. The second direction also shows $r_2(R)=|X\cap R|$, $r_1(E\setminus X)=|X\setminus R|$ and $|X|=r_1(E\setminus X)+r_2(X)$ as statements to prove the max-min equality separately. The final formalisation can be seen in Listing 11.

The number of iterations to build $G_X$ is $𝒪({|E|}^2)$. Each matroid comes with an oracle which is assumed to be ${\iota }_1$ or ${\iota }_2$, respectively. This results in $𝒪({|E|}^3\cdot ({\iota }_1+{\iota }_2))$ overall running time. We might have to check $|X|\cdot (|E|-|X|)$ pairs of vertices. If - depending on the problem - the size of the circuits ${\sigma }_1$ and ${\sigma }_2$ is assumed to be small, e.g. $𝒪(\log |E|)$ or even $𝒪(1)$, most of the inner for-loops’ iterations were wasted. If the circuits can be computed in time ${\kappa }_1,{\kappa }_2\in o(|E|)$, the time would be the more efficient $𝒪({|E|}^2\cdot ({\iota }_1+{\iota }_2+{\kappa }_1+{\kappa }_2+{\sigma }_1+{\sigma }_2))$.

In Isabelle/HOL, weak circuit oracles are assumed to return data structures storing ${𝒞}_{1/2}(X,y)\setminus \{y\}$ provided that $X$ is independent and $X\cup \{y\}$ is dependent. These are added to the locale for MaxMatroidIntersection, as well. A variant of the algorithm using circuit oracles is verified using the same methodology as before.

There is a verified implementation of Breadth-First Search (BFS) that works on adjacency maps by Abdulaziz [3]. It takes a set of sources and builds another adjacency map modelling a DAG of those edges that are actually explored by the search. If a vertex $v$ is reachable from a source $s$, there is a path $p$ in this DAG leading from a source $s^{\prime }$ to $v$ such that $p$ is a shortest path in the actual graph leading from $s^{\prime }$ to $v$. find_path runs BFS for the sources $S_X$ and uses a DFS to obtain a path in the DAG and, hence, a shortest $S_X$-$T_X$ path. For a concrete intersection problem and together with appropriate oracles, find_path can be used to instantiate the locale of the intersection algorithm.

An example for matroid intersection is maximum cardinality bipartite matching. Consider a bipartite graph with edges $E$ between two disjoint sets of vertices $L$ and $R$. For $e\in E$, we call the endpoint in $L$ the left and the one in $R$ the right endpoint. We say that $M\subseteq E$ is independent w.r.t. $L$ iff no edges in $M$ share a left endpoint. Independence w.r.t. $R$ is defined analogously. Valid matchings are sets of vertex-disjoint edges in $E$ and are thus exactly those $M$ that are independent w.r.t. both $L$ and $R$. The two independence predicates satisfy the matroid axioms making this a matroid intersection problem. Circuits w.r.t. $L$ or $R$ would be edges $e,d\in E$ sharing a left or right endpoint, respectively.

For $M\subseteq E$, we maintain a set data structure $[M]$, two maps $M_L$ and $M_R$, where $M_L$ associates every $x\in L$ with $e\in M$ for which $x$ is the left endpoint, and analogously for $M_R$. Weak independence and circuit oracles are very simple: If $M$ is independent w.r.t. $L$ ($R$), and $e\notin M$, we check in $M_L$ ($M_R$) that $e$’s left (right) endpoint is not associated to any another edge. If $M\cup \{e\}$ would be dependent w.r.t. $L$ or $R$, we would return the edges associated to $e$’s left or right endpoint as ${𝒞}_L(M,e)\setminus \{e\}$ or ${𝒞}_R(M,e)\setminus \{e\}$, respectively. We used these oracles to instantiate MaxMatroidIntersection to compute maximum matchings in bipartite graphs. The running time is $𝒪(\min \{|L|,|R|\}\cdot m\cdot (\log |R|+\log |L|+\log m))$ where the logarithms are due to using tree data structures, which is dominated by $𝒪(n\cdot m\cdot (\log n+\log m))$. Without circuit oracles, we would have another multiplicative factor of $\min \{|L|,|R|\}$.