Graph Theory

Motivation

Network data often come as a single observed graph, and the simplest summary of a graph is its degree sequence, the list of the numbers of neighbours of its vertices. A statistical model in which the degree sequence is a sufficient statistic is an exponential family on graphs, and the simplest such family is the β-model: each vertex $i$ carries a parameter $\beta_i$, and edges appear independently with log-odds $\beta_i+\beta_j$. The model appears in the directed case in Holland and Leinhardt (1981), in the undirected case in Park and Newman (2004) and Blitzstein and Diaconis (2011), and it is a close relative of the Bradley–Terry model for paired comparisons.

Fitting the model means solving the maximum likelihood equations. The difficulty for classical theory is that the number of parameters, $n$, equals the number of vertices: the parameter dimension grows with the sample, and standard consistency arguments for maximum likelihood do not apply. Chatterjee, Diaconis and Sly (2011) prove that, nevertheless, for parameters in a fixed bounded range the maximum likelihood estimate exists, is unique, and estimates every coordinate of $\beta$ uniformly at rate $\sqrt{\log n/n}$, with probability $1-O(n^{-2})$. This mission formalizes that result (Theorem 1.3 of the paper) and the lemmas of §4 on which its proof rests.

Setting

Let $n\ge 1$ and $\beta=(\beta_1,\dots,\beta_n)\in\mathbb R^n$. The β-model $\mathbb P_\beta$ is the law of the random simple graph $G$ on vertices $1,\dots,n$ in which, for each pair $i\ne j$, the edge $\{i,j\}$ is present with probability

$$p_{ij}=\frac{e^{\beta_i+\beta_j}}{1+e^{\beta_i+\beta_j}},$$

independently of all other edges. Write $d_1,\dots,d_n$ for the degrees of $G$. The maximum likelihood equations for an estimate $\hat\beta\in\mathbb R^n$ are

$$d_i=\sum_{j\ne i}\frac{e^{\hat\beta_i+\hat\beta_j}}{1+e^{\hat\beta_i+\hat\beta_j}},\qquad i=1,\dots,n. \tag{3}$$

The sup norm is $|x|_\infty=\max_i|x_i|$.

Two further objects enter the proof. $\mathcal D$ is the set of degree sequences of simple graphs on $n$ vertices and $\mathcal R$ the set of expected degree sequences of $\mathbb P_\beta$ as $\beta$ ranges over $\mathbb R^n$. For $d\in\mathbb R^n$ and $B\subseteq\{1,\dots,n\}$ the slack is

$$g(d,B)=\sum_{j\notin B}\min\{d_j,|B|\}+|B|(|B|-1)-\sum_{i\in B}d_i,$$

which is nonnegative for every degree sequence of a graph (the Erdős–Gallai inequalities). Finally $\varphi:\mathbb R^n\to\mathbb R^n$, $\varphi_i(x)=\log d_i-\log\sum_{j\ne i}(e^{-x_j}+e^{x_i})^{-1}$, is the map whose fixed points are the solutions of (3).

Formalization targets

Goal: Theorem 1.3

For every $L\ge 0$ there is $C(L)>0$ such that for every $n\ge 1$ and every $\beta$ with $|\beta_i|\le L$,

$$\mathbb P_\beta\Big(\exists!\,\hat\beta \text{ solving (3)},\ \ |\hat\beta-\beta|_\infty\le C(L)\sqrt{\tfrac{\log n}{n}}\Big)\ \ge\ 1-C(L)\,n^{-2}.$$

The constant depends only on $L$, and the statement holds for all $n$, small $n$ being absorbed into $C(L)$.

Milestones, in the order the proof uses them

1. The probability formula $\mathbb P_\beta(G)=e^{\sum_i\beta_id_i}/\prod_{i<j}(1+e^{\beta_i+\beta_j})$ (p. 6), with $\mathbb P_\beta$ a probability measure.
2. Theorem 1.4: $\mathrm{conv}(\mathcal D)=\overline{\mathcal R}$.
3. Lemma 4.1: if $d\in\overline{\mathcal R}$, $c_2(n-1)\le d_i\le c_1(n-1)$, and $g(d,B)\ge c_3n^2$ whenever $|B|\ge c_2^2n$, then (3) has a solution with $|\hat\beta|_\infty\le c_4(c_1,c_2,c_3)$.
4. Lemma 4.2: with probability $\ge1-2n^{-2}$ the observed degrees satisfy $c_2(n-1)\le d_i\le c_1(n-1)$ and $g(d,B)\ge(c_3-\sqrt{6\log n/n})n^2$ for $|B|\ge cn$.
5. Theorem 1.5: uniqueness of the solution of (3) and the a-priori bound $|x_0-\hat\beta|_\infty\le C|x_0-\varphi(x_0)|_\infty$.
6. The identity $(\beta-\varphi(\beta))_i=\log(\bar d_i/d_i)$, with $\bar d_i$ the expected degree of vertex $i$ (p. 21).

Significance

The theorem is a consistency result in a regime where the number of parameters is as large as the number of nodes, and it comes with a uniform rate: every vertex parameter is recovered to accuracy $O(\sqrt{\log n/n})$ simultaneously, from one graph. Existence of the MLE is itself not automatic (it fails, for instance, whenever the observed graph has an isolated vertex), so the theorem also says that the estimator is defined with high probability. The paper uses the same machinery for its graph-limit results on uniform random graphs with a given degree sequence (missions 4–5 of this series), and the β-model is the base case of a large family of exponential random graph models used in network analysis.

The result is proved in the paper; this mission produces the machine-checked version. None of the statements here is formalized on the platform or in Mathlib. Theorems 1.4 and 1.5 are the goals of missions 2 and 1 of this series and are restated here; a proof there transfers directly.

Difficulty

Standard maximum likelihood asymptotics fix the parameter dimension and let the sample size grow; here both grow together, and the ratio of squared dimension to number of observations, $n^2/\binom n2$, stays bounded, so the usual heuristic for when asymptotics apply is borderline at best. The likelihood is concave, but concavity alone gives neither existence of a maximizer (the supremum may be approached at $\beta_i=\pm\infty$) nor a bound on its size that is uniform in $n$. The central step, Lemma 4.1, is a deterministic bound on $|\hat\beta|_\infty$ that does not depend on $n$; it requires control of how the coordinates of $\hat\beta$ can spread out, expressed through a quantitative Erdős–Gallai margin. A coordinatewise argument cannot give it, because each equation of (3) involves all coordinates.

Formalization scope

Vertices are Fin n, graphs are SimpleGraph (Fin n) with the discrete σ-algebra, and $\mathbb P_\beta$ is the finite sum of point masses with the independent-edge weights $\prod_{i<j}p_{ij}^{\mathbf 1[ij\in G]}(1-p_{ij})^{\mathbf 1[ij\notin G]}$; vectors are Fin n → ℝ with Mathlib's sup norm. Probabilities are values of this measure in $[0,\infty]$, compared with $\max(0,1-Cn^{-2})$. Expected degrees are integrals against $\mathbb P_\beta$; $\mathcal R$ is not defined as the range of the right-hand side of (3), since that identification is part of the content of Theorem 1.4.

Every "constant depending only on …" is a quantifier placed before $n$: in Theorem 1.3, $C$ depends on $L$ only; in Lemma 4.1, $c_4$ is a function of $(c_1,c_2,c_3)$ alone, bounded on compact subsets of its domain, as §4 defines the phrase; in Lemma 4.2, $(C,c_1,c_2)$ on $L$ and $c_3$ on $(L,c)$. Choosing $C$ after $n$ and $\beta$ would make Theorem 1.3 trivial, since $1-Cn^{-2}<0$ for large $C$; this formalization rules that out. The paper's $L:=\max_i|\beta_i|$ is the hypothesis $|\beta_i|\le L$, and the paper's $\frac1{n^2}\inf_{B}\{\cdots\}\ge c_3$ is the bound $g(d,B)\ge c_3n^2$ for every admissible $B$ (a finite nonempty family). The phrase "there exists a unique solution $\hat\beta$ … that satisfies [the bound]" is read as: a solution exists, it is unique, and it satisfies the bound. Lemma 4.1 assumes $d\in\overline{\mathcal R}$, not $d\in\mathcal R$ (for $d\in\mathcal R$ existence would be immediate). Theorem 1.5 is stated, as in mission 1, for $n\ge3$ and $d_i>0$.

A complete development needs: the β-model as a measure and its exponential-family formula; Hoeffding's inequality for sums of independent non-identical indicators transported to $\mathbb P_\beta$ (Mathlib has Hoeffding for independent bounded variables); compactness in $\mathbb R^n$; and the results of missions 1 and 2. The β-model measure and the Erdős–Gallai slack are reusable beyond this mission. Proofs of any milestone, and of the transfer between the independent-edge and the product-space descriptions of $\mathbb P_\beta$, are welcome.

Selected references

• S. Chatterjee, P. Diaconis, A. Sly, Random graphs with a given degree sequence, Ann. Appl. Probab. 21(4), 1400–1435, 2011. arXiv:1005.1136v5. https://arxiv.org/abs/1005.1136 — https://doi.org/10.1214/10-AAP728
• P. W. Holland, S. Leinhardt, An exponential family of probability distributions for directed graphs, J. Amer. Statist. Assoc. 76, 33–50, 1981. https://doi.org/10.1080/01621459.1981.10477598
• J. Park, M. E. J. Newman, Statistical mechanics of networks, Phys. Rev. E 70, 066117, 2004. https://arxiv.org/abs/cond-mat/0405566
• J. Blitzstein, P. Diaconis, A sequential importance sampling algorithm for generating random graphs with prescribed degrees, Internet Math. 6(4), 489–522, 2011. https://doi.org/10.1080/15427951.2010.557277
• W. Hoeffding, Probability inequalities for sums of bounded random variables, J. Amer. Statist. Assoc. 58, 13–30, 1963. https://doi.org/10.1080/01621459.1963.10500830

Motivation

A uniformly random simple graph with a prescribed degree sequence is a basic null model in network science, statistics and combinatorics: it is what a network "looks like" when nothing but its degrees is known. Chatterjee, Diaconis and Sly (arXiv:1005.1136, Ann. Appl. Probab. 2011) show that when the normalized degree sequences converge to a limiting profile $f$, these random graphs converge almost surely to an explicit graph limit (their Theorem 1.1). That theorem has a hypothesis: $f$ must lie in the interior of the set $\mathcal F$ of all possible limiting degree profiles. A hypothesis of that kind is only useful if it can be checked, and the paper's Proposition 1.2 supplies the check, in the form of a continuum version of the Erdős–Gallai criterion (Erdős and Gallai, Mat. Lapok 1960), the classical test for whether a list of integers is the degree sequence of a simple graph.

This mission formalizes Proposition 1.2 and the steps of its proof in §5 of the paper, together with the Erdős–Gallai criterion itself, which the paper cites and uses in both directions.

Setting

A degree sequence on $n$ vertices is a vector $\mathbf d=(d_1,\dots,d_n)$ of nonnegative integers for which some simple graph (undirected, no loops, no multiple edges) on vertices $1,\dots,n$ has $\deg(i)=d_i$ for every $i$. Such sequences are written in nonincreasing order $d_1\ge d_2\ge\cdots\ge d_n$.

The space $D'[0,1]$ consists of the functions $f$ on $[0,1]$ that are nonincreasing and left continuous at every point of $(0,1)$. It carries the modified $L^1$ norm

$$\|f\|_{1'}:=|f(0)|+|f(1)|+\int_0^1|f(x)|\,dx.$$

Suppose that for every $n$ a degree sequence $\mathbf d^n=(d^n_1\ge\cdots\ge d^n_n)$ on $n$ vertices is given. The sequence $\{\mathbf d^n\}$ has scaling limit $f$, a nonincreasing function on $[0,1]$, if

$$\lim_{n\to\infty}\Bigl(\Bigl|\tfrac{d^n_1}{n}-f(0)\Bigr|+\Bigl|\tfrac{d^n_n}{n}-f(1)\Bigr|+\frac1n\sum_{i=1}^n\Bigl|\tfrac{d^n_i}{n}-f\bigl(\tfrac in\bigr)\Bigr|\Bigr)=0.\qquad(2)$$

The set $\mathcal F$ consists of the $f\in D'[0,1]$ that arise as scaling limits of degree sequences. Its interior is taken in $D'[0,1]$ with the topology of $\|\cdot\|_{1'}$: $f$ is interior if every $h\in D'[0,1]$ with $\|h-f\|_{1'}<\varepsilon$ lies in $\mathcal F$, for some $\varepsilon>0$.

For $f\in D'[0,1]$ and $x\in[0,1]$ the paper defines

$$G_f(x):=\int_x^1\min\{f(y),x\}\,dy+x^2-\int_0^x f(y)\,dy.$$

At $x=k/n$, $n^2G_f(x)$ approximates the slack $k(k-1)+\sum_{i>k}\min\{d_i,k\}-\sum_{i\le k}d_i$ in the $k$-th Erdős–Gallai inequality.

In Lean these objects are IsGraphic, InDprime, norm1', Gf, HasScalingLimit, setF and InteriorF, in the namespace GivenDegreeSeq.Interior.

Formalization targets

Goal: Proposition 1.2 (p. 5)

A function $f:[0,1]\to[0,1]$ in $D'[0,1]$ belongs to the interior of $\mathcal F$ if and only if

1. there are constants $c_1>0$ and $c_2<1$ with $c_1\le f(x)\le c_2$ for all $x\in[0,1]$, and
2. for each $x\in(0,1]$,

$$\int_x^1\min\{f(y),x\}\,dy+x^2-\int_0^x f(y)\,dy>0.$$

Milestones

• Remark 1 (Erdős–Gallai criterion). Nonnegative integers $d_1\ge\cdots\ge d_n$ form a degree sequence if and only if $\sum_i d_i$ is even and, for each $1\le k\le n$,

$$\sum_{i=1}^k d_i\le k(k-1)+\sum_{i=k+1}^n\min\{d_i,k\}.$$

• Continuity of $G_f$ on $[0,1]$ for $f\in D'[0,1]$ (p. 23).
• Necessity: every $f\in\mathcal F$ has $G_f\ge 0$ on $[0,1]$, and takes values in $[0,1]$ (p. 23).
• Membership: every $f\in D'[0,1]$ satisfying (i) and (ii) belongs to $\mathcal F$ (pp. 23–24).
• Stability: for $f,f'\in D'[0,1]$ and $0\le x\le1$, $|G_f(x)-G_{f'}(x)|\le\|f-f'\|_{1'}$ (p. 24).

Significance

Proposition 1.2 turns the hypothesis of the paper's graph-limit theorem into two explicit conditions on $f$. With it, for example, the constant profile $f\equiv p$ with $0<p<1$, the degree profile of the Erdős–Rényi graph $G(n,p)$, is seen to be interior (Remark 3, p. 6). The proposition also describes which limiting degree profiles are robust under small perturbations: away from the boundary given by the continuum Erdős–Gallai inequality and the trivial bounds $0$ and $1$.

The Erdős–Gallai criterion is a standard tool for degree sequences, threshold graphs and network models. To the knowledge of this mission it is formalized neither in Mathlib nor on the platform, and a proof of it here is reusable well beyond this paper. The continuum objects $D'[0,1]$, $\|\cdot\|_{1'}$, scaling limits and $\mathcal F$ are shared with the companion mission on the graph-limit theorem (mission 5 of this series). The proposition is proved in the paper; none of it has a machine-checked proof.

Difficulty

The obvious argument passes the Erdős–Gallai inequalities to the limit and back. Going to the limit is routine. Coming back is not, for two reasons. First, the discrete inequalities must hold for every $1\le k\le n$, and near $k=0$ the normalized slack $G_f(k/n)$ tends to $0$, so positivity of $G_f$ alone gives nothing for $k=o(n)$. The bounds $c_1>0$ and $c_2<1$ of condition (i) are what control this range. Second, the approximating integer sequences must satisfy the parity condition and stay nonincreasing, while still converging in the sense of (2).

For openness, the interior must be taken under $\|\cdot\|_{1'}$, and positivity of $G_h$ near $x=0$ has to be recovered for every nearby $h$ from condition (i), not from uniform convergence alone. In the converse direction, perturbations must stay inside $D'[0,1]$, which constrains how $f$ may be modified near a zero of $G_f$.

Formalization scope

• Functions on $[0,1]$ are ℝ → ℝ. Only their values on $[0,1]$ enter $D'[0,1]$, $\|\cdot\|_{1'}$, $G_f$, (2) and $\mathcal F$. Integrals are interval integrals. Every $f\in D'[0,1]$ is monotone, hence bounded and integrable on $[0,1]$.
• Vertices are Fin n, so the paper's $d^n_i$ is d n ⟨i-1,_⟩ and the paper's $f(i/n)$ is f ((i+1)/n). Degree sequences are vectors in Fin n → ℕ realized by a SimpleGraph (Fin n) and are nonincreasing.
• The bracket in (2) has no meaning at $n=0$ and is set to $0$ there. The sequence $\{\mathbf d^n\}$ is indexed by all $n$, not by a subsequence.
• The interior is the ball formulation in $D'[0,1]$ under $\|\cdot\|_{1'}$, and the balls range only over $h\in D'[0,1]$. The plain $L^1$ topology would be wrong: it ignores the endpoint values, and no $f$ would be interior. $\|\cdot\|_{1'}$ is a genuine norm on $D'[0,1]$, so the ball form is the topological interior.
• The goal keeps the page's hypothesis $f([0,1])\subseteq[0,1]$, although the "only if" direction makes it redundant.
• The scaling-limit set $\mathcal F$ requires every $\mathbf d^n$ to be graphic. Dropping that requirement trivializes the problem, because every nonincreasing $[0,1]$-valued function would then be a limit and the proposition would be false. The definitions here exclude it.

Infrastructure needed: the Erdős–Gallai theorem for finite sequences (both directions); Riemann-sum approximation of integrals of monotone functions; an integer-rounding construction with a parity fix. Proofs of the Erdős–Gallai criterion, and of the analytic lemmas on $D'[0,1]$, are welcome independently of the goal.

Selected references

• S. Chatterjee, P. Diaconis, A. Sly, Random graphs with a given degree sequence, Ann. Appl. Probab. 21(4) (2011) 1400–1435; arXiv:1005.1136v5. https://arxiv.org/abs/1005.1136 — DOI https://doi.org/10.1214/10-AAP728
• P. Erdős, T. Gallai, Gráfok előírt fokú pontokkal (Graphs with points of prescribed degree), Mat. Lapok 11 (1960) 264–274.
• N. V. R. Mahadev, U. N. Peled, Threshold Graphs and Related Topics, Annals of Discrete Mathematics 56, North-Holland, 1995.

Motivation

Scheduling jobs on identical parallel machines to minimize the total weighted completion time $\sum_j w_jC_j$, the problem $P\,|\,|\sum w_jC_j$, is one of the basic NP-hard problems of machine scheduling. On a single machine it is solved by Smith's ratio rule (Smith 1956); with several machines the only hard decision is which jobs share a machine. Section 6 of M. Skutella's paper Convex quadratic and semidefinite programming relaxations in scheduling (J. ACM 48 (2001)) observes that this decision is a graph partitioning problem: the cost of a schedule is, up to a constant, the weight of the edges that a partition of a weighted complete graph does not cut. Minimizing $\sum_j w_jC_j$ on $m$ machines is therefore equivalent to Max-$m$-Cut on that graph, and the paper shows that the equivalence preserves approximation in a quantified way.

The reduction explains, from the graph side, why semidefinite rounding works for two machines: with the 0.878-approximation for MaxCut of Goemans and Williamson (1995) it gives a 1.122-approximation for $P2\,|\,|\sum w_jC_j$ (Corollary 6.2 of the paper). For general $m$, the uniform random partition is both a $(1-1/m)$-approximation for Max-$m$-Cut and randomized rounding of the optimum of the convex quadratic relaxation (CQP).

Setting

There are $n$ jobs $J=\{1,\dots,n\}$ and $m\ge 1$ identical machines. Job $j$ has a processing time $p_j>0$ and a weight $w_j\ge 0$. Smith's order $\prec$ puts $j\prec k$ when $w_j/p_j>w_k/p_k$, ties broken by index. An assignment $\sigma:J\to\{1,\dots,m\}$ is a partition $J_1,\dots,J_m$ of the jobs; each machine processes its jobs in the order $\prec$ without idle time, so the completion time of $j$ is

$$C_j(\sigma)=p_j+\sum_{k\prec j,\ \sigma(k)=\sigma(j)}p_k .$$

The value of $\sigma$ is $\sum_j w_jC_j(\sigma)$, and $Z^*$ is the minimum value over all assignments.

The graph $G_J$ is the complete graph on $J$ in which the edge $\{j,k\}$ with $k\prec j$ has weight $c(jk)=w_jp_k$; $c(E_J)$ is its total weight. A partition induces the $m$-cut $E_{\mathrm{cut}}$, the edges whose endpoints lie in different parts, of weight $c(E_{\mathrm{cut}})$; $Z^*_{\mathrm{cut}}$ is the maximum weight of an $m$-cut.

The convex quadratic relaxation (CQP) of §2.2, specialised to identical machines, has variables $a_{ij}\ge 0$ with $\sum_i a_{ij}=1$ and objective $Z_{CQP}(a)=\sum_j w_jC_j$ where

$$C_j=\sum_{i=1}^m a_{ij}\Big(\frac{1+a_{ij}}{2}\,p_j+\sum_{k\prec j}a_{ik}\,p_k\Big)\qquad(11).$$

Its optimum value is $Z^*_{CQP}$.

Formalization targets

Goal: Theorem 6.1

For $\rho\le 1$, any assignment $\sigma$ whose $m$-cut weighs at least $\rho\cdot Z^*_{\mathrm{cut}}$ satisfies

$$\sum_j w_jC_j(\sigma)\le\big(\rho+m(1-\rho)\big)\,Z^* .$$

That is, a $\rho$-approximation algorithm for Max-$m$-Cut translates into a $(\rho+m(1-\rho))$-approximation algorithm for $Pm\,|\,|\sum w_jC_j$. The constant $\rho$ is a parameter, so the goal does not depend on the best known cut algorithm.

Milestones

1. (36): for every partition, $c(E_J)=\sum_j w_jC_j-\sum_j w_jp_j+c(E_{\mathrm{cut}})$.
2. Lemma 2.5: $\bar a_{ij}=1/m$ is an optimum of (CQP), unique when the ratios $w_j/p_j$ are pairwise different and positive.
3. (37): $Z^*\ge Z^*_{CQP}=\frac1m c(E_J)+\big(\frac12+\frac1{2m}\big)\sum_j w_jp_j$.
4. (38): $Z^*_{\mathrm{cut}}\le\frac{m-1}{m}c(E_J)+\big(\frac12-\frac1{2m}\big)\sum_j w_jp_j$.
5. Theorem 2.6 b) (supplementary): assigning each job independently and uniformly at random has expected value at most $\big(\frac32-\frac1{2m}\big)Z^*$.

Significance

The result. Theorem 6.1 makes Max-$m$-Cut algorithms usable for scheduling with an explicit loss: a cut algorithm with ratio $\rho$ close to $1$ yields a schedule within $1+m(1-\rho)$ of optimal. For $m=2$ and the Goemans–Williamson ratio $0.878$ the guarantee is $1.122$, better than the $5/4$ of Theorem 2.6 b) and the $1.2752$ of the paper's semidefinite rounding in §5. In the other direction, (38) bounds the maximum cut of $G_J$ by the scheduling lower bound $Z^*_{CQP}$, which is how a relaxation for scheduling becomes a bound for a cut problem. The problem itself is better understood today: $P\,|\,|\sum w_jC_j$ has a polynomial-time approximation scheme (Skutella and Woeginger 2000), and a fully polynomial one for fixed $m$ (Sahni 1976). The reduction remains of interest as a structural identity between the two problems and as the source of the closed-form relaxation bound (37).

Formalizing it. All statements are proved in the paper; none is known to have a machine-checked proof. The mission produces a formal model of identical-machine scheduling under Smith's rule, of the weighted graph $G_J$ and its $m$-cuts, and of (CQP) for identical machines, together with the closed-form optimum of (CQP) (Lemma 2.5), which is the basis of the $\frac32-\frac1{2m}$ guarantee of Theorem 2.6 b).

Difficulty

The bookkeeping identity (36) and the final chain of inequalities are finite-sum manipulations. The substance is Lemma 2.5: that the uniform vector $\bar a$ minimizes the quadratic objective (11) over the product of simplices. The objective is not separable, since the term $\sum_{k\prec j}a_{ik}p_k$ couples jobs through Smith's order, and its convexity on the feasible region (the positive semidefiniteness established in Lemma 2.4 of the paper) is the fact on which optimality and, with distinct positive ratios, uniqueness rest. The relaxation half of (37), that $Z^*_{CQP}$ is at most the value of every schedule, needs the observation that $Z_{CQP}$ evaluated at the 0/1 vector of an assignment equals the value of that assignment.

Formalization scope

Jobs are Fin n and machines Fin m, 0-based; Smith's order is cross-multiplied ($w_jp_k>w_kp_j$, or equality and $j<k$), equal to the ratio definition because $p>0$. Assignments are functions Fin n → Fin m, and every machine is sequenced by $\prec$; by Smith's rule (p. 7 of the paper, a classical result it cites) this loses no optimality, so $Z^*$ is the minimum over assignments and is never a primitive: "within factor $\alpha$ of $Z^*$" is stated against the value of every assignment. Likewise "weight at least $\rho\cdot Z^*_{\mathrm{cut}}$" is stated as $\rho\,c(E_{\mathrm{cut}}(\tau))\le c(E_{\mathrm{cut}}(\sigma))$ for every assignment $\tau$, so no supremum of an empty or unbounded set can enter. The edge weight is attached to the ordered pair $(j,k)$ with $k\prec j$ and is zero on the other orientation, so each edge of $G_J$ is counted once. Standing hypotheses on every theorem: $p_j>0$, $w_j\ge 0$ (p. 2 of the paper) and $m>0$ (needed for $1/m$). Theorem 6.1 keeps the page's $\rho\le 1$.

Not formalized: polynomial running time, the phrase "approximation algorithm" beyond the value bound it asserts, and the semidefinite results of §5 and Corollary 6.2. A trivializing reading, such as stating the cut condition against a junk-valued supremum or replacing $Z^*$ by a free variable, is excluded by the encodings above.

The development needs only finite sums over Fin types and real arithmetic; the model of identical-machine scheduling under Smith's rule and the closed form of (CQP) are reusable for other results on $P\,|\,|\sum w_jC_j$. Proofs of the milestones, alternative proofs of Lemma 2.5 (the KKT argument the paper mentions, or Goemans' symmetrization argument it gives), and a proof of Theorem 2.6 b) are all welcome.

Selected references

• M. Skutella, Convex quadratic and semidefinite programming relaxations in scheduling, Journal of the ACM 48(2), 2001. https://doi.org/10.1145/375827.375840
• W. E. Smith, Various optimizers for single-stage production, Naval Research Logistics Quarterly 3, 1956. https://doi.org/10.1002/nav.3800030106
• M. X. Goemans and D. P. Williamson, Improved approximation algorithms for maximum cut and satisfiability problems using semidefinite programming, Journal of the ACM 42(6), 1995. https://doi.org/10.1145/227683.227684
• A. Frieze and M. Jerrum, Improved approximation algorithms for MAX k-CUT and MAX BISECTION, Algorithmica 18, 1997. https://doi.org/10.1007/BF02523689
• M. Skutella and G. J. Woeginger, A PTAS for minimizing the total weighted completion time on identical parallel machines, Mathematics of Operations Research 25(1), 2000. https://doi.org/10.1287/moor.25.1.63.15212
• S. Sahni, Algorithms for scheduling independent tasks, Journal of the ACM 23(1), 1976. https://doi.org/10.1145/321921.321934