Graph Theory

Motivation

The maximum weight matching (MWM) problem asks, for a graph with edge weights, for a set of vertex-disjoint edges of largest total weight. It is a central problem of combinatorial optimization, with applications to transportation, assignment and scheduling, and as a subroutine for shortest paths, planar max cut, Chinese postman tours and metric TSP. Edmonds' blossom algorithm (1965) solves it on general graphs; the fastest implementation, due to Gabow, runs in $O(mn+n^2\log n)$ time, and the scaling algorithm of Gabow and Tarjan (1991) runs in $O(m\sqrt{n\log n}\,\log(nN))$ time on graphs with $n$ vertices, $m$ edges and integer weights of magnitude at most $N$. Applications such as switch scheduling, graph clustering and sparse linear solvers accept a slightly suboptimal matching in exchange for speed. This motivates $(1-\epsilon)$-approximate maximum weight matchings: matchings whose weight is at least a $1-\epsilon$ fraction of the optimum.

Timeline of linear and near-linear time approximation for general graphs (Section 1.3 and Table IV of the paper; the entries below are as the paper attributes them):

• Folklore: the greedy algorithm, which repeatedly takes the heaviest remaining edge, gives a $\tfrac12$-MWM in $O(m\log n)$ time.
• Preis (STACS 1999): a $\tfrac12$-MWM in linear time; Drake and Hougardy (2003) gave a simpler one.
• Drake and Hougardy (2003; journal version Vinkemeier and Hougardy, ACM Trans. Algorithms 2005): a $(\tfrac23-\epsilon)$-MWM in $O(m\epsilon^{-1})$ time; Pettie and Sanders (2004) improved this to $O(m\log\epsilon^{-1})$.
• Duan and Pettie (FOCS 2010) and Hanke and Hougardy (2010): a $(\tfrac34-\epsilon)$-MWM in $O(m\log n\log\epsilon^{-1})$ time.
• Duan and Pettie (2014): a $(1-\epsilon)$-MWM in $O(m\epsilon^{-1}\log\epsilon^{-1})$ time, which is linear for every fixed $\epsilon$.

Setting

Let $G=(V,E)$ be a finite simple graph with integer weights $w:E\to\{1,\dots,N\}$, $N=2^L$. A matching $M$ is a set of vertex-disjoint edges, with weight $w(M)=\sum_{e\in M}w(e)$; a vertex is free if no edge of $M$ touches it. $M$ is a $c$-MWM if $c\cdot w(M')\le w(M)$ for every matching $M'$.

A blossom is built recursively: a single vertex $\{v\}$ is a trivial blossom with $E_{\{v\}}=\emptyset$; an odd number $\ge3$ of disjoint blossoms $A_0,\dots,A_\ell$ joined in a cycle by edges $e_i\in A_i\times A_{i+1}$ form the blossom $B=\bigcup A_i$ with edge set $E_B=\bigcup E_{A_i}\cup\{e_0,\dots,e_\ell\}$. It is full if $|M\cap E_B|=(|B|-1)/2$. The algorithm keeps a laminar set $\Omega$ of full blossoms; a root blossom is a maximal one, and $G/\Omega$ contracts each root blossom to a single vertex.

Dual values $y:V\to\mathbb R$ and $z$ on odd vertex sets give each edge the value

$$yz(u,v)=y(u)+y(v)+\sum_{B\ \text{odd},\ u,v\in B} z(B).$$

The scaling algorithm (Figure 2 of the paper) has parameters $N$ and $\epsilon'=2^{-g}\le\tfrac14$. It runs scales $i=0,\dots,L$ with granularity $\delta_i=\epsilon'N/2^i$ and truncated weights $w_i(e)=\delta_i\lfloor w(e)/\delta_i\rfloor$. Each scale repeats four steps: augment along a maximal set of vertex-disjoint augmenting paths of the eligible graph $G_{\mathrm{elig}}$, shrink a maximal set of new blossoms, adjust the duals by $\pm\delta_i/2$, and dissolve root blossoms whose $z$-value has reached zero. It stops when the free vertices' $y$-values reach a scale-dependent value, which is $0$ at scale $L$. Eligibility is given by Definition 3.2; the linear-time variant keeps the algorithm unchanged and uses Definition 3.10, which additionally ignores an edge $e$ in scales $i>\mathrm{scale}(e)+\log\epsilon'^{-1}$ unless it is a blossom edge.

Formalization targets

Goal: Theorem 3.12, approximation half

For every $\epsilon$ with $\epsilon'\le\epsilon/7$, the algorithm of Figure 2 with Definition 3.10 eligibility has a terminating run, and every terminating run returns a matching $M$ with

$$w(M)\ \ge\ (1-\epsilon)\,w(M')\qquad\text{for every matching } M' \text{ of } G .$$

Milestones, in attack order

• Lemma 2.3: approximate complementary slackness ($yz(e)\ge(1-\epsilon_0)w(e)$ everywhere, $yz(e)\le(1+\epsilon_1)w(e)$ on matched and blossom edges, zero free duals) gives a $(1+\epsilon_1)^{-1}(1-\epsilon_0)$-MWM.
• Section 2 rescaling: rounding real weights to $\lfloor w/\gamma_r\rfloor$, $\gamma_r=\epsilon w_{\max}/n$, loses at most a factor $1-\epsilon/2$.
• Lemma 3.5: with Definition 3.2 the algorithm preserves Property 3.1, which consists of granularity, active blossoms, near domination $yz(e)\ge w_i(e)-\delta_i$, near tightness $yz(e)\le w_i(e)+2(\delta_j-\delta_i)$ for type-$j$ edges, and equal free duals.
• Lemma 3.6: eligible edges searched up to scale $i$ weigh at least $N/2^{i+1}+\delta_i$, and matched edges satisfy $yz(e)\le(1+4\epsilon')w(e)$.
• Lemma 3.7: the output under Definition 3.2 is a $(1-5\epsilon')$-MWM.
• Theorem 3.8: the approximation half of Theorem 3.8, with $\epsilon'\le\epsilon/5$.
• Lemma 3.11: the invariants under Definition 3.10, including $yz(e)>(1-\epsilon')w_i(e)$ and $yz(e)<(1+6\epsilon')w_i(e)$ once $i>\mathrm{scale}(e)+\gamma$.

Significance

The result. Theorem 3.12 gives the first algorithm for $(1-\epsilon)$-approximate maximum weight matching on general graphs that runs in linear time for every fixed $\epsilon$; earlier linear-time algorithms achieved only $\tfrac12$ or $\tfrac23-\epsilon$. Its analysis is a relaxation of Edmonds' complementary slackness conditions that grows weaker over the scales, but not uniformly, and Lemma 2.3 certifies an approximate matching by approximately feasible duals.

Formalizing it. The result is proved in the paper. Mathlib (at the pinned revision) has matchings, alternating walks and Tutte's theorem, but no blossoms, contracted graphs or weighted matching algorithms. A complete development gives a Lean model of blossoms, contraction and augmenting paths through blossoms, a verified primal–dual invariant for a scaling algorithm, and a checked approximate-slackness certificate for matchings. Each of these can be reused to formalize Edmonds' exact algorithm or the Gabow–Tarjan scaling algorithm.

Difficulty

The two halves of the argument pull against each other. Lemma 2.3 needs near domination and near tightness as multiplicative bounds. The algorithm maintains only additive bounds whose slack for an edge of type $j$ is $2(\delta_j-\delta_i)$, and this slack does not shrink as the scales advance. Converting it into a factor $1+O(\epsilon')$ requires a lower bound on the weight of every edge that ever became eligible, which in turn depends on the free vertices' duals following an exact schedule across scales.

For Definition 3.10 the obvious argument breaks down: an edge that is ignored after scale $\mathrm{scale}(e)+\gamma$ may violate near domination and near tightness by an amount that grows with every later dual adjustment. The claim is that the accumulated violation stays within an $O(\epsilon')$ fraction of $w_i(e)$, and establishing this requires tracking every adjustment that can reach an ignored edge.

On the combinatorial side, the Augmentation and Blossom Shrinking steps work in the contracted graph $G/\Omega$. Their correctness uses the classical facts that augmenting paths lift through full blossoms and that blossoms stay full after augmentation (Lemma 2.1), which have to be formalized from scratch.

Formalization scope

Graphs are SimpleGraph V on a Fintype V with decidable equality; edges are Sym2 V; matchings are Finset (Sym2 V) with pairwise vertex-disjoint edges of $G$; weights are $w:\mathrm{Sym2}\,V\to\mathbb N$ with $1\le w(e)\le 2^L$ on edges. Duals, $\delta_i$ and $w_i$ are real numbers. $z$ is a function on all finite vertex sets and $yz$ sums it over the odd sets that contain the edge, as on the page. $N=2^L$ and $\epsilon'=2^{-g}$, $g\ge2$, are given through their exponents. $\mathrm{scale}(e)$ uses the convention $\mu_{-1}=+\infty$. The paper's standing assumption $N\le n^2$ is used only for running time and is omitted.

The algorithm is a nondeterministic relation. A state holds $M$, $\Omega$ with its blossom edge sets, $y$, $z$, a ghost record of the scale in which each edge last entered $M\cup\bigcup_{B\in\Omega}E_B$, and the common free-vertex dual that drives the loop test. The maximal sets of augmenting paths and of new blossoms and the lifts of paths through blossoms are choices. Invariants are stated for states reachable by a run, and the goal asserts both that a terminating run exists and that every terminating run returns a $(1-\epsilon)$-MWM.

The running times $O(m\epsilon^{-1}\log N)$ of Theorem 3.8 and $O(m\epsilon^{-1}\log\epsilon^{-1})$ of Theorem 3.12 are not formalized: the paper fixes no cost model, and its bounds rely on a modified depth-first search and on word-RAM table lookups. The explicit constants $\epsilon'\le\epsilon/5$ (Theorem 3.8) and $\epsilon'\le\epsilon/7$ (Theorem 3.12) are the ones the proofs supply.

The following trivializing formalizations are ruled out: a "matching" that may contain non-edges or repeated edges; a goal about a state only assumed to satisfy Property 3.1 rather than reached by the algorithm; a run relation with no terminating run, which the existence conjunct excludes; eligibility or blossoms chosen freely instead of by the page's rules; and comparison only against matchings of the contracted graph instead of all matchings of $G$.

Welcome contributions include a Lean treatment of blossoms and their contraction (Lemma 2.1, which is not a milestone here), the lift of augmenting paths, Lemmas 3.3 and 3.4 as auxiliary results, and proofs of the milestones in the order listed.

Selected references

• R. Duan and S. Pettie, Linear-Time Approximation for Maximum Weight Matching, Journal of the ACM 61(1), Article 1, 2014. https://doi.org/10.1145/2529989
• J. Edmonds, Maximum matching and a polyhedron with 0,1-vertices, Journal of Research of the National Bureau of Standards 69B, 125–130, 1965. https://doi.org/10.6028/jres.069B.013
• H. N. Gabow and R. E. Tarjan, Faster scaling algorithms for general graph-matching problems, Journal of the ACM 38(4), 815–853, 1991. https://doi.org/10.1145/115234.115366
• R. Preis, Linear time 1/2-approximation algorithm for maximum weighted matching in general graphs, STACS 1999, LNCS 1563, 259–269 (cited from the bibliography of Duan and Pettie 2014).
• D. E. D. Vinkemeier and S. Hougardy, A linear-time approximation algorithm for weighted matchings in graphs, ACM Transactions on Algorithms 1(1), 107–122, 2005 (cited from the bibliography of Duan and Pettie 2014).
• S. Pettie and P. Sanders, A simpler linear time 2/3 − ϵ approximation to maximum weight matching, Information Processing Letters 91(6), 271–276, 2004 (cited from the bibliography of Duan and Pettie 2014).

Motivation

A sorting network is a sorting procedure whose sequence of comparisons is fixed in advance, independently of the data. Its depth, the number of rounds of simultaneous comparisons on disjoint pairs, is the parallel running time. Sorting networks are used in parallel and hardware sorting, in switching networks, and in cryptography, where a data-independent (oblivious) sequence of operations is required. How small the depth can be as a function of the number of inputs $n$ is a basic question of parallel computation.

Timeline:

• 1968. Batcher's odd-even merge sort and bitonic sort give networks of depth $O((\log n)^2)$ and size $O(n(\log n)^2)$ (K. E. Batcher, Sorting networks and their applications, AFIPS Spring Joint Computer Conference, 1968). For $n$ a power of two they remain the best explicit networks in practice.
• 1973. Knuth's The Art of Computer Programming, Vol. 3, §5.3.4, surveys sorting networks. A simple counting argument gives the lower bound: every sorting network has depth at least $\log_2 n$, since each output depends on at most $2^{\text{depth}}$ inputs.
• 1983. Ajtai, Komlós and Szemerédi construct networks of depth $O(\log n)$ and size $O(n\log n)$ (Combinatorica 3 (1983) 1–19, doi:10.1007/BF02579338), matching the lower bound up to a constant. The constant is not computed in the paper and is known to be very large.
• 1990. Paterson simplifies the construction and gives the first explicit, still very large, depth constant (M. S. Paterson, Improved sorting networks with O(log N) depth, Algorithmica 5 (1990) 75–92, doi:10.1007/BF01840378).
• 2014. Goodrich gives Zig-zag sort, a simpler deterministic data-oblivious sorting algorithm with $O(n\log n)$ comparisons that avoids the AKS machinery but is not of logarithmic depth (arXiv:1403.2777).

Setting

There are $n$ registers $R_1,\dots,R_n$ holding elements of a linearly ordered set. An elementary step (a comparator) $(i,j)$ with $i\neq j$ compares the contents of $R_i$ and $R_j$ and exchanges them if the content of $R_i$ is larger. Afterwards $R_i$ holds the minimum and $R_j$ the maximum of the two, and every other register is unchanged. A parallel step is a set of comparators in which no register occurs twice, so it has at most $n/2$ comparators. A comparator network $N$ is a finite sequence of parallel steps, fixed before the input is seen. Its depth $\operatorname{depth}(N)$ is the number of parallel steps and its size $\operatorname{size}(N)$ the total number of comparators. $N$ sorts if for every input $x=(x_1,\dots,x_n)$ the output $N(x)$ satisfies $N(x)_1\le\cdots\le N(x)_n$.

The construction runs on the tree $T$ of finite $0$-$1$ sequences, whose levels are ordered lexicographically. A chain on level $i$ assigns to every node of that level a set of registers, with the sets pairwise disjoint and of a common size $N(C)$. A ⟨k, ε⟩ expander on ⟨A, B⟩, for disjoint register sets $A$ and $B$, is a bipartite graph between $A$ and $B$ of maximum degree $k$ in which every nonempty $X\subseteq A$ has more than $(1-\varepsilon)\varepsilon^{-1}\min\{|X|,\varepsilon|B|\}$ neighbours, and symmetrically for $B$. The Lean development uses the names ComparatorNetwork, compareExchange, IsChain, chainN, IsExpander, IsLowerSection for these objects.

Formalization targets

Goal: the AKS theorem (Abstract and §1, p. 1)

$$\exists\, c>0\ \ \forall n\ge 2\ \ \exists N:\quad N \text{ sorts},\qquad \operatorname{depth}(N)\le c\log_2 n,\qquad \operatorname{size}(N)\le c\,n\log_2 n .$$

The constant is absolute and is not fixed. Any explicit value would be invalidated by the next improvement, and the paper gives none.

Milestones (the paper's numbered lemmas that hold as stated)

• Lemma 3 (p. 6): for $0<\varepsilon<1$ and $c\ge1$ there is $k(\varepsilon,c)$ such that every pair of disjoint sets with $1/c\le|A|/|B|\le c$ carries a $\langle k,\varepsilon\rangle$ expander.
• Lemma 4 (p. 7): performing every comparator of such an expander once, in any order, from $A$ to $B$ leaves all but an $\varepsilon$-fraction of any lower section $S$ with $|S|\le|A|$ in $A$, and symmetrically for upper sections in $B$:

$$|S\setminus\mathrm{Cont}(A)|\le\varepsilon|S| .$$

• Lemma 1 (pp. 3–4): the splitting $V(C,k)$ of a chain, which moves one register of each leaf set up the tree, produces chains with properties (1.1)–(1.5).
• Lemma 2 (p. 4): chains $W(C,k)$ with $a_k-1\le N(W(C,k))\le a_k$ exist under conditions (2a), (2.b).
• Lemma 12(a) (p. 14): a violation of the order relation $R^\beta_G$ between two nodes of a level is witnessed by two consecutive nodes.

Significance

The result. The AKS theorem settles the asymptotic depth of sorting networks at $\Theta(\log n)$ and their size at $\Theta(n\log n)$. It gives an $O(\log n)$-time sorting algorithm with $n$ processors that performs only data-independent comparisons. It is the standard reference point for oblivious sorting in parallel algorithms, circuit complexity (sorting is in $\mathsf{NC}^1$ via comparators) and oblivious RAM constructions. Lemma 4, the ε-halver property of expander comparisons, is the component that later constructions (Paterson) reuse.

Formalizing it. The theorem has been proved since 1983. No Lean proof of the AKS theorem is known. Mathlib has no expander graphs in the ⟨k, ε⟩ sense and no sorting networks. The mission asks for a formal proof of the headline theorem by any route (the AKS construction or Paterson's variant), and for formal proofs of the paper's verified lemmas as reusable components. The expander lemma needs either an explicit family (Margulis; Gabber–Galil) or a probabilistic existence argument, both substantial on their own.

Difficulty

Every elementary argument stalls at depth $O((\log n)^2)$: recursive merging needs $\log n$ merge rounds, and merging two sorted lists by a comparator network needs depth $\Omega(\log n)$. A depth of $O(\log n)$ therefore cannot come from exact merging. It must come from constant-depth approximate operations (ε-halvers, which require bounded-degree expanders) combined with a mechanism that corrects the errors they leave. In the paper this mechanism is a movement of registers up and down a binary tree, controlled by a family of constants chosen in a fixed order ("$\varepsilon_1\ll q_2\ll1-g\ll q_1\ll 1/c_1\ll1$", p. 2). The accounting that shows the misplaced elements decay geometrically is the hard part. Several intermediate lemmas of the paper are false as printed, so the paper's text is not a checklist to transcribe.

Formalization scope

Conventions committed to in Lean:

• Registers are Fin n, and contents lie in an arbitrary linearly ordered type. A network is a List of layers, each a List (Fin n × Fin n) of comparators with distinct endpoints, and no register occurs twice in a layer. A comparator $(i,j)$ puts the minimum into $i$, and both directions $i<j$ and $i>j$ are allowed. Sorts means the output is monotone for every linearly ordered type and every input, not only for permutations.
• $\log_2 n$ is Real.logb 2 n, and the goal is stated for $n\ge2$. The constant $c$ is quantified before $n$.
• Tree levels are Fin (2^i), with numeric order equal to lexicographic order. A chain is a Fin (2^i) → Finset R.
• Definition 2.2 of the paper, read literally, requires $|\Gamma_\emptyset|>0$, which fails, so no graph would be an expander. The expansion inequalities are imposed on nonempty sets only, and the strict inequality is kept.

Trivializing formalizations are ruled out. The goal is not "for every $n$ there is a network of depth $O(\log n)$" with the constant chosen after $n$, which is true for trivial reasons. Layers without the disjointness condition would let a single layer contain a whole insertion sort. A bound on the number of comparisons alone, with unbounded depth, is a different and much older result; the goal states both the depth and the size bound.

The mission states the AKS theorem and the paper's lemmas that are correct as stated. It does not formalize the AKS algorithm itself ($S^\alpha$, $P^\alpha$, the operations CH1–CH4, IMP) or its intermediate Lemmas 5–11 and 13–15. Those depend on unspecified constants constrained only by "sufficiently small" chains, and Lemmas 5, 10 and 12(b) are false as printed. A solver may of course define the algorithm, with pinned constants, as part of a proof.

Contributions welcome: a library of comparator networks (composition, the 0-1 principle, depth of Batcher's networks), existence of bounded-degree bipartite expanders, the ε-halver lemma, and any complete proof of the goal. The network and expander definitions are independent of this paper and reusable.

Selected references

• M. Ajtai, J. Komlós, E. Szemerédi, Sorting in c log n parallel steps, Combinatorica 3(1) (1983) 1–19. doi:10.1007/BF02579338
• K. E. Batcher, Sorting networks and their applications, Proc. AFIPS Spring Joint Computer Conference 32 (1968) 307–314. doi:10.1145/1468075.1468121
• D. E. Knuth, The Art of Computer Programming, Vol. 3: Sorting and Searching, Addison-Wesley, 1973, §5.3.4.
• G. A. Margulis, Explicit constructions of concentrators, Problems of Information Transmission 9 (1973) 325–332.
• O. Gabber, Z. Galil, Explicit constructions of linear-sized superconcentrators, J. Computer and System Sciences 22(3) (1981) 407–420. doi:10.1016/0022-0000(81)90040-4
• M. S. Paterson, Improved sorting networks with O(log N) depth, Algorithmica 5 (1990) 75–92. doi:10.1007/BF01840378
• M. T. Goodrich, Zig-zag sort: a simple deterministic data-oblivious sorting algorithm running in O(n log n) time, STOC 2014. arXiv:1403.2777

Motivation

A maximal independent set (MIS) of a graph is a set of pairwise non-adjacent vertices to which no further vertex can be added. Sequentially an MIS is found greedily in linear time, but the greedy scan is inherently serial. Whether an MIS can be computed by a fast parallel algorithm was a central question of parallel complexity in the early 1980s: Karp and Wigderson gave the first NC algorithm (STOC 1984), and Luby's paper, SIAM J. Comput. 15(4):1036–1053, 1986, gave a much simpler one. MIS is a subroutine of many parallel and distributed graph algorithms (colouring, matching, symmetry breaking), and Luby's randomized algorithm remains the standard one in distributed computing.

The paper's second contribution, the subject of this mission, is a general method for removing randomness: analyse the randomized algorithm under pairwise independence only, then realize pairwise independent random variables on a sample space of polynomial size and try every sample point in parallel. The same method, often attributed jointly to Luby (1986) and to Alon, Babai and Itai (J. Algorithms 7, 1986), became a standard tool of derandomization.

Setting

Let $G = (V, E)$ be a finite simple graph with $n = |V|$ vertices labelled $0, \dots, n-1$. The algorithm keeps a set $I$ (initially empty) and the current graph $G' = (V', E')$, the subgraph of $G$ induced on $V'$ (initially $V' = V$). For $W \subseteq V'$ the neighbourhood is $N(W) = \{ i \in V' : \exists j \in W, (i,j) \in E' \}$. Each execution of the loop body selects an independent set $I' \subseteq V'$, adds it to $I$, and deletes $I' \cup N(I')$ from $V'$; the loop runs while $V' \ne \emptyset$. Write $d(i)$ for the degree of $i$ in $G'$, $Y_k$ for the number of edges of $G'$ before the $k$-th execution, and $\mathrm{sum}(i) = \sum_{j \in \mathrm{adj}(i)} 1/d(j)$.

Algorithm B's select step draws a coin $\mathrm{coin}(i) \in \{0,1\}$ for each vertex, with $\Pr[\mathrm{coin}(i) = 1] = 1/2d(i)$, puts $X = \{ i : \mathrm{coin}(i) = 1 \}$, and removes from $X$ the endpoint of smaller degree of every edge inside $X$ (both endpoints on a tie).

The sample space. Fix a prime $q$ with $n \le q \le 2n$. The sample points are the pairs $(x, y)$ with $0 \le x, y \le q-1$, each of probability $1/q^2$. With $n(i) = \lfloor q/2d(i) \rfloor$, the coin of vertex $i$ at $(x,y)$ is $1$ iff $(x + y \cdot i) \bmod q < n(i)$, so $\Pr[\mathrm{coin}(i) = 1] = p'_i = \lfloor q/2d(i) \rfloor / q$, and distinct coins are pairwise independent.

Algorithm D. Each execution of the loop body first moves the isolated vertices of $G'$ into $I$. Then:

• Case 1. If a vertex $i$ of maximum degree has $d(i) \ge n/16$, it joins $I$, and $\{i\} \cup N(\{i\})$ is deleted.
• Case 2. Otherwise all $q^2$ sample points are tried, the one whose coins make Algorithm B's select step eliminate the most edges is kept, and its $I'$ is used.

No random bits are used.

Formalization targets

Goal: the round bound and correctness of Algorithm D

For every graph $G$ on $n$ vertices, every prime $q$ with $n \le q \le 2n$, and every run of Algorithm D (every tie-break among maximum-degree vertices and every maximizing sample point), the loop body is executed exactly $k$ times, with

$$k \ \le\ \frac{\log(n^2)}{\log(18/17)} + 16 \ \le\ 25 \cdot \log_2 n + 16,$$

and the output $I$ is a maximal independent set of $G$.

Milestones

1. The sample space: Lemma 1, $\Pr[X_i = R_j] = n_{ij}/q$, and Lemma 2, $\Pr[X_i = R_j, X_{i'} = R_{j'}] = n_{ij} n_{i'j'}/q^2$ for $i \ne i'$.
2. The Technical Lemma: for $p_1 \ge \dots \ge p_n \ge 0$ and $c > 0$, $\max_l (\alpha_l - c\beta_l) \ge \tfrac12 \min\{\alpha_n, 1/c\}$.
3. The two steps of the proof of Theorem 1: $E[Y_k - Y_{k+1}] \ge \tfrac12 \sum_i d(i) \Pr[i \in N(I')]$, and $\tfrac12 \sum_{\mathrm{sum}(i) \le 2} d(i)\,\mathrm{sum}(i) + \sum_{\mathrm{sum}(i) > 2} d(i) \ge |E'|$.
4. Lemma C and Theorem 2: with pairwise independent coins of law $1/2d(i)$,

$$\Pr[i \in N(I')] \ge \tfrac18 \min\{\mathrm{sum}(i), 1\}, \qquad E[Y_k - Y_{k+1}] \ge \tfrac{1}{16} Y_k .$$

5. The rounding bound $\tfrac89 p_i \le p'_i \le p_i$ when $d(i) < n/16$.
6. Lemma D and Theorem 3: with pairwise independent coins of law $p'_i$ and all $d(i) < n/16$,

$$\Pr[i \in N(I')] \ge \tfrac19 \min\{\mathrm{sum}(i), 1\}, \qquad E[Y_k - Y_{k+1}] \ge \tfrac{1}{18} Y_k .$$

7. In Case 2 some sample point eliminates at least $1/18$ of the edges; Case 1 occurs at most 16 times in any run before it terminates.

Significance

The goal is the deterministic half of Luby's result: an MIS is computed in $O(\log n)$ parallel rounds with no randomness, which places MIS in deterministic NC. The pairwise-independent analysis (Lemmas C, D, Theorems 2, 3) is the reusable part: it shows that the Monte Carlo algorithm's progress guarantee survives when mutual independence is weakened to pairwise independence, which is what makes a sample space of size $q^2 = O(n^2)$ sufficient. Lemmas 1 and 2 are the standard construction of pairwise independent variables with prescribed rational marginals.

All of these results are proved in the paper. None is formalized on the platform. A related but different object is the platform's dot-product hash family (AlmostLossless.pairwiseIndependent_dotHash), which has uniform marginals over a field and is not the $q^2$-point matrix space with prescribed marginals $n_{ij}/q$. The companion mission A Simple Parallel Algorithm for the Maximal Independent Set Problem I formalizes Theorem 1, the mutually independent analysis of Algorithms A and B.

Difficulty

The obvious route to Theorem 2 repeats the proof of Lemma B, which lower-bounds $\Pr[i \in N(I')]$ by a product over independent events. Under pairwise independence the probability of an intersection of three or more coin events is not determined by the marginals, so that product argument fails, and the constant degrades from $\tfrac18$ to $\tfrac1{16}$.

The round bound needs a separate argument for high-degree vertices. The rounded probabilities $p'_i$ are close to $p_i$ only when $q/2d(i)$ is large, which is why vertices of degree at least $n/16$ are handled by Case 1. Counting the Case 1 rounds uses the vertex count $n$ of the original graph, not of the current one. Correctness at termination requires an invariant linking $I$, $V'$ and $G$ across both kinds of rounds and the deletion of isolated vertices.

Formalization scope

Vertices are Fin n with labels $0, \dots, n-1$, which is §4.2's indexing of $X_0, \dots, X_{n-1}$; the label enters $\mathbb{Z}/q\mathbb{Z}$ as a residue, and labels are distinct mod $q$ because $n \le q$. The current graph is the induced subgraph kept on the full vertex type, with deleted vertices isolated. One execution of the loop body is a relation between states $(I, V')$ that leaves the maximizing vertex (Case 1) and the maximizing sample point (Case 2) free, as the page does, and a run is any sequence of states starting at $(\emptyset, V)$ that follows the relation while $V' \ne \emptyset$. The goal asks for the first index $k$ with $V' = \emptyset$, so a statement about a later state or a bound on $k$ without termination does not meet it.

The conditions $d(i) \ge n/16$ and $d(i) < n/16$ are encoded exactly as $n \le 16\,d(i)$ and $16\,d(i) < n$ in $\mathbb{N}$. $\lfloor q/2d(i) \rfloor$ is natural-number division. The printed code tests $(x + y\cdot i) \bmod q \le n(i)$, which puts $n(i) + 1$ residues in $X$ and contradicts $p'_i = \lfloor p_i q \rfloor / q$ stated on the same page; the formalization uses the strict test.

Lemmas C, D and Theorems 2, 3 quantify over every probability space carrying measurable, pairwise independent (IndepFun for each pair of distinct vertices) coins with the stated marginals at vertices of positive degree. Replacing pairwise by mutual independence, or fixing the probability space, would weaken them. They are stated for a fixed current graph, that is, as the expectation conditional on the state before the round, which is what their proofs establish. Expectations are Bochner integrals of a function with finitely many values and are therefore genuine. Lemma 2 carries the hypothesis $i \ne i'$, implicit on the page.

The development needs the induced subgraph and degree bookkeeping from Mathlib's SimpleGraph, pairwise independence from ProbabilityTheory.IndepFun, finite counting in ZMod q, and real logarithms. The pairwise-independent analysis (Lemma C to Theorem 3) and the sample-space lemmas are reusable beyond this mission. Contributions to any milestone are welcome.

Selected references

• M. Luby, A Simple Parallel Algorithm for the Maximal Independent Set Problem, SIAM J. Comput. 15(4):1036–1053, 1986. https://doi.org/10.1137/0215074
• R. M. Karp and A. Wigderson, A Fast Parallel Algorithm for the Maximal Independent Set Problem, J. ACM 32(4):762–773, 1985. https://doi.org/10.1145/4221.4226
• N. Alon, L. Babai and A. Itai, A Fast and Simple Randomized Parallel Algorithm for the Maximal Independent Set Problem, J. Algorithms 7(4):567–583, 1986. https://doi.org/10.1016/0196-6774(86)90019-2

Motivation

The minimum-cost circulation problem is a central problem of network optimization: transportation, assignment, shortest-path and maximum-flow problems are all special cases, and it is one of the few classes of linear programs with fast combinatorial algorithms. The oldest algorithm for it, the cycle-canceling algorithm of Klein (1967), repeatedly finds a residual cycle of negative cost and pushes as much flow as possible around it. With an arbitrary choice of cycle it can take exponentially many iterations even on integer data, and it need not terminate at all when capacities are irrational.

Goldberg and Tarjan (J. ACM 36(4), 1989) showed that one simple selection rule repairs this: always cancel a residual cycle whose mean cost (cost divided by number of arcs) is as small as possible. The resulting algorithm is strongly polynomial: its number of iterations is bounded by a polynomial in the number of vertices and arcs alone, independent of the magnitudes of capacities and costs. This mission formalizes that bound.

Timeline:

• 1967, Klein: the cycle-canceling algorithm, without an iteration bound.
• 1972, Edmonds and Karp: the first polynomial algorithm for minimum-cost flow (capacity scaling), polynomial in the bit length of the capacities.
• 1985, Tardos: the first strongly polynomial algorithm, introducing the arc-fixing idea that Theorem 3.8 generalizes.
• 1987–1989, Goldberg and Tarjan: generalized cost scaling and ε-optimality; in this paper, minimum-mean cycle canceling terminates after O(nm² log n) iterations for real costs (Theorem 3.9) and O(nm log(nC)) for integer costs bounded by C (Theorem 3.7).

Setting

A circulation network is a finite directed graph $G=(V,E)$ with $n=|V|$ vertices and $m=|E|$ arcs, which is symmetric ($(v,w)\in E$ iff $(w,v)\in E$, so $m$ counts both directions), together with real capacities $u(v,w)$ and real costs $c(v,w)$, the cost being antisymmetric: $c(v,w)=-c(w,v)$.

A circulation is a real function $f$ on arcs satisfying $f(v,w)\le u(v,w)$, $f(v,w)=-f(w,v)$ on every arc, and conservation $\sum_{v:(w,v)\in E} f(v,w)=0$ at every vertex $w$. Its cost is $\operatorname{cost}(f)=\tfrac12\sum_{(v,w)\in E}c(v,w)f(v,w)$, and $f$ is minimum-cost (optimal) if no circulation has smaller cost.

The residual capacity of an arc is $u_f(v,w)=u(v,w)-f(v,w)$; arcs with $u_f>0$ are residual arcs. A residual cycle is a simple cycle of residual arcs; its capacity is the minimum residual capacity along it, its cost $c(\Gamma)$ is the sum of its arc costs, and its mean cost is $c(\Gamma)/|\Gamma|$. Canceling a residual cycle raises the flow on each of its arcs by its capacity (and lowers the flow on each reverse arc by the same amount).

The minimum-mean cycle-canceling algorithm starts from any circulation and, while some residual cycle has negative cost, cancels a residual cycle whose mean cost is minimum among all residual cycles. Ties are broken arbitrarily, so the algorithm is a nondeterministic process; a run of length $K$ is any sequence $f_0,\dots,f_K$ of circulations produced by $K$ such iterations.

The analysis uses a price function $p:V\to\mathbb R$, the reduced cost $c_p(v,w)=c(v,w)+p(v)-p(w)$, and ε-optimality: for $\varepsilon\ge0$, $f$ is ε-optimal if some $p$ gives $c_p(v,w)\ge-\varepsilon$ on every residual arc. The quantity $\varepsilon(f)$ is the least such $\varepsilon$, and an arc is ε-fixed if all ε-optimal circulations carry the same flow on it.

Formalization targets

Goal: Theorem 3.9, with the proof's constant

For every circulation network with $n\ge2$ vertices, $m$ arcs, arbitrary real capacities and arbitrary real antisymmetric costs, every run of the minimum-mean cycle-canceling algorithm has length

$$K\ \le\ n\,m^2\,\lceil \ln n+1\rceil .$$

The statement quantifies over all starting circulations, all tie-breaking choices and all real data; it is the paper's $O(nm^2\log n)$ with the constant its proof establishes.

Milestones

In the order the proof uses them: Theorem 2.1 (optimal iff no negative residual cycle), Theorem 3.1 (optimal iff some price function has $c_p\ge0$ on residual arcs), Theorem 3.3 ($\varepsilon(f)=-\mu(f)$ for nonoptimal $f$, where $\mu(f)$ is the minimum cycle mean of the residual graph), Lemma 3.5 (a minimum-mean cancellation does not increase $\varepsilon(f)$), Lemma 3.6 ($m$ cancellations shrink $\varepsilon(f)$ by a factor $1-1/n$), and Theorem 3.8 (an arc with $|c_p(v,w)|\ge2n\varepsilon$ is ε-fixed).

Significance

Theorem 3.9 shows that a classical, natural algorithm is strongly polynomial: its iteration count depends only on the combinatorial size of the network. Combined with Karp's $O(nm)$ minimum-mean cycle algorithm it yields an $O(n^2m^3\log n)$ strongly polynomial algorithm (Theorem 3.10), and its method, measuring progress by the minimum cycle mean and fixing arcs once $\varepsilon(f)$ is small, underlies the faster cancel-and-tighten algorithm of Section 4 and later strongly polynomial analyses of network-flow and related algorithms.

The theorem has been proved since 1989; this mission's contribution is a machine-checked proof. To the best of the platform's catalogue, no cycle-canceling bound, minimum cycle mean or ε-optimality statement has been formalized. The platform does hold the negative-cycle optimality criterion in a different model (LinearOptimization.network_no_negative_cycle_optimal, Bertsimas–Tsitsiklis Theorem 7.6, with nonnegative flows and supplies) and a flow decomposition theorem (LinearOptimization.network_flow_decomposition); both are related to milestones here but are stated for a different network model.

Difficulty

The obvious potential function, the cost of the circulation, decreases at every iteration but by amounts that depend on the data, so it yields no bound independent of the capacities and costs. The analysis instead has to track $\varepsilon(f)$, an infimum over price functions, and relate it to the minimum cycle mean of a residual graph that changes after each cancellation, including arcs that appear only because of earlier cancellations. The strongly polynomial part needs a second ingredient: showing that the flow on some arc never changes again, which requires comparing the current circulation with all other ε-optimal circulations of the network, not only those the algorithm visits.

Formalization scope

Vertices form a finite type V; the arc set is E : Finset (V × V); capacities, costs and flows are real functions V → V → ℝ read only on E. $n$ is Fintype.card V and $m$ is E.card, counting $(v,w)$ and $(w,v)$ separately, as in the paper. Cycles are nonempty duplicate-free vertex lists, whose arcs are the cyclically consecutive pairs; one- and two-vertex cycles are allowed and have cost $0$. Minimum mean is taken over all residual simple cycles of the current circulation. $\varepsilon(f)$ is an infimum (sInf) over a set that is nonempty and bounded below for every circulation; its attainment is to be proved, never assumed.

Explicit constants replacing the paper's $O(\cdot)$:

• Theorem 3.9: the paper prints $O(nm^2\log n)$; its proof uses groups of $k=m\,n\lceil\ln n+1\rceil$ iterations, at most $m$ of them, so the goal states $K\le n\,m^2\lceil\ln n+1\rceil$ with the natural logarithm.
• The standing assumption $n\ge2$ (p. 874) is kept on the goal; the standing assumption $m\ge n$ is not used by the proof and is omitted.

"Terminates after at most $B$ iterations" means that every run has length at most $B$. Asserting only that some run is short, or that the process eventually stops, does not formalize the theorem; nor does a step relation that drops negativity, simplicity of the cycle, minimality of the mean over all residual cycles, or the update by exactly the cycle's capacity.

A complete development needs cycle decomposition of the difference of two circulations, LP duality for circulations (Theorem 3.1), and bookkeeping for the residual graph under cancellation. These are reusable for any cycle-canceling or cost-scaling analysis, and contributions of that infrastructure as separate lemmas are welcome. Theorem 3.7 (the integer-cost bound) and Section 4 are outside this mission.

Selected references

• A. V. Goldberg, R. E. Tarjan, Finding Minimum-Cost Circulations by Canceling Negative Cycles, J. ACM 36(4):873–886, 1989. https://doi.org/10.1145/76359.76368
• M. Klein, A primal method for minimal cost flows with applications to the assignment and transportation problems, Management Science 14(3):205–220, 1967. https://doi.org/10.1287/mnsc.14.3.205
• É. Tardos, A strongly polynomial minimum cost circulation algorithm, Combinatorica 5(3):247–255, 1985. https://doi.org/10.1007/BF02579369
• A. V. Goldberg, R. E. Tarjan, Finding minimum-cost circulations by successive approximation, Mathematics of Operations Research 15(3):430–466, 1990. https://doi.org/10.1287/moor.15.3.430
• R. M. Karp, A characterization of the minimum cycle mean in a digraph, Discrete Mathematics 23(3):309–311, 1978. https://doi.org/10.1016/0012-365X(78)90011-0
• J. Edmonds, R. M. Karp, Theoretical improvements in algorithmic efficiency for network flow problems, J. ACM 19(2):248–264, 1972. https://doi.org/10.1145/321694.321699

Motivation

A branching in a directed graph is a set of edges that contains no cycle (even ignoring directions) and in which no two edges point to the same node; a connected branching is an arborescence, a tree rooted at one node with all edges directed away from the root. The optimum branching problem asks, for real weights on the edges, for a branching of maximum total weight. It contains the minimum-cost spanning arborescence problem (the directed analogue of the minimum spanning tree), which appears in network design, in the analysis of broadcast and routing structures, in phylogenetics, and in dependency parsing in computational linguistics, where maximum spanning arborescences are the standard decoding step of graph-based parsers.

J. Edmonds solved the problem in Optimum branchings (J. Res. Nat. Bur. Standards 71B (1967) 233–240). The paper gives an algorithm (the shrinking algorithm usually attributed to Chu–Liu and Edmonds) and, proved together with it, a polyhedral theorem: the linear system that every branching obviously satisfies has no other vertices. This was one of the first integral polyhedron theorems beyond bipartite matching and network flows, and together with Edmonds' matching polytope (1965) it set the pattern of polyhedral combinatorics: describe the convex hull of the combinatorial objects by linear inequalities, and prove optimality by a linear programming dual.

Timeline:

• 1965: Y. J. Chu and T. H. Liu describe the shrinking algorithm for the maximum arborescence.
• 1965: Edmonds, Paths, trees, and flowers and Maximum matching and a polyhedron with 0,1-vertices: the matching polytope.
• 1967: Edmonds, Optimum branchings: the algorithm, Theorem 2 (vertices of the branching polyhedron), and the dual certificate built along the algorithm.
• 1970–1971: Edmonds' matroid intersection theorem, which contains the branching polyhedron theorem as the intersection of a graphic matroid and a partition matroid.
• 1977–1986: faster implementations (Tarjan; Gabow, Galil, Spencer and Tarjan).

Setting

A graph $G$ consists of a finite set $V$ of nodes and a finite set $E$ of edges. Each edge $e$ is directed toward a node $\mathrm{front}(e)$, its front end, and away from a different node $\mathrm{rear}(e)$, its rear end. Parallel edges are allowed; loops are not.

For $F\subseteq E$, a node $v$ meets $k$ edges of $F$ if $\#\{e\in F:\mathrm{front}(e)=v\}+\#\{e\in F:\mathrm{rear}(e)=v\}=k$. A set $B\subseteq E$ is a forest if it contains no polygon, i.e. no nonempty $F\subseteq B$ in which every node meets zero or two edges of $F$; it is a branching if in addition distinct edges of $B$ have distinct front ends. The incidence vector $x^B\in\mathbb R^E$ of $B$ has $x^B_e=1$ for $e\in B$ and $0$ otherwise.

The branching polyhedron $P_G\subseteq\mathbb R^E$ is the set of $x$ with

• $(L_1)$ $x_e\ge0$ for every edge $e$;
• $(L_2)$ $\sum_{e:\,\mathrm{front}(e)=v}x_e\le1$ for every node $v$;
• $(L_3)$ $\sum_{e:\,\mathrm{front}(e),\mathrm{rear}(e)\in S}x_e\le|S|-1$ for every set $S$ of two or more nodes.

A vertex of a set $P\subseteq\mathbb R^E$ is a point of $P$ that is the unique maximizer over $P$ of some linear function $x\mapsto\sum_e c_ex_e$.

For weights $c\in\mathbb R^E$, the dual variables are $y_h$ for each node $v_h$ and $y_S$ for each $S$ with $|S|\ge2$; write $w_e=\sum_{S\ni\mathrm{front}(e),\mathrm{rear}(e)}y_S$ and $(b,y)=\sum_hy_h+\sum_S(|S|-1)y_S$. Edmonds' conditions are (15) $y_h\ge0$, (16) $y_S\ge0$, (17) $y_{\mathrm{front}(e)}+w_e\ge c_e$ for every edge, and, for a branching $B$, (18) $y_h\ne0\Rightarrow$ some edge of $B$ enters $v_h$, (19) $y_S\ne0\Rightarrow$ exactly $|S|-1$ edges of $B$ lie inside $S$, (20) $y_{\mathrm{front}(e)}+w_e=c_e$ for $e\in B$.

Formalization targets

Goal: Theorem 2 (p. 235)

$$\{x:\ x\text{ is a vertex of }P_G\}\;=\;\{x^B:\ B\text{ is a branching of }G\}.$$

Both inclusions, for every finite loopless directed multigraph.

Milestones

1. §5, p. 236: for every branching $B$, $x^B\in P_G$.
2. §5, p. 236: for every branching $B$, $x^B$ is a vertex of $P_G$.
3. §6, (12)–(14): if $B$ is a branching and $y$ satisfies (15)–(20), then $(c,x^B)=(b,y)$, $x^B$ maximizes $(c,x)$ over $P_G$, and $y$ minimizes $(b,y)$ subject to (15)–(17).
4. §7, p. 237: for every $c\in\mathbb R^E$ there are a branching $B$ and a $y$ satisfying (15)–(20).
5. Lemma 1, p. 236: for every $c\in\mathbb R^E$ some branching vector lies in $P_G$ and maximizes $\sum_ec_ex_e$ over $P_G$.

Significance

Theorem 2 says that the linear program $\max\{(c,x):x\in P_G\}$ always has an optimal solution that is a branching, and that every vertex of $P_G$ is one. Consequently optimum branchings, and after the reductions of the paper's §2 optimum spanning and rooted arborescences, can be computed by linear programming, and their optimality is certified by a dual vector satisfying (15)–(20). The same statement underlies the separation-based treatment of arborescence constraints in integer programming formulations of network design and of the asymmetric travelling salesman problem. The integrality of the dual for integer weights (the paper's §8) yields min–max theorems of König type for branchings.

The result is proved and classical; no machine-checked proof of it in a proof assistant is known. The mission asks for the paper's own proof chain: branching vectors are points and vertices of $P_G$, linear programming optimality from complementary slackness, existence of a dual certificate for every weight vector, and the deduction of Theorem 2. Proofs through matroid intersection or total dual integrality would also establish the goal and are welcome as alternative routes.

Difficulty

The inclusion "branching vectors are vertices" and the certificate criterion are short. The substance is Milestone 4: for arbitrary real weights, a branching and a dual vector satisfying the complementary slackness conditions must exist simultaneously. Finiteness gives an optimum branching at once, but that says nothing about optimality over the fractional points of $P_G$; the difficulty is the dual. The natural attempt, taking $y_S=0$ for all sets and $y_h$ the largest positive weight entering $v_h$, violates (20) as soon as the greedy choice closes a circuit: the $(L_3)$ duals of nested node sets, arising from repeatedly shrinking circuits, are needed, and they must be kept nonnegative through weight changes of the form $c_3+c_0-c_4$ on edges entering a shrunk circuit.

Formalization scope

A graph is a structure Graph V E with front rear : E → V and a proof that front e ≠ rear e; V and E carry Fintype and DecidableEq. Edge sets are Finset E; vectors are E → ℝ; the linear function with weights c is ∑ e, c e * x e. A branching is defined combinatorially (no nonempty edge subset in which every node meets zero or two edges, and distinct front ends), never by counting edges inside node sets, and $P_G$ is the solution set of $(L_1)$–$(L_3)$, never a convex hull; either shortcut would make half of Theorem 2 true by definition. A vertex is a unique maximizer of a linear function, as on p. 236 (Mathlib's Set.exposedPoints has the same content); the set variables of the dual are a function Finset V → ℝ whose values on sets of fewer than two nodes are ignored. The right side of $(L_3)$ is the real number $|S|-1$.

Implicit conventions made explicit: the no-loop condition is part of the graph (with a loop $e$, the vector of $\{e\}$ is a vertex of $P_G$ but not a branching); parallel edges are allowed; weights have arbitrary sign and the empty branching is allowed. The mission does not model the algorithm of §4 or Theorem 1's notion of a "good" algorithm; Milestone 4 states only the existence of a certificate, which is what Lemma 1 uses.

Useful reusable infrastructure: finite directed multigraphs with an edge type, forests via polygons, and a finite LP duality lemma for $\max\{c^\top x: x\ge0,\ Ax\le b\}$; contributions of either are welcome.

Selected references

• J. Edmonds, Optimum branchings, J. Res. Nat. Bur. Standards Sect. B 71B (1967), 233–240. https://doi.org/10.6028/jres.071b.032
• Y. J. Chu and T. H. Liu, On the shortest arborescence of a directed graph, Scientia Sinica 14 (1965), 1396–1400.
• J. Edmonds, Maximum matching and a polyhedron with 0,1-vertices, J. Res. Nat. Bur. Standards 69B (1965), 125–130. https://doi.org/10.6028/jres.069B.013
• R. E. Tarjan, Finding optimum branchings, Networks 7 (1977), 25–35. https://doi.org/10.1002/net.3230070103
• H. N. Gabow, Z. Galil, T. Spencer and R. E. Tarjan, Efficient algorithms for finding minimum spanning trees in undirected and directed graphs, Combinatorica 6 (1986), 109–122. https://doi.org/10.1007/BF02579168
• A. Schrijver, Combinatorial Optimization: Polyhedra and Efficiency, Springer (2003), Chapter 52.