Graph Theory

Motivation

Minimum-cost circulation asks how to route flow around a directed network without accumulating flow at any vertex, while minimizing the total cost of the routed units. It is a basic network optimization problem: lower-bound and demand constraints in many flow models can be converted into circulation form. Goldberg and Tarjan's 1987 technical report develops a successive-approximation approach in which a local repair subroutine, refine, improves an approximately optimal circulation. The report was followed by a 1990 journal article; all theorem numbers and page citations in this mission refer to the 1987 report.

The mission isolates the generic form of refine, where an implementation may choose any applicable update at each step. Its question is whether every such choice sequence finishes after a controlled number of operations and returns a circulation with a stronger optimality certificate. The related Goldberg–Tarjan maximum-flow algorithm uses push and relabel operations with distance labels; here the labels are real-valued prices tied to arc costs. The authors' cycle-canceling work uses the same circulation network model and supplies published definitions reused in this development.

Setting

A circulation network has a finite vertex set $V$ and a symmetric set $E$ of directed arcs: whenever $(v,w)$ is an arc, so is $(w,v)$. Let $n=|V|$ and $m=|E|$, counting both orientations. Each arc has a real capacity $u(v,w)$ and cost $c(v,w)$, with $c(v,w)=-c(w,v)$. A pseudoflow $f$ respects capacities and the paired-arc relation $f(v,w)=-f(w,v)$. Its excess $e_f(v)$ is the sum of flow entering $v$. A circulation is a pseudoflow with zero excess everywhere. The already published CycleCanceling.MinMean.Network supplies this network, its circulation predicate, and residual capacity $u_f(v,w)=u(v,w)-f(v,w)$. An arc is residual when this capacity is positive.

A price function $p:V\to\mathbb R$ changes an arc's reduced cost to $c_p(v,w)=c(v,w)-p(v)+p(w)$. A pseudoflow is $\varepsilon$-optimal with respect to $p$ when every residual arc has reduced cost at least $-\varepsilon$. A vertex is active when its excess is positive. An admissible arc is a residual arc of negative reduced cost. Refine takes an input circulation that is $2\varepsilon$-optimal, saturates every arc whose reduced cost is negative, and then repeatedly applies an available update. A push sends flow from an active vertex along an admissible arc. A relabel raises the price of an active vertex with no outgoing admissible arc to the largest value permitted by $\varepsilon$-optimality. These rules are Figures 4 and 5, printed pages 18–19.

Formalization targets

The supporting targets are the paper's progress and correctness results, its price bound, and the three operation counts. For any generic refine run from a $2\varepsilon$-optimal circulation, Lemma 5.8 bounds each vertex's price increase by $3n\varepsilon$. Lemmas 5.9–5.11 bound the numbers $R,S,T$ of relabelings, saturating pushes, and nonsaturating pushes:

$$R\leq 3n(n-1),\qquad S\leq 3nm,\qquad T\leq 3n^2(m+n).$$

The goal combines the resulting bound on the number $K$ of updates with progress and correctness:

$$K\leq 3n(n-1)+3nm+3n^2(m+n).$$

If the final state has an active vertex, another update exists. If no update applies, the final pseudoflow is a circulation and is $\varepsilon$-optimal with respect to its final prices. This is the explicit operation-count content behind the generic subroutine's analysis in Section 5. It does not claim a bound for a particular data structure or a complete minimum-cost algorithm.

Significance

The theorem gives an order-independent finite bound: the choice of which applicable push or relabel to perform cannot cause generic refine to run forever or stop with an active vertex. Its output is a circulation whose approximate-optimality tolerance has been halved. That output can serve as the next input in the successive-approximation framework. For integral costs, the report's Theorem 2.3 later turns a sufficiently small tolerance into exact minimum cost; that outer-loop result is outside this mission.

This mission specifies the generic cost-scaling state machine in Lean and poses its quantitative analysis as open formalization targets. The shared network and circulation definitions from the published Goldberg–Tarjan 1989 series are available, and a related generic maximum-flow theorem in the 1988 series has a machine-checked proof. Those results do not prove refine's price-based bounds. Contributions that establish the paper's progress, price, or counting statements for this state machine, and reusable facts about finite residual networks, advance the open goal.

Difficulty

A push respects a capacity, but it can create activity at another vertex; a relabel changes which arcs are admissible. Thus checking a single update does not bound an arbitrary sequence. The price bound also depends on the circulation and prices supplied at entry, not merely on the current pseudoflow being $\varepsilon$-optimal. Finally, a vertex with no admissible outgoing arc may appear to be stuck when the relabel minimum is over an empty set. Feasibility of the original circulation network is needed to establish that an active vertex still has a genuine next update. The operation bound requires accounting for the three update types across every possible choice sequence.

Formalization scope

Vertices form a finite type, and capacities, costs, flows, and prices are real-valued functions. The network has symmetric ordered arcs and antisymmetric costs. There is no separate nonnegativity assumption on capacities; feasibility is supplied by the input circulation. The new $\varepsilon$ is positive, so the entry circulation is $2\varepsilon$-optimal before Figure 4 halves the error parameter. The run starts from the resulting saturated pseudoflow and records one applicable push or relabel per index $k<K$. Counts classify those actual steps by the selected arc's residual capacity after a push. Termination is the negation of the paper's loop guard, not a definition that assumes zero excess.

The reduced-cost sign is $c-p(v)+p(w)$, and relabel raises $p(v)$. This differs from the published 1989 epsilon-optimality definition, so only its network model is imported. The relabel relation requires an attained minimum over a nonempty set of outgoing residual arcs; it assigns no default value to an empty minimum. Loops may occur in the reused network model, but cost antisymmetry makes their reduced cost zero, so they cannot be push arcs. The explicit constants are the report's $3n\varepsilon$, $3n(n-1)$, $3nm$, and $3n^2(m+n)$; the goal sums the last three. The report's RAM-model $O(\cdot)$ running times are outside the formal statements. A definition that makes termination equivalent to conservation or assigns an arbitrary relabel price at an empty set would miss the target.

Selected references

• Andrew V. Goldberg and Robert E. Tarjan, Finding Minimum-Cost Circulations by Successive Approximation, MIT/LCS/TM-333, July 1987. Technical report.
• Andrew V. Goldberg and Robert E. Tarjan, Finding Minimum-Cost Circulations by Successive Approximation, Mathematics of Operations Research 15(3), 1990, pp. 430–466. DOI. The report above supplies this mission's numbering.
• Andrew V. Goldberg and Robert E. Tarjan, A New Approach to the Maximum-Flow Problem, Journal of the ACM 35(4), 1988. DOI.
• Andrew V. Goldberg and Robert E. Tarjan, Finding Minimum-Cost Circulations by Canceling Negative Cycles, Journal of the ACM 36(4), 1989. DOI.

Motivation

The diameter of a polyhedron is the largest number of edges needed to travel between two vertices of its graph, its 1-skeleton. Whether this number is bounded by a polynomial in the dimension $d$ and the number of facets $n$ is a long-standing open question in polyhedral combinatorics; edge walks are the moves of vertex-following methods such as the simplex method, so the question bounds what any such method can achieve in the worst case. For fixed dimension, Larman proved in 1970 that the diameter grows at most linearly in $n$, with a constant exponential in $d$ (Larman 1970).

Eisenbrand, Hähnle, Razborov and Rothvoß ask how much of the geometry of polyhedra such upper bounds actually use. They isolate a single combinatorial path property shared by the graphs of non-degenerate polyhedra and announce that the known upper bounds, Larman's among them, "continue to hold in the base abstraction" defined by that property (Dagstuhl abstract, p. 3). The next sentence of the abstract reads: "While the first bound is merely an adaption of the proof in [13], our proof of the second bound is much simpler than the one which was proved for polyhedra in [16]."

The held source is the five-page Dagstuhl extended abstract dated June 15, 2010, which states the results and proves none of them. The full proofs appear in Mathematics of Operations Research 35 (2010), 786–794 (journal article). The goal is an asserted theorem of the paper, not an open conjecture; the formal proof remains to be supplied.

Setting

Let $[n]=\{1,\ldots,n\}$ and write $\binom{[n]}{d}$ for the family of its $d$-element subsets. A graph $G=(V,E)$ in the base abstraction has a nonempty vertex set $V\subseteq\binom{[n]}{d}$: every vertex is a $d$-element set of labels, and distinct vertices carry distinct sets. The edges are arbitrary subject to condition i): for each $u,v\in V$ there exists a path connecting $u$ and $v$ whose intermediate vertices all contain $u\cap v$. Condition i) makes $G$ connected. The class of all such graphs is $\mathcal B_{d,n}$; $d$ is called the dimension and $n$ the number of facets of the abstraction, and $D(d,n)$ denotes the largest diameter of a graph in $\mathcal B_{d,n}$ (p. 2).

The distance $\operatorname{dist}_G(u,v)$ is the least number of edges of a path from $u$ to $v$. The motivating example is the graph of a non-degenerate polyhedron (each vertex on exactly $d$ facets), each vertex labelled by its $d$ facets: two vertices are joined by a path inside the minimal face containing both, and every vertex of that path lies on the facets the two endpoints share (pp. 2–3). The class $\mathcal B_{d,n}$ is not restricted to such graphs.

Formalization targets

Larman's bound in the base abstraction

The abstract prints the bound as $\Delta_u(d,n)\le 2^{d-1}\cdot n$ and states that it continues to hold in the base abstraction. The target is the pointwise form of $D(d,n)\le 2^{d-1}\, n$:

$$\forall d\ge 1,\ \forall n,\ \forall G\in\mathcal B_{d,n},\ \forall u,v\in V(G):\qquad \operatorname{dist}_G(u,v)\le 2^{d-1}\, n .$$

In Lean this is the existence, for every pair $u,v$, of a walk from $u$ to $v$ with at most $2^{d-1}n$ edges. The statement quantifies over every graph satisfying the paper's definition, not over polyhedron graphs or a chosen family.

Significance

For fixed $d$ the bound is linear in $n$, and it holds for a class defined only by finite sets and one path condition. Together with the almost-quadratic lower bound $D(n/4,n)=\Omega(n^2/\log n)$ announced in the same paper, it shows what this one property of polyhedra can and cannot deliver: linear growth in $n$ for fixed dimension, but not a linear bound uniform in $d$ and $n$. Since the graph of every non-degenerate polyhedron lies in $\mathcal B_{d,n}$ (a separate mission of this series), the result also recovers a Larman-type bound for polyhedra, with constant $2^{d-1}$.

Prove2Me already has proved polytope versions: Hirsch.larman_bound (the sharper constant $n\,2^{d-3}$ for nonempty bounded $H$-polytopes), Hirsch.larman_high_dimension, Hirsch.larman_layer_recursion, and Hirsch.tight_row_interval, the polytope form of the interval property that condition i) abstracts. They concern a different object, the vertex-edge graph of an $H$-polytope, and are credited as prior work; none states the bound for every graph of $\mathcal B_{d,n}$. The platform definition Hirsch_clf (connected layer families) is a related abstraction in layered form and is not the graph class used here.

Difficulty

The class contains graphs with no geometric realization, so a proof cannot use convexity, faces as polyhedra, or linear-algebraic facts about vertices; only labels, intersections and walks are available. Condition i) guarantees a path preserving the common labels of two endpoints, but says nothing directly about the length of that path. Mere connectivity on $d$-subsets of $[n]$ gives only the trivial bound $|V|-1\le\binom{n}{d}-1$, which is far from linear in $n$. A linear bound in $n$ has to be extracted from condition i) alone, uniformly over all graphs of the class. The abstract describes its proof only as much simpler than Larman's for polyhedra and states no intermediate lemma, so the mission carries no milestones.

Formalization scope

• $[n]$ is represented by Fin n, labels $0,\ldots,n-1$; only the number of labels matters.
• A vertex set is V : Finset (Finset (Fin n)) and the graph is G : SimpleGraph V; vertices are therefore distinct label sets, as in the paper. InB d n V G requires V.Nonempty, every vertex of cardinality $d$, and CondI V G.
• CondI asks for a walk all of whose vertices contain $u\cap v$. This is the source's path condition: a walk contains a path on a subset of its vertices, and the endpoints contain $u\cap v$ automatically.
• "Continue to hold in the base abstraction" is read as the bound for every graph of $\mathcal B_{d,n}$ and every pair of its vertices. No numeric $D(d,n)$ is defined, so no supremum with a default value enters; a bounded walk witnesses the distance bound.
• $d\ge 1$ is an explicit hypothesis: $d$ is the dimension, and it makes $d-1$ ordinary subtraction in $\mathbb N$. At $d=0$ the class consists only of the one-vertex graph on $\emptyset$, so nothing is lost. For $n<d$ the class is empty.
• The constant is $2^{d-1}$, the paper's constant for the abstraction; the polytope constant $2^{d-3}$ of Hirsch.larman_bound is not claimed here.

Trivializing formalizations are ruled out: labels are the vertices themselves (not an arbitrary labelling that could repeat), and condition i) is required for all pairs, not for one chosen path or only adjacent vertices. A proof only for polyhedron graphs, for graphs with extra structure, or with a larger constant leaves the goal open. Useful contributions include general lemmas about CondI and walk-length bookkeeping for SimpleGraph on a finite vertex type; these are reusable by the other missions of this series.

Selected references

• F. Eisenbrand, N. Hähnle, A. Razborov, T. Rothvoß, Diameter of Polyhedra: Limits of Abstraction, Dagstuhl Seminar Proceedings 10211 (Flexible Network Design), 2010. https://drops.dagstuhl.de/opus/volltexte/2010/2724
• F. Eisenbrand, N. Hähnle, A. Razborov, T. Rothvoß, Diameter of Polyhedra: Limits of Abstraction, Mathematics of Operations Research 35(4), 786–794, 2010. https://doi.org/10.1287/moor.1100.0470
• D. G. Larman, Paths on polytopes, Proceedings of the London Mathematical Society (3) 20, 161–178, 1970. https://doi.org/10.1112/plms/s3-20.1.161

Motivation

The diameter of a polyhedron is the largest number of edges needed to travel between two vertices of its graph. Bounding that number from the dimension and the number of facets is a central question in polyhedral combinatorics because edge walks are the discrete moves available to many vertex-based optimization methods. The Kalai–Kleitman bound gives a quasi-polynomial upper bound in these parameters. Eisenbrand, Hähnle, Razborov and Rothvoß ask how much of the geometry is needed to retain such a bound. They isolate one path property of polyhedron graphs and show that the upper bound persists for every graph satisfying it, including graphs that need not arise from a polyhedron (Dagstuhl abstract, pp. 1–3).

This mission concerns that extension of the Kalai–Kleitman bound. The held source is the five-page Dagstuhl extended abstract dated June 15, 2010. It states the result without its proof. The full proofs appeared in Mathematics of Operations Research 35 (2010), 786–794 (journal article). The goal is an asserted result of the paper, not an open conjecture; the formal proof remains to be supplied.

Setting

Let $[n]=\{1,\ldots,n\}$, and let $\binom{[n]}{d}$ be the family of its $d$-element subsets. A graph $G=(V,E)$ in the paper's base abstraction has a nonempty vertex set $V\subseteq\binom{[n]}{d}$. Thus each graph vertex is labelled by a distinct $d$-element subset. The edges can be chosen freely subject to condition i): for every pair $u,v\in V$, there is a path from $u$ to $v whose intermediate vertices all contain$u\cap v$. The condition implies that the graph is connected. The paper denotes the class of these graphs by$\mathcal B_{d,n}$and calls$d$the dimension and$n$ the number of facets of the abstraction (definition and footnote, p. 2).

The distance between two vertices is the minimum number of edges in a path between them. A graph's diameter is the largest of these distances, and $D(d,n)$ is the largest diameter among graphs in $\mathcal B_{d,n}$. Condition i) is motivated by non-degenerate polyhedra: if a vertex lies on exactly $d$ facets, its tight facets provide a $d$-element label, and two vertices can be connected inside the smallest face containing them. Every vertex on that path retains the facets common to the endpoints (pp. 2–3). This motivation does not restrict $G$ to a realizable polyhedron graph.

Formalization targets

Kalai–Kleitman bound in the base abstraction

For positive dimension, the target is the pointwise form of the paper's assertion that the upper bound continues to hold in the base abstraction:

$$\forall d\geq 1,\ \forall n,\ \forall G\in\mathcal B_{d,n},\ \forall u,v\in V(G),\quad \operatorname{dist}_G(u,v)\leq n^{1+\log_2 d}.$$

Equivalently, every pair has a connecting path with at most $n^{1+\log_2 d}$ edges. Consequently $D(d,n)\leq n^{1+\log_2 d}$. The statement covers every graph with the paper's labels and condition i), rather than a selected realization or a graph with extra geometric properties. The source prints the inequality for $\Delta_u(d,n)$, its polyhedron-diameter notation, and says in the same sentence that it continues to hold for the base abstraction (p. 3).

Significance

The bound shows that a common-facet path property is enough to prevent arbitrarily large diameter once $d$ and $n$ are fixed. It extends an upper bound first attached to graphs of polyhedra to a class specified entirely by finite sets and graph paths. This locates a concrete portion of the polyhedral diameter theory within combinatorics. The same paper gives an almost-quadratic lower bound for the abstraction, so the path property alone does not imply a linear bound in $n$ (p. 3).

A machine-checked proof would connect a precise finite graph model with the real-exponent inequality, without relying on a polyhedron representation. Prove2Me already has a proved theorem called Hirsch.kalai_kleitman_bound for a bounded $H$-polytope, with a different exponent $\log_2 d+2$, and a proved Hirsch.kalai_kleitman_recursion for that polytope model. It also has Hirsch.clf_endpoint_peeling for connected layer families. Those results concern different objects or bounds and are useful prior work, but none is a formalization of the present claim for all $G\in\mathcal B_{d,n}$.

Difficulty

The class permits edges and vertex families with no geometric realization, so a proof cannot use metric or convexity properties of a particular polyhedron. Condition i) guarantees one path preserving the common labels of two endpoints; it does not directly bound that path's length. Connectivity by itself would be too weak: a connected graph on the allowed labels can have a long shortest path unless its labels and the path condition constrain it. The formal task is to obtain the claimed uniform length bound from that condition across all finite families of $d$-sets. The Dagstuhl abstract calls the argument an adaptation of Kalai and Kleitman's proof but states no intermediate lemmas, so this proposal does not assign any in-source milestones (p. 3).

Formalization scope

Lean represents $[n]$ by Fin n, with labels $0,\ldots,n-1$ instead of $1,\ldots,n$; only the number of labels matters. A vertex set is a Finset of Finset (Fin n), and a SimpleGraph has exactly those sets as vertices. This representation enforces distinct labels. InB d n V G requires $V$ to be nonempty, every label to have cardinality $d$, and CondI for every ordered pair. The walk in CondI is equivalent to the source's path: repeated vertices can be erased, and the endpoints themselves contain $u\cap v$. Nonemptiness and condition i) together give the source's connectedness. A path through all graph vertices without the common-intersection condition would be a weaker and inadmissible model.

The theorem takes $d\geq1$, so the logarithm has its ordinary positive-dimension interpretation. The source does not print a logarithm base; the statement reads it as base two, following the cited Kalai–Kleitman convention. This interpretation is explicit in the theorem's prose and is an open source-reading question. The exponent is real: the path length is cast from a natural number to $\mathbb R$ for comparison with $(n:\mathbb R)^{1+\log_2 d}$. No floor is applied to the exponent. The theorem asserts a bounded walk for each pair; that avoids defining $D(d,n)$ through a supremum with an artificial value for an empty class. At $n=0$ with $d\geq1$, InB has no instance, as there are no $d$-element labels; at $d=1$, the bound is $n$, consistent with a connected graph on at most $n$ labels.

The development needs reusable finite-set reasoning about common intersections, graph walks and their lengths, and real-logarithm bounds. Contributions establishing those facts for the paper's CondI model are within scope. A proof only for polyhedron graphs, for graphs with extra edge restrictions, or for a single chosen graph would leave the goal open.

Selected references

• F. Eisenbrand, N. Hähnle, A. Razborov and T. Rothvoß, Diameter of Polyhedra: Limits of Abstraction, Dagstuhl Seminar Proceedings 10211, 2010. Extended abstract.
• F. Eisenbrand, N. Hähnle, A. Razborov and T. Rothvoß, Diameter of Polyhedra: Limits of Abstraction, Mathematics of Operations Research 35, 786–794, 2010. DOI.

Motivation

Finding the quickest route between two points of a road network is among the oldest problems of operations research. It is the subproblem inside vehicle routing, network flow and many dynamic programs. Richard Bellman's four-page note On a routing problem (Quarterly of Applied Mathematics, 1958) treats it as a dynamic program. The minimal travel times satisfy a nonlinear system of equations, and that system can be solved by successive approximations that terminate after a number of steps bounded in advance. The iteration is now known as the Bellman–Ford method. A footnote added in proof records that Max Woodbury and George Dantzig had obtained the same scheme independently, and Ford's RAND report of 1956 describes a closely related labelling procedure.

Timeline.

• 1956. L. R. Ford Jr., Network flow theory (RAND P-923): a label-improving procedure for shortest paths.
• 1957. Bellman's Dynamic Programming (Princeton) states the principle of optimality used here.
• 1958. Bellman's note: the routing equation, its uniqueness, approximation in policy space with an (N − 1)-step bound, and a second, monotone increasing scheme.
• 1959. Dijkstra gives a label-setting method for nonnegative lengths.
• 1962. Floyd's Algorithm 97 computes all pairs of shortest distances.

Setting

There are $N$ cities, numbered $1, \dots, N$. Every two of them are linked by a direct road, and city $N$ is the destination. The travel time from $i$ to $j$ is a real number $t_{ij}$; the matrix $T = (t_{ij})$ need not be symmetric. Throughout, $t_{ij} > 0$ for $i \ne j$.

A route from $i$ to $N$ is a sequence of cities $i = c_0, c_1, \dots, c_m = N$ in which consecutive cities differ. Its stops are $c_1, \dots, c_{m-1}$, and its time is $\sum_{r<m} t_{c_r c_{r+1}}$. The minimal time $f_i$ (3.1) is the least time of a route from $i$ to $N$, and $f_N = 0$.

The routing equation (3.2) is the system

$$F_i = \min_{j \ne i}\,[t_{ij} + F_j]\quad (i = 1, \dots, N-1), \qquad F_N = 0 .$$

Approximation in policy space (§5) starts from the direct-route policy (5.2), $f_i^{(0)} = t_{iN}$, and iterates (5.1):

$$f_i^{(k+1)} = \min_{j \ne i}\,[t_{ij} + f_j^{(k)}]\quad (i \ne N), \qquad f_N^{(k+1)} = 0 .$$

The second scheme (§7, (7.1)) starts instead from $\underline f_i^{(0)} = \min_{j\ne i} t_{ij}$ and uses the same step.

Formalization targets

Goal: convergence within $N - 1$ iterations

For every $k \ge N - 1$ the following hold. Each $f_i^{(k)}$ is the minimal time from $i$ to $N$, attained by a route. The vector $f^{(k)}$ solves (3.2). Every real solution of (3.2) equals $f^{(k)}$:

$$k \ge N-1 \;\Longrightarrow\; f^{(k)} = f = \text{the unique solution of (3.2)}.$$

This is the claim of the Summary ("converges after at most $(N-1)$ iterations") and of the last sentence of §5. The paper's bound $N - 1$ is kept, although $N - 2$ also suffices.

Milestones

1. (3.2): the minimal times exist and satisfy the routing equation.
2. §4: (3.2) has at most one solution.
3. (5.4): $f^{(1)} \le f^{(0)}$.
4. §5, the sentence after (5.4): $f_i^{(k)}$ is the minimal time over routes with at most $k$ stops.
5. (5.5): $f^{(k+1)} \le f^{(k)}$ for all $k$.
6. §7: the scheme (7.1) increases, stays below the solution of (3.2) (7.2), and equals it from some index on.

Significance

The result. The note turns an enumeration over exponentially many paths into $N - 1$ rounds of $N$ minimisations each, with a bound fixed before the computation starts. The uniqueness theorem makes the routing equation a characterisation of the minimal times, not merely a property of them. This is the template for later correctness proofs of shortest-path and value-iteration algorithms. The monotone decrease (5.5) is the first instance of policy improvement: every iterate is the value of an actual routing policy.

Formalizing it. The results are classical and proved. What this mission adds is a machine-checked development against the paper's own objects. Routes, their times and minimal times are defined from scratch. The iteration is stated exactly as printed, apart from the corrected initial value at the destination. The (N − 1)-step termination is asserted as an equality, not a limit. Related platform items treat other methods and do not cover these statements. One is the label-correcting method (BertsekasDP.label_correcting_correctness_of_nonneg_arcs, BertsekasDP.label_correcting_terminates). Another is the stochastic shortest path problem under a termination assumption that fails for deterministic routing (BertsekasDP.ssp_main_theorem). There are also the generic candidate-list algorithm (BertsekasNetwork.generic_shortest_path_algorithm), Floyd's Algorithm 97 and Dijkstra's method.

Difficulty

The minimum in (3.2) may be attained at a $j$ whose own optimal route passes back through $i$. The routing equation is a fixed-point equation for an operator that is monotone but not a contraction in any fixed norm. The standard contraction argument for discounted dynamic programs therefore does not apply. Uniqueness has to use $t_{ij} > 0$ to exclude zero-time cycles: with $t_{12} = t_{21} = 0$, the system (3.2) has infinitely many solutions. The $N - 1$ bound depends on the at-most-$k$-stops reading of $f^{(k)}$ and on the fact that an optimal route never needs to revisit a city. Neither is visible from the recursion alone. For the scheme of §7, the page gives no bound on the number of iterations, and none holds uniformly in $t$.

Formalization scope

Cities are Fin (n + 1), so $N = n + 1$, with standing hypothesis $n \ge 1$. City $N$ is Fin.last n, and travel times are t : Fin (n + 1) → Fin (n + 1) → ℝ with $t_{ij} > 0$ for $i \ne j$. Diagonal entries are unconstrained and never used. No symmetry, triangle inequality or integrality is assumed. A route is a list of cities with distinct consecutive entries ending at $N$. Repeated cities are allowed; with positive times this changes no minimum. Minimal times are attained minima over routes (IsMinTime, IsMinTimeWithin), not real infima. The minimum in (3.2) is a Finset.inf' over all $j \ne i$, the destination included.

The paper's loose phrases are made explicit as follows.

• "Using an optimal policy" (3.1) becomes a minimum attained by a route and below every route.
• "Represents the minimum time for a path with at most one stop" becomes, for every $k$, a minimum over routes with at most $k + 1$ roads.
• "Converges after at most $(N - 1)$ iterations" becomes $f^{(k)} = f$ for every $k \ge N - 1$.
• "Only a finite number of iterations will be required" (§7) becomes $\exists K, \forall k \ge K$, $\underline f^{(k)} = f$.
• "The solution of (3.2)" in §7 becomes an arbitrary solution of (3.2), which milestones 1–2 show is the vector of minimal times.

Two printed slips are corrected. (5.2) is printed for $i = 1, \dots, N$, which would set $f_N^{(0)} = t_{NN}$, and with $t_{NN} > 0$ statements (5.4), (5.5) and the goal would be false. The formalization uses $f_N^{(0)} = 0$, the value the paper's own justification needs. (7.1) prints "$N = 1$" for $N - 1$. Section 6 (computational aspects) and the closing expectation of §7 that the first method converges faster are not formalized.

The goal cannot be satisfied trivially. The minimal times are defined from routes, not as a solution of (3.2) or as a limit of the iteration, so the goal connects the recursion to the routing problem itself.

The development needs only finite minima, lists and induction; nothing beyond core Mathlib. The route and minimal-time layer is reusable for other deterministic shortest-path results. Proofs of any milestone are welcome, as are proofs of the sharper bound $N - 2$.

Selected references

• R. Bellman, On a routing problem, Quarterly of Applied Mathematics 16(1) (1958), 87–90. https://doi.org/10.1090/qam/102435
• R. Bellman, Dynamic Programming, Princeton University Press, 1957.
• R. Bellman, The theory of dynamic programming, Bull. Amer. Math. Soc. 60 (1954), 503–515. https://doi.org/10.1090/S0002-9904-1954-09848-8
• L. R. Ford Jr., Network flow theory, RAND Corporation P-923, 1956. https://www.rand.org/pubs/papers/P923.html
• E. W. Dijkstra, A note on two problems in connexion with graphs, Numerische Mathematik 1 (1959), 269–271. https://doi.org/10.1007/BF01386390
• R. W. Floyd, Algorithm 97: Shortest path, Communications of the ACM 5(6) (1962), 345. https://doi.org/10.1145/367766.368168

Motivation

In the single-machine scheduling problem $1|\mathrm{prec}|\sum w_jC_j$, a set $N$ of $n$ jobs, each with a processing time $p_j\ge 0$ and a weight $w_j\ge 0$, is processed on one machine without interruption, subject to precedence constraints given by a partial order $P$ on $N$. The aim is to minimize the weighted sum of completion times $\sum_j w_jC_j$. The problem is strongly NP-hard for general precedence constraints (Lawler 1978; Lenstra and Rinnooy Kan 1978), and its approximability was a recurring open question in scheduling theory (Schuurman and Woeginger 1999).

A line of work by Chudak and Hochbaum, Correa and Schulz, and Ambühl and Mastrolilli showed that the problem is a special case of minimum weighted vertex cover in a graph $G^S_P$ built from the instance. Many problems on partial orders become polynomial when the order is an interval order, so it is natural to ask whether this one does too. Section 7 of Ambühl, Mastrolilli, Mutsanas and Svensson (Math. Oper. Res. 2011) answers no: the problem stays NP-hard on interval orders. The proof is a reduction from vertex cover in connected graphs of maximum degree 3. This mission formalizes the correctness of that reduction.

Setting

A poset $P=(N,P)$ is read as a reflexive relation: $(x,y)\in P$ means $x\le y$. Jobs $x,y$ are incomparable if neither $(x,y)$ nor $(y,x)$ is in $P$, and $\operatorname{inc}(P)$ is the set of ordered incomparable pairs. The vertex cover graph $G^S_P$ has one node $(i,j)$ for each incomparable pair, weighted $p_iw_j$. Two nodes $(i,j)$ and $(k,\ell)$ are adjacent if $j=k$ and $i=\ell$, or $j=k$ and $(i,\ell)\in P$, or $(i,\ell)\in P$ and $(k,j)\in P$. Write $w(C_I)$ for the minimum weight of a vertex cover of $G^S_I$.

A poset is an interval order if each element $x$ can be assigned a closed real interval $[a_x,b_x]$ such that $x<y$ if and only if $b_x<a_y$.

The reduction starts from a graph $G=(V,E)$ with vertices $v_1,\dots,v_N$ and a spanning tree $T=(V,E_T)$ rooted at $v_1$, numbered so that each parent comes before its children. The paper uses a breadth-first search tree.

• Stage 1. The graph $G'$ is built from $T$. Each $v_i$ gets a pendant path $v_i - u^i_1 - u^i_2$. Each non-tree edge $\{v_i,v_j\}\in E\setminus E_T$ with $i<j$ gets the path $v_i - e^{ij}_1 - e^{ij}_2 - u^j_2$. The non-tree edges themselves are not edges of $G'$.
• Stage 2. The scheduling instance $S$ has jobs $s_0$, $s_1,\dots,s_N$, $m_1,\dots,m_N$, $e_1,\dots,e_N$, and $b_{ij}$ for each non-tree edge. Their intervals, processing times and weights are given in a table on p. 662. For example, $s_j$ has interval $[i,j]$, processing time $1/k^j$ and weight $k^i$, where $v_i$ is the parent of $v_j$. The precedence constraints $I$ are the interval order of these intervals. With $n$ the number of jobs, the parameter is $k=n^2+1$.
• The set $D$. It is $\{(s_0,s_1)\}\cup\{(s_i,s_j): v_i \text{ parent of } v_j\}\cup\{(s_i,m_i),(m_i,e_i)\}\cup\{(s_i,b_{ij}),(b_{ij},m_j)\}$. The graph $G'_I$ is the subgraph of $G^S_I$ induced by $D$.

Formalization targets

Goal: Theorem 7.1 (p. 661)

For every connected graph $G$ of maximum degree at most $3$, every parent-first spanning tree $T$ and every $m\in\mathbb N$, the precedence constraints $I$ of $S$ form an interval order, and

$$G \text{ has a vertex cover of size} \le m \iff \lfloor w(C_I)\rfloor \le m + |V| + |E\setminus E_T|.$$

Milestones, in the order the proof uses them

• Claim 1 (p. 662): $\tau(G') = \tau(G)+|V|+|E\setminus E_T|$, where $\tau$ is the vertex cover number.
• Remark 7.1 (p. 662): for jobs with intervals $[a,b]$ and $[c,d]$ and $a\le d$, $p_i\le 1/k^{\lceil b\rceil}$ and $w_j\le k^{\lceil c\rceil}$. On incomparable pairs $p_iw_j\in\{1\}\cup[0,1/k]$. Moreover, $p_iw_j\ge k$ forces $b<c$, and $p_iw_j=1$ forces $\lceil b\rceil=\lceil c\rceil$.
• Claim 2 (p. 663): an incomparable pair $(i,j)$ has $p_iw_j=1$ if it is in $D$, and $p_iw_j\le 1/k$ otherwise.
• Claim 3 (p. 663): $G'_I\cong G'$.
• §7, p. 664: with $k=n^2+1$, $\sum_{(i,j)\in\operatorname{inc}(I)\setminus D}p_iw_j<1$, and hence $w(C'_I)=\lfloor w(C_I)\rfloor$.

Significance

The result. Interval orders are a standard tractable class: several scheduling and order-theoretic problems that are hard in general become polynomial on them (Papadimitriou and Yannakakis 1979). Theorem 7.1 puts $1|\mathrm{prec}|\sum w_jC_j$ outside this pattern. Section 6 of the same paper shows that the problem nonetheless has a $3/2$-approximation on interval orders, so hardness and approximability are separated on this class. The paper also remarks that the proof makes weighted vertex cover NP-hard to approximate within some factor $r>1$ on the graphs $G^S_I$ arising from interval orders.

Formalizing it. The theorem is proved in the paper. Nothing in this mission is open, and none of it has been machine-checked before. The work splits into the following parts:

• a gadget argument on unweighted vertex covers (Claim 1, after Alimonti and Kann);
• an exact case analysis of incomparable pairs in a concrete interval order (Remark 7.1, Claim 2);
• a graph isomorphism (Claim 3);
• a rounding argument that links weighted and unweighted optima.

The definitions of $G^S_P$ and of minimum-weight vertex covers are shared with the other missions of this series.

Difficulty

The construction is explicit, and each step is elementary. The work is in the bookkeeping. Claim 2 requires classifying every incomparable pair of jobs, including pairs of different kinds such as $(b_{ij}, s_\ell)$, by comparing ceilings of interval endpoints. Half-integer endpoints ($m_i$, $b_{ij}$) are exactly what separates weight-one pairs from comparable ones. Claim 3 requires checking adjacency in $G^S_I$ for all pairs of nodes of $D$ in both directions. The paper writes out two cases in each direction and calls the rest similar.

Claim 1 has a direction that is not simply local. A vertex cover of $G'$ that misses both endpoints of a non-tree edge has to be repaired by swapping gadget vertices, and the repair must be repeated without increasing the size.

A natural first idea is to treat the light nodes (weight at most $1/k$) as negligible one at a time. This does not suffice: the argument needs their total weight to stay below $1$, which is what forces $k$ to grow with $n^2$.

Formalization scope

• Graph and tree. $G$ is a SimpleGraph (Fin N); vertex $v_{i+1}$ is i, and the root is index 0. The tree is a TreeLayout: a parent function returning none exactly at the root, with each parent of smaller index and adjacent in $G$. The statements hold for every such layout. This is stronger than the paper's breadth-first tree, and the proof uses only "parent before child".
• Hypotheses of the goal. Connectivity and the degree bound ((G.neighborSet v).ncard ≤ 3) are kept as in the paper. They matter only for the NP-completeness of the source problem.
• Jobs. The jobs form an inductive type with one constructor per row of the table. Their order is a PartialOrder instance: $x\le y$ iff $x=y$ or $b_x<a_y$. Processing times and weights are real numbers. Section 1 of the paper asks for nonnegative integers, but the instance uses $1/k^j$ and the formalization follows the instance as printed.
• Constants. The constants are explicit: $k=n^2+1$ with $n$ the cardinality of the job type, and $c=|V|+|E\setminus E_T|$. Remark 7.1 and Claim 2 are stated for every real $k>1$.
• Optimum values. $w(C_I)$ is a minimum over the finite family of vertex covers. Unweighted cover numbers are Mathlib's SimpleGraph.vertexCoverNum. The floor is Nat.floor, which agrees with the integer floor because $w(C_I)\ge 0$.
• Not formalized. The goal's wording ("NP-hard") is not formalized. Neither are the NP-completeness of degree-3 vertex cover (Garey, Johnson and Stockmeyer), the polynomial size of the construction, or Theorem 2.1 (cited), which turns a vertex cover of $G^S_I$ into a schedule. What is stated is the correctness of the reduction: the instance has interval-order constraints, and its optimum decides the vertex cover question.
• No trivialization. The instance $S$ is built from $G$ and $T$ exactly as in the table. The goal quantifies over all graphs and layouts, never over an instance $S$ assumed to have the properties.
• Contributions. Contributions are welcome on any milestone. Claims 1 and 3 are independent of the weights, and Claim 2 is independent of the graph theory.

Selected references

• C. Ambühl, M. Mastrolilli, N. Mutsanas, O. Svensson, On the Approximability of Single-Machine Scheduling with Precedence Constraints, Math. Oper. Res. 36(4):653–669, 2011. https://doi.org/10.1287/moor.1110.0512
• C. Ambühl, M. Mastrolilli, Single machine precedence constrained scheduling is a vertex cover problem, Algorithmica 53(4):488–503, 2009. https://doi.org/10.1007/s00453-008-9251-1
• J. R. Correa, A. S. Schulz, Single machine scheduling with precedence constraints, Math. Oper. Res. 30(4):1005–1021, 2005. https://doi.org/10.1287/moor.1050.0158
• P. Alimonti, V. Kann, Some APX-completeness results for cubic graphs, Theoret. Comput. Sci. 237(1–2):123–134, 2000. https://doi.org/10.1016/S0304-3975(98)00158-3
• M. R. Garey, D. S. Johnson, L. Stockmeyer, Some simplified NP-complete graph problems, Theoret. Comput. Sci. 1(3):237–267, 1976. https://doi.org/10.1016/0304-3975(76)90059-1
• C. H. Papadimitriou, M. Yannakakis, Scheduling interval-ordered tasks, SIAM J. Comput. 8(3):405–409, 1979. https://doi.org/10.1137/0208031

Why the variable cost matters

The problem $1|\mathrm{prec}|\sum w_jC_j$ asks for an order in which to process jobs on one machine, respecting precedence constraints, so as to minimize the weighted sum of completion times. It is strongly NP-hard, and for decades the best approximation ratio known has been $2$, achieved by several unrelated algorithms (LP relaxations, Sidney decompositions, primal–dual methods).

Correa and Schulz (2005) and Ambühl and Mastrolilli (2009) showed that the problem is a special case of weighted vertex cover: its objective splits into a fixed cost, the same for every feasible solution, and a variable cost, which equals the weight of a vertex cover in an auxiliary graph $G^S_{\mathbf P}$. Approximating vertex cover in $G^S_{\mathbf P}$ within a factor $\alpha$ therefore approximates the scheduling problem within $\alpha$. Uhan observed that the classical 2-approximations owe their guarantee to the fixed cost and can be arbitrarily bad on the variable cost alone.

Section 8 of Ambühl, Mastrolilli, Mutsanas and Svensson, Math. Oper. Res. 36(4) (2011) (DOI), proves the converse: approximating the variable cost is as hard as approximating vertex cover itself. A better-than-2 algorithm for $1|\mathrm{prec}|\sum w_jC_j$ must therefore either exploit the fixed cost or improve on the best known approximation for vertex cover, a long-standing open question.

Setting

Scheduling instance. A finite set $N$ of jobs, a partial order $\mathbf P = (N,P)$ (reflexive; $(i,j) \in P$, $i \ne j$, means $i$ precedes $j$), processing times $p_j \ge 0$ and weights $w_j \ge 0$.

Incomparable pairs. Jobs $x,y$ are incomparable, $x \parallel y$, if neither $(x,y)$ nor $(y,x)$ lies in $P$. The set $\operatorname{inc}(\mathbf P)$ consists of the ordered pairs $(x,y)$ with $x \parallel y$.

The vertex cover graph $G^S_{\mathbf P}$. One node per incomparable pair $(i,j)$, of weight $w_{(i,j)} = p_i w_j$. Distinct nodes $(i,j)$ and $(k,\ell)$ are adjacent when, in one of the two orders, $j=k$ and $i=\ell$, or $j=k$ and $(i,\ell)\in P$, or $(i,\ell),(k,j) \in P$. For a set $C$ of nodes, $w(C) = \sum_{u\in C} w_u$; for a vertex cover $C$ this is the variable cost, and $\tau_w(G^S_{\mathbf P})$ is its minimum over all vertex covers.

The instance $S(G,k)$. Given a graph $G=(V,E)$ with $V = \{v_1,\dots,v_n\}$ and $k > 0$, the instance has jobs $v'_i$ (processing time $k^{-i}$, weight $0$) and $v''_i$ (processing time $0$, weight $k^{i}$), and precedence constraints $v'_i < v''_j$ and $v'_j < v''_i$ for each edge $\{v_i,v_j\} \in E$, plus $v'_i < v''_j$ for all $i<j$. The nodes $(v'_i, v''_i)$ of $G^S_{\mathbf P}$ have weight $1$ and are called heavy; all others are light. For a set $C$ of nodes, $C_G = \{v_i : (v'_i,v''_i)\in C\}$. The vertex cover number of $G$ is $\tau(G)$.

Formalization targets

Goal: Theorem 8.1

For every graph $G$ on $n$ vertices, every $r \ge 1$, $\varepsilon>0$ and every $k \ge 1$ with $k > n^2r/\varepsilon$: if $C$ is a vertex cover of $G^S_{\mathbf P}$ for $S = S(G,k)$ with $w(C) \le r\,\tau_w(G^S_{\mathbf P})$, then $C_G$ is a vertex cover of $G$,

$$|C_G| \le r\Bigl(\tau(G) + \frac{n^2}{k}\Bigr),$$

and, when $E \ne \emptyset$,

$$|C_G| \le r\Bigl(1+\frac{n^2}{k}\Bigr)\tau(G) < (r+\varepsilon)\,\tau(G).$$

The paper words the theorem as "approximating the variable cost of $1|\mathrm{prec}|\sum w_jC_j$ is as hard as approximating vertex cover"; the statement above is the mathematical content its proof establishes.

Milestones (§8, p. 664)

1. In $G^S_{\mathbf P}$, every heavy node has weight $1$, every light node has weight at most $1/k$, and the light nodes have total weight at most $n^2/k$ (for $k \ge 1$).
2. Heavy nodes $(v'_i,v''_i)$ and $(v'_j,v''_j)$ are adjacent if and only if $\{v_i,v_j\}\in E$; for $k>1$ the subgraph induced by the weight-1 nodes is isomorphic to $G$ via $(v'_i,v''_i) \mapsto v_i$.

Significance

The result. Theorem 8.1 is one half of an equivalence: by Theorem 2.1 (Correa–Schulz, Ambühl–Mastrolilli), minimizing the variable cost is a special case of weighted vertex cover; by Theorem 8.1, it is also as hard to approximate. Any hardness of approximation for vertex cover (NP-hardness of factor $1.36$ by Dinur and Safra; factor $2-\delta$ under the unique games conjecture by Khot and Regev) transfers to the variable cost. It also explains why the known 2-approximations must rely on the fixed cost, and it frames the later result of Bansal and Khot that the full objective is hard to approximate within $2-\delta$ under a variant of the unique games conjecture.

Formalizing it. The theorem is proved in the paper; no machine-checked version exists. The mission produces a checked account of the reduction: the vertex cover graph of an arbitrary precedence-constrained instance, the adjacency-poset instance built from a graph, and the quantitative transfer of approximation ratios. The definition of $G^S_{\mathbf P}$ is shared with the other missions of this series.

Difficulty

The construction is short; the care is in the bookkeeping. One must check that the precedence relation is a partial order, determine exactly which ordered pairs are incomparable, verify that two heavy nodes are adjacent only through the third clause of the adjacency rule and only when the corresponding vertices are adjacent in $G$, and bound the weights of all remaining nodes, including the many nodes of weight $0$. The transfer then compares an approximate cover of $G^S_{\mathbf P}$ with an optimal one whose heavy part comes from an optimal cover of $G$; the additive error $n^2/k$ must be converted into a multiplicative one, which requires $\tau(G)\ge 1$.

A first reading of the page suggests that $G^S_{\mathbf P}$ has at most $n^2$ nodes; it does not. The pairs $(v'_i,v'_j)$ and $(v''_i,v''_j)$ with $i\ne j$ are incomparable nodes of weight $0$, so there can be up to $4n^2-2n$ nodes. Only nodes of positive weight are few.

Formalization scope

• Model. Jobs form a finite type; precedence constraints are an explicit reflexive partial-order relation P : N → N → Prop. Processing times and weights are nonnegative reals. The vertex cover graph is a SimpleGraph on the subtype of incomparable ordered pairs, using the symmetric closure of the printed adjacency rule without loops. Vertex covers are Mathlib's SimpleGraph.IsVertexCover; $\tau(G)$ is Mathlib's vertexCoverNum, finite for a finite graph and converted with toNat; $\tau_w(G^S_{\mathbf P})$ is a minimum over finite vertex covers.
• The instance. The graph is a SimpleGraph (Fin n); i : Fin n stands for $v_{i+1}$, so exponents are $i+1$ and the order $i<j$ is that of Fin n. Jobs are Fin n ⊕ Fin n ($v'$ left, $v''$ right). The parameter $k$ is in $\mathbb R_{\ge 0}$.
• Added hypotheses. $k \ge 1$, implicit in the page ("$k > n^2r/\varepsilon$" does not imply it when $\varepsilon$ is large, and for $k<1$ the light nodes outweigh the heavy ones). The isomorphism with $G$ is stated for $k > 1$, since at $k=1$ some light nodes also have weight $1$. The multiplicative bound requires $E \ne \emptyset$; the additive bound holds for every graph.
• Not formalized. The phrases "approximation algorithm", "polynomial time" and "as hard as"; the passage from vertex covers of $G^S_{\mathbf P}$ to schedules (Theorem 2.1, cited from Correa–Schulz and Ambühl–Mastrolilli); the fixed cost. What is stated instead is the explicit map $C \mapsto C_G$ and the ratio it achieves, $r(1+n^2/k) < r+\varepsilon$. The false count "at most $n^2$ vertices" is not stated.
• Ruled out. The goal is not a statement about an arbitrary graph or an assumed cover of $G$: it concerns the specific instance $S(G,k)$ and every $C$ that is an $r$-approximate vertex cover of its graph, and the fact that $C_G$ covers $G$ is a conclusion, not a hypothesis.
• Welcome contributions. Proofs of the two milestones and of the goal; general lemmas on $G^S_{\mathbf P}$ (weights of vertex covers, behaviour under induced subgraphs) are reusable across the series.

Selected references

• C. Ambühl, M. Mastrolilli, N. Mutsanas, O. Svensson, On the Approximability of Single-Machine Scheduling with Precedence Constraints, Mathematics of Operations Research 36(4):653–669, 2011. https://doi.org/10.1287/moor.1110.0512
• J. R. Correa, A. S. Schulz, Single-Machine Scheduling with Precedence Constraints, Mathematics of Operations Research 30(4):1005–1021, 2005. https://doi.org/10.1287/moor.1050.0158
• C. Ambühl, M. Mastrolilli, Single Machine Precedence Constrained Scheduling Is a Vertex Cover Problem, Algorithmica 53(4):488–503, 2009. https://doi.org/10.1007/s00453-008-9251-6
• I. Dinur, S. Safra, On the Hardness of Approximating Minimum Vertex Cover, Annals of Mathematics 162(1):439–485, 2005. https://doi.org/10.4007/annals.2005.162.439
• S. Khot, O. Regev, Vertex Cover Might Be Hard to Approximate to within 2 − ε, Journal of Computer and System Sciences 74(3):335–349, 2008. https://doi.org/10.1016/j.jcss.2007.06.019
• N. Bansal, S. Khot, Optimal Long Code Test with One Free Bit, FOCS 2009, 453–462. https://doi.org/10.1109/FOCS.2009.23