Theoretical Computer Science

Combinatorics Graph Theory·Captain: mikedeng1

Eigenvalues and Expanders: A Regular Bipartite Graph Is a Strong Expander If and Only If λ(G) Is Bounded Away from 0Research Paper

Motivation

Expander graphs are sparse graphs in which every set of vertices has many neighbours. Families of them with bounded degree and expansion bounded away from zero are a basic tool of theoretical computer science: they are the main component of the sorting network of Ajtai, Komlós and Szemerédi (AKS 1983), the building block of superconcentrators and other graphs with strong connectivity properties, and an ingredient of many later constructions in coding theory, derandomization and complexity.

Expansion is hard to certify. Checking that every set of vertices has many neighbours means looking at exponentially many sets, and computing the exact expansion of a graph is coNP-complete. A spectral quantity, by contrast, is computable in polynomial time. N. Alon's paper Eigenvalues and expanders (Combinatorica 6 (1986) 83–96) proves that for regular bipartite graphs the two notions are equivalent: a graph is a strong expander if and only if the second-smallest eigenvalue of its Laplacian is bounded away from 0, with explicit constants in both directions. This is a discrete counterpart of Cheeger's inequality for Riemannian manifolds.

Timeline.

1983: Ajtai, Komlós and Szemerédi use bounded-degree bipartite expanders to build sorting networks of depth $O(\log n)$ .
1984: Tanner (SIAM J. Alg. Disc. Meth. 5) bounds the neighbourhood size of a set in a regular bipartite graph by its second eigenvalue, the direction "eigenvalue gap implies expansion".
1985: Alon and Milman (J. Combin. Theory Ser. B 38) prove isoperimetric inequalities for graphs in terms of $\lambda(G)$ and introduce enlargers.
1986: Alon proves the converse direction, "expansion implies an eigenvalue gap" (Lemma 2.4 and Theorem 3.4 of the paper).

Setting

All graphs are finite and simple. For a graph $G = (V, E)$ and a set $X \subseteq V$ , $N(X) = \{v \in V : vx \in E \text{ for some } x \in X\}$ is the set of neighbours of $X$ ; it may meet $X$ .

The Laplacian of $G$ is $Q_G = \mathrm{diag}(d(v))_{v \in V} - A_G$ , where $A_G$ is the 0–1 adjacency matrix and $d(v)$ the degree of $v$ . It is symmetric with eigenvalues $0 = \lambda_0 \le \lambda_1 \le \dots \le \lambda_{n-1}$ , counted with multiplicity, and $\lambda(G) = \lambda_1$ is its second-smallest eigenvalue. It is positive exactly when $G$ is connected.

An $(n, d, c)$ -magnifier is a graph on $n$ vertices with maximal degree $d$ in which every $X \subseteq V$ with $|X| \le n/2$ satisfies $|N(X) - X| \ge c|X|$ .
An $(n, d, \varepsilon)$ -enlarger is a graph on $n$ vertices with maximal degree $d$ and $\lambda(G) \ge \varepsilon$ .
A bipartite graph $G = (I, O; E)$ has inputs $I$ , outputs $O$ and edges only between $I$ and $O$ . It is a strong $(n, d, c)$ -expander if $|I| = |O| = n$ , the maximal degree is $d$ , and for every $X \subseteq I$

|N(X)| \ge \Bigl(1 + c\Bigl(1 - \frac{|X|}{n}\Bigr)\Bigr)|X|.

Formalization targets

Goal: Theorem 3.4

Let $G = (I, O; E)$ be a $d$ -regular bipartite graph with $|I| = |O| = n$ and $\lambda = \lambda(G)$ .

If $G$ is a strong $(n, d, c)$ -expander then

\lambda \ge \frac{c^2}{1024 + 2c^2}.

If $\lambda \ge \varepsilon$ then $G$ is a strong $(n, d, c)$ -expander with

c = \frac{2d\varepsilon - \varepsilon^2}{d^2}.

Milestones, in the order of the paper

Lemma 2.2 (Alon–Milman, already on the platform): for disjoint sets $A, B$ at distance $\varrho > 1$ , $b \le (1-a)/(1 + (\lambda/d)a\varrho^2)$ .
Corollary 2.3: every $(n, d, \varepsilon)$ -enlarger is an $(n, d, 2\varepsilon/(d+2\varepsilon))$ -magnifier.
Eq. (2.1): if $f$ is an eigenvector of $Q_G$ for $\lambda(G)$ and $g$ its positive part, then $\sum_{uv \in E}(g(u)-g(v))^2 \le \lambda \sum_v g^2(v)$ .
Lemma 2.4: every $(n, d, c)$ -magnifier has $\lambda(G) \ge c^2/(4 + 2c^2)$ .
Lemma 3.1: a strong $(n, d, c)$ -expander is a $(2n, d, c/16)$ -magnifier.
Proof of Lemma 3.3, spectrum: the two largest eigenvalues of $C^TC$ , with $C$ the $I \times O$ biadjacency matrix, are $d^2$ and $(d - \lambda)^2$ .
Proof of Lemma 3.3, Tanner's bound: $|N(X)| \ge d^2|X| / \bigl(\alpha(d^2 - (d-\lambda)^2) + (d-\lambda)^2\bigr)$ with $\alpha = |X|/n$ .
Lemma 3.3: a $d$ -regular bipartite graph is a strong $(n, d, (2d\lambda - \lambda^2)/d^2)$ -expander.

Part (1) of the goal combines Lemmas 3.1 and 2.4; part (2) follows from Lemma 3.3.

Significance

The result. Theorem 3.4 makes expansion of regular bipartite graphs checkable in polynomial time up to a constant-factor loss. A random regular bipartite graph can be generated and its expansion certified by computing one eigenvalue. Lemma 2.4 is one of the first discrete Cheeger inequalities. Together with Corollary 2.3 it shows that magnifiers and enlargers are the same graphs up to the constants, and it underlies the later theory of spectral expanders, including the Alon–Boppana bound and Ramanujan graphs.

The formalization. The results are proved in the paper. The work is to formalize the known proofs. That includes Tanner's eigenvalue bound, which the paper only cites, and a max-flow min-cut argument, for which Mathlib has no general theorem. No machine-checked version of Lemma 2.4, Lemma 3.1, Lemma 3.3 or Theorem 3.4 is known to exist. Lemma 2.2 is already stated and proved on the platform as part of the Alon–Milman mission.

Difficulty

The direction "eigenvalue gap implies expansion" is a variational argument on the spectrum of $C^TC$ . The converse is the hard one. A first attempt bounds $\lambda(G)$ from below by testing the Rayleigh quotient on indicator vectors of sets. That only gives upper bounds on $\lambda$ : any one test vector does. A lower bound has to control every vector orthogonal to the constants at once. The paper first reduces to the positive part of an eigenvector (Eq. (2.1)). It then turns the combinatorial expansion of the graph into an analytic inequality for that function, using a network flow whose existence comes from the max-flow min-cut theorem. Step (ii) of the flow conditions printed on p. 87 is false as stated: the arcs $(u, u)$ of the network absorb part of the flow. The flow argument has to be repaired before it can be formalized.

Lemma 3.1 has its own obstacle: one-sided expansion of inputs must be converted into expansion of arbitrary vertex sets that mix inputs and outputs. This needs the strong form of expansion; for ordinary expanders the lemma is false.

Formalization scope

Graphs are SimpleGraph V on a Fintype. A bipartite graph lives on the sum type I ⊕ O, and IsIOBipartite forbids edges inside I and inside O. Cardinalities $|N(X)|$ are Set.ncard. "Maximal degree $d$ " is read as G.maxDegree ≤ d; every statement is monotone in $d$ or fixes $d$ by regularity (G.IsRegularOfDegree d). The condition $|X| \le n/2$ is written $2|X| \le n$ in $\mathbb{N}$ . All constants are real, and every subtraction and division is taken in $\mathbb{R}$ .

Reused published items:

$\lambda(G)$ is AlonMilman.Diameter.lambda1, the second-smallest eigenvalue of G.lapMatrix ℝ, which is $0$ by convention on fewer than two vertices.
$N(X)$ is AKSSorting.Core.neighbours.
Lemma 2.2 is AlonMilman.Diameter.theorem_2_5, which carries Alon–Milman's standing hypotheses that $G$ is connected and $n \ge 2$ ; outside them the inequality is trivial.

The page omits a few degenerate cases, and the following hypotheses are added for them. Each is necessary, with a counterexample recorded in the item's statement:

$n \ge 1$ and $c \ge 0$ in Theorem 3.4 (1);
$\varepsilon > 0$ in Theorem 3.4 (2);
$n \ge 2$ and $c \ge 0$ in Lemma 2.4;
$n \ge 2$ in Lemma 3.1 and in the $C^TC$ statement;
$d \ge 1$ in Lemma 3.3;
$\varepsilon \ge 0$ in Corollary 2.3.

Eq. (2.1) is stated in multiplied form, so no quotient by $\sum g^2$ appears.

The closing sentences of Theorem 2.5 and Theorem 3.4 ("Thus … one can prove efficiently …") are not formalized. Read as implications between expanders they reduce to monotonicity in $c$ , because $c' \le c$ ; their content is algorithmic.

Several encodings would trivialize the mission and are excluded:

a $\lambda$ other than the published second-smallest Laplacian eigenvalue, in particular one defined as the best constant of a quotient;
expansion or magnifier conditions with a negative constant in a hypothesis;
$|X| \le n/2$ with truncating natural-number division.

Contributions are welcome:

Tanner's bound in Lean, which is reusable for any regular bipartite graph;
a max-flow min-cut theorem for finite networks;
the corrected flow lemma behind Eqs. (2.2)–(2.3);
the spectral facts about $\lambda(G)$ for bipartite graphs ( $\lambda \le d$ for $n \ge 2$ , and $\lambda = d - \sigma_2(C)$ ).

Selected references

N. Alon, Eigenvalues and expanders, Combinatorica 6 (1986) 83–96. https://doi.org/10.1007/BF02579166
N. Alon and V. D. Milman, λ₁, isoperimetric inequalities for graphs, and superconcentrators, J. Combin. Theory Ser. B 38 (1985) 73–88. https://doi.org/10.1016/0095-8956(85)90092-9
R. M. Tanner, Explicit concentrators from generalized N-gons, SIAM J. Algebraic Discrete Methods 5 (1984) 287–293. https://doi.org/10.1137/0605030
M. Ajtai, J. Komlós and E. Szemerédi, Sorting in c log n parallel steps, Combinatorica 3 (1983) 1–19. https://doi.org/10.1007/BF02579338

16 thms3 active usersReviewed

Completed

Algorithmic Game Theory Linear Optimization Operations Research·Captain: mikedeng1

Online Primal-Dual Algorithms for Maximizing Ad-Auctions Revenue: The Competitive Ratio of the Primal-Dual Allocation AlgorithmResearch Paper

Motivation

Search engines sell advertisement slots next to their results through ad-auctions. Advertisers bid on keywords, and each advertiser also sets a daily budget: the most it is willing to pay in a day. Queries arrive one at a time and each must be assigned to an advertiser at once, with no knowledge of the queries still to come. The seller's revenue from an advertiser is capped by its budget, so an allocation rule that ignores budgets can exhaust a high bidder early and forgo revenue that a more even allocation would have collected. The question is how much of the offline optimum an online rule can guarantee against every arrival sequence.

Mehta, Saberi, Vazirani and Vazirani (FOCS 2005 / J. ACM 2007) gave a deterministic algorithm whose competitive ratio tends to $1 - 1/e$ when bids are small compared with budgets, and showed that no deterministic algorithm does better. Their algorithm builds on online bipartite matching (Karp, Vazirani and Vazirani, STOC 1990) and online $b$ -matching (Kalyanasundaram and Pruhs, 2000). Buchbinder, Jain and Naor (ESA 2007) rederived the $1 - 1/e$ bound with an online primal-dual algorithm, which gives the ratio in closed form for every value of the bid-to-budget ratio and extends to multiple slots, stochastic information, bounded degree and budget flexibility. This mission formalizes the basic algorithm of that paper and its Theorem 1.

Setting

There is a finite nonempty set $I$ of buyers. Buyer $i$ has a known budget $B(i) > 0$ . Products $j = 1, \dots, m$ arrive one by one; when product $j$ arrives, every buyer's bid $b(i,j) \ge 0$ on it is revealed. The bid-to-budget ratio is

R_{\max} = \max_{i \in I,\, j} \frac{b(i,j)}{B(i)} .

A fractional allocation $y(i,j) \ge 0$ assigns fractions of products to buyers; the revenue from buyer $i$ is the minimum of $\sum_j b(i,j)\,y(i,j)$ and $B(i)$ .

The offline fractional problem is the packing LP, which the paper calls the dual:

\max \sum_{j}\sum_{i} b(i,j)\,y(i,j) \quad\text{s.t.}\quad \sum_i y(i,j) \le 1 \ \ \forall j,\qquad \sum_j b(i,j)\,y(i,j) \le B(i)\ \ \forall i,\qquad y \ge 0 .

Its LP dual, the paper's primal, is the covering LP:

\min \sum_i B(i)\,x(i) + \sum_j z(j) \quad\text{s.t.}\quad b(i,j)\,x(i) + z(j) \ge b(i,j)\ \ \forall i,j,\qquad x, z \ge 0 .

The Allocation Algorithm has a parameter $c > 1$ and starts from $x \equiv 0$ . When product $j$ arrives it takes a buyer $i$ maximizing $b(i,j)(1 - x(i))$ . If $x(i) \ge 1$ , the product is not sold. Otherwise it charges $i$ the minimum of $b(i,j)$ and $i$ 's remaining budget, sets $y(i,j) \leftarrow 1$ and $z(j) \leftarrow b(i,j)(1 - x(i))$ , and updates

x(i) \leftarrow x(i)\Big(1 + \frac{b(i,j)}{B(i)}\Big) + \frac{b(i,j)}{(c-1)\,B(i)} .

Its revenue is the total amount charged.

Formalization targets

Goal: Theorem 1

For every instance and every bound $R > 0$ with $b(i,j) \le R\,B(i)$ for all $i, j$ , the Allocation Algorithm run with $c = (1+R)^{1/R}$ , under any tie-breaking of the maximum, satisfies for every feasible $y'$ of the packing LP

\mathrm{Revenue} \;\ge\; \Big(1 - \frac1c\Big)(1 - R)\sum_{j}\sum_{i} b(i,j)\,y'(i,j).

With $R = R_{\max}$ this is the paper's statement that the algorithm is $(1 - 1/c)(1 - R_{\max})$ -competitive; the fractional optimum bounds every integral offline allocation.

Milestones

The proof of Theorem 1 rests on three claims and three auxiliary facts, each a milestone:

the inequality $\ln(1+x)/x \ge \ln(1+y)/y$ for $0 < x \le y \le 1$ ;
Claim (1): the final $(x, z)$ is feasible for the covering LP;
Claim (2): the covering cost of the run equals $(1 + 1/(c-1))$ times the packing value of the run's own $y$ ;
Inequality (1): $x(i) \ge \frac{1}{c-1}\big(c^{\sum_j b(i,j) y(i,j)/B(i)} - 1\big)$ at every stage of the run;
Claim (3): $\sum_j b(i,j)\,y(i,j) \le B(i) + \max_j b(i,j)$ , and the amount charged to $i$ is at least $(1 - R)\sum_j b(i,j)\,y(i,j)$ ;
weak duality for the LP pair above;

and, separately, the second sentence of Theorem 1,

\lim_{R\to 0^+}\Big(1 - \frac{1}{(1+R)^{1/R}}\Big)(1-R) = 1 - \frac1e .

Significance

Theorem 1 gives an explicit ratio for every value of $R_{\max}$ , not only in the limit. It tends to the optimal deterministic ratio $1 - 1/e$ as bids become small, and it quantifies how the guarantee degrades as single bids become a larger share of a budget. The primal-dual analysis is the template for the paper's later sections and for a line of work on online packing and covering problems, surveyed in Buchbinder and Naor's monograph The Design of Competitive Online Algorithms via a Primal-Dual Approach (Foundations and Trends in TCS, 2009).

The result is proved in the paper, and the proof is short. What this mission adds is a machine-checked proof about an algorithm that is defined, not described: the run is computed by recursion from the instance, and the guarantee is proved for that run and every tie-breaking. A related private mission on the platform, The Design of Competitive Online Algorithms via a Primal-Dual Approach VI: Maximizing Ad-Auctions Revenue, states the monograph's Theorem 10.1, which is this theorem, in a form that takes the analysis's intermediate inequalities as hypotheses over arbitrary lists of won bids; the present mission states it for the algorithm itself. No machine-checked proof of Theorem 1 is known to this mission.

Difficulty

Each step of the proof is elementary; the difficulty is the bookkeeping of an online process. Claims (1) and (2) are statements about a single iteration that must be lifted to the whole run: Claim (1) uses that $x$ only increases, and Claim (2) that each product is processed once. Inequality (1) is an induction over the iterations that allocate to one buyer, interleaved with iterations that allocate to others and is the only place where the value of $c$ matters. Claim (3) needs a further invariant: the amount charged equals the minimum of the allocated bids and the budget.

A tempting shortcut is to take Inequality (1) and the "at most one undercharge" fact as hypotheses about some list of bids. That does not describe the algorithm and is not the theorem; here the only hypotheses are on the instance and on the tie-breaking rule.

Formalization scope

Buyers are a type I with [Fintype I] and [Nonempty I]; products are Fin m, whose order is the arrival order. Bids and budgets are real, with $B(i) > 0$ and $b(i,j) \ge 0$ . The state of the algorithm records $x$ , the amounts charged, $y$ and $z$ ; one iteration is step, the run after $k$ products is runPrefix, and revenue sums the charges of the final state. The tie-breaking rule is a function sel of the current $x$ and the product, required to return a maximizer of $b(i,j)(1-x(i))$ ; the theorem holds for every such rule. The constant $c = (1+R)^{1/R}$ is a real power and requires $R > 0$ . The theorem is stated for any bound $R$ on the ratios, of which the exact maximum is one instance. Claims (1) and (2) are stated for every $c > 1$ , which covers the paper's choice. The paper's inequality for $\ln(1+x)/x$ allows $x = 0$ , read as a limit; the Lean statement requires $x > 0$ .

A statement over an unconstrained allocation, or one conditioned on the proof's own intermediate inequalities, would be trivially true or false; the targets here concern only the run the definitions compute.

The development needs finite sums, real powers and logarithms from Mathlib and an induction principle for the run. The LP pair and weak duality are reusable for the paper's extensions, and the run invariants for any primal-dual online algorithm with multiplicative updates. Proofs of any milestone are welcome, as are sharper variants, such as the exact- $R_{\max}$ form or the bound against integral allocations.

Selected references

N. Buchbinder, K. Jain, J. Naor, Online Primal-Dual Algorithms for Maximizing Ad-Auctions Revenue, Algorithms – ESA 2007, LNCS 4698, 2007. https://doi.org/10.1007/978-3-540-75520-3_24
A. Mehta, A. Saberi, U. Vazirani, V. Vazirani, AdWords and Generalized Online Matching, Journal of the ACM 54(5), 2007. https://doi.org/10.1145/1284320.1284321
R. M. Karp, U. V. Vazirani, V. V. Vazirani, An Optimal Algorithm for On-line Bipartite Matching, STOC 1990. https://doi.org/10.1145/100216.100262
B. Kalyanasundaram, K. R. Pruhs, An Optimal Deterministic Algorithm for Online b-Matching, Theoretical Computer Science 233(1–2), 2000. https://doi.org/10.1016/S0304-3975(99)00140-1
N. Buchbinder, J. Naor, The Design of Competitive Online Algorithms via a Primal-Dual Approach, Foundations and Trends in Theoretical Computer Science 3(2–3), 2009. https://doi.org/10.1561/0400000024

10 thms3 active usersReviewed

Completed

Number Theory Probability Quantum Information·Captain: mikedeng1

Polynomial-Time Algorithms for Prime Factorization and Discrete Logarithms on a Quantum Computer 3: The Success Probability of Quantum Order FindingResearch Paper

Motivation

The security of the RSA cryptosystem rests on the assumed difficulty of factoring large integers, and the best known classical algorithms for factoring run in super-polynomial time. In 1994 Peter Shor showed that a quantum computer can factor an $n$ -digit integer in time polynomial in $n$ (Shor, SIAM J. Comput. 1997; conference version FOCS 1994). The algorithm has two parts. A classical reduction, due to Miller (1976), turns factoring into order finding: given $x$ coprime to $n$ , find the least $r \ge 1$ with $x^r \equiv 1 \pmod n$ . The quantum part solves order finding.

This mission formalizes the quantum part as Shor analyzes it in §5 of the journal paper: the construction of the quantum state, the probability of each measurement outcome, and the classical post-processing that reads $r$ off the measured value. The paper's claim is that one run of this procedure returns $r$ with probability at least $\varphi(r)/3r$ .

Timeline:

1976: Miller reduces factoring to order finding (with randomization).
1985–1994: Deutsch, Bernstein–Vazirani and Simon give the quantum Fourier sampling ideas the algorithm builds on.
1994: Shor's FOCS paper introduces the factoring and discrete logarithm algorithms.
1997: the SIAM J. Comput. version gives the analysis formalized here, with $q$ the power of $2$ in $[n^2, 2n^2)$ .

Setting

Fix an integer $n \ge 2$ and an integer $x$ coprime to $n$ . Its order $r$ is the least $r \ge 1$ with $x^r \equiv 1 \pmod n$ ; since $x$ is a unit, $r \le \varphi(n) < n$ . Let $q = 2^l$ be the power of $2$ with $n^2 \le q < 2n^2$ .

A quantum state on two registers, the first holding $0 \le a < q$ and the second a residue $y \in \mathbb{Z}/n$ , is a complex vector $\psi(a, y)$ indexed by the basis states $|a, y\rangle$ . Measuring it returns $|a, y\rangle$ with probability $|\psi(a, y)|^2$ .

The Fourier matrix $A_q$ is the $q \times q$ matrix with entries $(A_q)_{a,c} = q^{-1/2}\exp(2\pi i a c/q)$ , with rows indexing inputs and columns outputs. The algorithm

prepares $\frac{1}{q^{1/2}}\sum_{a=0}^{q-1}|a\rangle|x^a \bmod n\rangle$ (eq. (5.2)),
applies $A_q$ to the first register, obtaining $\frac1q\sum_{a,c}\exp(2\pi iac/q)|c\rangle|x^a \bmod n\rangle$ (eq. (5.4)),
measures, obtaining some $|c, y\rangle$ ,
rounds $c/q$ to the nearest fraction with denominator smaller than $n$ .

The observed $c$ gives us $r$ if some fraction with lowest-terms denominator below $n$ is within $1/2q$ of $c/q$ , and every such fraction has lowest-terms denominator exactly $r$ . In the Lean development these objects are preFourierState, finalState, outcomeProb and yieldsOrder, in the namespace ShorAlgorithms.OrderFinding, and the shared definition ShorAlgorithms.Shared.fourierMatrix.

Formalization targets

Goal: success probability at least $\varphi(r)/3r$

For all sufficiently large $n$ , with $x$ , $r$ and $q$ as above,

\Pr\bigl[\text{the observed } c \text{ gives us } r\bigr] \;=\; \sum_{c\ \text{gives}\ r}\ \sum_{y \in \mathbb{Z}/n} |\Psi(c, y)|^2 \;\ge\; \frac{\varphi(r)}{3r},

where $\Psi$ is the state (5.4). The threshold on $n$ is uniform in $x$ and $q$ ; it is the paper's "for sufficiently large $n$ " from the per-state bound.

Milestones

Eqs. (5.5)–(5.6). For $0 \le k < r$ , the probability of $|c, x^k\rangle$ equals $\left|\frac1q\sum_{b=0}^{\lfloor (q-k-1)/r\rfloor}\exp(2\pi i(br+k)c/q)\right|^2$ .
Eq. (5.11). For $n$ past a threshold, every $|c, x^k\rangle$ with $-r/2 \le rc - dq \le r/2$ for some integer $d$ has probability at least $1/3r^2$ .
Eq. (5.13). If $n^2 \le q$ , at most one fraction with denominator below $n$ lies within $1/2q$ of $c/q$ .
p. 1500. Such a fraction is a convergent of the continued fraction of $c/q$ .
p. 1501. At least $\varphi(r)$ values of $c$ are within $1/2q$ of some $d/r$ with $\gcd(d, r) = 1$ ; with the $r$ distinct values of $x^k$ this gives at least $r\varphi(r)$ states $|c, x^k\rangle$ , and each such $c$ gives us $r$ .

Significance

The goal is the quantitative statement behind "order finding is in bounded-error quantum polynomial time": since $\varphi(r)/r \ge \delta/\log\log r$ for a constant $\delta$ (Hardy and Wright, Thm. 328), $O(\log\log r)$ repetitions find $r$ with high probability, and Miller's reduction then factors $n$ . Without the bound, the algorithm is a procedure with no guarantee.

The result is proved, in the paper and in textbooks (Nielsen and Chuang, 2000, §5.3), usually with a phase-estimation analysis rather than Shor's direct count. What this mission adds is a machine-checked proof of Shor's own argument, with his choice of $q$ and his constants, starting from the state built by applying $A_q$ to (5.2). Formal proofs of idealized versions exist elsewhere, for instance in the exact-period model where $r$ divides $q$ and the output is uniform on $r$ peaks, but that model removes the approximation that the $1/3r^2$ bound is about. Legendre's theorem on continued fractions is already on the platform (FamousTheorems.legendre_continued_fraction_theorem) and is included as a reference item.

Difficulty

The obvious route is to compute the output distribution in closed form. That works only when $r$ divides $q$ ; here $q$ is a power of $2$ and $r$ is arbitrary, so the amplitudes are geometric sums of $\lfloor (q-k-1)/r\rfloor + 1$ terms whose phases do not cancel exactly. The per-state bound $1/3r^2$ requires a lower bound on such a sum that is uniform in $r$ , $c$ and $k$ , with error terms of order $1/q$ controlled against a main term of order $1/r^2$ . The constant $1/3$ leaves only a small margin below the limiting value $4/\pi^2 \approx 0.405$ , so the errors must be bounded explicitly, not merely shown to vanish.

The second difficulty is the counting: distinct coprime numerators $d$ must give distinct outcomes $c$ in $[0, q)$ , and each good $c$ must determine $r$ uniquely, which uses $r < n$ and $n^2 \le q$ .

Formalization scope

Conventions the statements commit to:

States are functions Fin q × ZMod n → ℂ; the matrix convention is row = input, so applying $A_q$ to the first register gives the amplitude $\sum_a \psi(a, y)(A_q)_{a,c}$ at $(c, y)$ .
The final state is built by applying $A_q$ to the state (5.2); the closed forms (5.5) and (5.6) are theorems, not definitions. No normalization hypothesis is assumed.
Probabilities are squared moduli; the probability of the event " $c$ gives us $r$ " sums over all $y \in \mathbb{Z}/n$ , which is exact because $y$ that are not powers of $x$ have probability zero.
$x$ is a natural number with $\gcd(x, n) = 1$ ; $r$ is orderOf (x : ZMod n). $q$ enters through the three hypotheses $q = 2^l$ , $n^2 \le q$ , $q < 2n^2$ , not through a function of $n$ .
Fractions are rationals, and "in lowest terms" is Rat.den.
Thresholds "for sufficiently large $n$ " are $\exists N,\ \forall n \ge N$ , with $N$ quantified before $x$ , $q$ , $c$ and $k$ .
Condition (5.11) is stated in its equivalent form (5.12), with an integer $d$ .
Printed slip. Eq. (5.13)'s justification says "Because $q > n^2$ ", but $q$ was chosen with $n^2 \le q$ , and $q = n^2$ when $n$ is a power of $2$ . The uniqueness claim holds under $n^2 \le q$ , and that is what is stated.

Typing the closed form (5.4)–(5.6) in as the definition of the final state would make milestone 1 trivial and hide whether the probability model is the paper's; the definitions exclude this by construction.

Not stated: the polynomial running time of any step, the $O(\log\log r)$ repetition count (no explicit constant), the reversible modular exponentiation of §3, and the post-processing heuristics on p. 1501. Needed infrastructure: bounds on geometric exponential sums, Euler's totient, Diophantine approximation by fractions with bounded denominator, and Mathlib's continued fractions. Lemmas on geometric sums of roots of unity and on the order of units mod $n$ are reusable in the companion discrete logarithm mission.

Selected references

P. W. Shor, Polynomial-Time Algorithms for Prime Factorization and Discrete Logarithms on a Quantum Computer, SIAM J. Comput. 26(5):1484–1509, 1997. https://doi.org/10.1137/S0097539795293172
P. W. Shor, Algorithms for quantum computation: discrete logarithms and factoring, Proc. 35th FOCS, 1994. https://doi.org/10.1109/SFCS.1994.365700
G. L. Miller, Riemann's hypothesis and tests for primality, J. Comput. System Sci. 13(3):300–317, 1976. https://doi.org/10.1016/S0022-0000(76)80043-8
G. H. Hardy and E. M. Wright, An Introduction to the Theory of Numbers, 5th ed., Oxford, 1979 (Ch. X, continued fractions; Thm. 328).
M. A. Nielsen and I. L. Chuang, Quantum Computation and Quantum Information, Cambridge, 2000. https://doi.org/10.1017/CBO9780511976667

12 thms3 active usersReviewed

Linear Optimization Operations Research Probability·Captain: mikedeng1

Competitive Randomized Algorithms for Nonuniform Problems IV: The Optimal Randomized Two-Server Ratio 1652/1069 on the 3-4-5 TriangleResearch Paper

Motivation

The $k$ -server problem is a basic model of on-line decision making. $k$ mobile servers move in a metric space, requests for points arrive one at a time, and each request has to be covered by a server before the next one arrives. The cost is the total distance the servers move. The problem includes paging, caching and disk-head scheduling as special cases (Manasse, McGeoch, Sleator 1990). An on-line algorithm is judged by its competitive factor: how much its cost can exceed that of an off-line algorithm that knows the whole request sequence in advance.

For randomized algorithms against an oblivious adversary (one that fixes the whole request sequence before the algorithm flips any coins), the best-understood case is paging, which is the $k$ -server problem on a uniform metric space. There the optimal factor is the harmonic number $H_k=\sum_{i=1}^k 1/i$ . Fiat et al. proved the lower bound (1991) and McGeoch and Sleator the matching upper bound (1991). Karlin, Manasse, McGeoch and Owicki (Algorithmica 11, 1994, §5) asked whether $H_k$ -competitive algorithms also exist when the metric space is not uniform. They answered no, already for two servers on three points: on certain triangles the optimal randomized factor is strictly larger than $H_2 = 3/2$ . This mission formalizes their Theorem 13, which gives the exact optimal factor on the triangle with edge lengths 3, 4 and 5.

Timeline:

1990: Manasse, McGeoch and Sleator introduce the $k$ -server problem; $k$ is the deterministic optimum for $k=2$ .
1991: Fiat, Karp, Luby, McGeoch, Sleator and Young prove the $H_k$ lower bound for randomized paging. McGeoch and Sleator give an $H_k$ -competitive paging algorithm.
1994: Karlin, Manasse, McGeoch and Owicki determine the optimal randomized two-server factors on the isosceles triangles $1$ - $d$ - $d$ (Theorem 12) and on the 3-4-5 triangle (Theorem 13, the ratio $1652/1069$ ). Both exceed $3/2$ .

Setting

Let $M$ be a metric space with exactly three points $a, b, c$ , where $d(a,b)=3$ , $d(a,c)=5$ and $d(b,c)=4$ . A configuration $C$ gives the positions of two labelled servers in $M$ . A request sequence $\sigma$ is a finite list of points of $M$ .

A deterministic on-line algorithm assigns to each prefix of a request sequence a configuration, in which the last request is covered. Its configuration after a prefix therefore cannot depend on later requests. Its initial configuration is the one it assigns to the empty prefix, and its cost $C_A(\sigma)$ on $\sigma$ is the total distance its servers move while serving $\sigma$ request by request.

The optimal off-line cost $C_{opt}(\sigma)$ from an initial configuration $C_0$ is the infimum, over all schedules that start at $C_0$ and cover each request of $\sigma$ in turn, of the total distance moved.

A randomized on-line algorithm $A$ is a probability distribution over deterministic on-line algorithms, all starting at $C_0$ . The cost on each fixed $\sigma$ is required to be measurable in the random choice, and $\mathbf{E}C_A(\sigma)$ is the expected cost. $A$ is $\rho$ -competitive against an oblivious adversary if there is a constant $a$ such that for every request sequence $\sigma$ ,

\mathbf{E}C_A(\sigma) \le \rho\cdot C_{opt}(\sigma) + a .

These are the definitions of p. 543 of the paper. They are the platform's published KServer_model and KServer_randomized, which this mission reuses unchanged: KServer.RandomizedAlgorithm 2 M and A.IsCompetitiveFrom C₀ ρ.

Formalization targets

Goal: Theorem 13

For every initial configuration $C_0$ of the two servers,

\Big(\forall A,\ \forall \rho,\ A \text{ is } \rho\text{-competitive from } C_0 \Rightarrow \rho \ge \tfrac{1652}{1069}\Big)\ \wedge\ \Big(\exists A,\ A \text{ is } \tfrac{1652}{1069}\text{-competitive from } C_0\Big).

The first claim is quantified over all randomized algorithms, so it also covers deterministic ones (point masses). The second claim asks for one algorithm. Together they say that $1652/1069 \approx 1.545$ is the exact optimal randomized factor on this triangle.

Milestones

The phase LP lower bound (p. 568). Twelve linear constraints in nine probabilities $\pi_1,\dots,\pi_9$ , three potentials $\Phi_{ab},\Phi_{ac},\Phi_{bc}$ and a ratio $\alpha$ , one constraint for each possible phase of the request sequence, of the form

\text{A's cost} \le \alpha\cdot(\text{opt's cost}) + \Phi_{\text{initial}} - \Phi_{\text{final}}.

Every real solution has $\alpha \ge 1652/1069$ . 2. The LP attainment (p. 568). The paper's printed probabilities lie in $[0,1]$ , and with suitable potentials they satisfy all twelve constraints at $\alpha = 1652/1069$ . 3. Theorem 13, first claim: the lower bound for every randomized algorithm. 4. Theorem 13, second claim: a $1652/1069$ -competitive randomized algorithm exists.

Significance

The result. Theorem 13 shows that the $H_k$ behaviour of randomized paging does not carry over to general metric spaces. Two servers on a three-point space already force a factor above $3/2$ . The value is exact, which makes this triangle a test case for any general theory of randomized $k$ -server algorithms on small metric spaces. With Theorem 12 (the isosceles triangles, a companion mission of this series), it is one of the few non-uniform metric spaces with a known optimal randomized factor.

Formalizing it. The result has been proved since 1994. To our knowledge there is no machine-checked proof. The paper derives both bounds from two framework theorems for phase-based algorithms: Theorem 3 (an LP lower bound for phase-based algorithms bounds every algorithm) and Theorem 2 (a lazy phase-based algorithm with LP bound $\alpha$ is $\alpha$ -competitive). The phase tables themselves (which phases can occur and what they cost) are stated without detailed proof. A formal proof has to supply both framework arguments for this space and verify the phase tables, as well as the finite linear algebra of milestones 1 and 2. The milestones isolate the exact-arithmetic core so that it can be closed independently of the probabilistic part.

Difficulty

The two LP milestones are finite exact-arithmetic facts. The hard part is linking them to Theorem 13.

For the lower bound, an algorithm need not be phase-based at all. Its probabilities may depend on the whole history, not only on the current phase, and it may leave the configuration of the off-line optimum at the end of a phase. The obvious attempt is to fix one hard request sequence and compare costs, but that cannot work: randomization defeats any single sequence. The reduction from arbitrary algorithms to phase-based ones (the paper's Theorem 3) is the substantive step.

For the upper bound, the printed probabilities describe the algorithm's marginal position after each prefix of a phase. They have to be realized as a single probability distribution over deterministic on-line algorithms that is lazy (it moves only to serve a request) and whose expected cost per phase equals the table's entry. On top of this, the LP accounting has to be turned into a bound on arbitrary request sequences, including partial phases and a start away from the optimum's configuration.

Formalization scope

Model. The platform definitions KServer_model and KServer_randomized are used unchanged. Servers are labelled (Config 2 M = Fin 2 → M). A deterministic algorithm is a function of the request prefix, which makes it on-line by construction. A randomized algorithm is a mixed strategy with a probability measure and a measurability field, and its expected cost is the lower Lebesgue integral of the nonnegative cost. The off-line optimum is a real infimum over schedules from $C_0$ ; the set is nonempty and bounded below by $0$ . Competitiveness allows any real additive constant.
The triangle is given by hypotheses on an arbitrary metric space: every point equals $a$ , $b$ or $c$ , and $d(a,b)=3$ , $d(a,c)=5$ , $d(b,c)=4$ . These hypotheses are satisfiable ( $3+4\ge5$ ) and force three distinct points.
Initial configuration. Both claims are stated for every initial configuration $C_0$ , including both servers on one point. The paper does not fix the start; the additive constant absorbs it.
LP milestones. The thirteen LP variables are free reals, with no box $0\le\pi_i\le 1$ , exactly as the paper permits. This makes milestone 1 stronger than the boxed version; the minimum is the same either way. The twelve constraints are written out one per hypothesis, in the table's order, with the potential difference $\Phi_{\text{initial}} - \Phi_{\text{final}}$ on the right. In milestone 2 the potentials are existentially quantified, since the paper names none.
Not stated. The paper's Theorems 2 and 3 (the phase framework) and the phase tables are not separate milestones. Milestone 1 feeds the first claim through Theorem 3, and milestone 2 feeds the second claim through Theorem 2. Contributions formalizing phase-based algorithms, laziness and the LP-bound reduction for finite metric spaces would be reusable for Theorem 12 and Theorem 14 of the same paper.
Ruled out. The lower bound is not restricted to deterministic or to phase-based algorithms, and it is not stated as "one sequence defeats every algorithm". The constant is exactly $1652/1069$ , not an approximation, and the attainment claim is not weakened to "for some initial configuration".

Selected references

A. R. Karlin, M. S. Manasse, L. A. McGeoch, S. Owicki, Competitive Randomized Algorithms for Nonuniform Problems, Algorithmica 11 (1994) 542–571. https://doi.org/10.1007/BF01189993
M. S. Manasse, L. A. McGeoch, D. D. Sleator, Competitive Algorithms for Server Problems, Journal of Algorithms 11 (1990) 208–230. https://doi.org/10.1016/0196-6774(90)90003-W
A. Fiat, R. M. Karp, M. Luby, L. A. McGeoch, D. D. Sleator, N. E. Young, Competitive Paging Algorithms, Journal of Algorithms 12 (1991) 685–699. https://doi.org/10.1016/0196-6774(91)90041-V
L. A. McGeoch, D. D. Sleator, A Strongly Competitive Randomized Paging Algorithm, Algorithmica 6 (1991) 816–825. https://doi.org/10.1007/BF01759073

7 thms3 active usersReviewed

Linear Optimization Operations Research Probability·Captain: mikedeng1

Competitive Randomized Algorithms for Nonuniform Problems III: The Optimal Randomized Two-Server Ratio on the 1-d-d Isosceles TriangleResearch Paper

Motivation

The k-server problem of Manasse, McGeoch and Sleator (J. Algorithms 11 (1990)) asks how $k$ mobile servers in a metric space should respond, on-line, to a sequence of requests at points of the space, each of which must be covered by a server. It is the central model of on-line computation: paging is the special case of a uniform metric, and many caching and scheduling problems reduce to it. For two servers the deterministic picture is complete: the optimal competitive ratio is $2$ on every metric space with at least three points.

Randomization changes the picture, and the smallest nontrivial case already shows how. On the equilateral triangle the optimal randomized ratio against an oblivious adversary is $3/2$ . Karlin, Manasse, McGeoch and Owicki (Algorithmica 11 (1994) 542–571) computed the exact optimal randomized ratio for several nonuniform triangles, where the distances differ, and showed that it depends on the geometry. Their Theorem 12 settles the whole family of isosceles triangles with edge lengths $1$ , $d$ , $d$ . These exact values are among the few known optimal randomized ratios for server problems.

Timeline:

1990: Manasse, McGeoch and Sleator introduce the $k$ -server problem and prove the deterministic two-server ratio is $2$ .
1990–1994: Karlin, Manasse, McGeoch and Owicki submit this paper (received August 1990, revised September 1991) and publish it in Algorithmica in 1994, with the isosceles-triangle ratios of Theorem 12 and the 3-4-5 triangle ratio $1652/1069$ of Theorem 13.
Later: Karloff, Rabani and Ravid extend the technique to $\Omega(\log\log k)$ and $\Omega(\log k)$ randomized lower bounds (cited on p. 564); Bubeck, Coester and Rabani (STOC 2023) refute the randomized $k$ -server conjecture.

Setting

Fix an integer $d\ge1$ . The isosceles triangle $M$ has three points $a$ , $b$ , $c$ with

\operatorname{dist}(a,b)=1,\qquad \operatorname{dist}(a,c)=\operatorname{dist}(b,c)=d.

A configuration $C:\{0,1\}\to M$ places two labelled servers on points of $M$ . A deterministic on-line algorithm assigns to every finite request sequence $\sigma=(r_1,\dots,r_n)$ a configuration, computed from $\sigma$ alone and covering the last request; its value on the empty sequence is its initial configuration. Its cost $C_A(\sigma)$ is the total distance its servers move while serving $\sigma$ request by request. The off-line optimum $C_{opt}(\sigma)$ from an initial configuration $C_0$ is the least total movement of any schedule that starts at $C_0$ and covers each request in turn, knowing $\sigma$ in advance.

A randomized algorithm is a probability distribution on deterministic on-line algorithms; its expected cost is $\mathbf{E}C_A(\sigma)$ . It is $\rho$ -competitive against an oblivious adversary from $C_0$ if every algorithm in its support starts at $C_0$ and there is a constant $a$ such that

\mathbf{E}C_A(\sigma)\le\rho\cdot C_{opt}(\sigma)+a\qquad\text{for every request sequence }\sigma.

The request sequence is fixed in advance and does not react to the algorithm's coin flips.

Write $e_p=(1+1/p)^p$ and

\alpha_d=\frac{e_{2d-1}+1/4d}{(e_{2d-1}-1)+1/2d},\qquad e_{2d-1}=\left(\frac{2d}{2d-1}\right)^{2d-1}.

In Lean this is NonuniformCompetitive.Isosceles.isoscelesRatio d.

Formalization targets

Goal: Theorem 12

For every $d\ge1$ and every initial configuration $C_0$ :

\forall A,\ \forall\rho,\quad A\text{ is }\rho\text{-competitive from }C_0\ \Longrightarrow\ \rho\ge\alpha_d,

\exists A:\ A\text{ is }\alpha_d\text{-competitive from }C_0.

The two claims are also milestones of their own (no_better_ratio, ratio_attained).

The phase LP (§5, pp. 565–566)

For free real $\pi_1,\dots,\pi_{2d-1}$ and real $\alpha$ with

(\pi_k)2d+\sum_{i=1}^k(1-\pi_i)\le\alpha k\ \ (1\le k<2d),\qquad 2d+\sum_{i=1}^{2d-1}(1-\pi_i)+\tfrac12\le\alpha\cdot2d,

one has $\alpha\ge\alpha_d$ (lp_lower_bound); and $\pi_k=(\alpha_d-1)\big((2d/(2d-1))^k-1\big)$ , $\pi_{2d}=1$ is nondecreasing from $\pi_1\ge0$ to $1$ and makes every constraint an equality (lp_attained).

The limit remark (§5, p. 566)

\alpha_1<\alpha_2<\alpha_3<\cdots,\qquad \lim_{d\to\infty}\alpha_d=\frac{e}{e-1}

(ratio_increases_to_e_ratio).

Significance

The theorem gives an exact optimal randomized ratio for an infinite family of metric spaces. It shows that the optimal randomized two-server ratio is not a constant: it runs from $3/2$ on the equilateral triangle to $e/(e-1)\approx1.582$ as the triangle becomes long and thin, where the problem resembles ski rental. With the deterministic ratio $2$ , it quantifies exactly how much randomization gains on these spaces.

The results are proved in the paper; none is formalized on Prove2Me, and no machine-checked proof of them is known. A formal proof would require the paper's phase framework (Theorems 1–3 and the appendix's Theorem 15) for server problems, which this mission does not state separately, and a concrete randomized algorithm as a measurable mixed strategy. Both would be reusable for Theorem 13 (the 3-4-5 triangle) and for other exact ratios on small metric spaces.

Difficulty

The phase LP milestones are finite real arithmetic. The difficulty is the passage between them and the goal. The lower bound must hold for every randomized algorithm, not only phase-based lazy ones: an arbitrary algorithm may condition on the whole history, move non-lazily, and randomize in ways that do not reduce to the probabilities $\pi_k$ . The paper handles this with Theorem 3, which says that the LP bound of phase-based algorithms bounds the competitive factor of all algorithms; its proof uses an averaging argument over histories that must be made rigorous. The upper bound needs a mixed strategy over infinitely many phases, with measurable costs, an explicit additive constant covering the first partial phase from an arbitrary initial configuration, and an accounting of $C_{opt}$ across phase boundaries.

Formalization scope

The model is the platform's published KServer_model and KServer_randomized (reference items): labelled servers Fin 2 → M; a deterministic on-line algorithm as a map from request prefixes to configurations; a randomized algorithm as a probability measure over deterministic algorithms, with the cost of each fixed sequence measurable in the random outcome; expected cost as a lower Lebesgue integral in $[0,\infty]$ ; the off-line optimum as a real infimum over schedules from $C_0$ (nonempty and bounded below by $0$ ); and IsCompetitiveFrom A C₀ c with a real additive constant.

Committed conventions:

The triangle is any metric space whose points are exactly $a,b,c$ at distances $1,d,d$ , with $d$ a natural number and $d\ge1$ . Every such space is isometric to the paper's triangle; at $d=0$ it would not be a triangle.
Both claims are stated for every initial configuration, including both servers on one point. The paper treats the initial state $\{a,b\}$ separately and absorbs the first partial phase into the additive constant.
The lower bound quantifies over all randomized algorithms (deterministic ones are point masses), never over phase-based ones only.
In the LP milestones the $\pi_k$ are free reals, as printed; no box $0\le\pi_k\le1$ is imposed.
"Grows" in the limit remark is read as strictly increasing.
The paper prints the recurrence on p. 565 as $\pi_k=\frac{\alpha-1+(\pi_{k-1})2d-1}{2d}$ ; the equations $(*)$ give $\pi_k=\frac{\alpha-1+2d\,\pi_{k-1}}{2d-1}$ . The recurrence is not used; the closed form printed on p. 566 is correct and is the one stated.

Without the measurability field of a randomized algorithm the lower integral would under-report expected cost and the attainment claim would become easier than the paper's; the published definition includes it. The lower bound is not vacuous: the triangle hypotheses are satisfiable for every $d\ge1$ .

Welcome contributions: a formal version of the phase framework (Theorems 1–3, 15) for finite metric spaces, reusable across missions III and IV; a measurable construction of phase-based randomized algorithms; and proofs of the LP milestones.

Selected references

A. R. Karlin, M. S. Manasse, L. A. McGeoch, S. Owicki, Competitive Randomized Algorithms for Nonuniform Problems, Algorithmica 11 (1994) 542–571. https://doi.org/10.1007/BF01189993
M. S. Manasse, L. A. McGeoch, D. D. Sleator, Competitive Algorithms for Server Problems, J. Algorithms 11 (1990) 208–230. https://doi.org/10.1016/0196-6774(90)90003-W
H. Karloff, Y. Rabani, Y. Ravid, Lower Bounds for Randomized k-Server and Motion-Planning Algorithms, SIAM J. Comput. 23 (1994) 293–312. https://doi.org/10.1137/S0097539792224838
S. Bubeck, C. Coester, Y. Rabani, The Randomized k-Server Conjecture Is False!, STOC 2023. https://arxiv.org/abs/2211.05753

9 thms3 active usersReviewed

Completed

Combinatorics Complexity Theory Operations Research+2·Captain: mikedeng1

Maximizing Non-Monotone Submodular Functions V: Beating 1/2 for Symmetric Functions Requires Exponentially Many Value QueriesResearch Paper

Motivation

Maximizing a nonnegative submodular set function without constraints contains Max Cut, Max Directed Cut and facility-location problems as special cases. In the value-oracle model an algorithm knows nothing about the function except the values $f(S)$ of the sets $S$ it queries, and it is judged by the number of queries it makes. Feige, Mirrokni and Vondrák (SIAM J. Comput. 40(4), 2011) gave constant-factor algorithms in this model and matching limits on what any algorithm can do. For symmetric functions, such as cut functions of undirected graphs, a uniformly random set already achieves $\tfrac12$ of the optimum in expectation (Theorem 2.1 of the paper). The question this mission formalizes is whether any algorithm can do better, and the answer given by Theorem 4.5 is: not without exponentially many value queries. The same factor $\tfrac12$ was later shown to be achievable for general (non-symmetric) nonnegative submodular functions by Buchbinder, Feldman, Naor and Schwartz (FOCS 2012 / SIAM J. Comput. 2015), so the bound of Theorem 4.5 is the tight limit of the whole problem in the value-oracle model.

Timeline:

2007 (FOCS) / 2011 (SIAM J. Comput.): Feige, Mirrokni and Vondrák prove that no algorithm with subexponentially many value queries achieves $(\tfrac12 + \epsilon)$ of the optimum on symmetric nonnegative submodular functions, and give $\tfrac25$ for general functions.
2011: Vondrák's symmetry-gap framework (SIAM J. Comput. 42(1), 2013) generalizes the construction to constrained problems.
2012: Buchbinder, Feldman, Naor and Schwartz give a randomized $\tfrac12$ -approximation for general nonnegative submodular functions, matching the bound.

Setting

Let $[n] = \{0, \dots, n-1\}$ be the ground set, with $n$ even. A set function $f : 2^{[n]} \to \mathbb{R}$ is submodular if $f(S \cup T) + f(S \cap T) \le f(S) + f(T)$ for all $S, T$ , symmetric if $f([n]\setminus S) = f(S)$ for all $S$ , and $\mathrm{OPT}(f) = \max_{S} f(S)$ .

Fix an integer $m$ with $1 \le m \le n/2$ and write $\epsilon = m/n$ , so that $\epsilon n$ is an integer. For integers $k, \ell$ put

f(k,\ell) = \begin{cases} (k+\ell)(n-k-\ell) & |k-\ell| \le m,\\ k(n-2\ell) + (n-2k)\ell + m^2 - 2m|k-\ell| & |k-\ell| > m. \end{cases}

For a set $C \subseteq [n]$ with $|C| = n/2$ and $D = [n] \setminus C$ , the hard instance is $f_C(S) = f(|S\cap C|, |S\cap D|)$ . The cut function of the complete graph is $g(S) = |S|(n-|S|)$ , with maximum $\tfrac14 n^2$ . A set $Q$ is balanced for $C$ if $\bigl||Q\cap C| - |Q\cap D|\bigr| \le m$ ; on balanced sets $f_C = g$ .

A deterministic adaptive $q$ -query algorithm $A$ chooses each query from the answers received so far, and after $q$ answers outputs a set $A(h)$ when run against an oracle $h$ . A randomized algorithm is a distribution $\mu$ over deterministic ones, with expected value $\mathbb{E}_{A\sim\mu}[h(A(h))]$ .

Formalization targets

Goal: Theorem 4.5 with the constants of its proof

For every such $n, m$ :

every $f_C$ with $|C| = n/2$ is nonnegative, symmetric and submodular, with

\mathrm{OPT}(f_C) = \tfrac12 n^2 (1 - 2\epsilon + 2\epsilon^2);

for every $q < e^{\epsilon^2 n/8}$ and every randomized $q$ -query algorithm $\mu$ there is a $C$ with $|C| = n/2$ and

\mathbb{E}_{A\sim\mu}\bigl[f_C(A(f_C))\bigr] \le \tfrac14 n^2 + \bigl(2e^{-\epsilon^2 n/8} + 2e^{-\epsilon^2 n/4}\bigr)\,\mathrm{OPT}(f_C).

Hence the ratio attained is at most $\frac{1}{2(1-2\epsilon+2\epsilon^2)} + 4e^{-\epsilon^2 n/8} = \tfrac12 + \epsilon + O(\epsilon^2) + 4e^{-\epsilon^2 n/8}$ .

Milestones

Theorem 1.2, the Chernoff bound for independent variables in $[-1,1]$ .
Submodularity of $f_C$ .
The value $\mathrm{OPT}(f_C) = \tfrac12 n^2(1 - 2\epsilon + 2\epsilon^2)$ , attained at $S = C$ .
A fixed query is unbalanced for at most a $2e^{-\epsilon^2 n/4}$ fraction of the half-size sets $C$ .
If all queries are balanced, the algorithm cannot distinguish $f_C$ from $g$ .
The deterministic case of the bound, averaged over $C$ .

Significance

The theorem shows that the factor $\tfrac12$ for symmetric submodular maximization, and hence for unconstrained submodular maximization in general, cannot be improved by any algorithm that uses a subexponential number of value queries, whatever its running time. It is an information-theoretic bound and needs no complexity assumption. Along with the later matching $\tfrac12$ -approximation, it settles the value-oracle approximability of the problem. The construction, a function equal to a symmetric function on "balanced" sets and larger elsewhere, is the prototype of the symmetry-gap technique used for many later oracle lower bounds.

The result is proved in the paper. No machine-checked version is known to exist: the platform has no value-oracle or query-lower-bound statement. Formalizing it requires a precise model of adaptive randomized query algorithms, a concentration bound for the hypergeometric distribution, and a finite verification of submodularity of an explicit two-regime function, and it fixes the constants that the printed statement leaves as $O(\cdot)$ terms.

Difficulty

Two steps of the printed argument do not go through as written. First, the proof bounds the probability that a fixed query is unbalanced by citing the Chernoff bound for independent variables, but for a uniformly random half-size set $C$ the count $|Q\cap C|$ is hypergeometric, and the summands are not independent. A bound for sampling without replacement is needed instead. Replacing the balanced partition by independent coin flips is not an option: then $|C| \ne n/2$ in general, and the function is no longer the paper's instance.

Second, the argument counts only the queries, but the value an algorithm receives is $f_C$ of its output, which equals $g$ of the output only if the output is balanced as well. That event has to be controlled too.

Finally, submodularity of $f_C$ must be checked across the boundary $|k-\ell| = \epsilon n$ between the two regimes, where the formula changes.

Formalization scope

The ground set is Fin n with $n$ even; $\epsilon n$ is an integer $m$ with $1 \le m$ and $2m \le n$ , following the paper's "assume that $\epsilon n$ is an integer". Sets are Finset (Fin n), and all values are real.
$\mathrm{OPT}$ is Finset.sup' over all subsets. There is no junk value.
The partition $(C, D)$ is uniform over half-size sets; probabilities over it are counts of n/2-subsets divided by $\binom{n}{n/2}$ , written multiplied out.
A deterministic algorithm is a pair of decision rules query, output : List ℝ → Finset (Fin n) making exactly $q$ adaptive queries with arbitrary real answers. A randomized algorithm is a PMF over deterministic algorithms, which covers every randomization with countable support. The algorithm sees $f$ only through query answers; it never receives $C$ .
Pinned-down constants. The printed theorem, "fewer than $e^{\epsilon^2 n/8}$ queries" and "expected value at least $(\tfrac12+\epsilon)\mathrm{OPT}$ ", is not what the proof gives for one and the same $\epsilon$ . On the proof's instances $\mathrm{OPT} = \tfrac12 n^2(1-2\epsilon+2\epsilon^2)$ , and the ratio held is $\frac{1}{2(1-2\epsilon+2\epsilon^2)} > \tfrac12 + \epsilon$ . The formal goal states the explicit bound the proof establishes. The literal printed pair, stated for the proof's family with the same $\epsilon$ , is false: the zero-query algorithm that outputs a fixed half-size set gets at least $\tfrac14 n^2 > (\tfrac12+\epsilon)\mathrm{OPT}$ .
Added term. The error term $2e^{-\epsilon^2 n/4}$ for the output set is added to the paper's $2e^{-\epsilon^2 n/8}$ .
Ruled-out trivializations. A restricted algorithm class (non-adaptive, deterministic, or one that must return a queried set) would give a different, weaker theorem. So would a bound that lets the algorithm read $C$ , which would make the statement false. Both the instance's properties (nonnegativity, symmetry, submodularity, the value of OPT) and the bound are part of the goal, so an empty or degenerate family cannot satisfy it. The quantifier order is: for every algorithm there is an instance.
Needed infrastructure: a value-oracle algorithm model; tail bounds for the hypergeometric distribution (Hoeffding's inequality for sampling without replacement), which Mathlib lacks; averaging over a PMF of algorithms. The algorithm model and the hypergeometric bound are reusable for other oracle lower bounds. Proofs of any milestone, and alternative derivations of the balance bound, are welcome.

Selected references

U. Feige, V. S. Mirrokni, J. Vondrák, Maximizing Non-Monotone Submodular Functions, SIAM J. Comput. 40(4):1133–1153, 2011. https://doi.org/10.1137/090779346
N. Alon, J. H. Spencer, The Probabilistic Method, Wiley (source of Theorem 1.2).
W. Hoeffding, Probability Inequalities for Sums of Bounded Random Variables, J. Amer. Statist. Assoc. 58(301):13–30, 1963. https://doi.org/10.1080/01621459.1963.10500830
J. Vondrák, Symmetry and Approximability of Submodular Maximization Problems, SIAM J. Comput. 42(1):265–304, 2013. https://doi.org/10.1137/110832318
N. Buchbinder, M. Feldman, J. Naor, R. Schwartz, A Tight Linear Time (1/2)-Approximation for Unconstrained Submodular Maximization, SIAM J. Comput. 44(5):1384–1402, 2015. https://doi.org/10.1137/130929205

12 thms3 active usersReviewed

Completed

Combinatorics Operations Research Optimization+1·Captain: mikedeng1

Maximizing Non-Monotone Submodular Functions IV: Smooth Local Search Achieves 2/5 of the OptimumResearch Paper

Motivation

Many optimization problems ask for a subset of a finite ground set that maximizes a submodular function, a set function with diminishing marginal returns. Max Cut and Max Directed Cut in graphs, facility location with fixed costs, and the maximization of mutual information or entropy of a subset of random variables are all of this form. Unlike the monotone case, where a greedy algorithm achieves $1 - 1/e$ , a general nonnegative submodular function may decrease when elements are added, and the empty set and the full set can both be poor. The question is how large a constant fraction of the optimum a polynomial-time algorithm can guarantee when the function is given only through an oracle that returns $f(S)$ for a queried set $S$ .

Feige, Mirrokni and Vondrák (SIAM J. Comput. 40(4), 2011) gave the first constant-factor algorithms for this problem. A uniformly random set achieves $1/4$ of the optimum, a deterministic local search achieves $1/3 - \epsilon/n$ , and a randomized smooth local search achieves $2/5 - o(1)$ . The last result is the paper's best approximation for general nonnegative submodular functions (Table 1, p. 1136), and it is the subject of this mission.

Timeline. Feige, Mirrokni and Vondrák: $1/4$ , $1/3$ and $2/5$ (FOCS 2007; journal version 2011). Gharan and Vondrák (SODA 2011): about $0.41$ by simulated annealing. Buchbinder, Feldman, Naor and Schwartz (FOCS 2012; SIAM J. Comput. 2015): a randomized double greedy algorithm achieving $1/2$ , which matches the $1/2$ hardness in the value oracle model proved in the same paper by Feige, Mirrokni and Vondrák.

Setting

Let $X$ be a finite ground set with $n = |X| \ge 1$ elements and $f : 2^X \to \mathbb{R}$ a function with $f(S) \ge 0$ for all $S$ and

f(S \cup T) + f(S \cap T) \le f(S) + f(T) \quad (S, T \subseteq X).

Write $OPT = \max_{S \subseteq X} f(S)$ . The multilinear extension of $f$ is

F(x) = \sum_{S \subseteq X} f(S) \prod_{i \in S} x_i \prod_{j \notin S} (1 - x_j),

the expected value of $f$ on a random set containing each $i$ independently with probability $x_i$ .

For $A \subseteq X$ and $\delta \in [-1,1]$ , the random set $\mathcal{R}(A,\delta)$ is sampled with bias $\delta$ based on $A$ : each element of $A$ is included independently with probability $p = (1+\delta)/2$ , each element of $B = X \setminus A$ with probability $q = (1-\delta)/2$ . The potential is $\Phi(A) = \mathbf{E}[f(\mathcal{R}(A,\delta))]$ and the smoothed marginal value of $x$ is

\omega_{A,\delta}(x) = \mathbf{E}[f(\mathcal{R}(A,\delta) \cup \{x\})] - \mathbf{E}[f(\mathcal{R}(A,\delta) \setminus \{x\})].

Algorithm SLS starts from $A = \emptyset$ . At each iteration it obtains estimates $\tilde\omega_{A,\delta}(x)$ within $\pm\frac{1}{n^2}OPT$ of $\omega_{A,\delta}(x)$ . If some $x \notin A$ has $\tilde\omega_{A,\delta}(x) > \frac{2}{n^2}OPT$ it adds $x$ ; otherwise, if some $x \in A$ has $\tilde\omega_{A,\delta}(x) < -\frac{2}{n^2}OPT$ it removes $x$ ; otherwise it stops and returns a random set $\mathcal{R}(A, \delta')$ .

Formalization targets

Goal: Theorem 3.6 in the explicit form of its proof

With $\delta = 1/3$ , and $\delta' = 1/3$ with probability $0.9$ or $\delta' = -1$ with probability $0.1$ : for every run from $\emptyset$ whose estimates are all accurate and which has terminated at $A$ ,

\tfrac{9}{10}\,\mathbf{E}[f(\mathcal{R}(A,\tfrac13))] + \tfrac{1}{10}\,f(X \setminus A) \ge \Big(\frac{2}{5} - \frac{9}{5n}\Big) OPT,

and, for every $\delta \in (0,1]$ , every run of $k$ iterations with accurate estimates has $k < n^2/\delta$ (fewer than $3n^2$ for $\delta = 1/3$ ).

Milestones, in attack order

Lemma 2.2: $\mathbf{E}[g(A(p))] \ge (1-p)g(\emptyset) + p\,g(A)$ .
Display (∗): for three independently sampled sets, $\mathbf{E}[f(A_1(p_1) \cup A_2(p_2) \cup A_3(p_3))] \ge \sum_{I \subseteq \{1,2,3\}} \prod_{i\in I} p_i \prod_{i \notin I}(1-p_i) f(\bigcup_{i \in I} A_i)$ .
The increment identity $\Phi(A \cup \{x\}) - \Phi(A) = \delta\,\omega_{A,\delta}(x)$ for $x \notin A$ , and its removal counterpart.
$0 \le \Phi(A) \le OPT$ .
The terminal upper estimates $\mathbf{E}[f(R \cup (B\cap C))],\ \mathbf{E}[f(R \cap (B \cup C))] \le \mathbf{E}[f(R)] + \frac{2}{n}OPT$ .
The two lower bounds in $27$ ths on the same two expectations.
The final chain $\mathbf{E}[f(R)] + \frac19 f(B) + \frac2n OPT \ge \frac49 OPT$ .

Significance

The $2/5$ bound showed that local search on a smoothed objective, the multilinear extension restricted to points with two coordinate values, beats both uniform sampling and plain local search for non-monotone submodular maximization. The multilinear extension later became the standard tool for submodular maximization under constraints, through continuous greedy methods, contention resolution schemes and the analysis of randomized rounding. Display (∗) and Lemma 2.2 are the basic sampling inequalities for submodular functions and are reused throughout that literature.

The result is proved in the paper; it has been superseded in ratio by later algorithms reaching $1/2$ . To our knowledge none of it is machine-checked: Mathlib has no multilinear extension and no submodular maximization results. This mission produces a checked form of the analysis with every constant explicit: the $o(1)$ as $\frac{9}{5n}$ , "polynomial time" as $n^2/\delta$ iterations, and the dependence on the accuracy of the sampled estimates as an explicit hypothesis.

Difficulty

The iteration bound and the increment identity are routine once the multilinear extension is set up. The substance lies in the lower bounds. The returned set $R$ is random, so the comparison with the optimal set $C$ cannot be made through a single local-optimality inequality as in deterministic local search; and approximate local optimality holds only for the smoothed marginals $\omega_{A,\delta}$ , which are averages over the random set, not for $f$ at any fixed set. Sampling inequalities such as (∗) are stated for independent samples of arbitrary, possibly overlapping sets, and their expectations are sums over products of subsets; the bookkeeping of such sums is the main formalization burden. The constants must also balance exactly: with $\delta = 1/3$ the $27$ ths add up so that the $\frac{9}{10}/\frac{1}{10}$ mixture yields $2/5$ . A different split or a different $\delta$ gives a different constant.

Formalization scope

The ground set is a Fintype X with decidable equality; sets are Finset X; $f$ is real valued, with nonnegativity and submodularity as hypotheses. The standing assumptions of the paper are made explicit: $f \ge 0$ (§3), value-oracle access (modelled by $f$ itself), $n = |X|$ , and $n \ge 1$ (Nonempty X), so that $\frac{1}{n^2}$ and $\frac{9}{5n}$ are not Lean's junk value of division by zero. $OPT$ is Finset.sup' over all subsets, which has no junk value. Every expectation over independently sampled sets is an exact finite sum: the multilinear extension for $\mathcal{R}(A,\delta)$ , and iterated sums over subsets for the several independent samples in Lemma 2.2 and (∗). Sampling probabilities carry $0 \le p \le 1$ .

The algorithm is a relation, not a choice: any element meeting the step-3 condition may be added, and removal is allowed only when no addition applies. The goal quantifies over every run from $\emptyset$ , every choice of accurate estimates, recomputed at every iteration, and every termination point. Accuracy is non-strict ("within $\pm$ "); the thresholds are strict. The thresholds and accuracy use $OPT$ itself, as the proof does, although step 1 of the algorithm says an estimate of $OPT$ is used. The sampling that produces the estimates and its "with high probability" are not modelled, and the goal is conditional on accurate estimates. The value of the $\delta' = -1$ branch is written as $\mathbf{E}[f(\mathcal{R}(A,-1))]$ , which equals $f(X \setminus A)$ .

A statement "every $A$ satisfying the terminal conditions gives $2/5 - 9/(5n)$ " would be the final milestone plus arithmetic and is not the goal. The goal fixes the start at $\emptyset$ , the thresholds, the step order, the accuracy of every estimate, termination and the $0.9/0.1$ mixture.

A complete development needs basic calculus of the multilinear extension: affinity in one coordinate, translation $f(\cdot \cup D)$ and restriction $f(\cdot \cap D)$ , and splitting a sample into disjoint pieces. These lemmas are reusable for any work on submodular maximization, and contributions of them as separate theorems are welcome. The golden-ratio variant $\delta = \delta'$ (proof omitted in the paper), the tight example and the hardness results of §4 are out of scope.

Selected references

U. Feige, V. S. Mirrokni, J. Vondrák, Maximizing Non-Monotone Submodular Functions, SIAM J. Comput. 40(4):1133–1153, 2011. https://doi.org/10.1137/090779346
S. O. Gharan, J. Vondrák, Submodular Maximization by Simulated Annealing, SODA 2011. https://doi.org/10.1137/1.9781611973082.83
N. Buchbinder, M. Feldman, J. Naor, R. Schwartz, A Tight Linear Time (1/2)-Approximation for Unconstrained Submodular Maximization, SIAM J. Comput. 44(5):1384–1402, 2015. https://doi.org/10.1137/130929205
G. Calinescu, C. Chekuri, M. Pál, J. Vondrák, Maximizing a Monotone Submodular Function Subject to a Matroid Constraint, SIAM J. Comput. 40(6):1740–1766, 2011. https://doi.org/10.1137/080733991

14 thms3 active usersReviewed

Completed

Combinatorics·Captain: mikedeng1

Three Partition Refinement Algorithms 1: Distinguishing-Prefix Refinement Finds Every Distinguishing Prefix Within m′ Refinement StepsResearch Paper

Motivation

Sorting a collection of strings in lexicographic order is a basic subroutine in compilers, string indexing, suffix sorting and the construction of tries. The classical method, due to Aho, Hopcroft and Ullman (The Design and Analysis of Computer Algorithms, 1974), is a multipass radix sort that processes the strings from the last position to the first and runs in time proportional to the total length $m$ of the input plus the alphabet size $k$ . Mehlhorn showed that a straightforward first-to-last scan of equal-length strings needs $\Omega(km)$ time.

Paige and Tarjan (Three Partition Refinement Algorithms, SIAM J. Comput. 16(6):973–989, 1987, doi:10.1137/0216062) observed that most of the input is usually irrelevant to the sorted order: only the shortest prefix of each string that tells it apart from the others matters. Their algorithm separates the problem into two steps: (1) find this distinguishing prefix of every string, and (2) sort the distinguishing prefixes. The first step is carried out by partition refinement, the same technique that the paper then applies to the relational coarsest partition problem (the second mission of this series) and to double lexical ordering. This mission formalizes the correctness and the termination bound of the first step.

Setting

Fix $k \ge 1$ and the alphabet $\Sigma = \{1, 2, \dots, k\}$ , together with an end marker $0$ that is smaller than every symbol. A string is a finite sequence over $\Sigma \cup \{0\}$ ; $\lambda$ is the empty string, $|x|$ is the length of $x$ , and $x(i)$ is its $i$ -th symbol (positions start at $1$ ). A string $\alpha$ is a prefix of $y$ if $y = \alpha z$ for some string $z$ ; every string is a prefix of itself. $\Sigma^*0$ is the set of strings over $\Sigma$ followed by one $0$ .

The input is a multiset $U = \{x_1, \dots, x_n\} \subseteq \Sigma^*0$ with $n \ge 1$ ; repeated strings are allowed. The distinguishing prefix $x'_i$ of $x_i$ in $U$ is

the shortest prefix of $x_i$ that is not a prefix of any other string of $U$ , if $x_i$ occurs only once in $U$ ;
$x_i$ itself, if $x_i$ occurs more than once.

Write $m' = \sum_{i=1}^n |x'_i|$ .

For a string $\alpha$ , the labeled block $B_\alpha$ is the multiset of strings of $U$ having $\alpha$ as a prefix, and $\alpha$ is its associated prefix. The block is finished if $\alpha = x'_i$ for some $i$ , and unfinished otherwise. A state $P$ is a set of labeled blocks. For an unfinished block $B_\alpha \in P$ ,

\mathrm{split}(B_\alpha, P) = \bigl(P \setminus \{B_\alpha\}\bigr) \cup \{\, B_{\alpha u} : u \in \Sigma \cup \{0\},\ \exists x \in B_\alpha,\ x(|\alpha| + 1) = u \,\}.

The refinement algorithm starts from $P_0 = \{B_\lambda\}$ and repeatedly applies the step Refine: pick any unfinished block $B_\alpha \in P$ and replace $P$ by $\mathrm{split}(B_\alpha, P)$ . A run with $K$ steps is a sequence $P_0, P_1, \dots, P_K$ produced this way; any choice of unfinished block is allowed at every step.

Formalization targets

Goal: Theorem 1 with its explicit bound

For every run $P_0, \dots, P_K$ of the refinement algorithm,

K \le m' \qquad\text{and}\qquad \bigl(\text{no block of } P_K \text{ is unfinished}\bigr) \implies P_K = \{B_{x'_1}, \dots, B_{x'_n}\}.

The paper states Theorem 1 as "The algorithm terminates and is correct"; the bound $K \le m'$ is the explicit count proved in the last sentence of its proof (p. 975). The goal leaves the choice of unfinished block free, so it holds for every refinement order.

Milestones

End markers (§2, p. 974). No string of $U$ is a proper prefix of another string of $U$ .
Lemma 1 (p. 975). Along every run, every finished block $B_\beta$ is contained in a block of the current state, and there is $B_\alpha \in P_j$ with $\alpha$ a prefix of $\beta$ .
Proof of Theorem 1, second sentence. For every state of every run, $\sum_{B_\alpha \in P_j} |\alpha| \le m'$ .
Proof of Theorem 1, third sentence. Every Refine step strictly increases $\sum_{B_\alpha \in P} |\alpha|$ .

A supplementary item states the fact on p. 974 that motivates the two-step design: distinct strings have distinct distinguishing prefixes, and $x_i \le x_j$ iff $x'_i \le x'_j$ in lexicographic order.

Significance

Theorem 1 is the correctness half of the lexicographic sorting algorithm: once the distinguishing prefixes are known, sorting $U$ reduces to sorting strings of total length $m'$ , which is how the paper obtains its $O(m' + k)$ time bound in place of $O(m + k)$ . The paper notes that under a natural probability model $m'$ is of order $n \log_k n$ , so the gain is large whenever the strings are long. The invariant of Lemma 1 is also the pattern on which the later partition refinement algorithms of the paper are built: a target partition is shown to refine every intermediate partition, and a potential function bounds the number of refinement steps.

The result has been proved since 1987. What this mission adds is a machine-checked account of the algorithm at the level of its abstract refinement steps, with the explicit bound $m'$ rather than an asymptotic statement, and with the standing assumptions of §2 (non-empty input, end markers) made explicit. No formal proof of this algorithm is present in Mathlib or on the platform.

Difficulty

The obvious argument, "each step makes the labels longer, and labels never grow past the distinguishing prefixes", needs two facts that are not immediate from the definitions. First, the labels of a reached state must form a partition of $U$ into non-empty blocks whose labels are pairwise incomparable under the prefix order; this is an invariant of the algorithm, not part of the definition of a state, and it fails for arbitrary sets of labels. Second, the label of an unfinished block must be a proper prefix of every finished label below it, which rests on the end marker: without end markers a string can be a proper prefix of another, a block can be unfinished yet have no strictly longer children, and the algorithm can stall. Bounding the sum of label lengths by $m'$ is not a label-by-label comparison: a state can have fewer labels than strings, and the distinguishing prefixes of different strings can share a label as a common prefix.

Formalization scope

Strings are List (Fin (k + 1)), with 0 : Fin (k + 1) the end marker and prefix the Mathlib relation <+:. The multiset $U$ is a family x : Fin n → List (Fin (k + 1)), so repetitions are distinct indices. The hypotheses 0 < n and EndMarked x ( $U \subseteq \Sigma^*0$ ) are the paper's standing assumptions. A block is identified by its label, not by its set of members: two different labels can carry the same strings (for instance $B_\lambda = B_1$ when every string begins with $1$ ), and they are different blocks. A state is a Finset of labels; a run is a map Fin (K + 1) → Finset (List (Fin (k + 1))) starting at {[]}. Positions are 1-based in the paper and 0-based in Lean, so $x(|\alpha|+1)$ is (x i)[α.length]?. The distinguishing prefix follows the literal definition; for $n = 1$ it is the empty string.

The running times $O(m' + k)$ and $O(n + k)$ space, the implementation with a queue and a global index, and step two (sorting the prefixes via the refinement tree) are RAM-model statements and are not formalized. Only the explicit step count $m'$ is. A formalization in which split added all $k + 1$ children, added none, or allowed refining a finished block would change the theorem (the bound fails or the goal becomes vacuous); the definitions add exactly the children realized by some string of the block and refine only unfinished blocks.

Contributions welcome: proofs of the milestones, a general API for prefix-closed partition refinement on List, and a proof of the order-preservation item via Mathlib's List.Lex.

Selected references

R. Paige, R. E. Tarjan, Three Partition Refinement Algorithms, SIAM Journal on Computing 16(6):973–989, 1987. https://doi.org/10.1137/0216062
A. V. Aho, J. E. Hopcroft, J. D. Ullman, The Design and Analysis of Computer Algorithms, Addison-Wesley, 1974.
K. Mehlhorn, Data Structures and Algorithms 1: Sorting and Searching, Springer, 1984. https://doi.org/10.1007/978-3-642-69672-5

7 thms3 active usersReviewed

Completed

Combinatorics Graph Theory Operations Research·Captain: mikedeng1

A Linear-Time Algorithm for Finding a Sparse k-Connected Spanning Subgraph of a k-Connected Graph 2: FOREST's Forests E_i Preserve Local Node-Connectivity up to i in a Simple GraphResearch Paper

Motivation

Given a $k$ -connected graph, many connectivity algorithms run in time that grows with the number of edges $|E|$ . A sparse certificate is a spanning subgraph with only $O(k|V|)$ edges that is still $k$ -connected; computing one first and running the expensive algorithm on it replaces $|E|$ by $k|V|$ in the bound. Finding a $k$ -connected spanning subgraph with the minimum number of edges is NP-complete for every fixed $k \ge 2$ (Garey and Johnson, problem GT31), so the question is how cheaply a sparse, not necessarily minimum, certificate can be found.

Nagamochi and Ibaraki (Algorithmica 7 (1992) 583–596) answered this with a single linear-time scanning procedure, FOREST, which partitions the edges into classes $E_1, E_2, \dots, E_{|E|}$ . They showed that the prefix unions $E_1 \cup \dots \cup E_k$ are certificates for edge-connectivity and, for simple graphs, for node-connectivity. The node-connectivity result is the subject of this mission; the edge-connectivity result is the preceding mission of this series.

Timeline:

1980: Galil gives an algorithm testing $\kappa(G) \ge k$ whose running time depends on $|E|$ (SIAM J. Comput. 9).
Before 1992 (as cited on p. 583): Suzuki et al. give $O(|E|)$ -time algorithms for sparse 2- and 3-node-connected spanning subgraphs; Nishizeki and Poljak find, for general $k$ , a $k$ -node-connected spanning subgraph with at most $k(|V|-1)$ edges in $O(|V|^{1/2}|E|^2)$ time.
1992: Nagamochi and Ibaraki prove that FOREST, which runs in $O(|V| + |E|)$ time, yields a $k$ -node-connected spanning subgraph $G_k$ of every simple $k$ -node-connected graph, with $|E(G_k)| \le k|V| - k(k+1)/2$ . Their Theorem 3.1 states a stronger, local form.
1993: Cheriyan, Kao and Thurimella isolate "scan-first search" as the general principle behind such certificates (SIAM J. Comput. 22 (1993)).

Setting

A graph $G = (V, E)$ has a finite node set $V$ with $|V| \ge 2$ and a finite edge set $E$ ; each edge has an unordered pair of two distinct end nodes. In this mission the graph is simple: no two edges have the same end nodes. For $F \subseteq E$ , $(V, F)$ is the spanning subgraph with edge set $F$ .

The local node-connectivity $\kappa(x, y; H)$ of nodes $x, y$ in a graph $H$ on $V$ is $|V| - 1$ if $x$ and $y$ are adjacent in $H$ , and otherwise the minimum size of a node set $W \subseteq V - \{x, y\}$ whose deletion leaves no $x$ – $y$ path. The node connectivity is $\kappa(G) = \min_{x, y} \kappa(x, y; G)$ .

Procedure FOREST keeps a label $r(v) \ge 0$ on each node, initially $0$ . While some node is unscanned, it chooses an unscanned node $x$ of largest label; for each unscanned edge $e = (x, y)$ it puts $e$ into the class $E_{r(y)+1}$ , increases $r(x)$ by one if $r(x) = r(y)$ , and increases $r(y)$ by one; then it marks $x$ scanned. Ties are broken arbitrarily. The time instants are the states between these elementary operations; $E^*_i$ denotes the class $i$ at an instant, and $E_i$ its final value. Put

G_i = (V,\ E_1 \cup E_2 \cup \dots \cup E_i).

Formalization targets

Goal: Theorem 3.1

For a simple graph $G$ and the classes of any completed run of FOREST, for $1 \le i \le |E|$ ,

\kappa(x, y; G_i) \ \ge\ \min\{\kappa(x, y; G),\ i\} \qquad \text{for any } x, y \in V. \tag{3.1}

The statement is local: it holds pair by pair, not only for the global minimum, and for every tie-breaking of the procedure.

Milestones, in the order the proof uses them

Lemma 2.2: at every instant, a node $v$ meets $E_i$ exactly for $i = 1, \dots, r(v)$ .
Lemma 2.4(b): at every instant, a $u$ – $v$ path in $E^*_j$ yields $u$ – $v$ paths in every $E^*_i$ , $i < j$ .
In-degree at most one (§2, p. 588): orienting each edge from the earlier-scanned to the later-scanned end, every node has at most one entering arc in each class.
Lemma 3.1: if an $x$ – $y$ path of $E^*_j$ has the form $x, u_1, \dots, u_k = w, y$ with $k = 1$ or $u_1$ scanned before $w$ , then any $w$ – $x$ and $w$ – $y$ paths in $E^*_i$ ( $i < j$ ) share a node other than $w$ .
Lemma 3.2: for a node cut set $W = \{w_1, \dots, w_i\}$ of $G_{i+1}$ (in scan order) separating a component $X$ from the rest $Y$ , immediately after $w_t$ is scanned every $X$ – $Y$ path of $E^*_t$ passes through $w_t$ , and $E^*_j$ has no $X$ – $Y$ path for $t + 1 \le j \le i + 1$ .

A companion item states the paper's announcement in §3: $G_k$ is $k$ -node-connected for every $1 \le k \le \kappa(G)$ .

Significance

Theorem 3.1 at $i = k$ shows that the first $k$ classes of FOREST form a $k$ -node-connected spanning subgraph whenever $G$ is, and the edge-count analysis of the companion mission bounds its size by $k|V| - k(k+1)/2$ . Since FOREST runs in linear time, any algorithm testing $\kappa(G) \ge k$ can be run on $G_k$ instead of $G$ ; the paper uses this to improve the bound for testing $\kappa(G) \ge k$ from $O(\max\{k^2|V|^{1/2}, k|V|\}|E|)$ to $O(\max\{k^3|V|^{3/2}, k^2|V|^2\})$ , and similar gains for computing the number of node-disjoint paths between two nodes. The local form (3.1) is what makes the $s$ – $t$ applications possible.

The result is proved on paper. As far as a search of the platform shows, neither FOREST nor local node-connectivity has a machine-checked treatment there; Mathlib has no notion of vertex connectivity of a pair of nodes. This mission produces a formal model of FOREST as a nondeterministic transition system and the statements needed to verify the paper's proof step by step.

Difficulty

For edge-connectivity the analogous statement follows from a general principle: any sequence of maximal spanning forests, each taken in what remains of the graph, preserves local edge-connectivity up to its length. The obvious attempt is to prove (3.1) the same way, from the fact that each $E_i$ is a maximal spanning forest of what the earlier classes leave. The paper gives no such argument for node-connectivity: its proof uses the specific scan order of FOREST in an essential way, through the orientation of edges from earlier- to later-scanned nodes and the in-degree bound of that orientation (Lemmas 3.1 and 3.2). The argument tracks, for a hypothetical node cut $W$ of size $i$ in $G_{i+1}$ , the classes at the moments the nodes of $W$ are scanned, which requires reasoning about intermediate states of the algorithm and about paths in several classes at once. None of this reduces to a static property of the output partition.

Formalization scope

Graphs. A node type V and an edge type E, both finite, with ends : E → Sym2 V; loop-freeness is ∀ e, ¬ (ends e).IsDiag and simplicity is Function.Injective ends. The standing assumptions of p. 583 and p. 589 ( $|V| \ge 2$ , no self-loop, a simple graph when node-connectivity is discussed) appear as hypotheses; §2 items are stated for loopless graphs, as on the page.
Connectivity. $\kappa(x, y; (V, F))$ is valued in $\mathbb N_\infty$ : $|V| - 1$ on adjacent pairs, the minimum node cut otherwise, and $\top$ when $x = y$ , where (3.1) holds trivially.
FOREST. A nondeterministic step relation with three steps (select, scan, finish), a run of length $K$ from the initial state, and completion when every node is scanned. Every tie-breaking is allowed, so the theorems quantify over all completed runs. A time instant is a state of a run; "scanned before" compares positions in the run's selection order; "immediately after $w_t$ has been scanned" is the state right after the finish step of $w_t$ .
Excluded. The running time " $O(|V| + |E|)$ " and everything in §4 (the connectivity-testing algorithms and their bounds) are not stated: the paper fixes no machine model. The edge bounds on $|E_i|$ belong to the edge-connectivity mission.
Ruled out. Stating (3.1) for an arbitrary partition into maximal spanning forests, or reading the classes $E^*_j$ of Lemmas 3.1–3.2 off the final state, would state a different theorem from the one the paper proves; the classes are those of a run of FOREST at the instant the page specifies.
Infrastructure. Reachability avoiding a node set, walks and paths in SimpleGraph, and invariants of the FOREST transition system. The definitions duplicate those of the edge-connectivity mission by design and are candidates for a shared layer. Contributions of general lemmas about the run (label invariants, monotonicity of classes along a run) are welcome.

Selected references

H. Nagamochi, T. Ibaraki, A linear-time algorithm for finding a sparse $k$ -connected spanning subgraph of a $k$ -connected graph, Algorithmica 7 (1992), 583–596. https://doi.org/10.1007/BF01758778
Z. Galil, Finding the vertex connectivity of graphs, SIAM J. Comput. 9 (1980), 197–199. https://doi.org/10.1137/0209016
J. Cheriyan, M.-Y. Kao, R. Thurimella, Scan-first search and sparse certificates: an improved parallel algorithm for $k$ -vertex connectivity, SIAM J. Comput. 22 (1993), 157–174. https://doi.org/10.1137/0222013
M. R. Garey, D. S. Johnson, Computers and Intractability: A Guide to the Theory of NP-Completeness, Freeman, 1979.

9 thms3 active usersReviewed

Completed

Combinatorics Graph Theory Operations Research·Captain: mikedeng1

A Linear-Time Algorithm for Finding a Sparse k-Connected Spanning Subgraph of a k-Connected Graph 1: The FOREST Decomposition Preserves Local Edge-ConnectivityResearch Paper

Motivation

Many graph algorithms for connectivity questions run in time proportional to the number of edges. When the question is only whether a graph is $k$ -edge-connected, or what its local edge-connectivities are up to a threshold $k$ , most edges are irrelevant: a spanning subgraph with $O(k|V|)$ edges already carries the answer. Such a subgraph is called a sparse certificate. Computing one first and running the expensive algorithm on it replaces $|E|$ by $k|V|$ in the running time of connectivity testing, of Matula-type edge-connectivity algorithms, and of $s$ – $t$ flow computations used as connectivity oracles.

Nagamochi and Ibaraki (Algorithmica 7, 1992) gave a procedure, FOREST, that computes such a certificate for edge-connectivity and, on simple graphs, for node-connectivity, with a single graph search. The same partition of the edges into forests is the engine of their deterministic minimum-cut algorithm for multigraphs (SIAM J. Discrete Math. 5, 1992), which later became the maximum-adjacency ordering of the Stoer–Wagner minimum-cut algorithm (J. ACM 44, 1997).

Timeline:

1927: Menger identifies the minimum number of edges separating two nodes with the maximum number of edge-disjoint paths between them.
1992: Nagamochi and Ibaraki publish Procedure FOREST and prove that its $i$ -th prefix preserves local edge-connectivity up to $i$ in multigraphs, and local node-connectivity up to $i$ in simple graphs.
1993: Cheriyan, Kao and Thurimella (SIAM J. Comput. 22) obtain sparse certificates by scan-first search; Frank, Ibaraki and Nagamochi (J. Graph Theory 17) give a shorter proof for the node-connectivity case.
1994: Nishizeki and Poljak (Discrete Appl. Math. 55) publish the forest-decomposition lemma (Lemma 2.1 below), found independently.

Setting

A graph $G = (V, E)$ is finite and undirected, has $|V| \ge 2$ nodes, may have multiple edges (several edges with the same pair of end nodes), and has no self-loop. It is simple if no two edges have the same end nodes. For $F \subseteq E$ , $(V, F)$ is the spanning subgraph with edge set $F$ . It is a forest if it has no cycle; two parallel edges form a cycle. It is a maximal spanning forest in $(V, H)$ , for $F \subseteq H$ , if adding any edge of $H \setminus F$ to $F$ creates a cycle.

The local edge-connectivity $\lambda(x, y; H)$ is the minimum number of edges of $H$ whose removal leaves no path from $x$ to $y$ ; parallel edges count separately. It is $\infty$ when $x = y$ .

Procedure FOREST keeps a label $r(v) \in \mathbb{N}$ on every node, initially $0$ , and classes $E_1, E_2, \dots, E_{|E|}$ , initially empty. While an unscanned node exists, it picks an unscanned node $x$ of largest label; for every unscanned edge $e$ from $x$ to a node $y$ , it puts $e$ into $E_{r(y)+1}$ , increases $r(x)$ by one if $r(x) = r(y)$ , increases $r(y)$ by one, and marks $e$ scanned; then it marks $x$ scanned. Ties among nodes and the order of edges are free. On termination, $G_i = (V, E_1 \cup \cdots \cup E_i)$ .

Formalization targets

Goal: Theorem 2.1 (pp. 588–589), without the running time

For every graph $G$ and every completed execution of FOREST on $G$ :

every edge lies in exactly one class $E_i$ , $1 \le i \le |E|$ ;
for $i = 1, \dots, |E|$ ,

\lambda(x, y; G_i) \ge \min\{\lambda(x, y; G),\ i\} \qquad \text{for all } x, y \in V; \tag{2.1}

$|E_i| \le |V| - 1$ for all $i$ ;
if $G$ is simple, $|E_i| \le |V| - i$ for $i \le |V| - 1$ and $E_i = \emptyset$ for $i \ge |V|$ .

Milestones

Lemma 2.2 (p. 587): during the execution, a node $v$ has incident edges in exactly the classes $E_1, \dots, E_{r(v)}$ .
Lemma 2.3 (p. 587): each $(V, E_i)$ is a forest at every instant.
Lemma 2.4 (p. 588): (a) an edge $(u, v)$ added to $E_i$ has its end nodes joined by a path in $E_{i-1}$ ; (b) a path in $E_j$ between $u$ and $v$ yields a path in every $E_i$ , $i < j$ .
Lemma 2.5 (p. 588): each output $(V, E_i)$ is a maximal spanning forest in $G - E_1 \cup \cdots \cup E_{i-1}$ .
Lemma 2.1 (p. 584): any sequence of successive maximal spanning forests satisfies (2.1).

Companions

the sparse certificate (p. 589): if $\lambda(x, y; G) \ge k$ for all $x, y$ , then $G_k$ is $k$ -edge-connected with $|E(G_k)| \le k(|V| - 1)$ , and $|E(G_k)| \le k|V| - k(k+1)/2$ for simple $G$ ;
Lemma 2.6 (p. 589): for $k \le \delta(G)$ , $G_k$ has a node of degree exactly $k$ .

Significance

(2.1) says that one search produces, for every threshold $k$ at once, a subgraph with at most $k(|V|-1)$ edges that keeps every local edge-connectivity up to $k$ . Any algorithm whose running time grows with $|E|$ can then be run on $G_k$ in place of $G$ ; §4 of the paper uses this to speed up $k$ -connectivity tests and the computation of local connectivities. The same forest partition is the structural fact behind the Nagamochi–Ibaraki and Stoer–Wagner minimum-cut algorithms. Lemma 2.6 shows that the certificate is tight: its edge-connectivity is exactly $k$ when $\lambda(G) \ge k$ .

The results are proved in the paper. No machine-checked proof of them is known. Formalizing them means formalizing a graph search with free tie-breaking as a transition system, reasoning about invariants of all its executions, and proving a cut-counting statement for multigraphs. Mathlib's connectivity notions, such as SimpleGraph.IsEdgeReachable, do not see parallel edges, so the multigraph cut theory here is new.

Difficulty

Lemma 2.1 is a short cut argument once maximality is available. The difficulty is showing that FOREST, which assigns each edge to a class by looking only at the label of one end node, produces maximal forests in the successive residual graphs (Lemma 2.5). The obvious invariant, that the class of an edge is the first forest it does not close a cycle in, is not what line 7 computes. The label $r(y)$ records only which classes touch $y$ , not which component of each class contains $y$ . The paper's argument needs Lemma 2.4(a): at the moment an edge is added to $E_i$ its ends already lie in one tree of $E_{i-1}$ . That relies on the choice of the unscanned node of largest label, on the order of lines 8 and 9, and on an argument about the scan order of tree roots.

Formalization scope

Graphs. A graph is a finite node type V with $|V| \ge 2$ , a finite edge type E, and ends : E → Sym2 V with no diagonal value (no self-loops). Parallel edges are distinct elements of E. Simplicity is injectivity of ends, and edge subsets are Finset E. A forest is an edge set in which every edge is a bridge, a condition that sees parallel edges.
Connectivity. $\lambda$ is an infimum in ℕ∞ over separating edge sets, $\infty$ at $x = y$ . (2.1) is kept "for all $x, y$ ", as printed.
FOREST. FOREST is a nondeterministic step relation (select, scan, finish) on explicit states: labels, class index per edge ( $0$ = unscanned), scanned nodes, current node and selection order. The theorems quantify over every run from the initial state, so no tie-breaking rule is fixed. "At some time instant" is a state of the run; "upon completion" is a run whose last state has every node scanned. Lemma 2.2 is stated at every state, not only after a scan block (the other steps change neither labels nor classes). Lemma 2.4(a) assumes $i \ge 2$ , since $E_0$ does not exist.
Exclusions. Theorem 2.1's clause "is found in $O(|V| + |E|)$ time", the bucket implementation, and the time bound of the certificate are not formalized: the paper fixes no machine model. The goal consists of the structural conclusions only. The bound printed "if $G$ is multiple" is stated for every loopless graph.
Non-triviality. The goal is about the classes of a run of FOREST. An arbitrary partition of $E$ into maximal spanning forests is Lemma 2.1's hypothesis, not a formalization of Theorem 2.1. A statement in which the classes are unconstrained variables, or in which the run hypotheses cannot be met, would be trivial. A separate sanity file checks that a complete run on the triangle $K_3$ exists and attains $|E_1| = |V| - 1$ , $|E_2| = |V| - 2$ .
Welcome contributions. Useful reusable infrastructure includes:
- a cut and Menger layer for finite multigraphs;
- forest and bridge lemmas for edge-indexed graphs;
- invariant-style reasoning over runs.

Selected references

H. Nagamochi, T. Ibaraki, A linear-time algorithm for finding a sparse $k$ -connected spanning subgraph of a $k$ -connected graph, Algorithmica 7 (1992) 583–596. https://doi.org/10.1007/BF01758778
H. Nagamochi, T. Ibaraki, Computing edge-connectivity in multigraphs and capacitated graphs, SIAM J. Discrete Math. 5 (1992) 54–66. https://doi.org/10.1137/0405004
T. Nishizeki, S. Poljak, $k$ -connectivity and decomposition of graphs into forests, Discrete Appl. Math. 55 (1994) 295–301. https://doi.org/10.1016/0166-218X(94)90014-0
J. Cheriyan, M.-Y. Kao, R. Thurimella, Scan-first search and sparse certificates: an improved parallel algorithm for $k$ -vertex connectivity, SIAM J. Comput. 22 (1993) 157–174. https://doi.org/10.1137/0222013
A. Frank, T. Ibaraki, H. Nagamochi, On sparse subgraphs preserving connectivity properties, J. Graph Theory 17 (1993) 275–281. https://doi.org/10.1002/jgt.3190170302
M. Stoer, F. Wagner, A simple min-cut algorithm, J. ACM 44 (1997) 585–591. https://doi.org/10.1145/263867.263872

10 thms3 active usersReviewed

Completed

Control Theory Operations Research·Captain: mikedeng1

Supervisory Control of a Class of Discrete Event Processes I: Minimally Restrictive Supervisors Exist iff the Supremal Controllable Legal Sublanguage Contains the Minimal Acceptable LanguageResearch Paper

Motivation

Manufacturing cells, communication protocols, traffic systems and database transaction managers are naturally described not by differential equations but by sequences of discrete events: a machine starts, a part arrives, a message is lost. Ramadge and Wonham's 1987 paper (SIAM J. Control Optim. 25(1)) set up a control theory for such systems in which the plant is an automaton, the controller is another automaton that may disable some events, and specifications are formal languages. The framework, now called supervisory control theory or the Ramadge–Wonham framework, is the standard model for the logical control of discrete event systems and underlies the textbook treatment in Cassandras and Lafortune (Introduction to Discrete Event Systems, 2008) and Wonham and Cai (Supervisory Control of Discrete-Event Systems, 2019).

The question the paper answers is the basic synthesis question of the theory: given a plant, a set of legal behaviours and a set of minimally acceptable behaviours, when does a controller exist that keeps the plant legal, achieves at least the acceptable behaviour, and never deadlocks, and what is the least restrictive such controller?

Setting

A generator is $\mathcal G = (Q, \Sigma, \delta, q_0, Q_m)$ with a state set $Q$ , a finite alphabet $\Sigma$ of events, a partial transition function $\delta : \Sigma \times Q \to Q$ , an initial state $q_0$ and marker states $Q_m \subseteq Q$ . Extending $\delta$ to strings, the generated language $L(\mathcal G)$ is the set of strings $w$ for which $\delta(w, q_0)$ is defined, and the marked language $L_m(\mathcal G)$ is the subset of those that end in $Q_m$ . The closure $\bar K$ of a language $K$ is its set of prefixes; $K$ is closed if $K = \bar K$ . Throughout, $\mathcal G$ is assumed trim in the sense $L(\mathcal G) = \bar L_m(\mathcal G)$ : every generated string can be completed to a marked one.

The alphabet is split into controllable events $\Sigma_c$ and uncontrollable events $\Sigma_u = \Sigma - \Sigma_c$ . A supervisor $\mathcal S = (S, \phi)$ consists of a deterministic, accessible automaton $S = (X, \Sigma, \xi, x_0, X_m)$ , whose state set $X$ may be infinite, and a map $\phi$ assigning to each state $x$ the set of controllable events it enables; uncontrollable events are always enabled. The closed loop $\mathcal S/\mathcal G$ runs $S$ and $\mathcal G$ in lockstep: an event occurs when the plant can execute it, the supervisor enables it, and the supervisor's automaton can follow it. This defines the languages $L(\mathcal S/\mathcal G)$ , $L_m(\mathcal S/\mathcal G)$ and the controlled language $L_c(\mathcal S/\mathcal G) = L(\mathcal S/\mathcal G) \cap L_m(\mathcal G)$ .

$\mathcal S$ is complete if its automaton never refuses an event that the plant can execute and $\phi$ enables; it is proper if it is complete and

\bar L_m(\mathcal S/\mathcal G) = \bar L_c(\mathcal S/\mathcal G) = L(\mathcal S/\mathcal G),

that is, every closed-loop string can be completed to a marked task. A language $K$ is controllable if $K \subseteq L(\mathcal G)$ and $\bar K \Sigma_u \cap L(\mathcal G) \subseteq \bar K$ . For $L \subseteq L(\mathcal G)$ , $\mathbf C_{\mathcal G}(L)$ is the class of controllable sublanguages of $L$ and $\mathbf F_{\mathcal G}(L)$ the class of sublanguages $K$ of $L$ with $K = \bar K \cap L_m(\mathcal G)$ .

Given $\emptyset \neq L_a \subseteq L_g \subseteq L_m(\mathcal G)$ , the Supervisory Marking Problem (SMP) asks for a proper $\mathcal S$ with $L_a \subseteq L_m(\mathcal S/\mathcal G) \subseteq L_g$ , and the Supervisory Control Problem (SCP) for a proper $\mathcal S$ with $L_a \subseteq L_c(\mathcal S/\mathcal G) \subseteq L_g$ .

Formalization targets

Goal: Theorem 7.1 (pp. 218–219)

\text{SMP solvable} \iff \sup \mathbf C_{\mathcal G}(L_g) \supseteq L_a, \qquad \text{SCP solvable} \iff \sup\{\mathbf C_{\mathcal G}(L_g) \cap \mathbf F_{\mathcal G}(L_g)\} \supseteq L_a,

and in each case the solving supervisor can be taken minimally restrictive: its marked (respectively controlled) language equals the supremal element and contains that of every proper supervisor whose language lies in $L_g$ .

Milestones

Proposition 4.1 (i), (ii): marking is independent of control; every $K \subseteq L_m(\mathcal G)$ , or $K \subseteq L \cap L_m(\mathcal G)$ for an achievable closed $L$ , is the marked language of a complete supervisor.
Proposition 5.1: a complete supervisor realizes $(L_m, L_c, L) = (K_1, K_2, K_3)$ iff $K_1 \subseteq K_2$ , $K_2 = K_3 \cap L_m(\mathcal G)$ and $K_3$ is closed and controllable.
Theorem 6.1 (i), (ii): a proper supervisor with $L_m(\mathcal S/\mathcal G) = K$ exists iff $K$ is controllable; one with $L_c(\mathcal S/\mathcal G) = K$ exists iff $K$ is controllable and $L_m(\mathcal G)$ -closed.
Proposition 7.1: $\mathbf C_{\mathcal G}(L)$ and $\mathbf F_{\mathcal G}(L)$ contain $\emptyset$ and are closed under arbitrary unions.
The supremal elements (p. 218): $\sup \mathbf C_{\mathcal G}(L)$ , $\sup \mathbf F_{\mathcal G}(L)$ and $\sup\{\mathbf C_{\mathcal G}(L) \cap \mathbf F_{\mathcal G}(L)\}$ belong to their classes.

Significance

Theorem 7.1 reduces the existence of a correct, non-blocking controller to a single language inclusion, and identifies the supremal controllable sublanguage as the behaviour of the least restrictive solution. That object is the backbone of the later theory: modular and decentralized control, control under partial observation, and the computational results that $\sup \mathbf C_{\mathcal G}(L)$ is regular and computable when $\mathcal G$ is finite and $L$ regular all start from it.

The result is proved in the paper and has been taught for decades; it is not open. Mathlib has no model of generators with partial transitions, supervisors or controllability (its DFA has a total transition function and a single accepted language), and no formalization of this theory exists on the platform. This mission provides one: a reusable Lean model of generators with partial transitions, supervisors with possibly infinite state, closed loops and controllability, together with the paper's existence theorems stated against it. A second mission on the same paper (quotients of supervisors, Theorem 10.1) builds on the same objects.

Difficulty

The combinatorial core of Proposition 7.1 is a short prefix-closure computation. The work lies in the constructions: to show existence, a supervisor must be built for an arbitrary controllable language, which in general is not regular, so the supervisor needs an infinite state set (for example strings of the target language) together with a proof that the closed loop generates exactly the intended language, is complete, and is proper. The converse directions require relating the closed-loop run to separate runs of the plant and of the supervisor's automaton. The naive shortcut of reading the "sup" as an arbitrary member of $\mathbf C_{\mathcal G}(L_g)$ containing $L_a$ skips the content of the supremal-element milestone; the goal is stated with the actual union.

Formalization scope

The alphabet is a type α with [Fintype α]; strings are List α, the empty string is [], and $s\sigma$ is s ++ [σ]. Languages are Set (List α); the closure is pre K = {s | ∃ t, s ++ t ∈ K}.
A generator is a structure with a state type Q : Type, a partial transition δ : α → Q → Option Q, an initial state and a marker set. No finiteness is assumed on states, of the plant or of the supervisor. Supervisors and generators live in Type 1.
$\phi$ maps states to Ec → Bool; an event outside $\Sigma_c$ is enabled by definition, so uncontrollable events cannot be disabled.
The closed loop is the product run from $(x_0, q_0)$ ; the accessible part in the paper's display (2.1) changes no language and is not built.
Standing assumptions carried by every theorem: $\Sigma$ finite, $L(\mathcal G) = \bar L_m(\mathcal G)$ , supervisor automata accessible (as a hypothesis on every input supervisor and a conjunct of every "there exists a supervisor").
$\sup$ is sSup in the complete lattice Set (List α).
A formalization in which the closed loop ignores $\phi$ or the plant, in which completeness is dropped from properness, or in which the supervisor is restricted to finitely many states, is not the paper's theorem and is ruled out by the definitions above.

Welcome contributions: the basic run lemmas (closed-loop runs project to plant and supervisor runs), the string-state supervisor construction, and proofs of the milestones in the given order.

Selected references

P. J. Ramadge and W. M. Wonham, Supervisory Control of a Class of Discrete Event Processes, SIAM J. Control Optim. 25(1):206–230, 1987. https://doi.org/10.1137/0325013
W. M. Wonham and P. J. Ramadge, On the Supremal Controllable Sublanguage of a Given Language, SIAM J. Control Optim. 25(3):637–659, 1987. https://doi.org/10.1137/0325036
C. G. Cassandras and S. Lafortune, Introduction to Discrete Event Systems, 2nd ed., Springer, 2008. https://doi.org/10.1007/978-0-387-68612-7
W. M. Wonham and K. Cai, Supervisory Control of Discrete-Event Systems, Springer, 2019. https://doi.org/10.1007/978-3-319-77452-7

12 thms3 active usersReviewed

Completed

Combinatorics Operations Research Optimization·Captain: mikedeng1

Approximation Algorithms for Combinatorial Problems V: The Overlap-Ratio Greedy C2 Is Within 1 + ln k of the Least-Overlap Cover on EC(k)Research Paper

Motivation

David S. Johnson's 1974 paper Approximation Algorithms for Combinatorial Problems (J. Comput. System Sci. 9 (1974) 256–278) was one of the first systematic worst-case analyses of polynomial-time heuristics for NP-complete optimization problems. Its Section 5 proves the harmonic bound $\sum_{j=1}^k 1/j$ for the greedy algorithm on minimum-cardinality set cover, a result that still underlies the standard $\ln n$ approximation guarantee.

Section 6, the subject of this mission, asks what happens when the cost of a cover is its total size rather than its number of sets. This problem, SET COVERING II (EC), is the optimization version of the EXACT COVER recognition problem of Karp's list (Karp 1972): a family has a disjoint subcover exactly when the optimum equals the number of covered points. Johnson shows that the change of measure breaks the cardinality greedy but that a greedy rule based on an overlap ratio recovers essentially the same guarantee. The same accounting (paying for each newly covered point) later became the standard analysis of greedy weighted set cover (Chvátal 1979).

Setting

An input is a finite family $F = \{S_1, \dots, S_p\}$ of finite sets. Its covered set is $T = \bigcup_{S \in F} S$ . A subcover is a subfamily $F' \subseteq F$ with $\bigcup_{S\in F'} S = T$ , and its measure is

m_{EC}(F') = \sum_{S \in F'} |S|.

The optimum $F^*$ is the least measure of a subcover; since every subcover has measure at least $|T|$ , an optimal subcover is one with the least possible overlapping. The subproblem EC $(k)$ admits only families in which every set has at most $k$ points.

Algorithm C2 keeps a subfamily SUB (initially empty), the unused sets LEFT (initially $F$ ) and the uncovered points UNCOV (initially $T$ ). While UNCOV is nonempty it chooses $S' \in$ LEFT minimizing

\mathrm{Ratio}(S) = \frac{|S - \mathrm{UNCOV}|}{|S \cap \mathrm{UNCOV}|},

the number of already-covered points of $S$ per newly covered point, and moves $S'$ from LEFT to SUB, removing its points from UNCOV. When several sets tie, any of them may be chosen; a subcover is choosable by C2 if some sequence of admissible choices returns it.

The overlap of a chosen set is $|S' - \mathrm{UNCOV}|$ at the moment it is chosen, and the cumulative overlap $\mathrm{OV}(F_1)$ of a run returning $F_1$ is the sum of these overlaps.

Formalization targets

Goal: Theorem 6 (p. 271)

For all $k \ge 1$ and $n > 0$ ,

R[C2, EC(k)](n) \le 1 + \ln(k) \le \sum_{j=1}^k \frac1j + \frac12,

and for all sufficiently large $n$ , $R[C2, EC(k)](n) \ge \sum_{j=1}^k (1/j)$ . In the size-free form used here, for every $k \ge 1$ :

every subcover $M$ choosable by C2 on an input of EC $(k)$ satisfies $m_{EC}(M) \le (1 + \ln k)\,F^*$ ;
$1 + \ln k \le \sum_{j=1}^k 1/j + 1/2$ ;
some input of EC $(k)$ with $F^* > 0$ has a choosable subcover with $m_{EC}(M) \ge \big(\sum_{j=1}^k 1/j\big) F^*$ .

Milestones (proof of Theorem 6, pp. 271–272)

the measure of the output is $|T| + \mathrm{OV}(F_1)$ ;
if C2 may choose a set with $\mathrm{Ratio}(S') \ge y$ , then $(y+1)\,|\mathrm{UNCOV}| \le F^*$ ;
with $a = F^*/|T|$ and $x = |T - \mathrm{UNCOV}|/|T|$ , the next chosen set has $\mathrm{Ratio}(S') \le a/(1-x) - 1$ ;
on EC $(k)$ , $\mathrm{OV}(F_1) \le |T|\,(a[\ln(k) + 1] - 1)$ ;
the analytic inequality $1 + \ln(k) \le \sum_{j=1}^k 1/j + 1/2$ ;
the lower-bound input (Fig. 1 of the paper with every set of $F_1$ filled out to exactly $k$ points) on which C2 may pay $\sum_{j=1}^k 1/j$ times the optimum.

Significance

The result. The measure $\sum|S|$ penalizes overlap, and the paper notes (without proof, p. 270) that an algorithm returning an optimal cover for the cardinality measure can be a factor $k$ from optimal for this one. Theorem 6 shows that the ratio rule C2 is within $1 + \ln k$ of the least-overlap cover, and the lower bound shows that no analysis of C2 can beat $\sum_{j=1}^k 1/j$ . The two bounds differ by less than $1/2$ for every $k$ . The theorem was an early instance of a logarithmic guarantee for a weighted covering problem, where each set's cost is its size.

Formalizing it. The theorem has been proved since 1974; no machine-checked proof is known to exist. The mission produces a formal model of the EC problem and of C2 as a nondeterministic process, the overlap identity, and the discrete form of the paper's area-under-a-curve estimate. The last is the part the paper argues informally, through a step function and an integral.

Difficulty

The cardinality argument for C1 counts the sets chosen; here the sets have different sizes, so it does not apply. The overlap C2 pays per newly covered point is not bounded by a constant: early choices can be free and late ones cost up to $k-1$ per point, and the bound on the cumulative overlap must hold against the whole run, for every sequence of tie-breaks.

In a formal proof the integral must be replaced by a sum. Covered points arrive in blocks (one block per chosen set), the charge is constant on a block but the bound depends on the covered fraction at the start of the block, and the sum has to be compared with a logarithm. The terms $a\ln a$ and $a/k$ that the paper drops using $1 \le a \le k$ must be controlled as well, and the relation $1 \le a \le k$ must itself be proved from optimality. The lower bound needs an explicit run of C2 through ties on an input with $k \cdot k!$ points, checking at every stage that the intended set is a ratio minimizer.

Formalization scope

Inputs. A family is p : ℕ with S : Fin p → Finset α (0-based, repetitions allowed; a repeated set counts twice in the measure if both copies are chosen, which C2 never does). Subcovers and SUB, LEFT are index sets. $F^*$ is a minimum over the finite, nonempty set of subcovers (Finset.inf'), never a junk value.
Algorithm. C2 is a step relation on states (SUB, LEFT, UNCOV). The choice at Step 3 is existential over all minimizers, so every result quantifies over every choosable output (the paper's WORST). $\mathrm{Ratio}(S)$ is $+\infty$ when $S \cap \mathrm{UNCOV} = \emptyset$ ; the formal rule requires the chosen set to meet UNCOV and compares ratios by cross-multiplication, with no division.
Overlap. The cumulative overlap depends on the run, not on the output alone, so it is carried by an inductive run relation RunOV.
No problem size. The paper's $R[A, P](n)$ maximizes over inputs of size at most $n$ in an unspecified encoding. Upper bounds are stated for every input and every choosable output; the lower bound exhibits one input and one choosable output. Given monotonicity of $R$ in $n$ , these are equivalent to the paper's claims. Ratios are stated multiplicatively, so $F^* = 0$ does not create a vacuous bound.
Numbers. Measures are natural numbers cast to $\mathbb R$ ; $\ln$ is Real.log; $\sum_{j=1}^k 1/j$ is Mathlib's harmonic k.
Ruled out. A deterministic tie-break would prove a weaker upper bound and could not realize the lower-bound run, and a ratio with $x/0 = 0$ would make disjoint-from-UNCOV sets the most attractive choice. The formalization uses neither.

The overlap identity and the discrete integral comparison are reusable for any greedy covering analysis that charges cost per newly covered point. Contributions welcome include proofs of the milestones, the invariants of the C2 run relation (SUB and LEFT partition the indices; UNCOV $= T - \bigcup$ SUB), and the explicit lower-bound run.

Selected references

D. S. Johnson, Approximation algorithms for combinatorial problems, J. Comput. System Sci. 9 (1974), 256–278. https://doi.org/10.1016/S0022-0000(74)80044-9
R. M. Karp, Reducibility among combinatorial problems, in Complexity of Computer Computations, Plenum, 1972, 85–103. https://doi.org/10.1007/978-1-4684-2001-2_9
V. Chvátal, A greedy heuristic for the set-covering problem, Math. Oper. Res. 4 (1979), 233–235. https://doi.org/10.1287/moor.4.3.233

10 thms3 active usersReviewed

Completed

Combinatorics Linear algebra·Captain: mikedeng1

Sparse Approximate Solutions to Linear Systems 2: An Exact Cover by 3-Sets Exists iff Its Incidence System Has a 1/2-Approximate Solution with at Most m/3 NonzerosResearch Paper

Motivation

Many problems in signal processing, statistics and function interpolation ask for a solution of a linear system $Ax\approx b$ that uses as few columns of $A$ as possible: a sparse approximate solution. Natarajan's 1995 paper Sparse Approximate Solutions to Linear Systems (SIAM J. Comput. 24(2):227–234) was motivated by radial basis interpolation, where each column corresponds to a basis function and fewer columns mean a cheaper interpolant. The paper does two things. It proves that finding the sparsest approximate solution is computationally hard (§2, Theorem 1), and it analyses a greedy column-selection algorithm whose number of chosen columns is within a factor, depending on the conditioning of $A$ , of the optimum (§3, Theorem 2; a separate mission of this series).

The hardness theorem is the reason the second half of the paper exists: once exact minimization is ruled out, one settles for approximation guarantees. It is cited throughout the compressed-sensing literature as the canonical statement that $\ell_0$ -minimization under an $\ell_2$ error constraint is NP-hard, and is the starting point for the later theory of when convex relaxations recover sparse solutions.

The argument follows the classical reduction from Exact Cover by 3-sets (X3C) to minimum-weight solutions of linear systems in Garey and Johnson (1979), pp. 221 and 246, adapted to an approximate right-hand side.

Setting

Sparse approximate solution (SAS). Given a matrix $A\in\mathbb R^{m\times n}$ , a vector $b\in\mathbb R^m$ and a tolerance $\varepsilon>0$ , find a vector $x\in\mathbb R^n$ with $\|Ax-b\|_2\le\varepsilon$ whose number of nonzero entries, written $\|x\|_0=|\{j : x_j\neq0\}|$ , is as small as possible. Here $\|\cdot\|_2$ is the Euclidean norm.

Exact Cover by 3-sets (X3C). An instance is a ground set $S=\{s_1,\dots,s_m\}$ and a list $C=c_1,\dots,c_n$ of subsets of $S$ , each with exactly three elements. An exact cover is a sub-collection $\hat C=\{c_j : j\in J\}$ , $J\subseteq\{1,\dots,n\}$ , such that every element of $S$ occurs in exactly one set of $\hat C$ .

The transformation. From an X3C instance build the SAS instance with

the incidence matrix $A\in\mathbb R^{m\times n}$ : $A_{ij}=1$ if $s_i\in c_j$ and $A_{ij}=0$ otherwise, so column $j$ is the characteristic vector of $c_j$ ;
the all-ones vector $b=(1,1,\dots,1)\in\mathbb R^m$ ;
the tolerance $\varepsilon=\tfrac12$ .

In Lean, $S$ is Fin m, the collection is C : Fin n → Finset (Fin m) with hC : ∀ j, (C j).card = 3, an exact cover is an index set J with IsExactCover C J, the matrix is incidence C, the vector $b$ is onesVec m, $Ax$ is Matrix.toEuclideanLin (incidence C) x, and $\|x\|_0$ is nnz x.

Formalization targets

Goal: correctness of the reduction

For every X3C instance $(S,C)$ as above,

\bigl(\exists J,\ \{c_j\}_{j\in J}\text{ is an exact cover of }S\bigr)\iff\bigl(\exists x\in\mathbb R^n,\ \|Ax-b\|_2\le\tfrac12\ \text{and}\ 3\,\|x\|_0\le m\bigr).

This is the sentence the proof of Theorem 1 (p. 228) establishes: "the constructed instance of SAS has a solution with $m/3$ or fewer entries if and only if the given instance of X3C has a solution."

Milestones

Forward direction. If $\{c_j\}_{j\in J}$ is an exact cover, the indicator vector $x=\mathbf 1_J$ satisfies $Ax=b$ and $3\|x\|_0=m$ .
Entry bounds. For every $x$ with $\|Ax-b\|_2\le\frac12$ , each entry of $Ax$ lies in $[\frac12,\frac32]$ .
Lower bound on sparsity. For every such $x$ , $m\le3\|x\|_0$ .
Exact cover from a sparse solution. If moreover $3\|x\|_0\le m$ , the sets $c_j$ with $x_j\neq0$ form an exact cover.

Significance

The result. The equivalence shows that deciding whether a sparse approximate solution with a prescribed number of nonzeros exists is at least as hard as X3C, which is NP-complete. Consequently no polynomial-time algorithm computes the optimum of SAS unless P = NP, and approximation algorithms such as the greedy method of §3 are the natural object of study. The same instance shows hardness persists for 0/1 matrices, a right-hand side of all ones and a constant tolerance, so the difficulty does not come from ill-conditioned data or from vanishing precision.

Formalizing it. The reduction is proved in the paper; this mission produces a machine-checked proof of its correctness, the combinatorial core of every NP-hardness claim for $\ell_0$ -constrained least squares. No prior machine-checked version is known to exist, on the platform or elsewhere. The complexity-theoretic wrapper is out of scope (see below).

Difficulty

The forward direction is a direct computation. The converse contains the only real step, which the paper passes over with "it is clear". From $\|Ax-b\|_2\le\frac12$ one gets only that every entry of $Ax$ is in $[\frac12,\frac32]$ ; the entries of $x$ themselves are arbitrary reals, possibly negative or not equal to $1$ , so $x$ need not be an indicator vector and $Ax=b$ need not hold. The exact-cover property must therefore be extracted from support sizes alone: every element is covered by some column in the support, the support has at most $m/3$ columns of three elements each, and a counting argument forces the chosen sets to be pairwise disjoint. Reading off a cover from the values of $x$ (for instance, taking the $j$ with $x_j=1$ ) does not work.

Formalization scope

Vectors live in EuclideanSpace ℝ (Fin m) and EuclideanSpace ℝ (Fin n), so ‖·‖ is the paper's $\|\cdot\|_2$ . Using the sup norm of Fin m → ℝ would give a different statement.
The tolerance is exactly $\varepsilon=\frac12$ , as printed.
The collection is indexed, C : Fin n → Finset (Fin m): repeated sets are allowed and are distinct indices; an exact cover is a set of indices, and on the SAS side one nonzero entry is counted per index, so both sides treat duplicates consistently.
" $m/3$ or fewer" is written $3\|x\|_0\le m$ , never with natural-number division. With this form the equivalence holds for every $m$ (both sides are false when $3\nmid m$ ), which absorbs the paper's "without loss of generality $m$ is a multiple of 3"; no divisibility hypothesis is assumed. For $m=0$ both sides are true.
The hypothesis that every set has exactly three elements is essential for the converse (with $m=9$ , $O=\{s_3,\dots,s_9\}$ , $c_1=\{s_1\}\cup O$ , $c_2=\{s_2\}\cup O$ , $c_3=O$ , the vector $x=(1,1,-1)$ solves $Ax=b$ with $3\|x\|_0=m$ , yet $C$ has no exact cover since $c_1$ and $c_2$ must both be chosen) and is kept as hC.
Not formalized: the infinite-precision RAM machine model, polynomial-time many-one reductions, polynomial-time computability of the transformation (evident: an $m\times n$ 0/1 matrix), and the NP-completeness of X3C (cited by the paper from Garey–Johnson). The goal is therefore the correctness of the transformation, not a statement titled "SAS is NP-hard". A statement that only records the forward direction, or that fixes $x$ to be a 0/1 vector on the SAS side, would trivialize the converse and is not the target.
Tools a solver will need are in Mathlib: coordinate bounds for the Euclidean norm (PiLp.norm_apply_le), Finset.card_biUnion_le, and Finset.card_biUnion for disjoint unions. Contributions of a reusable exact-cover API, or of a polynomial-time reduction framework that could later wrap this equivalence into an NP-hardness theorem, are welcome.

Selected references

B. K. Natarajan, Sparse Approximate Solutions to Linear Systems, SIAM Journal on Computing 24(2):227–234, 1995. https://doi.org/10.1137/s0097539792240406
M. R. Garey and D. S. Johnson, Computers and Intractability: A Guide to the Theory of NP-Completeness, W. H. Freeman, 1979 (X3C: problem [SP2], p. 221; minimum weight solution to linear equations: [MP5], p. 246).
F. P. Preparata and M. I. Shamos, Computational Geometry: An Introduction, Springer, 1985 (the real RAM model). https://doi.org/10.1007/978-1-4612-1098-6

6 thms3 active usersReviewed

Completed

Combinatorics Graph Theory Number Theory·Captain: mikedeng1

Fast Algorithms for Finding Nearest Common Ancestors II: Nearest Common Ancestors in a Complete Binary Tree by Symmetric-Order ArithmeticResearch Paper

Motivation

The nearest common ancestor (nca) problem asks, for a fixed rooted tree and a sequence of vertex pairs $(v, w)$ , for the deepest vertex that is an ancestor of both. It is a basic step in suffix-tree string algorithms and is equivalent to range-minimum queries (Bender, Farach-Colton, 2000). Harel and Tarjan, Fast Algorithms for Finding Nearest Common Ancestors, SIAM J. Comput. 13 (1984) 338–355, gave the first algorithm answering each query on a static tree in constant time on a random-access machine after linear preprocessing.

Their construction reduces the general problem to the case of a complete binary tree, where §3 of the paper shows that nca queries can be answered "by direct calculation" on vertex numbers: multiplication, division, powers of two, the base-two logarithm and bitwise exclusive or. The later simplification of Schieber and Vishkin (1988) is built on the same in-order numbering of a complete binary tree. This mission formalizes that arithmetic core.

Timeline, as reviewed in the paper's §1 (pp. 338–340):

1976: Aho, Hopcroft and Ullman (SIAM J. Comput. 5) give an $O(n + m\alpha(m+n, n))$ -time off-line algorithm on a pointer machine, and for static trees a random-access algorithm with $O(n \log\log n)$ preprocessing and $O(\log\log n)$ time per query.
1976: van Leeuwen (unpublished report) gives an $O(n + m \log\log n)$ -time algorithm for linking roots and static trees that runs on a pointer machine in $O(n)$ space.
1980: Harel (Proc. 21st FOCS) gives a preliminary version of the paper's results.
1984: Harel and Tarjan prove that pointer machines need $\Omega(\log\log n)$ time per query on static trees (Theorem 1), and give the $O(n)$ -preprocessing, $O(1)$ -query random-access algorithm whose base case is the subject of this mission.

Setting

Fix $d \ge 0$ and let $T$ be the complete binary tree of depth $d$ . A vertex is identified with the path from the root to it, a word of at most $d$ left or right turns; the root is the empty word and $T$ has $n = 2^{d+1} - 1$ vertices. Following the paper's Appendix (pp. 354–355):

$w$ is an ancestor of $v$ ( $v$ a descendant of $w$ ) if the word $w$ is a prefix of the word $v$ ; every vertex is its own ancestor. $v$ and $w$ are unrelated if neither is an ancestor of the other.
The depth of $v$ is its distance to the root; its height $h(v)$ is the length of the longest path from a leaf to $v$ , which in $T$ is $d - \operatorname{depth}(v)$ .
$\operatorname{nca}(v, w)$ is the vertex of greatest depth that is an ancestor of both: the longest common prefix.

The vertices of $T$ are numbered from $1$ to $n$ in symmetric order (in-order): at every vertex, first the left subtree, then the vertex, then the right subtree. $\mathrm{sym}(v)$ is the number of $v$ and $\mathrm{sym}^{-1}(i)$ the vertex numbered $i$ . For $d = 4$ (Fig. 1 of the paper) the root is $16$ , its children $8$ and $24$ , and the leaves $1, 3, 5, \dots, 31$ . $i \oplus j$ denotes bitwise exclusive or and $\lg$ the base-two logarithm.

Two procedures of §3 use only numbers, heights and $d$ :

the nca depth algorithm: return $d - h(v)$ if $\mathrm{sym}(w) \in [\mathrm{sym}(v) - 2^{h(v)} + 1, \mathrm{sym}(v) + 2^{h(v)} - 1]$ ; else $d - h(w)$ if the same holds with $v, w$ exchanged; else $d - \lfloor \lg(\mathrm{sym}(v) \oplus \mathrm{sym}(w)) \rfloor$ ;
the depth algorithm: given $v$ and a depth $d_2 \le \operatorname{depth}(v)$ , with $h = d - d_2$ , return $\mathrm{sym}^{-1}\bigl(2^{h+1}\lfloor \mathrm{sym}(v)/2^{h+1}\rfloor + 2^h\bigr)$ .

Formalization targets

Goal: the nca algorithm is correct

The algorithm to compute $\operatorname{nca}(v,w)$ (p. 342) runs the nca depth algorithm to obtain $d_0$ and then the depth algorithm on $(v, d_0)$ . The goal states that it returns the nearest common ancestor: for all vertices $v, w$ of $T$ , with $d_0$ the output of the nca depth algorithm and $h = d - d_0$ ,

\mathrm{sym}(\operatorname{nca}(v,w)) = 2^{h+1}\left\lfloor \frac{\mathrm{sym}(v)}{2^{h+1}} \right\rfloor + 2^h .

Milestones

In the order the paper uses them:

Numbers at height $h$ (p. 341): the vertices of height $h$ are numbered $2^h, 3\cdot 2^h, 5\cdot 2^h, \dots$ from left to right.
Lemma 1: $h(v)$ is the largest $h$ with $2^h \mid \mathrm{sym}(v)$ .
Lemma 2: the descendants of $v$ are the vertices numbered in $[\mathrm{sym}(v) - 2^{h(v)} + 1, \mathrm{sym}(v) + 2^{h(v)} - 1]$ .
Lemma 3: for a height $h \ge h(v)$ , the height- $h$ ancestor of $v$ has number $2^{h+1}\lfloor \mathrm{sym}(v)/2^{h+1}\rfloor + 2^h$ .
Lemma 4: for unrelated $v, w$ ,

h(\operatorname{nca}(v,w)) = \lfloor \lg(\mathrm{sym}(v) \oplus \mathrm{sym}(w)) \rfloor .

The nca depth algorithm returns $\operatorname{depth}(\operatorname{nca}(v,w))$ .
The depth algorithm returns the number of the depth- $d_2$ ancestor of $v$ .

Two supporting statements pin the definitions to the paper: $\mathrm{sym}$ is a bijection onto $\{1, \dots, 2^{d+1} - 1\}$ , and the longest common prefix is the deepest common ancestor.

Significance

The constant-time nca computation on complete binary trees is the base case of the whole paper: §§4–5 embed an arbitrary tree into a moderately sized complete binary tree through a compressed tree and a balanced binary tree, and every query ends with the arithmetic of §3. The same idea, that in-order numbers encode ancestry in their low-order bits, underlies the Schieber–Vishkin algorithm. Lemma 1 identifies the height with the 2-adic valuation of the number, and Lemma 4 identifies the nca height with the position of the highest differing bit.

The results are proved in the paper, with the proofs left as "easy to verify". No machine-checked version of this numbering or of these four lemmas is known to exist in Mathlib or on this platform. A formal development supplies proofs of the four lemmas and the two algorithms, and a reusable library connecting in-order ranks of a complete binary tree to binary arithmetic (Nat.log, bitwise xor, 2-adic valuation).

Difficulty

The numbering is defined by a traversal order, while the lemmas speak about divisibility, floor division and exclusive or. The work lies in connecting the rank of a vertex in symmetric order to its closed form $(2j+1)\cdot 2^{h(v)}$ , where $j$ is its left-to-right position. That counting argument sums the sizes of the subtrees that precede $v$ and is where most of the effort goes. Lemma 4 then needs the observation that two unrelated numbers agree in all bits above the height of their nca and differ in the bit at that height. This is a statement about Nat.testBit of the exclusive or, and it fails for related vertices. The algorithm statements add a case analysis whose first two cases overlap when $v = w$ .

Formalization scope

A vertex of the tree of depth $d$ is a List Bool of length at most $d$ (false = left). Ancestry is the prefix relation, $\operatorname{nca}$ the longest common prefix, depth the length, and height $d - \text{length}$ . None of these structural notions uses the numbering.
$\mathrm{sym}(v)$ is the number of vertices whose in-order sort key is lexicographically at most that of $v$ . The key is the path with left $\mapsto 0$ , right $\mapsto 2$ , followed by $1$ . The numbering is not defined by the closed form or by a recursion on numbers: a definition of that kind would make the height- $h$ numbering and Lemma 1 immediate and move the content of the mission into an uncheckable definition.
$\lfloor \lg x \rfloor$ is Nat.log 2 x, which agrees for $x \ge 1$ . $\oplus$ is ^^^ on $\mathbb N$ , and floor division is / on $\mathbb N$ .
Interval tests $a \in [b - c + 1, b + c - 1]$ are written additively as $b + 1 \le a + c$ and $a + 1 \le b + c$ . The subtractions $d - h(v)$ and $d - d_2$ never truncate for heights and depths of vertices.
Lemma 3 states explicitly that $h \le d$ (" $h$ is a height") and that the ancestor exists. The depth algorithm assumes $d_2 \le \operatorname{depth}(v)$ , as printed.
$\mathrm{sym}^{-1}$ is not defined as a function. The goal and the depth algorithm state that a vertex has the computed number if and only if it is the nearest common ancestor (respectively the ancestor at depth $d_2$ ), which says that $\mathrm{sym}^{-1}$ of that number is that vertex.
The $O(1)$ time bounds are not formalized, since the random-access machine model is out of scope.

Proofs of any milestone are welcome.

Selected references

D. Harel and R. E. Tarjan, Fast Algorithms for Finding Nearest Common Ancestors, SIAM J. Comput. 13(2) (1984), 338–355. https://doi.org/10.1137/0213024
A. V. Aho, J. E. Hopcroft and J. D. Ullman, On Finding Lowest Common Ancestors in Trees, SIAM J. Comput. 5(1) (1976), 115–132. https://doi.org/10.1137/0205011
B. Schieber and U. Vishkin, On Finding Lowest Common Ancestors: Simplification and Parallelization, SIAM J. Comput. 17(6) (1988), 1253–1262. https://doi.org/10.1137/0217079
M. A. Bender and M. Farach-Colton, The LCA Problem Revisited, LATIN 2000, LNCS 1776, 88–94. https://doi.org/10.1007/10719839_9

11 thms3 active usersReviewed

Completed

Combinatorics Complexity Theory·Captain: mikedeng1

Fast Algorithms for Finding Nearest Common Ancestors I: A Lower Bound for Pointer MachinesResearch Paper

Motivation

The nearest common ancestor problem asks, for a rooted tree and two of its vertices $x$ and $y$ , for the deepest vertex that is an ancestor of both, written $\operatorname{nca}(x,y)$ . It appears as a subroutine in string algorithms (suffix trees), in graph algorithms (path queries, dominators) and in the analysis of set-union structures. Aho, Hopcroft and Ullman (On finding lowest common ancestors in trees, SIAM J. Comput. 5, 1976) posed it in several versions, differing in how much the tree changes while the queries are answered.

Harel and Tarjan (Fast Algorithms for Finding Nearest Common Ancestors, SIAM J. Comput. 13, 1984) study how the answer depends on the machine model. On a random-access machine, where addresses can be computed arithmetically, they preprocess a static tree in linear time and then answer each query in constant time. On a pointer machine, where memory can only be traversed by following pointers, their §2 shows that no representation of the tree allows constant-time queries: $\Omega(\log\log n)$ steps are needed in the worst case. This mission formalizes that lower bound.

Timeline.

1976: Aho, Hopcroft and Ullman give an $O(\log\log n)$ -per-query random-access algorithm for static trees.
1976: van Leeuwen (Finding lowest common ancestors in less than logarithmic time, unpublished report, reference [14] of Harel–Tarjan) gives an $O(n + m\log\log n)$ algorithm for static trees that runs on a pointer machine.
1984: Harel and Tarjan prove Theorem 1, the matching $\Omega(\log\log n)$ lower bound for pointer machines, and the $O(1)$ -per-query random-access algorithm.

Setting

A pointer machine stores its data as a collection of nodes. Each node has a fixed number of fields, and a pointer field holds either a node or nil. The machine can follow a pointer from a node it holds, but it cannot compute an address. Following Harel and Tarjan (p. 340), a static tree is represented by a list structure: each tree vertex $v$ is represented by a single node $\mathrm{rep}(v)$ , distinct vertices by distinct nodes, and the structure may contain further nodes that represent no vertex. Each node has two pointer fields; the paper reduces any fixed number of pointers to two "without loss of generality". To answer a query on $x$ and $y$ , the machine is given pointers to $\mathrm{rep}(x)$ and $\mathrm{rep}(y)$ and must return a pointer to $\mathrm{rep}(\operatorname{nca}(x,y))$ .

The node $b$ is accessible from $a$ in $j$ steps or less if it can be reached from $a$ by following at most $j$ pointers. Write $\mathrm{acc}_j(a)$ for the set of such nodes. A run of $t$ steps from input nodes $a$ and $b$ is a sequence $n_1,\dots,n_t$ in which each $n_s$ is the content of a pointer field of a node among $a, b, n_1, \dots, n_{s-1}$ . A query with answer $c$ is answered in $k$ steps if some run of at most $k$ steps holds $c$ .

The tree is the complete binary tree $T$ of height $h$ , with $n = 2^h$ leaves. Its vertices are the words $w \in \{0,1\}^{\le h}$ (the root-to-vertex path, $0$ = left), the ancestors of $v$ are its prefixes, the depth of $w$ is $|w|$ and its height is $h - |w|$ . Then $\operatorname{nca}(x,y)$ is the longest common prefix of $x$ and $y$ . Logarithms are binary: $\lg = \log_2$ .

Formalization targets

Goal: Theorem 1 in the explicit form of its proof

For every $h$ , every node type, every list structure with two pointers per node and every injective representation $\mathrm{rep}$ of the complete binary tree with $n = 2^h$ leaves: if every nca query on two leaves is answered in $k$ steps, then

k > \lg\lg n - 2 .

This is the last display of the proof (p. 341), which is what the paper's $\Omega(\log\log n)$ means. The representation is arbitrary and is quantified before the query bound, so the bound holds for every representation.

Milestones: the claims of the proof

A query answered in $k$ steps reaches only nodes in $\mathrm{acc}_k(\mathrm{rep}(x)) \cup \mathrm{acc}_k(\mathrm{rep}(y))$ .
$|\mathrm{acc}_j(a)| \le 2^{j+1} - 1$ for every node $a$ .
With $A_x$ the set of vertices whose nodes are accessible from $\mathrm{rep}(x)$ in $k$ steps or less: for a nonleaf $w$ with children $u, v$ , either $w \in A_x$ for every leaf $x$ below $u$ , or $w \in A_y$ for every leaf $y$ below $v$ .
A vertex of height $i \ge 1$ lies in $A_x$ for at least $2^{i-1}$ leaves $x$ .

\sum_{x \in L} |A_x| \ge \frac{n}{2}\lg n,

where $L$ is the set of leaves.

Significance

The result. Theorem 1 shows that van Leeuwen's pointer-machine algorithm for static trees is optimal up to a constant factor, and that the constant-time queries of the paper's §§3–5 depend on address arithmetic. It is an early nontrivial lower bound for pointer machines on a natural problem; the paper compares it with Tarjan's lower bound for disjoint-set union on a pointer machine (J. Comput. System Sci. 18, 1979).

Formalizing it. The theorem is proved in the paper; as far as could be determined no machine-checked version exists, and Mathlib has no pointer-machine model. The mission produces an explicit, reusable definition of pointer-machine runs and accessibility together with a complete proof of the explicit bound. A formal model of this kind is the precondition for stating any other pointer-machine lower bound.

Difficulty

The statement must hold for every representation, including structures with many auxiliary nodes and arbitrary pointers between tree nodes. Arguing about one natural representation, such as parent pointers, where a leaf is far from its ancestors, says nothing about other representations: a structure with shortcut pointers or auxiliary nodes may bring some ancestors close to some leaves, and the bound must survive every such choice. In the formal setting the counting also has to handle overlaps: nodes reachable from several leaves, nodes that represent no vertex, and pointer cycles.

Formalization scope

Model. Nodes form an arbitrary type N, not necessarily finite. ptr : N → Fin 2 → Option N gives the two pointer fields (none = nil), and rep : Vertex h → N is required to be injective. acc ptr j a is defined recursively. Run ptr a b t held is an inductive predicate for runs of $t$ steps, AnsweredIn asks for some run of at most $k$ steps holding the answer, and AnswersLeafQueriesIn ptr rep k requires this for every pair of leaves.
Conventions.
- Two pointer fields per node, as the paper's "without loss of generality" reduction allows; the reduction itself is not formalized.
- Only queries on two leaves are assumed answerable. This is weaker than all queries, so the theorem is at least as strong as the paper's.
- Time is counted as pointer-following steps. Mutation of the structure during a query and non-pointer fields are not modelled: neither lets the machine hold a node it has not reached by following pointers. The clause "the algorithm remembers nothing between queries" is built into the static structure.
- Vertex h is {s : List Bool // s.length ≤ h}, nca is the longest common prefix, and a separate theorem identifies it with the Appendix's deepest common ancestor. $n = 2^h$ counts leaves, not vertices.
- $\lg$ is Real.logb 2. For $h = 0$ Lean's $\log_2 0 = 0$ gives the true statement $k > -2$ ; for $h \ge 1$ , $\lg\lg n = \log_2 h$ .
- Cardinalities in the milestones are Set.encard in $\mathbb N \cup \{\infty\}$ , so finiteness is part of each claim. Divisions are cleared: $h\,2^h \le 2\sum_x |A_x|$ .
Ruling out trivial formalizations. The hypothesis AnswersLeafQueriesIn is satisfiable: the parent-pointer representation answers every leaf query in $h$ steps. If rep were not injective, a constant rep would answer every query in zero steps, so injectivity is kept in the goal. The milestones do not need it and do not assume it.
Infrastructure. The goal needs finite-set counting over the leaves of the complete binary tree and a double count over heights. The run and accessibility definitions are reusable for other pointer-machine arguments. Proofs of the milestones, and of the ℕ form $h < 2^{k+2}$ that the goal reduces to, are welcome.

Selected references

D. Harel, R. E. Tarjan, Fast Algorithms for Finding Nearest Common Ancestors, SIAM J. Comput. 13(2):338–355, 1984. https://doi.org/10.1137/0213024
A. V. Aho, J. E. Hopcroft, J. D. Ullman, On finding lowest common ancestors in trees, SIAM J. Comput. 5(1):115–132, 1976. https://doi.org/10.1137/0205011
A. Schönhage, Storage modification machines, SIAM J. Comput. 9(3):490–508, 1980. https://doi.org/10.1137/0209036
R. E. Tarjan, A class of algorithms which require nonlinear time to maintain disjoint sets, J. Comput. System Sci. 18(2):110–127, 1979. https://doi.org/10.1016/0022-0000(79)90042-4

8 thms3 active usersReviewed

Completed

Graph Theory Operations Research Optimization·Captain: mikedeng1

A New Approach to the Maximum-Flow Problem 2: The Nonsaturating-Push Bound for FIFO Push-RelabelResearch Paper

Motivation

The maximum-flow problem asks how much of a commodity can be sent from a source to a sink through a network whose edges carry capacities. It is a basic model of operations research. Transportation, scheduling, bipartite matching and image segmentation reduce to it, and it is the inner step of many combinatorial algorithms.

Goldberg and Tarjan introduced the push–relabel (preflow) method in A New Approach to the Maximum-Flow Problem (J. ACM 35(4), 1988). Ford–Fulkerson-type algorithms augment along whole source–sink paths. The push–relabel method instead moves excess flow across single edges, guided by integer distance labels on the vertices. Whatever order its local operations are applied in, it is correct and performs $O(n^2 m)$ of them (§3 of the paper). Section 4 shows that one particular order, processing the active vertices first-in, first-out, cuts the dominant term, the number of nonsaturating pushes, to $O(n^3)$ . The method and its FIFO and highest-label variants are the standard practical maximum-flow codes.

Timeline:

1956: Ford and Fulkerson, augmenting paths and max-flow min-cut.
1970–72: Dinic, and Edmonds and Karp, give polynomial augmenting-path bounds.
1974: Karzanov introduces preflows and obtains $O(n^3)$ .
1982: Shiloach and Vishkin give a parallel $O(n^2 \log n)$ preflow algorithm with a first-in, first-out flavour.
1988: Goldberg and Tarjan, the generic push–relabel method, the FIFO bound of this mission, and $O(nm \log(n^2/m))$ with dynamic trees.

Setting

A flow network has a finite vertex set $V$ with $n = |V|$ , a capacity $c(v,w) \ge 0$ on every ordered pair, a source $s$ and a sink $t \neq s$ . The edges are the pairs with $c(v,w) > 0$ , and there are no loops. A preflow is a function $f$ on vertex pairs with $f(v,w) \le c(v,w)$ and $f(v,w) = -f(w,v)$ . Its excess $e(v) = \sum_u f(u,v)$ must be nonnegative at every $v \neq s$ . The residual capacity is $r_f(v,w) = c(v,w) - f(v,w)$ . A labeling $d$ assigns each vertex a value in $\mathbb{N} \cup \{\infty\}$ . A vertex $v \notin \{s,t\}$ is active if $d(v) < \infty$ and $e(v) > 0$ .

The two basic operations (Fig. 1 of the paper) are:

push $(v,w)$ , applicable when $v$ is active, $r_f(v,w) > 0$ and $d(v) = d(w)+1$ . It sends $\delta = \min(e(v), r_f(v,w))$ from $v$ to $w$ . The push is saturating if $r_f(v,w) = 0$ afterwards and nonsaturating otherwise.
relabel $(v)$ , applicable when $v$ is active and $d(v) \le d(w)$ for every residual edge $(v,w)$ . It sets $d(v) \leftarrow \min\{d(w)+1 : r_f(v,w) > 0\}$ .

The algorithm starts by saturating every edge leaving $s$ , with $d(s) = n$ and $d(v) = 0$ for $v \neq s$ .

In the first-in, first-out algorithm (§4), each vertex $v$ scans a fixed list $L(v)$ of its neighbours through a current edge. The push/relabel $(v)$ operation pushes through the current edge if possible. Otherwise it advances the current edge, or, at the end of the list, returns to the first edge and relabels $v$ . Active vertices wait in a queue $Q$ , initially $\{v \in V - \{s,t\} : c(s,v) > 0\}$ . The discharge operation removes the front vertex $v$ and repeats push/relabel $(v)$ until $e(v) = 0$ or $d(v)$ increases. Every vertex that becomes active meanwhile is appended to $Q$ , and $v$ is appended too if it is still active. Passes over the queue are defined inductively. Pass 1 consists of the discharges of the initially queued vertices. Pass $i+1$ consists of the discharges of vertices added during pass $i$ .

Formalization targets

Goal: Corollary 4.4 (p. 931)

For every network, every edge-list order, every initial queue order, and every run of the FIFO algorithm,

\#\{\text{nonsaturating pushes}\} \le 4n^3 .

The constant is the printed one.

Milestones

Lemma 4.1 (p. 929): the push/relabel operation relabels only when relabeling is applicable.
Lemma 3.5 (p. 926): from any vertex with positive excess, the source is reachable in the residual graph.
Lemma 3.7 (p. 927): at any time, $d(v) \le 2n-1$ for every vertex.
Lemma 3.8 (p. 927): at most $2n-1$ relabelings per vertex and at most $(2n-1)(n-2) < 2n^2$ in total.
Lemma 4.3 (p. 930): at most $4n^2$ passes over the queue.

Significance

Corollary 4.4 is the combinatorial core of Theorem 4.5, which states that the FIFO algorithm runs in $O(n^3)$ time. Theorem 4.2 shows that the remaining work of the implementation is $O(nm)$ plus constant time per nonsaturating push. The bound of Corollary 4.4 is therefore what separates the $O(n^3)$ FIFO method from the $O(n^2 m)$ bound of the generic method, which matters on dense networks. The same pass-counting argument is reused for the parallel algorithm of §6 and underlies later analyses of highest-label and wave variants.

The results are proved in the paper. Formalizing them adds an analysis of a push–relabel algorithm, which the platform does not yet have. Its existing network-flow material states max-flow min-cut and Ford–Fulkerson termination in an arc-based model with nonnegative flows (the Introduction to Linear Optimization missions). The mission builds a precise operational model of the FIFO implementation, with edge lists, current edges and a queue carrying pass numbers, and states an explicit operation count for it. A companion mission in this series treats the generic algorithm's correctness and its $(2n-1)(n-2) + 2nm + 4n^2m$ operation bound.

Difficulty

The obvious argument is the potential-function count of §3, over the sum of the labels of active vertices. It yields only $4n^2 m$ and does not use the queue discipline at all. The $4n^3$ bound has to charge nonsaturating pushes to passes over the queue, and then bound the number of passes by the total growth of the labels. Neither step is visible in the generic algorithm, because both depend on the order in which vertices are processed.

Making this rigorous requires invariants of the implementation that the paper uses silently:

a vertex is in the queue exactly when it is active, and at most once;
pass numbers are nondecreasing along the queue;
current edges only move forward between relabelings.

Lemma 4.1 in particular depends on the current-edge scan: an edge passed over earlier stays inadmissible until $v$ is relabeled.

Formalization scope

The Lean development works in namespace GoldbergTarjan.FIFO. Vertices form a type V with [Fintype V] [DecidableEq V], and $n$ is Fintype.card V. Capacities are c : V → V → ℝ with c ≥ 0 and c v v = 0. Flows are antisymmetric real functions on all ordered pairs, not nonnegative arc flows. Excess is computed from the flow. Labels are in ℕ∞, and the empty minimum in relabel is ⊤.

The state of the algorithm consists of the flow, the labels, the current-edge index cur v into the edge list L v, and the queue Q : List (V × ℕ), each entry tagged with its pass number. Push/relabel (Fig. 3) is a total function, and a discharge (Fig. 4) is a relation carrying the number of push/relabel operations it performs. A run consists of the states S 0, …, S K with S 0 the initial state and consecutive states related by one discharge. The printed variant of Fig. 4, which stops as soon as $v$ is relabeled, is the one formalized. Counts are natural numbers over all push/relabel operations of all discharges. The number of passes is the largest pass tag of a discharged entry.

All constants are explicit, exactly as printed:

$2n-1$ (Lemmas 3.7, 3.8);
$(2n-1)(n-2)$ and $2n^2$ (Lemma 3.8);
$4n^2$ (Lemma 4.3);
$4n^3$ (Corollary 4.4).

No asymptotic notation is used, and no $m \ge n-1$ assumption is made.

A model without current edges, where relabeling happens whenever no push applies, would make Lemma 4.1 vacuous and change the algorithm. Pass numbers that are not propagated by the "added during pass $i$ " rule would make the pass count arbitrary. Both are ruled out by the definitions. A sorry-free check, outside the proposal, exhibits a three-vertex network with two legal discharges, two passes and no nonsaturating push, so the run hypotheses are satisfiable.

Reusable beyond this mission are the network, preflow, push and relabel definitions and Lemma 3.5, which is about an arbitrary preflow. Contributions welcome: invariants of FIFO runs (preflow, valid labeling, queue = active set, cur within bounds), proofs of the milestones, and the reduction of Corollary 4.4 to Lemma 4.3.

Selected references

A. V. Goldberg, R. E. Tarjan, A New Approach to the Maximum-Flow Problem, Journal of the ACM 35(4):921–940, 1988. https://doi.org/10.1145/48014.61051
A. V. Karzanov, Determining the maximal flow in a network by the method of preflows, Soviet Math. Doklady 15:434–437, 1974.
Y. Shiloach, U. Vishkin, An O(n² log n) parallel max-flow algorithm, Journal of Algorithms 3(2):128–146, 1982. https://doi.org/10.1016/0196-6774(82)90013-X
L. R. Ford, D. R. Fulkerson, Maximal flow through a network, Canadian Journal of Mathematics 8:399–404, 1956. https://doi.org/10.4153/CJM-1956-045-5
J. Edmonds, R. M. Karp, Theoretical improvements in algorithmic efficiency for network flow problems, Journal of the ACM 19(2):248–264, 1972. https://doi.org/10.1145/321694.321699

10 thms3 active usersReviewed

Completed

Graph Theory Operations Research Optimization·Captain: mikedeng1

A New Approach to the Maximum-Flow Problem 1: The Generic Push-Relabel Algorithm and Its Operation BoundResearch Paper

Motivation

The maximum-flow problem asks how much of a commodity can be sent from a source to a sink through a network whose edges have capacities. It is a basic model in operations research (transportation, scheduling, bipartite matching) and a standard subroutine in combinatorial optimization.

Classical algorithms, from Ford and Fulkerson (1956) through Edmonds–Karp and Dinic (1970–1972) and Karzanov (1974), increase a feasible flow along augmenting paths or blocking flows. Goldberg and Tarjan, A New Approach to the Maximum-Flow Problem (J. ACM 35(4), 1988, doi:10.1145/48014.61051), replaced this global view by a local one: the push-relabel method maintains a preflow, which may violate conservation at intermediate vertices, and moves excess along edges toward vertices with smaller distance labels. The generic method, with the basic operations applied in any order, is the starting point of the FIFO, highest-label and dynamic-tree implementations analysed later in the same paper, and push-relabel codes remain among the fastest practical maximum-flow solvers.

This mission formalizes §2–§3 of the paper: the generic algorithm is correct, and it stops after a number of basic operations bounded by an explicit polynomial in the numbers of vertices and edges, whatever order of operations is chosen.

Setting

A flow network has a finite vertex set $V$ with $n = |V|$ , a source $s$ and a sink $t \ne s$ , and a capacity $c(v,w) \ge 0$ for every ordered pair of vertices, positive exactly on the edges $E = \{(v,w) : c(v,w) > 0\}$ ; $m = |E|$ , and there are no loops, $c(v,v) = 0$ .

Flows are real functions on all vertex pairs. A function $f$ satisfies the capacity constraint if $f(v,w) \le c(v,w)$ and antisymmetry if $f(v,w) = -f(w,v)$ for all pairs. The excess of $v$ is $e(v) = \sum_{u} f(u,v)$ . A flow also has $e(v) = 0$ for $v \notin \{s,t\}$ ; a preflow only $e(v) \ge 0$ for $v \ne s$ . The value of a flow is $|f| = \sum_v f(v,t)$ , and a maximum flow is a flow of maximum value.

The residual capacity is $r_f(v,w) = c(v,w) - f(v,w)$ ; pairs with $r_f(v,w) > 0$ are the edges of the residual graph $G_f$ . A valid labeling is $d : V \to \mathbb{N} \cup \{\infty\}$ with $d(s) = n$ , $d(t) = 0$ and $d(v) \le d(w) + 1$ on every residual edge. A vertex $v$ is active if $v \notin \{s,t\}$ , $d(v) < \infty$ and $e(v) > 0$ .

The two basic operations (Fig. 1 of the paper) are:

Push $(v,w)$ , applicable when $v$ is active, $r_f(v,w) > 0$ and $d(v) = d(w)+1$ : send $\delta = \min(e(v), r_f(v,w))$ , i.e. $f(v,w) \mathrel{+}= \delta$ , $f(w,v) \mathrel{-}= \delta$ . It is saturating if $r_f(v,w) = 0$ afterwards and nonsaturating otherwise.
Relabel $(v)$ , applicable when $v$ is active and $d(v) \le d(w)$ for every residual edge $(v,w)$ : set $d(v) \leftarrow \min\{d(w)+1 : (v,w) \in E_f\}$ ( $\infty$ if there is none).

The generic algorithm (Fig. 2) starts from the preflow that saturates every edge leaving $s$ and is zero elsewhere, with the simple labeling $d(s) = n$ , $d(v) = 0$ otherwise, and applies applicable basic operations in any order while one exists. An execution with $K$ basic operations is a sequence of states $(f_0,d_0),\dots,(f_K,d_K)$ from the initial state, each obtained from the previous one by one applicable operation.

Formalization targets

Goal: Theorems 3.11 and 3.4

Assume the paper's standing assumption $m \ge n-1$ . For every execution with $K$ basic operations,

K \le (2n-1)(n-2) + 2nm + 4n^2 m,

and if no basic operation applies in the final state, then $f_K$ is a maximum flow. The paper states the bound as $O(n^2m)$ and proves it as "immediate from Lemmas 3.8, 3.9, and 3.10"; the goal states the sum of those three printed bounds. Since every execution is this short, no order of operations runs forever.

Milestones

In the order the proof uses them: Lemma 2.1 (at an active vertex a push or a relabel applies); Lemma 3.1 (the labeling stays valid); Theorem 3.2 (Ford–Fulkerson: a flow is maximum iff $t$ is unreachable from $s$ in $G_f$ ); Lemma 3.3 (under a valid labeling $t$ is unreachable from $s$ ); Lemma 3.5 (from any vertex with positive excess, $s$ is reachable); Lemma 3.6 (labels never decrease; a relabeling increases the label); Lemma 3.7 ( $d(v) \le 2n-1$ throughout); Theorem 3.4 (termination with finite labels gives a maximum flow); Lemma 3.8 ( $\le 2n-1$ relabelings per vertex, $\le (2n-1)(n-2) < 2n^2$ in total); Lemma 3.9 ( $\le 2nm$ saturating pushes); Lemma 3.10 ( $\le 4n^2m$ nonsaturating pushes, under $m \ge n-1$ ). A further, non-milestone item states the unnumbered invariant that every $f_k$ is a preflow.

Significance

The generic bound shows that push-relabel terminates in a polynomial number of steps without any rule for choosing the next operation; the specific orderings of §4–§5 of the paper (first-in first-out, $O(n^3)$ ; dynamic trees, $O(nm\log(n^2/m))$ ) refine only the count of nonsaturating pushes, and reuse Lemmas 3.1–3.9 unchanged. The correctness argument, a valid labeling excludes augmenting paths, is the template for the push-relabel minimum-cost flow and assignment algorithms that followed.

These results are proved in the paper and are textbook material. Their machine-checked counterparts are, as far as is known here, not on the Prove2Me platform: the platform's network-flow statements (from Introduction to Linear Optimization, e.g. LinearOptimization.max_flow_min_cut) use a different model, with arc-indexed nonnegative flows and extended-real capacities, and contain nothing about preflows, labels or operation counts. This mission produces a formal account of the antisymmetric-flow model, of Ford–Fulkerson in that model, and of the amortized counting arguments, with the constants the paper prints.

Difficulty

The correctness half is short once the invariants are in place; the difficulty is in the counting. The label bound (Lemma 3.7) is a statement about the whole execution, and it depends on a structural fact about preflows (Lemma 3.5) whose truth rests on antisymmetry and on the nonnegativity of excesses. The obvious first idea for the push counts, bounding pushes per edge or per vertex locally, fails for nonsaturating pushes: flow pushed across a pair can be pushed back later, and nothing local limits how often this happens, so Lemma 3.10 holds only as an amortized statement over the entire execution and depends on both earlier counts. Saturating pushes on a pair can also recur, in both directions, and Lemma 3.9 has to control the interaction between the two directions.

Formally, all of this is reasoning about arbitrary interleavings of operations, with labels in $\mathbb{N} \cup \{\infty\}$ and real-valued flows.

Formalization scope

Vertices form a finite type with decidable equality; $n$ is its cardinality, $s \ne t$ , so $n \ge 2$ and the natural-number subtractions $2n-1$ and $n-2$ are exact. Capacities are a real function on all pairs, nonnegative, zero on the diagonal; $E$ is its support and $m$ its cardinality.
Flows and preflows are antisymmetric real functions on all pairs (not nonnegative arc flows); the excess is computed from $f$ , never stored. A maximum flow is a flow whose value is at least that of every flow.
Labels live in ℕ∞, with $\infty + 1 = \infty$ ; the relabel value is an infimum, which is $\infty$ on the empty set.
An execution is a sequence of states σ : ℕ → State V with a length $K$ , starting at the Fig. 2 state with the simple labeling (the paper's own assumption for its proofs), each step an applicable push or relabel. "Terminates" means that no basic operation applies, the loop guard of Fig. 2. The three counts are cardinalities of the sets of step indices of each kind.
Explicit constants: $2n-1$ per-vertex relabelings, $(2n-1)(n-2) < 2n^2$ total relabelings, $2nm$ saturating pushes, $4n^2m$ nonsaturating pushes, label bound $2n-1$ , and the total $(2n-1)(n-2)+2nm+4n^2m$ . The standing assumption $m \ge n-1$ appears only on Lemma 3.10 and the goal.
A trivializing formalization is ruled out: the step relation fixes the pushed amount $\delta = \min(e(v), r_f(v,w))$ and the new label exactly as in Fig. 1, termination is the loop guard rather than "the result is a flow", and a sorry-free check exhibits a concrete network $s \to a \to t$ with a two-step execution (relabel $a$ , then push $(a,t)$ ), so the run hypotheses are satisfiable.

Welcome contributions: proofs of the invariants (preflow, valid labeling, label monotonicity), of Ford–Fulkerson for antisymmetric flows (reusable beyond this mission), and of the counting lemmas. The FIFO bound of §4 is the subject of a companion mission.

Selected references

A. V. Goldberg, R. E. Tarjan, A New Approach to the Maximum-Flow Problem, Journal of the ACM 35(4):921–940, 1988. doi:10.1145/48014.61051
L. R. Ford, D. R. Fulkerson, Flows in Networks, Princeton University Press, 1962.
J. Edmonds, R. M. Karp, Theoretical improvements in algorithmic efficiency for network flow problems, Journal of the ACM 19(2):248–264, 1972. doi:10.1145/321694.321699
R. K. Ahuja, T. L. Magnanti, J. B. Orlin, Network Flows: Theory, Algorithms, and Applications, Prentice Hall, 1993.

17 thms3 active usersReviewed

Completed

Operations Research Probability·Captain: mikedeng1

Competitive Paging Algorithms III: No Randomized Paging Algorithm Is Better than H_k-CompetitiveResearch Paper

Motivation

Paging is the problem of managing a two-level memory: a cache holds $k$ of the $n$ pages a program uses, every request must find its page in the cache, and a request to a page outside the cache (a page fault) forces the algorithm to bring the page in and evict another. An on-line algorithm chooses what to evict without seeing future requests. Sleator and Tarjan (CACM 1985) measured on-line paging algorithms against the optimal off-line algorithm, which knows the whole request sequence, and showed that no deterministic on-line algorithm can be within a factor smaller than $k$ of it.

Randomization changes that picture. Fiat, Karp, Luby, McGeoch, Sleator and Young (J. Algorithms 1991; arXiv:cs/0205038) gave a randomized algorithm, the marking algorithm, whose expected number of faults is within $2H_k$ of the optimum, where $H_k = 1 + \tfrac12 + \dots + \tfrac1k \approx \ln k$ . This mission formalizes the other half of their paper's picture: no randomized paging algorithm can do better than $H_k$ . The bound says that the logarithmic behaviour is not an artefact of one algorithm but a property of the problem.

Timeline:

1985 — Sleator and Tarjan: deterministic paging algorithms have competitive factor at least $k$ ; LRU and FIFO achieve $k$ .
1988 — Karlin, Manasse, Rudolph and Sleator (Algorithmica 3, 1988) introduce the term competitive; Manasse, McGeoch and Sleator (STOC 1988; J. Algorithms 1990) extend it to randomized algorithms and pose the $k$ -server problem, of which paging is the uniform-metric case.
1991 — Fiat et al.: the marking algorithm is $2H_k$ -competitive, and no randomized algorithm is better than $H_k$ -competitive (Theorem 4 and Corollary 5 of the paper). Raghavan gave an alternative proof of the lower bound through Yao's minimax principle.
1991 — McGeoch and Sleator give an $H_k$ -competitive randomized paging algorithm (Algorithmica 6, 1991), so the lower bound is tight.

Setting

Let $M$ be a set of $n$ vertices with the uniform metric: any two distinct vertices are at distance $1$ . A configuration of $k$ servers is a map $C : \{1,\dots,k\} \to M$ ; server $s$ sits at $C(s)$ , and a vertex is covered when some server sits on it. A request sequence $\sigma$ is a finite list of vertices. A deterministic on-line algorithm assigns to every prefix of requests the configuration after serving it, in such a way that the vertex just requested is covered; its cost on $\sigma$ is the total distance travelled by its servers, which on the uniform metric is the number of server moves. Paging with $k$ cache slots and $n$ pages is exactly this $k$ -server problem on $n$ uniform vertices.

The optimal off-line cost $\mathrm{OPT}_{C_0}(\sigma)$ is the least cost of any schedule of configurations that starts at $C_0$ and covers each request of $\sigma$ in turn.

A randomized on-line algorithm $A$ is a probability space $(\Omega,\mu)$ of coin outcomes together with a deterministic on-line algorithm $A_\omega$ for each outcome $\omega$ . Its expected cost $C_A(\sigma)$ is the average of the cost of $A_\omega$ on $\sigma$ over $\omega$ . The request sequence is fixed in advance and does not depend on the coins (an oblivious adversary). Following the paper, $A$ is $c$ -competitive from the initial configuration $C_0$ if there is a constant $a$ such that

C_A(\sigma) \;\le\; c \cdot \mathrm{OPT}_{C_0}(\sigma) + a \qquad \text{for every request sequence } \sigma .

For the lower-bound argument, the probability vector $p=(p_i)_{i\in M}$ after a prefix $\sigma$ has $p_i$ equal to the probability, over $\omega$ , that vertex $i$ is not covered by $A_\omega$ after serving $\sigma$ . A set $S$ of marked vertices and the number $u = n - |S|$ of unmarked vertices are bookkeeping of the adversary, updated as the marking algorithm would update them.

Formalization targets

Goal: Corollary 5

For $1 \le k \le n-1$ , every randomized on-line algorithm $A$ with $k$ servers on $n$ uniform vertices, every initial configuration $C_0$ and every real $c$ ,

c < H_k \;\Longrightarrow\; A \text{ is not } c\text{-competitive from } C_0 .

Theorem 4 (milestone)

The case $k = n-1$ : no randomized algorithm for the uniform $(n-1)$ -server problem on $n$ vertices is $c$ -competitive with $c < H_{n-1}$ .

Claims of the proof of Theorem 4 (milestones)

With $p$ the probability vector, $S$ the marked set, $P = \sum_{i\in S} p_i$ and $u = n - |S|$ :

\sum_i p_i = 1 \quad(\text{servers on distinct vertices}),\qquad C_A(\sigma\,i) \ge C_A(\sigma) + p_i,

P = 0 \Rightarrow \exists\, i\notin S,\ p_i \ge \tfrac1u, \qquad P > \epsilon > 0 \Rightarrow \max_{j\in S} p_j \ge \tfrac{\epsilon}{|S|} > 0,

p_j = \max_{j'\notin S} p_{j'} \Rightarrow p_j \ge \tfrac{1-P}{u}, \qquad P \le \epsilon \Rightarrow \epsilon + p_j \ge \epsilon + \tfrac{1-P}{u} \ge \epsilon + \tfrac{1-\epsilon}{u} \ge \tfrac1u .

Significance

The result. Together with the marking algorithm's $2H_k$ upper bound, the corollary pins the randomized competitive ratio of paging to $\Theta(\log k)$ , an exponential improvement over the deterministic ratio $k$ that no randomized algorithm can push below $H_k$ . For $k = n-1$ the marking algorithm itself is $H_{n-1}$ -competitive, so Theorem 4 makes it optimal there. The $H_k$ bound is the benchmark every later randomized paging algorithm is measured against, including the $H_k$ -competitive algorithm of McGeoch and Sleator, and it is the uniform-metric base case of the randomized $k$ -server conjecture.

Formalizing it. The theorem is proved and classical; no machine-checked proof is known to exist. The platform already has the deterministic bound (KServer.uniform_not_competitive_below_k, ratio $k$ ) and a formal Yao averaging principle for randomized $k$ -server algorithms (KServer.randomized_yao_averaging), but no randomized paging lower bound. This mission produces the first formal $H_k$ lower bound, stated against the published randomized $k$ -server model, and a formal version of the paper's adversary argument. Either route — the paper's adaptive construction of a nemesis sequence from the probability vector, or Raghavan's distributional argument through Yao's principle — is welcome.

Difficulty

The adversary may not look at the coins, yet it must build one fixed sequence against which the expected cost is high in every phase. Requesting an uncovered vertex is not available, since which vertex is uncovered depends on the coins; requesting the vertex with the largest uncovered probability gives only $1/n$ per request and loses the harmonic sum. Lifting the per-phase bound to the asymptotic statement also requires handling the additive constant $a$ , the initial configuration of the off-line algorithm, and, for Corollary 5, the reduction from $n$ vertices to $k+1$ of them for an algorithm that may still place servers on the others.

Formalization scope

The Lean development reuses the published definitions KServer_model (configurations Fin k → M, deterministic on-line algorithms as functions of the request prefix, offlineCost) and KServer_randomized (RandomizedAlgorithm: a probability measure on coin outcomes, a deterministic algorithm per outcome, measurable costs; expCost as a lower Lebesgue integral in $[0,\infty]$ ; IsCompetitiveFrom C₀ c: every drawn algorithm starts at $C_0$ and there is one constant $a$ , fixed before the sequence, with expCost σ ≤ ENNReal.ofReal (c * offlineCost C₀ σ + a)). The clamp at $0$ in ENNReal.ofReal only weakens the property the goal refutes. The vertex set is an abstract type $M$ with an equivalence Fin n ≃ M and the uniform metric as a hypothesis, never the line metric of Fin n. $H_k$ is Mathlib's harmonic k cast to $\mathbb R$ . The goal quantifies over every algorithm and every initial configuration, with no laziness or distinct-positions assumption, and over every real $c < H_k$ , including $c \le 0$ .

A formalization in which competitiveness is vacuous (a model with no algorithms, or a cost that is always infinite), in which the adversary may choose the sequence after seeing the coins, or which fixes $c$ or the additive constant, would be a different statement and is ruled out by the published definitions used here.

The probability vector is the one new definition, uncoveredProb A σ i. Milestones about it assume the uncovered events measurable, the standing convention that $p_i$ is a probability; the model itself only guarantees measurable costs. The milestone $\sum_i p_i = 1$ assumes the $n-1$ servers occupy distinct vertices, as in the paper; in general $\sum_i p_i \ge 1$ . The arithmetic milestones are stated for an arbitrary probability vector on a finite set. Reusable pieces: the probability vector and the cost lemma apply to any randomized $k$ -server algorithm on a uniform metric, and a restriction lemma (from $n$ vertices to $k+1$ ) would serve other paging lower bounds.

Selected references

A. Fiat, R. M. Karp, M. Luby, L. A. McGeoch, D. D. Sleator, N. E. Young, Competitive Paging Algorithms, J. Algorithms 12(4):685–699, 1991. https://doi.org/10.1016/0196-6774(91)90041-V ; preprint arXiv:cs/0205038v1 (cited version). https://arxiv.org/abs/cs/0205038
D. D. Sleator, R. E. Tarjan, Amortized Efficiency of List Update and Paging Rules, Comm. ACM 28(2):202–208, 1985. https://doi.org/10.1145/2786.2793
M. S. Manasse, L. A. McGeoch, D. D. Sleator, Competitive Algorithms for Server Problems, J. Algorithms 11(2):208–230, 1990. https://doi.org/10.1016/0196-6774(90)90003-W
L. A. McGeoch, D. D. Sleator, A Strongly Competitive Randomized Paging Algorithm, Algorithmica 6:816–825, 1991.
P. Raghavan, Lecture Notes on Randomized Algorithms, IBM Research Report, Yorktown Heights, 1990 (the alternative proof of the lower bound, pp. 118–119).

11 thms3 active usersReviewed

Completed

Operations Research Probability·Captain: mikedeng1

Competitive Paging Algorithms II: Algorithm EATR Is 3/2-Competitive for Two ServersResearch Paper

Motivation

Paging is the problem of managing a two-level memory: a fast cache holding $k$ pages and a slow memory holding the rest. When a requested page is not in the cache (a page fault), it must be brought in and, if the cache is full, some page must be evicted. An on-line paging algorithm decides which page to evict without knowing future requests. Sleator and Tarjan (CACM 1985) compared on-line algorithms with the optimal off-line algorithm on every request sequence and showed that the best deterministic algorithms (LRU, FIFO) lose a factor of exactly $k$ , and that no deterministic on-line algorithm does better.

Randomization changes this picture. Fiat, Karp, Luby, McGeoch, Sleator and Young (J. Algorithms 1991; arXiv:cs/0205038) showed that the randomized marking algorithm is $2H_k$ -competitive, where $H_k=1+\tfrac12+\dots+\tfrac1k$ , and that no randomized algorithm is better than $H_k$ -competitive. For $k<n-1$ the marking algorithm does not reach $H_k$ , already for $k=2$ and $n=4$ . For two servers the same paper gives a different algorithm, EATR ("end after twice requested"), and proves it $3/2$ -competitive. Since $H_2=3/2$ , EATR is strongly competitive for $k=2$ : no randomized algorithm has a smaller competitive factor. This mission formalizes that result.

Timeline:

1985: Sleator and Tarjan, deterministic paging: factor $k$ , and $k$ is optimal.
1988: Karlin, Manasse, Rudolph and Sleator introduce the term competitive (Algorithmica 3:79–119); Manasse, McGeoch and Sleator formulate the $k$ -server problem and extend competitiveness to randomized algorithms (J. Algorithms 1990).
1991: Fiat et al.: the marking algorithm is $2H_k$ -competitive, the lower bound $H_k$ , and EATR is $3/2$ -competitive for $k=2$ .
1991: McGeoch and Sleator give an $H_k$ -competitive algorithm for every $k$ (Algorithmica 6, 1991; reference [12] of the paper).

Setting

The uniform $2$ -server problem has a finite set $M$ of $n\ge 2$ vertices, any two distinct vertices at distance $1$ , and two servers. A request sequence $\sigma=\sigma(0),\sigma(1),\dots$ is a list of vertices; each request must be covered by a server when it is served, and the cost is the number of server moves. This is paging with a cache of two pages: vertices are pages and the covered vertices are the cache.

A deterministic algorithm $B$ has a cost $C_B(\sigma)$ ; a randomized algorithm $A$ has an expected cost $C_A(\sigma)$ , averaged over its random choices. $A$ is $c$ -competitive if there is a constant $a$ such that for every request sequence $\sigma$ and every deterministic algorithm $B$ (on-line or off-line),

C_A(\sigma)\le c\cdot C_B(\sigma)+a.

Algorithm EATR. The servers start on the vertices $1$ and $2$ . The algorithm divides $\sigma$ into phases; the first phase starts at the first request to a vertex other than $1$ and $2$ . Let $P$ be the set of vertices occupied by the servers at the end of the previous phase ( $\{1,2\}$ before the first phase). During a phase, a vertex is clean if it is not in $P$ and has not been requested during this phase; a vertex is stale if it is neither clean nor the most recently requested vertex $\ell$ . EATR keeps one server on $\ell$ and the other uniformly at random on the stale set. When a stale vertex $r$ is requested, the servers are placed on $\ell$ and $r$ and the phase ends; the next phase starts at the next request to a vertex not covered by a server. Requests between phases, and repeated requests to $\ell$ , move nothing.

For a phase, $l$ denotes the number of clean vertices requested in it. For a deterministic algorithm $A$ , $d$ and $d'$ denote the numbers of $A$ 's servers that do not coincide with any of EATR's servers at the beginning and at the end of the phase. An algorithm is lazy if it moves no server on a request to a covered vertex and exactly one server on a request to an uncovered one.

Formalization targets

Goal: Theorem 3

With $\mathrm{OPT}(\sigma)$ the optimal off-line cost of serving $\sigma$ from the servers' starting position $(1,2)$ , there is a constant $c$ such that for all $\sigma$

C_{\mathrm{EATR}}(\sigma)\le \tfrac32\,\mathrm{OPT}(\sigma)+c.

The constant $c$ is left free; the factor $3/2$ is the paper's and is optimal.

Milestones, in the order of the proof

Laziness (p. 4): every deterministic algorithm is dominated by a lazy one (a published theorem, reused).
Adversary bound for structured phases (p. 5): in a complete EATR phase with $l$ clean requests, a lazy $A$ pays at least $l-d+d'$ .
Stale set before the terminating request (p. 6): it has $l+1$ elements, each covered with probability $1/(l+1)$ .
Expected cost of a phase to EATR (p. 6): exactly $l+\frac{l}{l+1}$ .
Per-phase ratio (p. 6): EATR's expected phase cost is at most $\tfrac32(C_A+d-d')$ , since $\frac{l+l/(l+1)}{l}=1+\frac{1}{l+1}\le\frac32$ .

Significance

The result. Theorem 3 settles the randomized competitive ratio of paging with two cache slots: combined with the paper's lower bound $H_k$ (Corollary 5, the subject of a companion mission), the optimal factor for $k=2$ is exactly $3/2$ , against $2$ for every deterministic algorithm. The general case was settled later by McGeoch and Sleator's $H_k$ -competitive partitioning algorithm, which is considerably more complicated.

Formalizing it. The result has been proved since 1991; no machine-checked proof of it is on the platform (a search for EATR, randomized paging and two-server results on 2026-09-26 found only deterministic $k$ -server theorems). The mission produces a formal model of a randomized on-line algorithm as a probability distribution over states evolving with the request sequence, a formal treatment of the phase decomposition and of the telescoping amortization that relates expected on-line cost to the optimal off-line cost, and a first strongly competitive randomized paging result on the platform, alongside the deterministic $k$ -server results already there.

Difficulty

The per-phase computations are short. The main difficulty is the global accounting. The adversary's cost in a phase is bounded only in amortized form, $l-d+d'$ , where $d$ and $d'$ compare the adversary's servers with EATR's at the phase boundaries; the bound becomes a statement about $\mathrm{OPT}$ only after the $d$ and $d'$ terms telescope across phases. This needs care with the requests that lie outside every phase (before the first phase, between phases, and in an unfinished last phase), during which the adversary may move. A further difficulty is that the off-line optimum ranges over arbitrary schedules, which may move several servers on one request, while the phase bound is proved for lazy on-line algorithms: the reduction from one to the other must be made explicit. Finally, the uniform law of the stale server is an invariant of a Markov chain on states that must be tracked through the whole phase.

Formalization scope

The vertices are an abstract metric space $M$ with an enumeration $e:\mathrm{Fin}\,n\simeq M$ , $2\le n$ , and the hypothesis that distinct points are at distance $1$ ; the metric of $\mathrm{Fin}\,n$ is not used. The starting vertices $1,2$ are $e(0),e(1)$ . $\mathrm{OPT}$ is KServer.offlineCost of the published KServer model: the infimum of total movement over all schedules serving $\sigma$ from $(e(0),e(1))$ . Comparing with this infimum covers every deterministic $B$ starting from EATR's position; a $B$ starting elsewhere differs by at most $2$ , which the constant absorbs. The constant is quantified before $\sigma$ .

EATR is a PMF over states: a deterministic record (the set $P$ , whether a phase is in progress, the last requested vertex, the vertices requested in the phase) and the random position of the second server. Its expected cost is the expected number of server moves, summed over the requests. The paper fixes only that the second server is uniform on the stale set; when a clean request enlarges the stale set, the formalization moves one server by a fixed coupling that keeps the law uniform, and this choice is stated in the definition. A formalization that defines EATR's expected cost by the closed formula of the proof, or that restricts $\sigma$ to complete phases, would make the goal a different statement; neither is done here. The pre-phase prefix and an unfinished last phase belong to $\sigma$ and are covered by the constant.

Needed infrastructure: finite probability distributions (Mathlib's PMF), the published KServer model and its laziness theorem, and bookkeeping lemmas on the deterministic phase record. The phase record and the amortization argument are reusable for the marking algorithm of the companion mission. Proofs of any milestone, and alternative decompositions of the goal, are welcome.

Selected references

A. Fiat, R. M. Karp, M. Luby, L. A. McGeoch, D. D. Sleator, N. E. Young, Competitive Paging Algorithms, Journal of Algorithms 12(4):685–699, 1991. https://doi.org/10.1016/0196-6774(91)90041-V ; arXiv:cs/0205038v1, https://arxiv.org/abs/cs/0205038
D. D. Sleator, R. E. Tarjan, Amortized Efficiency of List Update and Paging Rules, Communications of the ACM 28(2):202–208, 1985. https://doi.org/10.1145/2786.2793
M. S. Manasse, L. A. McGeoch, D. D. Sleator, Competitive Algorithms for Server Problems, Journal of Algorithms 11(2):208–230, 1990. https://doi.org/10.1016/0196-6774(90)90003-W
L. A. McGeoch, D. D. Sleator, A Strongly Competitive Randomized Paging Algorithm, Algorithmica 6:816–825, 1991 (reference [12] of the paper).
A. R. Karlin, M. S. Manasse, L. Rudolph, D. D. Sleator, Competitive Snoopy Caching, Algorithmica 3(1):79–119, 1988 (reference [9] of the paper).

8 thms3 active usersReviewed

Combinatorics Complexity Theory Operations Research+1·Captain: mikedeng1

A Threshold of ln n for Approximating Set Cover II: The Inapproximability of Max k-CoverResearch Paper

Motivation

Max $k$ -cover is the basic coverage problem of combinatorial optimization. The input is a collection of subsets of a finite ground set and a number $k$ ; the task is to choose $k$ subsets that together cover as many points as possible. It models facility and sensor placement, the selection of a small committee or feature set representing a population, and budgeted versions of set cover. It is also the prototype of maximizing a monotone submodular function under a cardinality constraint.

The greedy algorithm covers at least a $1-1/e\approx 0.632$ fraction of the optimum. This bound goes back to Hochbaum and Pathria and, for general submodular functions, to Nemhauser, Wolsey and Fisher (1978). For two decades it was not known whether a polynomial-time algorithm could do better. Uriel Feige answered the question in A Threshold of ln n for Approximating Set Cover (J. ACM 45(4), 1998, pp. 634–652, doi:10.1145/285055.285059), Section 5. His Theorem 5.3 (p. 648) states: "For any $\epsilon > 0$ , max $k$ -cover cannot be approximated in polynomial time within a ratio of $(1 - 1/e + \epsilon)$ , unless $P = NP$ ." Together with the greedy bound, it makes $1-1/e$ the exact approximation threshold of max $k$ -cover.

Timeline:

1978: Nemhauser, Wolsey and Fisher prove the greedy $1-1/e$ bound for monotone submodular maximization.
1992: Arora, Lund, Motwani, Sudan and Szegedy prove the PCP theorem. With Papadimitriou–Yannakakis (1991) it gives Theorem 2.1.1 of the paper: MAX 3SAT-B has a constant gap unless P = NP.
1994: Lund and Yannakakis introduce partition-system reductions from multi-prover proof systems to set cover.
1995: Raz proves the parallel repetition theorem (Theorem 2.2.2 of the paper).
1998: Feige proves the ln n threshold for set cover (the subject of mission I of this series) and the $1-1/e$ threshold for max $k$ -cover.

Setting

An instance consists of $n$ points $\{0,\dots,n-1\}$ , a list of subsets $S_1,\dots,S_s$ of the points, and a number $k$ . Its value $\mathrm{opt}$ is the largest number of points covered by at most $k$ of the sets. Instances are written over a three-letter alphabet:

$n$ in unary;
each set as its characteristic bit-vector;
$k$ in unary.

Following p. 648, a polynomial-time algorithm approximates max $k$ -cover within a ratio $\delta$ if on every input it outputs a number $v$ with

\delta\cdot\mathrm{opt}\le v\le\mathrm{opt}.

The algorithm need not name the sets. This is the non-constructive notion of approximation.

The proof is a reduction from the MAX 3SAT-5 problem. A 3CNF-5 formula has exactly three literals per clause, over three distinct variables, and every variable occurs in exactly five clauses. The reduction goes through a $k$ -prover proof system for such a formula $\varphi$ with $M$ clauses:

The verifier picks $\ell$ clauses at random, and a distinguished variable in each; there are $R=(3M)^\ell$ random strings $r$ .
Each prover $P_i$ is attached to a code word of length $\ell$ and weight $\ell/2$ ; distinct words are at Hamming distance at least $\ell/3$ .
On coordinate $j$ , prover $P_i$ receives the clause if its bit is 1, and the distinguished variable if its bit is 0.
Answers are satisfying assignments of the received clauses and bits for the received variables.
Two provers are consistent if they assign the same values to the distinguished variables. The verifier weakly accepts if some pair of distinct provers is consistent, and strongly accepts if every pair is.

The max $k'$ -cover instance of §5 attaches to every random string $r$ a copy $B_r$ of the explicit partition system. Its points are the vectors in $\{0,\dots,k-1\}^L$ with $L=2^\ell$ , so $m=k^L$ . Its $L$ partitions are labelled by the $\ell$ -bit strings, and each splits the points by the value of one coordinate. There are $N=mR$ points in all. For each prover $i$ , question $q$ and answer $a$ , the set $S_{(q,a,i)}$ collects, for every $r$ on which $P_i$ receives $q$ , the $i$ th part of the partition of $B_r$ labelled by the values that $a$ gives to the distinguished variables of $r$ . The budget is $k'=kQ$ , where $Q$ is the number of questions a single prover can receive.

Formalization targets

Goal: Theorem 5.3

\forall\varepsilon>0:\quad \text{max } k\text{-cover is approximable within } 1-\tfrac1e+\varepsilon \ \Longrightarrow\ \mathrm{P}=\mathrm{NP},

conditional on the two cited results below. The ratio is left free (any $\varepsilon>0$ ), so the goal records the shape of the threshold and not a particular constant.

Milestones

Proposition 2.1.2 (p. 640): for some $\varepsilon>0$ it is NP-hard to distinguish satisfiable 3CNF-5 formulas from those in which at most a $(1-\varepsilon)$ -fraction of the clauses can be satisfied simultaneously.
Lemma 2.3.1 (p. 643): a satisfiable $\varphi$ admits a strategy that always strongly accepts; on a far-from-satisfiable $\varphi$ the weak acceptance probability is at most $k^2\,2^{-c\ell}$ .
Coverage of the explicit partition system (p. 649): $j$ subsets from pairwise different partitions cover exactly $(1-(1-1/k)^j)m$ points.
Proposition 5.4 (p. 649): if at most $kQ$ sets cover a $(1-1/e+\varepsilon)$ -fraction of the points, then at least an $\varepsilon/3$ -fraction of the random strings are good. Here $r$ is good if $w_r\le3k/\varepsilon$ sets meet $B_r$ and two of them from different provers lie in the same partition.
Decoding (p. 649): such a covering yields a strategy that weakly accepts with probability at least $(\varepsilon/3)(\varepsilon/3k)^2$ .
Gap (p. 649): a satisfiable formula gives a cover of all $N$ points by $kQ$ sets. If at most a $(1-\varepsilon')$ -fraction of the clauses are satisfiable, $kQ$ sets cover at most $(1-1/e+g(k))N$ points, where $g(k)\to0$ , for all large $\ell$ .
Proposition 5.1 (p. 647): every greedy run covers at least $(1-1/e)\,\mathrm{opt}$ points.

Significance

The result closes the approximability of max $k$ -cover: the greedy algorithm cannot be beaten by any constant unless P = NP. Consequences:

Submodular maximization. Coverage functions are monotone submodular, so the bound transfers to monotone submodular maximization under a cardinality constraint, whenever the function is given in a form that encodes a coverage instance.
Other problems. Hardness results for facility location, budgeted allocation, and welfare maximization with coverage valuations reduce from it.
The reduction itself. The $\ell$ -fold $k$ -prover system combined with a partition system that is exactly countable is the template for later $1-1/e$ hardness proofs.

Status: the theorem has been proved since 1998. It has not been formalized; neither the reduction nor the underlying proof systems exist in Mathlib or on this platform. This mission produces:

a machine-checked reduction from MAX 3SAT-5 to max $k$ -cover;
an exact counting lemma for product partition systems;
the averaging and concavity argument of Proposition 5.4;
a formal statement of the greedy bound for coverage.

The cited PCP-based gap (Theorem 2.1.1) and parallel repetition (Theorem 2.2.2) remain hypotheses. They are separate, much larger formalization projects.

Difficulty

The obvious argument uses the soundness of the proof system directly: a large cover should force consistent answers. It fails because a cover may spend many sets on a few random strings and cover them completely, while covering the rest partially without any two sets from the same partition. What saves the argument is exact counting. For sets from pairwise different partitions, coverage is exactly $h(j)=(1-(1-1/k)^j)m$ , a concave function of the number $j$ of sets used. Since the sets meet a random string $k$ times on average, Jensen's inequality caps the total coverage of such "unstructured" strings at about $(1-(1-1/k)^k)$ , which tends to $1-1/e$ . A further obstacle is that the reduction must run in polynomial time. The paper therefore takes $\ell$ and $k$ constant (unlike the set-cover reduction, where $\ell=\Theta(\log\log n)$ ), and the soundness bound $k^2 2^{-c\ell}$ must beat $(\varepsilon/3)(\varepsilon/3k)^2$ at a constant $\ell$ . The quantifier order ( $k$ large first, then $\ell$ large) is part of the difficulty.

A second obstacle is the machine model. The goal is a statement about polynomial-time Turing machines, so the reduction and the decision procedure built from a hypothetical approximation algorithm must be compiled into Cook's one-tape machines.

Formalization scope

Machine model. CookPvsNP_defs (a published platform definition): one-tape Turing machines, $\mathrm{P}$ , $\mathrm{NP}$ , polynomial-time computable functions, CNF formulas and their encoding. "P = NP" is P Bool = NP Bool, the form in which CookPvsNP.P_ne_NP states the open problem.
Cited results as hypotheses. Theorem 2.1.1 enters as Thm211. Raz's theorem enters as RazRepetition, its consequence stated on p. 642: the $\ell$ -fold clause–variable game on a far-from-satisfiable 3CNF-5 formula has acceptance probability at most $2^{-c\ell}$ . This is weaker than Raz's general theorem, so the conditional statement is stronger. No hypothesis about max $k$ -cover is assumed.
Approximation. The value form above, with no size threshold. For $\varepsilon>1/e$ the ratio exceeds one and the hypothesis is unsatisfiable on any instance with $\mathrm{opt}>0$ ; those values are vacuous, as in the paper.
$\mathrm{opt}$ . Taken over at most $k$ sets. This agrees with the paper's "exactly $k$ " whenever $k\le s$ .
Probability and counting. Probabilities are uniform counts over the $(3M)^\ell$ random strings. Fractions in lower-bound statements are written as counts compared with multiples of $R$ .
Canonical answers. The type of answers is restricted to satisfying assignments of the received clauses, following the paper's "without loss of generality" (p. 643). All indices are 0-based.
Partition system. The §4 construction is defined for any partition system with $\ell$ -bit partition labels and instantiated with the explicit product system. Its $L=2^\ell$ coordinates are the $\ell$ -bit strings themselves.
Not formalized. The running time of the greedy algorithm, and the constructive variant (Proposition 5.2), which belongs to the set-cover mission.

A trivializing formalization is ruled out: every cited input is a named, satisfiable proposition about 3CNF formulas or the two-prover game, never about max $k$ -cover, and the approximation hypothesis is satisfiable for ratios up to $1$ .

Needed infrastructure, reusable beyond this mission:

composition and simulation lemmas for Cook's machines;
the uniformity of the verifier's questions on 3CNF-5 formulas;
concavity of $j\mapsto 1-(1-1/k)^j$ ;
$(1-1/k)^k\to 1/e$ bounds.

Contributions to any of these, or to either cited theorem, are welcome.

Selected references

U. Feige, A threshold of ln n for approximating set cover, J. ACM 45(4) (1998) 634–652. https://doi.org/10.1145/285055.285059
R. Raz, A parallel repetition theorem, SIAM J. Comput. 27(3) (1998) 763–803 (STOC 1995). https://doi.org/10.1137/S0097539795280895
S. Arora, C. Lund, R. Motwani, M. Sudan, M. Szegedy, Proof verification and the hardness of approximation problems, J. ACM 45(3) (1998) 501–555. https://doi.org/10.1145/278298.278306
C. Papadimitriou, M. Yannakakis, Optimization, approximation, and complexity classes, J. Comput. System Sci. 43(3) (1991) 425–440. https://doi.org/10.1016/0022-0000(91)90023-X
C. Lund, M. Yannakakis, On the hardness of approximating minimization problems, J. ACM 41(5) (1994) 960–981. https://doi.org/10.1145/185675.306789
G. L. Nemhauser, L. A. Wolsey, M. L. Fisher, An analysis of approximations for maximizing submodular set functions—I, Math. Programming 14 (1978) 265–294. https://doi.org/10.1007/BF01588971
S. Cook, The P versus NP problem, Clay Mathematics Institute. https://www.claymath.org/wp-content/uploads/2022/06/pvsnp.pdf

13 thms3 active usersReviewed

Combinatorics Complexity Theory Operations Research·Captain: mikedeng1

A Threshold of ln n for Approximating Set Cover I: The ln n Inapproximability of Set CoverResearch Paper

Motivation

Set cover is the problem of covering a finite ground set with as few members of a given family of subsets as possible. It models facility location, crew scheduling, test-suite minimization and many other selection problems in operations research, and it is one of the canonical NP-hard problems. The greedy algorithm, which repeatedly picks the subset covering the most uncovered points, finds a cover at most about $\ln n$ times larger than the optimum on an instance with $n$ points (Johnson 1974; Lovász 1975; Chvátal 1979). Whether any efficient algorithm does substantially better was open for two decades.

Timeline of the lower bounds:

1992. The PCP theorem (Arora, Lund, Motwani, Sudan, Szegedy) implies that set cover cannot be approximated within some constant $1+\varepsilon$ unless P = NP.
1994. Lund and Yannakakis showed that set cover cannot be approximated within $\tfrac14\log_2 n$ unless $\mathrm{NP}\subseteq\mathrm{TIME}(n^{O(\mathrm{polylog}\, n)})$ , and within $\tfrac12\log_2 n\approx 0.72\ln n$ under a randomized assumption.
1998. Feige showed that for every $\varepsilon>0$ , set cover cannot be approximated within $(1-\varepsilon)\ln n$ unless $\mathrm{NP}\subseteq\mathrm{TIME}(n^{O(\log\log n)})$ (J. ACM 45(4), 634–652). This matches the greedy bound up to lower-order terms.
2014. Dinur and Steurer replaced the assumption by P ≠ NP (STOC 2014).

This mission formalizes Feige's theorem, the result that fixed $\ln n$ as the threshold.

Setting

An instance consists of $n$ points $\{0,\dots,n-1\}$ and a list of subsets $S_1,\dots,S_s$ . A cover is a set of indices whose subsets together contain every point. The instance is coverable if every point lies in some $S_i$ . It is written as a string: $n$ in unary, then each subset as its characteristic vector.

A deterministic polynomial-time algorithm approximates set cover within $\rho(n)$ if, for some threshold $n_0$ and every coverable instance with $n \ge n_0$ points, the value $v$ it outputs satisfies $\mathrm{OPT}\le v\le\rho(n)\cdot\mathrm{OPT}$ , where $\mathrm{OPT}$ is the size of a smallest cover.

$\mathrm{TIME}(n^{O(\log\log n)})$ is the class of languages that a deterministic one-tape Turing machine decides within $|w|^{c(\log_2\log_2|w|+1)}+c$ steps, for some constant $c$ . Machines, $\mathrm{P}$ and $\mathrm{NP}$ are those of the published definition CookPvsNP_defs.

The proof passes through three objects, each defined in the mission:

3CNF-5 formulas: CNF formulas in which every clause has three literals on distinct variables and every variable occurs in exactly five clauses.
The $k$ -prover proof system of §2.3. A verifier picks $\ell$ random clauses and a distinguished variable in each. Each prover, according to its code word, receives some of these clauses and the distinguished variables of the others. Under the weak acceptance predicate, some two provers give consistent answers on the distinguished variables. Under the strong acceptance predicate, all provers do.
Partition systems $B(m,L,k,d)$ (Definition 3.1). These are $L$ partitions of $m$ points, each into $k$ parts, such that covering the points with parts taken from pairwise different partitions needs at least $d$ parts.

Formalization targets

Goal: Theorem 4.4

\exists\,\varepsilon>0:\ \text{set cover is approximable within }(1-\varepsilon)\ln n\ \Longrightarrow\ \mathrm{NP}\subseteq\mathrm{TIME}\big(n^{O(\log\log n)}\big).

The statement fixes no constant beyond $\varepsilon$ . The parameters $k$ , $\ell$ and $m$ of the reduction are choices made inside the proof. The goal carries three cited results as hypotheses: Theorem 2.1.1 (MAX 3SAT-B gap), the consequence of Raz's parallel repetition theorem for the clause–variable game, and the Naor–Schulman–Srinivasan construction of partition systems.

Milestones, in the order the proof uses them

Proposition 2.1.2: MAX 3SAT-5 is gap NP-hard.
Proposition 2.2.1: the one-round clause–variable game has value $1-\varepsilon/3$ .
Lemma 2.3.1: the $k$ -prover system is complete with strong acceptance and has soundness $k^2 2^{-c\ell}$ for weak acceptance.
Lemma 3.2: partition systems with $d=(1-2/k)k\ln m$ exist.
Propositions 4.2 and 4.3: a cover with $(1-\delta)kQ\ln m$ subsets yields a prover strategy that is weakly accepted with probability at least $2\delta/(k\ln m)^2$ .
Lemma 4.1: the gap between $kQ$ and $(1-2f(k))kQ\ln m$ .

Significance

The result. Combined with the greedy algorithm, Theorem 4.4 shows that $\ln n$ is the approximation threshold of set cover under a mild complexity assumption. Set cover reduces approximation-preservingly to many covering problems, so the threshold transfers to them. Examples are dominating set, several facility-location and group Steiner problems, and hitting-set formulations used in scheduling and testing. The $k$ -prover system with two acceptance predicates and the partition-system gadget became standard tools for later hardness-of-approximation proofs.

Formalizing it. The theorem is proved and has been strengthened (Dinur–Steurer 2014), but no machine-checked proof of any $\Omega(\log n)$ inapproximability of set cover is known. This mission contributes:

a Lean model of multi-prover proof systems with uniform-count probabilities;
partition systems and their probabilistic existence proof;
a gap-preserving reduction whose running time is analysed on Turing machines, not merely asserted.

Difficulty

The ratio comes from two gaps at once. One is a gap in acceptance probability. The other is a gap between strong and weak acceptance. A reduction from a two-prover system, as in Lund–Yannakakis, loses a constant factor because a cheating cover can use two parts of the same partition. Feige's analysis must turn every small cover into a strategy under which some pair of provers is consistent (Proposition 4.3), and this averaging argument has to lose only a factor $(k\ln m)^2$ .
Parameters interlock. $\ell=\Theta(\log\log n)$ must make $k^2 2^{-c\ell}$ smaller than $2\delta/(k\ln m)^2$ while keeping the instance of size $n^{O(\log\log n)}$ . The time bound must hold for a one-tape machine, including the deterministic partition-system construction.
Encoding. The reduction must be computed by an explicit machine on string encodings. Showing that a "clearly polynomial" construction meets the time bound on such a machine is substantial work.

Formalization scope

Cited results as hypotheses. Theorem 2.1.1, Raz's theorem and the Naor et al. construction are not proved in the mission; each is a named proposition (Thm211, RazRepetition, NaorPartitionSystems) and a hypothesis of the goal.
- RazRepetition is only the consequence of Raz's theorem that the paper uses (p. 642): a $2^{-c\ell}$ error bound for the repeated clause–variable game on 3CNF-5 formulas far from satisfiable.
- NaorPartitionSystems relaxes "time linear in $m$ " to polynomial time and renders " $L$ polynomial in $d$ " as $L\le\lfloor\log_2 m\rfloor^a$ . Both relaxations weaken the hypothesis.
Approximation in value form. The algorithm outputs a number $v$ with $\mathrm{OPT}\le v\le\rho(n)\mathrm{OPT}$ , and only on coverable instances with $n\ge n_0$ . Any algorithm that outputs a cover yields such a value, so this hypothesis is weaker than the paper's. The guard $n\ge n_0$ is needed because $(1-\varepsilon)\ln n<1$ for small $n$ .
Machine model. The machines are Cook's deterministic one-tape machines. Multi-tape simulation costs a quadratic factor, which the class absorbs.
Probabilities are uniform counts over the $(5n)^\ell$ random strings. Strategies are deterministic. Answers are canonical (satisfying on clause coordinates), as the paper assumes without loss of generality.
Not formalized. Randomized classes (ZTIME) are not defined here, so the following are omitted: the last sentence of Lemma 3.2, Proposition 6.1, and the randomized variants.
Ruling out a trivial formalization. The gap notion requires far-from-satisfiable formulas to have at least one clause. Otherwise the empty formula would be both a yes-instance and a no-instance, and Theorem 2.1.1 would hold trivially.
Infrastructure and reuse. The shared layer can serve other PCP-based hardness proofs: 3CNF-5 formulas, the $k$ $k$ -prover system, partition systems, and the gap-NP-hardness notion. Welcome contributions include:
- time bounds for list and table manipulations on one-tape machines;
- a Hadamard-code construction satisfying the weight and distance conditions;
- the union-bound and averaging lemmas behind Lemma 2.3.1 and Proposition 4.2.

Selected references

U. Feige, A threshold of ln n for approximating set cover, J. ACM 45(4), 634–652, 1998. https://doi.org/10.1145/285055.285059
C. Lund, M. Yannakakis, On the hardness of approximating minimization problems, J. ACM 41(5), 960–981, 1994. https://doi.org/10.1145/185675.306789
R. Raz, A parallel repetition theorem, SIAM J. Comput. 27(3), 763–803, 1998 (STOC 1995). https://doi.org/10.1137/S0097539795280895
M. Naor, L. J. Schulman, A. Srinivasan, Splitters and near-optimal derandomization, FOCS 1995, 182–191. https://doi.org/10.1109/SFCS.1995.492475
S. Arora, C. Lund, R. Motwani, M. Sudan, M. Szegedy, Proof verification and the hardness of approximation problems, J. ACM 45(3), 501–555, 1998. https://doi.org/10.1145/278298.278306
C. Papadimitriou, M. Yannakakis, Optimization, approximation, and complexity classes, J. Comput. Syst. Sci. 43(3), 425–440, 1991. https://doi.org/10.1016/0022-0000(91)90023-X
V. Chvátal, A greedy heuristic for the set-covering problem, Math. Oper. Res. 4(3), 233–235, 1979. https://doi.org/10.1287/moor.4.3.233
I. Dinur, D. Steurer, Analytical approach to parallel repetition, STOC 2014, 624–633. https://doi.org/10.1145/2591796.2591884

15 thms3 active usersReviewed

Combinatorics Complexity Theory Operations Research·Captain: mikedeng1

Scheduling Subject to Resource Constraints: Classification and Complexity I: Unit-Time Chains on Two Identical Machines with One Unit Resource Are Strongly NP-hardResearch Paper

Resource constraints and the easy/hard borderline in scheduling

Machine scheduling asks how to assign jobs to machines over time so that a criterion such as the makespan $C_{\max}$ , the time at which the last job completes, is as small as possible. In practice jobs also compete for scarce resources beyond the machines themselves: tools, operators, memory, power. Błażewicz, Lenstra and Rinnooy Kan (DAM 1983) extended the standard three-field classification $\alpha\mid\beta\mid\gamma$ of Graham, Lawler, Lenstra and Rinnooy Kan (1979) by a resource field $res\lambda\sigma\rho$ . They then settled the complexity of every problem with parallel identical or uniform machines, unit-time jobs, precedence constraints and the $C_{\max}$ criterion. Their Fig. 2 separates the maximal polynomially solvable problems from the minimal NP-hard ones, and it has been the reference map for resource-constrained scheduling since.

Brief timeline of the problems involved:

1975. Garey and Johnson (SIAM J. Comput. 4) show that $P2\mid res\cdots, p_j=1\mid C_{\max}$ is solvable in polynomial time via matchings, and that $P3\mid res1\cdot\cdot, p_j=1\mid C_{\max}$ and $P2\mid res1\cdot\cdot, tree, p_j=1\mid C_{\max}$ are NP-hard in the strong sense, by reduction from 3-PARTITION.
1976. Ullman (Complexity of sequencing problems, in Coffman, ed., Computer & Job/Shop Scheduling Theory, Wiley) gives strong NP-hardness of $P2\mid res111, prec, p_j=1\mid C_{\max}$ under arbitrary precedence constraints.
1983. Błażewicz, Lenstra and Rinnooy Kan prove Theorem 7: chains suffice. Two identical machines, one resource of size one, requirements in $\{0,1\}$ and chain-like precedence already give a strongly NP-hard problem. The result dominates both earlier two-machine results.

Setting

There are $n$ jobs $J_1,\dots,J_n$ and $m$ machines $M_1,\dots,M_m$ . Every job has processing time $1$ on every machine, each machine handles at most one job at a time, and jobs are not preempted. There are $l$ resources; resource $R_h$ has a positive integer size $s_h$ , the amount available at any time, and job $J_j$ has a nonnegative integer requirement $r_{hj}$ , the amount it holds throughout its execution. A directed acyclic graph $H$ on the jobs gives the precedence constraints: if $H$ has a path from $j$ to $k$ ( $J_j\to J_k$ ), then $J_j$ must complete before $J_k$ starts. The precedence is chain-like when every vertex of $H$ has indegree and outdegree at most one.

A schedule gives each job a machine and a real start time $S_j$ ; the job occupies $[S_j, S_j+1)$ and completes at $C_j = S_j+1$ . It is feasible if jobs on one machine do not overlap, precedence is respected, and at every time $t$ the jobs running at $t$ require at most $s_h$ of each resource $R_h$ . The makespan is $C_{\max} = \max_j C_j$ .

The problem $P2\mid res111, chain, p_j=1\mid C_{\max}$ restricts this to $m=2$ , one resource ( $\lambda=1$ ) of size $1$ ( $\sigma=1$ ), every requirement at most $1$ ( $\rho=1$ ), and chain-like precedence. The problem $P3\mid res1\cdot\cdot, p_j=1\mid C_{\max}$ has $m=3$ , one resource of arbitrary size and requirements, and no precedence.

3-PARTITION: given $t$ , a positive integer $b$ and positive integers $a_1,\dots,a_{3t}$ with $\sum_j a_j = tb$ and $\tfrac14 b<a_j<\tfrac12 b$ , can $\{1,\dots,3t\}$ be split into $t$ disjoint 3-element sets $S_i$ with $\sum_{j\in S_i}a_j=b$ ?

A problem is NP-hard in the strong sense if it remains NP-hard when every number of the instance is written in unary.

Formalization targets

Goal: Theorem 7

\text{3-PARTITION is NP-hard in the strong sense} \;\Longrightarrow\; P2\mid res111,\ chain,\ p_j=1\mid C_{\max}\ \text{is NP-hard in the strong sense.}

The hypothesis is Garey and Johnson's theorem on 3-PARTITION, which the paper cites and does not prove. The conclusion concerns the decision version: given an instance and $y\in\mathbb N$ , is there a feasible schedule with $C_{\max}\le y$ ?

Milestones

Proof of Theorem 4, the saturation equivalence. For positive $b$ , $a_j$ with $\sum_j a_j=tb$ , the $P3\mid res1\cdot\cdot$ instance with $3t$ unit jobs, resource size $b$ and requirements $a_j$ has a feasible schedule with $C_{\max}\le t$ iff the 3-PARTITION instance has a solution.
Theorem 4 (Garey and Johnson). Under the same hypothesis as the goal, $P3\mid res1\cdot\cdot, p_j=1\mid C_{\max}$ is NP-hard in the strong sense.
Proof of Theorem 7, "if". A 3-PARTITION solution yields a feasible schedule of the constructed two-machine instance with $C_{\max}=2tb$ .
Proof of Theorem 7, "only if". A feasible schedule of the constructed instance with $C_{\max}\le 2tb$ yields a 3-PARTITION solution.

Significance

Theorem 7 is the sharpest hardness result of the paper's classification. Without resources, two-machine unit-time scheduling with arbitrary precedence is polynomial (Coffman and Graham, Acta Inform. 1972); without precedence, it is polynomial under arbitrary resources (Theorem 1 of the paper). The theorem shows that combining the weakest nontrivial versions of both constraints, chains and one unit resource, already crosses the borderline. The paper's §4.1 extends the same reduction to the $\sum C_j$ and $L_{\max}$ criteria.

On the formal side, the mission provides a machine-checked model of resource-constrained scheduling with real start times, a definition of NP-hardness in the strong sense on top of the platform's Turing-machine formalization of $\mathrm P$ and $\mathrm{NP}$ , and 3-PARTITION as a reusable source problem. As far as the platform's corpus shows, none of Theorems 4 and 7, 3-PARTITION, or strong NP-hardness has been formalized before. Both theorems are proved in the literature; what remains is to formalize the reductions and their polynomial running time.

Difficulty

The combinatorial heart is the "only if" direction: a schedule of length $2tb$ must be shown to be rigid. Start times are arbitrary reals, so the first obstacle is to show that both machines are busy throughout $[0,2tb)$ , that the chain $L$ forces unit spacing, and that the primed jobs of the chains $K'_j$ can only run in the intervals the chain $L$ leaves free of the resource. Only after this is established can the index sets $S_i$ be read off. Arguing on integer time slots from the start is not enough: the model allows fractional start times, and ruling them out is part of the proof.

The second obstacle is the complexity layer. NP-hardness is stated with respect to polynomial-time many-one reductions computed by one-tape Turing machines. The reduction from 3-PARTITION therefore has to be implemented and its running time bounded on unary codes. The constructed instance has $4tb$ jobs, which is polynomial in the unary length of the 3-PARTITION instance; this is exactly why the reduction proves hardness in the strong sense.

Formalization scope

Model. Jobs are Fin n and machines Fin m, 0-based. Only identical machines with unit processing times are modelled. Start times are real, execution intervals are half-open, and the resource constraint is imposed at every real time. Precedence is the transitive closure of the arc list of $H$ . $C_{\max}=0$ for an empty instance.
Decision version. Thresholds $y$ are natural numbers; this narrower class makes the hardness statement stronger.
Encoding. An instance is described by its list of numbers ( $n,m,l$ , the sizes, the requirements row by row, the number of arcs and the arcs, then $y$ ). The unary language is the set of unary codes of yes-instances over a two-letter alphabet. No pairing function is used. The class conditions (two machines, one unit resource, requirements at most one, chain-like acyclic $H$ ) are part of the yes-predicate.
Strong sense. Strong NP-hardness is NP-hardness of the unary language. This is equivalent to Garey and Johnson's definition, which bounds the largest number by a polynomial in the instance length.
Cited hypothesis. The goal and Theorem 4 assume strong NP-hardness of 3-PARTITION (with $\tfrac14 b<a_j<\tfrac12 b$ ) and nothing else. Stating the goal as a bare reduction between the two languages, or adding $\mathrm P\ne\mathrm{NP}$ , would not be Theorem 7.
Constructions. The two scheduling instances built from a 3-PARTITION instance are explicit definitions following the page, not arbitrary instances with a property.
Reuse. The scheduling model and the strong-NP-hardness layer are shared with the other missions of this series; 3-PARTITION serves any strong NP-hardness proof by number partitioning.

Welcome contributions: proofs of the four milestones; a formalized polynomial-time implementation of the reduction on unary codes; general lemmas about composing polynomial-time reductions on the one-tape machine model.

Selected references

J. Błażewicz, J. K. Lenstra, A. H. G. Rinnooy Kan, Scheduling subject to resource constraints: classification and complexity, Discrete Applied Mathematics 5 (1983) 11–24. https://doi.org/10.1016/0166-218X(83)90012-4
M. R. Garey, D. S. Johnson, Complexity results for multiprocessor scheduling under resource constraints, SIAM J. Comput. 4 (1975) 397–411. https://doi.org/10.1137/0204035
M. R. Garey, D. S. Johnson, Computers and Intractability: A Guide to the Theory of NP-Completeness, Freeman, 1979.
R. L. Graham, E. L. Lawler, J. K. Lenstra, A. H. G. Rinnooy Kan, Optimization and approximation in deterministic sequencing and scheduling: a survey, Ann. Discrete Math. 5 (1979) 287–326. https://doi.org/10.1016/S0167-5060(08)70356-X
J. D. Ullman, Complexity of sequencing problems, in: E. G. Coffman, Jr., ed., Computer & Job/Shop Scheduling Theory, Wiley, 1976, 139–164.
E. G. Coffman, Jr., R. L. Graham, Optimal scheduling for two-processor systems, Acta Informatica 1 (1972) 200–213. https://doi.org/10.1007/BF00288685
S. Cook, The P versus NP problem, Clay Mathematics Institute official problem description.

11 thms3 active usersReviewed

Completed

Combinatorics Operations Research Optimization+1·Captain: mikedeng1

Maximizing Non-Monotone Submodular Functions II: A Nonadaptive Algorithm Achieves 1/3 of the OptimumResearch Paper

Motivation

Maximizing a submodular set function without constraints contains Max Cut, Max Directed Cut, maximum facility location and several graph and hypergraph cut problems as special cases, and it appears in operations research wherever a value exhibits diminishing returns but is not monotone (profit that combines coverage with a cost, for example). These problems are NP-hard, so the question is which fraction of the optimum an efficient algorithm can guarantee when the function is accessible only through a value oracle that returns $f(S)$ for a queried set $S$ .

Feige, Mirrokni and Vondrák (SIAM J. Comput. 40(4), 2011) gave the first constant-factor approximation algorithms for maximizing a general nonnegative submodular function. The simplest of them returns a uniformly random set and achieves $1/4$ of the optimum; this mission is about the next one, a nonadaptive algorithm: it decides all of its oracle queries before seeing any answer, then computes a set from the answers. Such an algorithm can be run in one round of parallel queries. The paper shows that this restricted access already beats $1/4$ and reaches $1/3$ .

Timeline. For Max Directed Cut, a random cut achieves $1/4$ . Feige, Mirrokni and Vondrák (FOCS 2007; journal version 2011) proved $1/4$ for a random set and $1/3$ nonadaptively for general nonnegative submodular functions, $1/3$ and $2/5$ by adaptive local search, and that $1/2$ requires exponentially many queries. Buchbinder, Feldman, Naor and Schwartz (FOCS 2012, SIAM J. Comput. 2015) later reached the optimal $1/2$ with a randomized double-greedy algorithm.

Setting

Let $X$ be a finite ground set with $n = |X| \ge 1$ elements. A function $f : 2^X \to \mathbb{R}$ is submodular (Definition 1.1) if

f(S \cup T) + f(S \cap T) \le f(S) + f(T) \qquad \text{for all } S, T \subseteq X .

Throughout, $f$ is nonnegative, the paper's standing assumption, and $OPT = \max_{S \subseteq X} f(S)$ .

For $p \in [0,1]$ , $X(p)$ denotes the random subset of $X$ containing each element independently with probability $p$ ; $R = X(1/2)$ is a uniformly random subset. For a set $A \subseteq X$ , $A(p)$ is the analogous random subset of $A$ . The averaged marginal value of an element (Definition 2.4) is

\omega(x) = \mathbf{E}\big[f(R \cup \{x\}) - f(R \setminus \{x\})\big], \qquad R = X(1/2).

Algorithm NA (p. 1139):

by random sampling, compute estimates $\tilde\omega(x)$ with $|\tilde\omega(x) - \omega(x)| < OPT/n^2$ for all $x$ , with high probability;
independently, sample $R = X(1/2)$ ;
with probability $8/9$ return $R$ ;
with probability $1/9$ return $A = \{x \in X : \tilde\omega(x) > 0\}$ .

Given the estimates, the expected value NA returns is $\tfrac89\,\mathbf{E}[f(X(1/2))] + \tfrac19 f(A)$ .

Formalization targets

Goal: Theorem 2.6 in the explicit form of its proof

For every nonnegative submodular $f$ and every estimate $\tilde\omega$ with $|\tilde\omega(x) - \omega(x)| < OPT/n^2$ for all $x$ ,

\frac89\,\mathbf{E}[f(X(1/2))] + \frac19\, f\big(\{x : \tilde\omega(x) > 0\}\big) \ \ge\ \Big(\frac13 - \frac{4}{9n}\Big)\, OPT .

The printed theorem says "at least $(1/3 - o(1))\,OPT$ "; the term $4/(9n)$ is what the proof establishes (p. 1140, last display).

Milestones

Lemma 2.2: $\mathbf{E}[g(A(p))] \ge (1-p)\,g(\emptyset) + p\,g(A)$ for submodular $g$ .
Lemma 2.3: $\mathbf{E}[f(A(p) \cup B(q))] \ge (1-p)(1-q) f(\emptyset) + p(1-q) f(A) + (1-p)q f(B) + pq f(A \cup B)$ for independently sampled, possibly overlapping $A, B$ .
For $B = X \setminus A$ and any $C$ : $f(A) + f(B \cap C) + f(B \cup C) \ge f(C)$ .
If $\omega \le OPT/n^2$ on $B$ : $\mathbf{E}[f(R \cup (B \cap C))] \le \mathbf{E}[f(R)] + OPT/(2n)$ .
$\mathbf{E}[f(R \cup (B \cap C))] \ge \tfrac14 f(B \cap C) + \tfrac14 f(C)$ .
If $\omega \ge -OPT/n^2$ on $A$ and $B = X \setminus A$ : $\mathbf{E}[f(R)] \ge \mathbf{E}[f(R \cap (B \cup C))] - OPT/(2n)$ .
$\mathbf{E}[f(R \cap (B \cup C))] \ge \tfrac14 f(C) + \tfrac14 f(B \cup C)$ .

Milestones 3–7 are the displayed steps of the proof of Theorem 2.6, stated for arbitrary sets where the page's argument does not use the optimality of $C$ .

Significance

The theorem shows that nonadaptive access, a fixed batch of polynomially many value queries followed by a computation, suffices for a $1/3$ -approximation of unconstrained nonnegative submodular maximization, strictly better than the $1/4$ of any algorithm that must return one of its queried sets (the paper shows $1/4$ is optimal in that class, §4.2). The quantity $\omega$ generalizes the in-degree/out-degree test for Max Directed Cut to arbitrary submodular functions, and Lemmas 2.2 and 2.3 are general sampling inequalities for submodular functions that the paper reuses for its adaptive smooth local search.

Formalizing it produces machine-checked versions of Lemmas 2.2 and 2.3 as statements about exact finite averages, a reusable expectation operator on product-distributed random subsets, and a checked version of the $1/3$ argument with its explicit error term. The result is proved in the paper; to our knowledge none of it has been formalized in a proof assistant.

Difficulty

The two regimes the proof separates, " $A$ is already good" and "one of $f(B \cap C)$ , $f(B \cup C)$ is large", must be tied to the value of a uniformly random set, whereas the elements of $A$ and $B$ are chosen from estimated averages, not from the optimal set $C$ . The natural attempt, comparing $f(R)$ with $f(C)$ element by element, fails because $f$ is not monotone: adding elements of $C$ to $R$ can decrease the value. The accuracy $OPT/n^2$ of the estimates must also be propagated through a sum over up to $n$ elements, which is where the error term $4/(9n)$ comes from. The sampling lemmas require handling expectations over pairs of independent random subsets of possibly overlapping sets.

Formalization scope

The ground set is a Fintype X with DecidableEq, assumed Nonempty, so $n = |X| \ge 1$ and the divisions by $n$ and $n^2$ are genuine; sets are Finset X; $f$ is real valued with nonnegativity $\forall S,\ 0 \le f(S)$ as an explicit hypothesis. Lemmas 2.2 and 2.3 are stated for real $f$ with no sign condition, as printed.
$OPT$ is Finset.univ.sup' _ f, the true maximum over all subsets.
Every expectation over an independently sampled random set is the exact finite sum $F(x) = \sum_{S} f(S)\prod_{i \in S} x_i \prod_{i \notin S}(1 - x_i)$ ; $X(1/2)$ is $x \equiv 1/2$ . Expectations over two independent samples (Lemma 2.3) are the corresponding iterated sums. Sampling probabilities carry the hypotheses $0 \le p, q \le 1$ .
The goal quantifies over every estimate $\tilde\omega$ satisfying the printed accuracy $|\tilde\omega(x) - \omega(x)| < OPT/n^2$ (strict), with $A = \{x : \tilde\omega(x) > 0\}$ (strict). The "with high probability" of NA's first step is this hypothesis; the sampling estimate that makes it likely (Lemma 2.5, a Chernoff-bound argument) is not part of the goal. When $OPT = 0$ the hypothesis is unsatisfiable, but then $f \equiv 0$ and nothing is lost.
The left-hand side is exactly the mixture $\tfrac89\,\mathbf{E}[f(X(1/2))] + \tfrac19 f(A)$ . A statement with the maximum of the two terms, with exact values $\tilde\omega = \omega$ , or with the $o(1)$ replaced by an existential constant or a limit, is a different (and weaker or stronger) theorem and does not close this mission.
Printed slip corrected: in the second display on p. 1140, the " $=$ " before $-|A \setminus C|\,OPT/(2n^2)$ should be " $\ge$ "; milestone 6 states the inequality.

Welcome contributions: proofs of Lemmas 2.2 and 2.3 (reusable for mission IV of this series), the identity $\mathbf{E}[f(R \cup \{x\}) - f(R)] = \tfrac12\omega(x)$ , and general lemmas about the operator $F$ (splitting a uniform random set along a partition).

Selected references

U. Feige, V. S. Mirrokni, J. Vondrák, Maximizing Non-Monotone Submodular Functions, SIAM J. Comput. 40(4):1133–1153, 2011. https://doi.org/10.1137/090779346
N. Buchbinder, M. Feldman, J. Naor, R. Schwartz, A Tight Linear Time (1/2)-Approximation for Unconstrained Submodular Maximization, SIAM J. Comput. 44(5):1384–1402, 2015. https://doi.org/10.1137/130929205

12 thms3 active usersReviewed

Completed

Graph Theory Probability·Captain: mikedeng1

A Simple Parallel Algorithm for the Maximal Independent Set Problem I: One Round of Monte Carlo Algorithm A or B Removes an Expected Eighth of the EdgesResearch Paper

Motivation

A maximal independent set (MIS) of a graph is a set of vertices, no two adjacent, 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 found fast in parallel was a central question of parallel complexity in the early 1980s: an MIS algorithm is a subroutine for maximal matching, vertex colouring with $\Delta + 1$ colours, and many other symmetry-breaking tasks.

Karp and Wigderson (STOC 1984; J. ACM 32, 1985) gave the first fast parallel algorithms for MIS: a randomized one and a deterministic one, both with running time $O((\log n)^4)$ , placing MIS in NC $^4$ .
Luby (SIAM J. Comput. 15(4), 1986) gave the Monte Carlo algorithms analysed in this mission, together with a derandomization that yields a deterministic EREW P-RAM algorithm with $O((\log n)^2)$ running time, placing MIS in NC $^2$ . Alon, Babai and Itai (J. Algorithms 7, 1986) independently found a Monte Carlo algorithm similar to Algorithm B.

Luby's algorithm is the standard textbook example of a randomized parallel algorithm and remains the basis of distributed MIS algorithms in the LOCAL model. Its analysis rests on one statement, Theorem 1 of the paper, which this mission formalizes.

Setting

All algorithms in the paper run the same loop on a finite simple undirected input graph $G = (V, E)$ with $n = |V|$ vertices. The current graph is $G' = (V', E')$ , initially $G$ . For $W \subseteq V'$ the neighbourhood is $N(W) = \{ i \in V' : \exists j \in W,\ (i,j) \in E' \}$ . One execution of the loop body selects a set $I' \subseteq V'$ independent in $G'$ , adds it to the output, and replaces $G'$ by the subgraph induced on $V' - (I' \cup N(I'))$ . The loop stops when $G'$ is empty.

For $i \in V'$ write $\mathrm{adj}(i)$ for its neighbours and $d(i) = |\mathrm{adj}(i)|$ for its degree. The two Monte Carlo select steps are:

Algorithm A. Every vertex draws a priority $\pi(i)$ uniformly from $\{1, \dots, n^4\}$ , independently. A vertex enters $I'$ when its priority is strictly smaller than the priority of each of its neighbours.
Algorithm B. Every vertex independently sets $\mathrm{coin}(i) = 1$ with probability $1/(2d(i))$ , or always if $d(i) = 0$ . Let $X$ be the set of vertices with coin $1$ . A vertex of $X$ enters $I'$ when each of its neighbours in $X$ has strictly smaller degree.

Let $Y_k$ be the number of edges of $E'$ before the $k$ -th execution of the loop body. The number of edges eliminated by that execution is $Y_k - Y_{k+1}$ : exactly the edges of $G'$ with at least one endpoint in $I' \cup N(I')$ . For $d(i) \ge 1$ the paper uses the weight $\mathrm{sum}(i) = \sum_{j \in \mathrm{adj}(i)} 1/d(j)$ .

Formalization targets

Goal: Theorem 1

For the current graph $G'$ and $n \ge \max(1, |V'|)$ ,

E\big[Y_k^A - Y_{k+1}^A\big] \ge \tfrac18\, Y_k^A - \tfrac1{16}, \qquad E\big[Y_k^B - Y_{k+1}^B\big] \ge \tfrac18\, Y_k^B .

The constants are those printed in the paper. No connectivity, degree or size condition on $G'$ is assumed.

Milestones

§3.2, p. 1040. The priorities of Algorithm A are pairwise distinct with probability at least $1 - 1/(2n^2)$ .
TECHNICAL LEMMA, p. 1043. For $p_1 \ge \dots \ge p_n \ge 0$ and $c > 0$ , with $\alpha_l = \sum_{j \le l} p_j$ , $\beta_l = \sum_{j < k \le l} p_j p_k$ and $\gamma_l = \alpha_l - c\beta_l$ ,

\max_{1 \le l \le n} \gamma_l \ge \tfrac12 \min\{\alpha_n, 1/c\}.

LEMMA A (Beame), p. 1041. For Algorithm A and $d(i) \ge 1$ ,

\Pr[i \in N(I')] \ge \big[\tfrac14\min\{\mathrm{sum}(i), 1\}\big]\big(1 - \tfrac{1}{2n^2}\big).

LEMMA B, p. 1042. For Algorithm B and $d(i) \ge 1$ ,

\Pr[i \in N(I')] \ge \tfrac14 \min\{\mathrm{sum}(i)/2, 1\}.

Proof of Theorem 1, first display, p. 1041. For any random choice of $I'$ ,

E[Y_k - Y_{k+1}] \ge \tfrac12 \sum_i d(i)\Pr[i \in I' \cup N(I')] \ge \tfrac12 \sum_i d(i) \Pr[i \in N(I')].

Proof of Theorem 1, closing chain, p. 1041.

\tfrac12 \sum_{\mathrm{sum}(i) \le 2} d(i)\,\mathrm{sum}(i) + \sum_{\mathrm{sum}(i) > 2} d(i) \ge |E'|.

Significance

Theorem 1 says that each round removes, in expectation, a constant fraction of the remaining edges. From it the paper derives that the expected number of rounds of either algorithm is $O(\log n)$ , and hence that MIS has a Monte Carlo algorithm running in $O(\log n)$ expected time on a CRCW P-RAM and $O((\log n)^2)$ on an EREW P-RAM with $O(m)$ processors. Algorithm B and the proof of part (2) are also the basis of the paper's deterministic algorithm: the analysis of Lemma B uses only pairwise independence of the coins. The companion mission (A Simple Parallel Algorithm for the Maximal Independent Set Problem II) formalizes that derandomization and reuses the statements of milestones 2, 5 and 6.

The results are proved in the paper and reproduced in textbooks (e.g. Motwani and Raghavan, Randomized Algorithms), but not formalized: no statement of Theorem 1, Lemma A or Lemma B was found on the platform. A formal proof would make the per-round analysis of a standard parallel randomized algorithm reusable. That includes the degree-weighted counting of milestone 6 and the Bonferroni-type bound of the Technical Lemma, both of which recur in later analyses of distributed symmetry breaking.

Difficulty

The obvious argument tries to show that a fixed vertex enters $I'$ with good probability. That fails, because a high-degree vertex rarely wins against all its neighbours. The analysis instead bounds the probability that a vertex is removed, i.e. lands in $N(I')$ . This event is a union over neighbours of dependent events, so the first Bonferroni inequality alone does not give a lower bound: the pairwise-intersection terms must be controlled. The union bound can also be very lossy when $\mathrm{sum}(i)$ is large, which is why the conclusion involves a minimum with a constant.

A second obstacle is the passage from vertices to edges: vertices of small $\mathrm{sum}(i)$ can have high degree while contributing little probability. The per-vertex bounds therefore have to be summed with degree weights and redistributed over edges. For Algorithm A there is an additional complication: priorities from $\{1, \dots, n^4\}$ can collide, so the argument about a uniformly random order holds only on the event that $\pi$ is injective. That event appears as the factor $1 - 1/(2n^2)$ .

Formalization scope

Graph. The current graph $G'$ is a SimpleGraph V on a finite type with decidable adjacency, and $V' = V$ . The degree is SimpleGraph.degree, $\mathrm{adj}(i)$ is neighborFinset, and $Y_k = |E'|$ is edgeFinset.card.
Conditional form. Theorem 1 is stated for a fixed current graph $G'$ , i.e. conditionally on the first $k - 1$ rounds, as in the paper's proof. The unconditional statement follows by averaging.
Input size. $n$ is a parameter with $1 \le n$ and $|V'| \le n$ . It is not fixed to $|V'|$ , which would cover only the first round.
Select steps. Both endpoints' ALGEDGE runs are applied to every edge, since $E'$ contains each edge in both orientations. Hence Algorithm A keeps $i$ iff $\pi(i) < \pi(j)$ for all neighbours $j$ . Algorithm B keeps $i \in X$ iff $d(j) < d(i)$ for all neighbours $j \in X$ . Algorithm B's $I'$ starts at $X$ ; the page leaves $I'$ uninitialized in §3.3, and Algorithm D's code (p. 1047) has $I' \leftarrow X$ .
Laws. Probabilities and expectations are explicit finite sums: uniform over the $(n^4)^{|V|}$ priority vectors, and the product law over the $2^{|V|}$ coin vectors. A coin of an isolated vertex is $1$ with probability $1$ , as on the page.
Milestones. Milestone 5 is stated for an arbitrary finite distribution of $I'$ , which contains both algorithms' laws. Milestone 6 divides out the common factor $\tfrac18$ of the printed chain.

Theorem 1 is false for arbitrary distributions of priorities or coins. A formalization that takes "Pr" as an unconstrained parameter, conditions on the event of interest, or replaces $n$ by $|V'|$ does not state the paper's theorem.

A complete development needs finite product probability spaces, inclusion–exclusion (Bonferroni) inequalities for finite unions, the symmetry of uniform priorities conditioned on injectivity, and degree-sum identities (SimpleGraph.sum_degrees_eq_twice_card_edges). The Technical Lemma and milestones 5 and 6 are reusable beyond this mission. Proofs of any milestone, and alternative proofs of Lemmas A and B, 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
R. Motwani and P. Raghavan, Randomized Algorithms, Cambridge University Press, 1995. https://doi.org/10.1017/CBO9780511814075

8 thms3 active usersReviewed

Combinatorics Operations Research Optimization·Captain: mikedeng1

Worst-Case Performance Bounds for Simple One-Dimensional Packing Algorithms 4: First-Fit Decreasing Uses at Most 71/60 L* + 5 Bins When No Item Exceeds 1/2Research Paper

Motivation

Bin packing asks how to place a list of items with sizes in $(0,1]$ into as few unit-capacity bins as possible. It models the cutting of stock material, the packing of files onto tracks of a disc and the assignment of jobs to machines with a common deadline. Deciding the optimum is NP-hard, so in practice simple rules are used, and the question is how far they can stray from the optimum in the worst case.

Johnson, Demers, Ullman, Garey and Graham (SIAM J. Comput. 3(4), 1974) gave the first sharp worst-case bounds for the four classical rules. For First-Fit Decreasing (FFD), the rule that sorts the items into nonincreasing order and then places each into the first bin with room, they announced the bound $FFD(L)\le\frac{11}{9}L^*+4$ , whose full proof in Johnson's thesis exceeds 75 pages. To show the method, Section 4 of the paper proves a simpler bound in detail: when no item exceeds $1/2$ , FFD uses at most $\frac{71}{60}L^*+5$ bins. That result is the subject of this mission.

Timeline:

1973: D. S. Johnson's MIT thesis, Near-optimal bin packing algorithms, contains the complete proofs of the $11/9$ and $71/60$ bounds.
1974: Johnson, Demers, Ullman, Garey and Graham publish the $71/60$ bound for lists in $(0,1/2]$ (Theorem 4.1) with a proof that is complete except for parts of two lemmas, and show by example that $71/60$ cannot be lowered.
1985: B. S. Baker gives a shorter proof of the $11/9$ bound for FFD (J. Algorithms 6, 1985).
2007: G. Dósa determines the tight additive constant $6/9$ in the $11/9$ bound (ESCAPE 2007, LNCS 4614).

Setting

A list is a finite sequence $L=(a_1,\dots,a_n)$ of real numbers in $(0,1]$ ; values may repeat. A bin has capacity $1$ ; its level is the sum of the numbers in it. The optimum $L^*$ is the least number of bins into which the elements of $L$ can be placed with no bin level exceeding $1$ .

First-Fit places $a_1,a_2,\dots$ in order into bins $B_1,B_2,\dots$ , each initially at level $0$ : $a_i$ goes into the bin of least index whose level $\beta$ satisfies $\beta\le 1-a_i$ . First-Fit Decreasing first arranges $L$ into nonincreasing order and then runs First-Fit. $FFD(L)$ is the number of bins it uses.

The proof uses a weight $W$ on finite sets of elements. For an integer $k\ge1$ , $x$ is a $k$ -piece if $x\in(\frac1{k+1},\frac1k]$ , and a $k$ -bin is a bin whose largest element is a $k$ -piece. Set $w_1(x)=\lfloor 1/x\rfloor^{-1}$ . A pair $(x,y)$ obeys relation $k$ if $x$ is a $k$ -piece and $kx+y\le1$ ; then $w_2(x,y)=w_1(x)+\frac{k-1}{k}w_1(y)$ , and otherwise $w_2(x,y)=w_1(x)+w_1(y)$ . For a partition $\pi$ of $X$ into one- and two-element sets, with each pair ordered (earlier, later) in the nonincreasing order,

w_{12}(\pi)=\sum_{\{x\}\in\pi}w_1(x)+\sum_{(x,y)\in\pi}w_2(x,y),\qquad W(X)=\min_\pi w_{12}(\pi).

BASIC is the set of elements of $L$ that are $k$ -pieces lying in a $k$ -bin of the FFD packing of $L$ , for some $k$ ; SURPLUS is the rest of $L$ .

Formalization targets

Goal: Theorem 4.1

\text{for every list } L\subseteq(0,\tfrac12]:\qquad FFD(L)\le\frac{71}{60}L^*+5 .

The constants are those printed in the paper. The multiplicative constant $71/60$ is best possible.

Milestones

Lemma 3.3 (FFD part): if $FFD(L)>rL^*+d$ with $r,d\ge1$ , the list $L'$ of the elements of $L$ exceeding $(r-1)/r$ also has $FFD(L')>rL'^*+d$ .
Claim 4.2.1: for $N\ge4$ and $L\subseteq(\frac1N,\frac12]$ , $\sum_{x\in\mathrm{BASIC}}w_1(x)\ge FFD(L)-\sum_{j=2}^{N-1}\frac{j-1}{j}$ .
Claim 4.2.2: for $N\ge4$ , $L\subseteq(\frac1N,\frac12]$ and every partition $\pi$ of $L$ into one- and two-element sets, $w_{12}(\pi)\ge w_1(\mathrm{BASIC})-\sum_{j=3}^{N-1}\frac1j$ .
Lemma 4.2: for $N\ge4$ and $L\subseteq(\frac1N,\frac12]$ , $W(L)\ge FFD(L)-N+2$ .
Subadditivity: $W(X_1\cup\dots\cup X_k)\le\sum_i W(X_i)$ .
Lemma 4.3: if $X\subseteq(\frac17,\frac12]$ and $\sum_{x\in X}x\le1$ , then $W(X)\le\frac{71}{60}$ .

A companion item states the Remark after Theorem 4.1: for every $N\ge1$ there is a list with all elements below $1/3$ , $L^*=60N$ and $FFD(L)=71N$ .

Significance

Theorem 4.1 shows the weighting-function method in its simplest nontrivial form: a weight whose total is within a constant of the algorithm's bin count, and which no feasible bin can exceed by more than the target ratio. The same method, with more elaborate weights, gives the $11/9$ bound for FFD, and it is the model for later worst-case analyses of packing heuristics. The Remark shows that $71/60$ is exact for items in $(0,1/2]$ , and the Corollary on p. 322 extends the analysis to the asymptotic ratio $R^\alpha_{FFD}$ when items are bounded by $\alpha\in(8/29,1/2]$ .

The source proof is partial. The billing argument behind Claim 4.2.2 is given only when two auxiliary conditions (G1) and (G2) hold ("The more intricate argument here omitted", p. 321), and Lemma 4.3 is checked in four of about seventy-four cases ("leaving the remaining 70-odd, more or less routine, cases to the ambitious reader", p. 321). Complete details are in Johnson's thesis. The theorem itself is established. A formalization therefore gives the first complete, checked proof in a single place. The finite case analysis of Lemma 4.3 is well suited to machine checking. No machine-checked proof of any FFD bound is known to exist.

Difficulty

The obvious weight $w_1$ alone fails. Claim 4.2.1 shows that $w_1(\mathrm{BASIC})$ covers the FFD bins, but many sets $X$ of elements with sum at most $1$ have $w_1(X)>71/60$ , for example two $2$ -pieces, a $5$ -piece and a $6$ -piece. The pair discounts of $w_2$ repair Lemma 4.3, but they must then be paid for in Lemma 4.2, for every partition. That is Claim 4.2.2: a charge from each discounted pair to distinct SURPLUS elements that are no larger. The charge is straightforward only when no member of a pair obeying relation $k$ lies in a bin of type $k'<k$ . In general a pair's larger element may already have been charged by a smaller relation, and the paper omits the argument that handles this. Lemma 4.3 is elementary but has many cases, each determined by the piece types in $X$ and the relations they obey.

Formalization scope

A list is L : List ℝ with IsList L ( $0<a\le1$ for each element) in every statement. $L^*$ is optBins L, the least $b$ such that some map from positions to Fin b has every bin sum at most $1$ . The First-Fit run keeps the nonempty bins as a List (List ℝ), and opens a new bin at the end exactly when no existing bin fits, which is the paper's "least $j$ ". The fit test is $\beta+a\le1$ . FFD is First-Fit on sortDesc L, the mergeSort into nonincreasing order; ties do not affect the bin count. Indices are $0$ -based.

$W(X)$ sorts $X$ into nonincreasing order and minimises $w_{12}$ over the involutions of its positions: fixed points are singletons, and a pair $i<\sigma(i)$ is oriented (larger, smaller). The minimum is over a finite nonempty set, so it is attained. BASIC is a set of positions of sortDesc L, and each position's bin is its bin in the final FFD packing. In $w_2$ , $k=\lfloor1/x\rfloor$ is the piece type of the first element. Sums $\sum_{j=2}^{N-1}$ are over Finset.Icc 2 (N - 1) with $N\ge4$ .

The goal's range is $(0,1/2]$ . The restriction to $(1/7,1/2]$ belongs only to the proof, through Lemma 3.3. Stating the goal for $(1/7,1/2]$ , weakening $71/60$ or $5$ , or making $W$ an unattained infimum would each change the theorem. Only the FFD half of Lemma 3.3 is stated. Claim 4.2.1 is stated with Lemma 4.2's standing hypothesis $N\ge4$ . The Remark's printed range $0<\varepsilon\le5/87$ is a misprint: its FFD packing needs $\varepsilon<1/174$ , and the companion item states only the existence claim.

Infrastructure needed: a usable API for the First-Fit run (the invariants of the fold, bin levels, the order of bins), a lemma that FFD bins receive items in nonincreasing order, and a decision procedure for Lemma 4.3's case analysis over piece types. The model file and the weight file are reusable for the $11/9$ bound (mission 3 of this series) and for the bounded- $\alpha$ corollaries. Contributions of proofs of Lemma 4.3 by computer-checked case enumeration, and of the missing general case of Claim 4.2.2, are especially welcome.

Selected references

D. S. Johnson, A. Demers, J. D. Ullman, M. R. Garey, R. L. Graham, Worst-Case Performance Bounds for Simple One-Dimensional Packing Algorithms, SIAM J. Comput. 3(4):299–325, 1974. https://doi.org/10.1137/0203025
D. S. Johnson, Near-Optimal Bin Packing Algorithms, Ph.D. thesis, Massachusetts Institute of Technology, 1973 (reference [8] of the paper).
B. S. Baker, A new proof for the first-fit decreasing bin-packing algorithm, J. Algorithms 6, 1985.
G. Dósa, The tight bound of first fit decreasing bin-packing algorithm is FFD(I) ≤ 11/9 OPT(I) + 6/9, ESCAPE 2007, Lecture Notes in Computer Science 4614, 2007.

9 thms3 active usersReviewed

Theoretical Computer Science

Missions

Eigenvalues and Expanders: A Regular Bipartite Graph Is a Strong Expander If and Only If λ(G) Is Bounded Away from 0Research Paper

Motivation

Setting

Formalization targets

Goal: Theorem 3.4

Milestones, in the order of the paper

Significance

Difficulty

Formalization scope

Selected references

Online Primal-Dual Algorithms for Maximizing Ad-Auctions Revenue: The Competitive Ratio of the Primal-Dual Allocation AlgorithmResearch Paper

Motivation

Setting

Formalization targets

Goal: Theorem 1

Milestones

Significance

Difficulty

Formalization scope

Selected references

Polynomial-Time Algorithms for Prime Factorization and Discrete Logarithms on a Quantum Computer 3: The Success Probability of Quantum Order FindingResearch Paper

Motivation

Setting

Formalization targets

Goal: success probability at least φ(r)/3r\varphi(r)/3rφ(r)/3r

Milestones

Significance

Difficulty

Formalization scope

Selected references

Competitive Randomized Algorithms for Nonuniform Problems IV: The Optimal Randomized Two-Server Ratio 1652/1069 on the 3-4-5 TriangleResearch Paper

Motivation

Setting

Formalization targets

Goal: Theorem 13

Milestones

Significance

Difficulty

Formalization scope

Selected references

Competitive Randomized Algorithms for Nonuniform Problems III: The Optimal Randomized Two-Server Ratio on the 1-d-d Isosceles TriangleResearch Paper

Motivation

Setting

Formalization targets

Goal: Theorem 12

The phase LP (§5, pp. 565–566)

The limit remark (§5, p. 566)

Significance

Difficulty

Formalization scope

Selected references

Maximizing Non-Monotone Submodular Functions V: Beating 1/2 for Symmetric Functions Requires Exponentially Many Value QueriesResearch Paper

Motivation

Setting

Formalization targets

Goal: Theorem 4.5 with the constants of its proof

Milestones

Significance

Difficulty

Formalization scope

Selected references

Maximizing Non-Monotone Submodular Functions IV: Smooth Local Search Achieves 2/5 of the OptimumResearch Paper

Motivation

Setting

Formalization targets

Goal: Theorem 3.6 in the explicit form of its proof

Milestones, in attack order

Significance

Difficulty

Formalization scope

Selected references

Three Partition Refinement Algorithms 1: Distinguishing-Prefix Refinement Finds Every Distinguishing Prefix Within m′ Refinement StepsResearch Paper

Motivation

Setting

Formalization targets

Goal: Theorem 1 with its explicit bound

Milestones

Significance

Goal: success probability at least $\varphi(r)/3r$