Theoretical Computer Science

Complexity Theory Graph Theory Operations Research·Captain: mikedeng1

Complexity of Machine Scheduling Problems 6: DIRECTED HAMILTON PATH Reduces to No-Wait Flow Shop Makespan and Total Completion TimeResearch Paper

Motivation

In a no-wait flow shop every job passes through the machines $M_1,\dots,M_m$ in the same order, and once it has started it may never wait between two machines. The constraint comes from processes in which the material changes state if it is left standing, such as hot metal rolling, chemical and food processing, and some pharmaceutical lines; see the survey of Hall and Sriskandarajah (doi:10.1287/opre.44.3.510). The question of how hard it is to schedule such a shop well is the question this mission formalizes.

Brucker, Lenstra and Rinnooy Kan settled it for the case in which the number of machines is part of the input. In their report Complexity of Machine Scheduling Problems (Mathematisch Centrum, 1975; journal version in Annals of Discrete Mathematics 1, 1977, doi:10.1016/S0167-5060(08)70743-X), Theorem 5 reduces DIRECTED HAMILTON PATH to the no-wait flow shop. Both minimizing the makespan $C_{\max}$ and minimizing the total completion time $\sum C_j$ are thereby NP-complete.

Timeline.

1964: Gilmore and Gomory solve the two-machine no-wait flow shop with makespan in polynomial time (doi:10.1287/opre.12.5.655).
1972: Wismer (doi:10.1287/opre.20.3.689) and Reddi and Ramamoorthy (doi:10.1057/jors.1972.52) show that no-wait makespan minimization is a travelling-salesman problem with arc weights computed from the processing times.
1972: Karp proves DIRECTED HAMILTON CIRCUIT NP-complete (doi:10.1007/978-1-4684-2001-2_9).
1975: Brucker, Lenstra and Rinnooy Kan reduce DIRECTED HAMILTON CIRCUIT to DIRECTED HAMILTON PATH (their Theorem 2(d)), and DIRECTED HAMILTON PATH to $n|m|F,\textit{no wait}|C_{\max}$ and to $n|m|F,\textit{no wait},w_j=1|\sum w_jC_j$ (Theorem 5).
1984: Röck shows that the problem stays NP-hard for three machines (doi:10.1145/62.65).

Setting

There are $n$ jobs $J_1,\dots,J_n$ and $m$ machines. Job $J_\ell$ needs processing time $p_{\ell i}\in\mathbb N$ on machine $M_i$ . Write

q_{\ell i}=\sum_{r=1}^{i}p_{\ell r},\qquad q_{\ell 0}=0,

for the time job $J_\ell$ spends on its first $i$ machines. Because a job never waits, a schedule is determined by the start times $B_\ell\in\mathbb N$ . The operation of $J_\ell$ on $M_i$ occupies $[B_\ell+q_{\ell,i-1},\,B_\ell+q_{\ell i})$ , and job $J_\ell$ completes at $C_\ell=B_\ell+q_{\ell m}$ . A schedule is feasible when no two distinct jobs occupy the same machine at the same time. The delay

c_{jk}=\max_{1\le i\le m}\{q_{ji}-q_{k,i-1}\}

is the least gap $B_k-B_j$ that lets $J_k$ follow $J_j$ on every machine.

A directed graph $G=(V,A)$ on $V=\{0,\dots,n-1\}$ has a Hamilton path if its vertices can be ordered $\sigma(0),\dots,\sigma(n-1)$ with every $(\sigma(i),\sigma(i+1))\in A$ .

From $G$ the paper builds an instance with $n$ jobs and $m=n(n-1)+2$ machines. Each ordered pair $(j,k)$ of distinct jobs is assigned a middle machine $\iota(j,k)\in\{2,\dots,m-1\}$ , and the partial sums $q_{\ell i}$ are perturbed from $i\mu$ by $\pm\lambda$ or $\pm(\lambda+1)$ on the machines $\iota(\ell,\cdot)$ and just before the machines $\iota(\cdot,\ell)$ , depending on whether the pair is an arc. The parameters satisfy $\lambda\ge1$ and $\mu\ge2\lambda+3$ .

Formalization targets

Goal (Theorem 5)

\text{DIRECTED HAMILTON PATH}\ \propto\ n|m|F,\textit{no wait}|C_{\max}\quad\text{and}\quad \text{DIRECTED HAMILTON PATH}\ \propto\ n|m|F,\textit{no wait},w_j=1|\textstyle\sum w_jC_j,

where $\propto$ is polynomial-time many-one reducibility between the binary-coded recognition languages.

Milestones, in the order the proof uses them

Eq. (9): $c_{jk}$ is the least gap between $B_j$ and $B_k$ for which $J_k$ follows $J_j$ on every machine.
The travelling-salesman reformulation: if all processing times are positive, a feasible schedule with $C_{\max}\le y$ (resp. $\sum C_\ell\le y$ ) exists iff some job order has path length (resp. summed completion times along the path) at most $y$ .
An admissible ordering $\iota$ exists for every $n\ne2$ .
All processing times of the construction are at least $1$ .
The delays of the construction: $c_{jk}=\mu+2\lambda$ if $(j,k)\in A$ , and $\mu+2\lambda+2$ otherwise.
Theorem 5(a), the equivalence: $G$ has a Hamilton path $\iff$ $C_{\max}\le(n-1)(\mu+2\lambda)+m\mu$ .
Theorem 5(b), the equivalence: $G$ has a Hamilton path $\iff$ $\sum_jC_j\le\tfrac12n(n-1)(\mu+2\lambda)+nm\mu$ .
Theorem 2(d), off the goal's path: $G'$ has a Hamilton circuit iff the graph obtained by splitting a vertex $v'$ into $v'$ and a new sink $v''$ has a Hamilton path.

Significance

The result. Theorem 5, together with the NP-completeness of DIRECTED HAMILTON PATH, places both no-wait criteria among the NP-complete problems once $m$ is part of the input. The Gilmore–Gomory algorithm for two machines therefore cannot be extended to arbitrary $m$ unless P = NP, and heuristics and exact exponential methods for no-wait shops are justified. The reduction also gives a structural fact of independent use: every directed graph can be realized, up to two arc-weight values, as the delay matrix of a no-wait flow shop.

Formalizing it. The result has been proved for fifty years; to our knowledge no machine-checked version exists. This mission produces a checked no-wait flow shop model, a checked travelling-salesman reformulation of it, the correctness of the paper's construction, and a polynomial-time reduction in an explicit Turing-machine model. It also records a gap in the printed proof: the ordering $\iota$ the paper calls easy to construct does not exist for $n=2$ .

Difficulty

Three steps are not routine.

The passage from schedules to job orders assumes that the order in which jobs start is the order in which they visit every machine. With zero processing times this fails, so the reformulation needs the positivity milestone.
Computing the delays requires a case analysis over all machines and all pairs of perturbations. The property of $\iota$ is exactly what keeps the " $+$ " and " $-$ " cases from colliding, and the constants $\lambda\ge1$ , $\mu\ge2\lambda+3$ are tight enough that the comparison must be done carefully.
The goal asks for an actual Turing machine with a polynomial step bound. It has to build $\iota$ for every $n\ne2$ and handle $n\le2$ separately. The equivalences alone do not give this.

Formalization scope

Jobs and machines are $0$ -based (Fin n, Fin m); cum p ℓ i is the paper's $q_{\ell i}$ , and the machine indices $\iota(j,k)$ are the paper's $1$ -based indices. Start times are natural numbers, and release dates are $0$ . Section 3 computes times from processing orders on integer data, and every criterion is regular, so real start times would not change the yes-instances. A zero-length operation occupies the empty interval. $C_{\max}\le y$ is stated as $C_\ell\le y$ for every job. The delays, the partial sums of the construction and its processing times are computed in $\mathbb Z$ . The instance uses their conversion to $\mathbb N$ , which is exact by milestone 4. The threshold of Theorem 5(b) is compared in $\mathbb Q$ , as printed.

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

"scheduled directly after" means "precedes on every machine";
"equivalent to solving the TRAVELLING SALESMAN problem" means the two threshold equivalences of milestone 2, with the $\sum C_j$ version as the reading of "constructed as in (a)";
"such an ordering can easily be constructed" is stated for $n\ne2$ , the only case in which it is true.

Directed graphs are Boolean adjacency matrices. A graph with $0$ or $1$ vertices has a Hamilton path, and a one-vertex graph has a Hamilton circuit iff it has a loop.

The goal is CookPvsNP.PolyReducible from the published definition CookPvsNP_defs, with polynomial time measured on Cook's one-tape Turing machines. Instances are coded with the alphabet BSym and binary code encNats of the published ProjSchedTW.Complexity.Encoding (Neumann, Schwindt and Zimmermann). A graph is coded as $n$ followed by its adjacency matrix; a flow-shop instance as $n$ , $m$ , the matrix $(p_{\ell i})$ and the threshold $y$ .

Stating only the equivalences 6–7 and calling the result "reducible" would drop polynomiality; the goal therefore asserts PolyReducible. The target languages contain exactly the no-wait flow-shop instances, with no waiting allowed, so the reduction cannot land in a looser problem. The parameters $\lambda,\mu$ always carry $\lambda\ge1$ , $\mu\ge2\lambda+3$ .

Contributions are welcome at every level:

the general travelling-salesman reformulation, which is reusable for any no-wait flow-shop result;
the combinatorial existence of $\iota$ ;
the arithmetic of the construction;
Turing-machine infrastructure for computing arithmetic list transformations in polynomial time, which every reduction in this series needs.

Selected references

P. Brucker, J. K. Lenstra, A. H. G. Rinnooy Kan, Complexity of Machine Scheduling Problems, Mathematisch Centrum Report BW 43/75, Amsterdam, 1975; Annals of Discrete Mathematics 1 (1977) 343–362. doi:10.1016/S0167-5060(08)70743-X
R. M. Karp, Reducibility among combinatorial problems, in Complexity of Computer Computations, Plenum, 1972, 85–103. doi:10.1007/978-1-4684-2001-2_9
P. C. Gilmore, R. E. Gomory, Sequencing a one state-variable machine: a solvable case of the traveling salesman problem, Operations Research 12 (1964) 655–679. doi:10.1287/opre.12.5.655
D. A. Wismer, Solution of the flowshop-scheduling problem with no intermediate queues, Operations Research 20 (1972) 689–697. doi:10.1287/opre.20.3.689
S. S. Reddi, C. V. Ramamoorthy, On the flow-shop sequencing problem with no wait in process, Operational Research Quarterly 23 (1972) 323–331. doi:10.1057/jors.1972.52
H. Röck, The three-machine no-wait flow shop is NP-complete, Journal of the ACM 31 (1984) 336–345. doi:10.1145/62.65
N. G. Hall, C. Sriskandarajah, A survey of machine scheduling problems with blocking and no-wait in process, Operations Research 44 (1996) 510–525. doi:10.1287/opre.44.3.510
S. A. Cook, The complexity of theorem-proving procedures, STOC 1971, 151–158. doi:10.1145/800157.805047

14 thms3 active usersReviewed

Complexity Theory Operations Research·Captain: mikedeng1

Complexity of Machine Scheduling Problems 3: KNAPSACK Reduces to Single-Machine Total Weighted TardinessResearch Paper

Motivation

Minimizing total weighted tardiness on a single machine, written $n|1||\sum w_jT_j$ , is one of the basic problems of deterministic scheduling. A job that finishes after its due date is penalized in proportion to its lateness and its weight. Practitioners use this criterion to model penalty clauses and customer priority. In the theory it was a reference problem for branch-and-bound methods and dominance rules throughout the 1960s and 1970s.

Close relatives are easy: with equal weights and a common due date, shortest-processing-time order is optimal. Whether the weighted problem admits a polynomial algorithm was open until the report of Brucker, Lenstra and Rinnooy Kan in 1975. Their Theorem 4(d) shows that KNAPSACK reduces to it, so the problem is NP-hard. The unweighted case $n|1||\sum T_j$ is listed there as open (Section 5) and was settled only later by Du and Leung (1990).

Timeline:

1972: Karp proves KNAPSACK NP-complete (Karp 1972).
1975: Brucker, Lenstra and Rinnooy Kan, Mathematisch Centrum Report BW 43/75, Theorem 4(d), reduce KNAPSACK to $n|1||\sum w_jT_j$ (journal version: Annals of Discrete Mathematics 1, 1977).
1977: Lawler gives a pseudopolynomial algorithm for $n|1||\sum T_j$ and shows that $n|1||\sum w_jT_j$ is strongly NP-hard (Lawler 1977).
1990: Du and Leung prove $n|1||\sum T_j$ NP-hard (Du & Leung 1990).

Setting

A KNAPSACK instance consists of positive integers $a_1,\dots,a_t$ and $b$ . It is a yes-instance if some subset $S\subseteq T=\{1,\dots,t\}$ satisfies $\sum_{j\in S}a_j=b$ . Write $A=\sum_{j\in T}a_j$ and $a_*=\max_{j\in T}a_j$ .

An instance of $n|1||\sum w_jT_j$ consists of $n$ jobs. Job $j$ has a processing time $p_j$ , a weight $w_j$ and a due date $d_j$ , all nonnegative integers, and every job is available at time $0$ . A schedule gives each job a start time $B_j\in\mathbb N$ , and no two jobs may overlap on the machine. Job $j$ completes at $C_j=B_j+p_j$ and has tardiness $T_j=\max\{0,C_j-d_j\}$ . The instance with threshold $y$ is a yes-instance if some schedule satisfies $\sum_jw_jT_j\le y$ . A processing order $\pi=(\pi(1),\dots,\pi(n))$ determines the schedule without idle time, in which $C_{\pi(k)}=\sum_{i\le k}p_{\pi(i)}$ .

Reducibility (Section 2 of the paper) is polynomial-time many-one reducibility between the recognition versions. A polynomial-time Turing machine must map codes of KNAPSACK instances to codes of scheduling instances so that yes-instances map exactly to yes-instances.

The paper's construction has $n=t+t'$ jobs: for $j\in T$ , $p_j=\tau+a_j$ , $w_j=\tau+a_j+1$ , $d_j=t\tau+b$ ; for each of the $t'$ dummy jobs, $p_j=\tau$ , $w_j=\tau+1$ , $d_j=t\tau+b$ . The threshold is $y=\tfrac12t'(t'+1)\tau(\tau+1)+(t'+1)\tau(A-b)+t'$ , with $t'=\tfrac12(t+1)(A-b)+\tfrac12t(t+1)a_*^2$ and $\tau>2t'+A$ . The proof is phrased in terms of $c_\pi=C_{\pi(t)}-(t\tau+b)$ , the amount by which the $t$ -th job of the order misses the common due date.

Formalization targets

Goal: Theorem 4(d)

\text{KNAPSACK}\;\propto\;n|1||\textstyle\sum w_jT_j,

stated as CookPvsNP.PolyReducible SchedComplexity.OneMachine.knapsackLang wtLangMult. The scheduling side uses the multiplicity encoding of the paper's Remark (p. 23), in which a class of identical jobs is written once together with its cardinality.

The equivalence and its claims

Each milestone is a statement of the paper's proof (pp. 20–21) about the construction above, for every admissible $\tau$ :

removal of idle time: every schedule is matched or improved by the schedule without idle time of some processing order;
KNAPSACK has a solution iff some order has $C_{\pi(t)}=t\tau+b$ ; moreover $-b\le c_\pi\le A-b$ ;
identities and bounds (2)–(7) for the tail sums $\sum_{j>t}v_{\pi(j)}(C_{\pi(j)}-C_{\pi(t)})$ ;
claims (A) $c_\pi=0\Rightarrow\exists\pi'$ with $c_{\pi'}=0$ and $\sum w_jT_j\le y$ ; (B) $c_\pi>0\Rightarrow\sum w_jT_j>y$ ; (C) $c_\pi<0\Rightarrow\sum w_jT_j>y$ ;
the equivalence: KNAPSACK has a solution iff the constructed instance has a schedule with $\sum w_jT_j\le y$ .

Significance

The theorem places $n|1||\sum w_jT_j$ among the NP-hard problems, so (unless P = NP) the research on it has to aim at enumerative methods, pseudopolynomial algorithms or approximation, not at an exact polynomial algorithm. Together with the companion reductions of Theorem 4, it drew the boundary between easy and hard single-machine problems that the later classification of Lageweg, Lawler, Lenstra and Rinnooy Kan made systematic.

The result is proved in the paper, and Lawler's later strong NP-hardness proof supersedes it. No machine-checked proof is known to exist. A formal proof adds three things. It makes the paper's "it is easily seen" steps and the encoding argument of the Remark explicit. It produces a reusable single-machine tardiness model with processing orders. It also fixes a gap in the printed construction: the printed $t'$ need not be an integer.

Difficulty

The equivalence is not a local exchange argument. The threshold $y$ must separate orders with $c_\pi=0$ from all others, and the objective is a quadratic function of the order. The orders with $c_\pi=0$ can still differ in $\sum w_jT_j$ by the cross terms $\sum a_{\pi(j)}a_{\pi(k)}$ and by how the late jobs are arranged. The construction therefore needs a slack $t'$ that absorbs these terms, and a scale $\tau$ large enough that a nonzero $c_\pi$ always costs more than the slack. Keeping exact track of every constant, including $t'$ and $y$ , is where errors creep in.

Polynomiality is a second, separate difficulty. The construction has $\Theta(t^2a_*^2+tA)$ jobs, which is exponential in the binary length of the KNAPSACK input. The goal holds only for the encoding of the Remark, and a solver must also produce an explicit polynomial-time Turing machine.

Formalization scope

Jobs of the order-based statements are Fin n, numbered from $0$ ; a processing order is Equiv.Perm (Fin n) with π i the paper's $\pi(i+1)$ . posCompletion p π k is the paper's $C_{\pi(k)}$ for the 1-based position $k$ .
Start times are in $\mathbb N$ . Every criterion is regular and the paper determines schedules by processing orders, so integer start times lose nothing. Tardiness and $\sum w_jT_j$ are computed in $\mathbb Z$ ; the bounds with halves are stated over $\mathbb R$ exactly as printed.
Corrected gap: the printed $t'=\tfrac12(t+1)(A-b)+\tfrac12t(t+1)a_*^2$ is a half-integer when $(t+1)(A-b)$ is odd. The formalization uses its ceiling and computes $y$ from the same $t'$ .
$\tau$ is quantified over all integers with $\tau>2t'+A$ ; the positivity of the $a_j$ and $0<b<A$ are hypotheses, as the paper assumes them.
Explicit readings of the paper's loose phrases: "we may assume [no idle time]" becomes a theorem that the schedule without idle time of some order is at least as good as any schedule; "easily seen" becomes the equivalence with $C_{\pi(t)}=t\tau+b$ ; "for some $\pi$ " in (5) and (7) becomes a reordering that keeps the first $t$ positions, and so keeps $c_\pi$ ; "we may assume $0<b<A$ " is a hypothesis of the milestones but not of the goal, whose reduction must handle every KNAPSACK instance.
Reducibility is CookPvsNP.PolyReducible from the published CookPvsNP_defs. Codes use the alphabet BSym and the binary numerals encNats of the published ProjSchedTW.Complexity.Encoding (Neumann, Schwindt and Zimmermann's encoding). KNAPSACK is restricted to positive integers, so that encoding's subsetSumLang is not reused.
The goal must not be weakened to the bare equivalence: polynomial-time computability of the reduction is part of the statement. The one-copy-per-job encoding of the target is ruled out: the paper does not claim polynomiality for it, and the goal uses the multiplicity encoding instead.
Welcome contributions: proofs of the claims, a reusable lemma that idle time can be removed for regular criteria, and Turing-machine constructions for arithmetic on binary numerals, which the sibling missions of this series also need.

Selected references

P. Brucker, J. K. Lenstra, A. H. G. Rinnooy Kan, Complexity of Machine Scheduling Problems, Mathematisch Centrum Report BW 43/75, Amsterdam, 1975; Annals of Discrete Mathematics 1 (1977) 343–362. https://ir.cwi.nl/pub/9725 , https://doi.org/10.1016/S0167-5060(08)70743-X
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
E. L. Lawler, A "pseudopolynomial" algorithm for sequencing jobs to minimize total tardiness, Annals of Discrete Mathematics 1 (1977) 331–342. https://doi.org/10.1016/S0167-5060(08)70742-8
J. Du, J. Y.-T. Leung, Minimizing total tardiness on one machine is NP-hard, Mathematics of Operations Research 15 (1990) 483–495. https://doi.org/10.1287/moor.15.3.483
S. Cook, The P versus NP problem, Clay Mathematics Institute problem description, 2000. https://www.claymath.org/wp-content/uploads/2022/06/pvsnp.pdf

18 thms3 active usersReviewed

Complexity Theory Operations Research·Captain: mikedeng1

Complexity of Machine Scheduling Problems 2: KNAPSACK Reduces to Single-Machine Maximum Lateness, Weighted Number of Late Jobs, and Weighted Completion Time with DeadlinesResearch Paper

Motivation

Deterministic machine scheduling was one of the first application areas of the theory of NP-completeness. After Cook (1971) and Karp (1972) showed that a large family of combinatorial problems are polynomially equivalent, Brucker, Lenstra and Rinnooy Kan set out to locate the boundary between the polynomially solvable and the NP-complete scheduling problems. Their report Complexity of Machine Scheduling Problems (Mathematisch Centrum, Report BW 43/75, 1975; journal version in Annals of Discrete Mathematics 1, 1977) introduced the four-field notation $n|m|\ell,\lambda|k$ that, in refined form, is still the standard classification of scheduling problems, and proved NP-completeness of the "easiest" hard problems by explicit reductions.

Single-machine problems with due dates sit right at that boundary. Minimizing the maximum lateness $L_{\max}$ is solved by Jackson's earliest-due-date rule (1955), and minimizing the number of late jobs by Moore's algorithm (1968). Theorem 4 of the report shows that small changes to these problems — one release date, job weights, or due dates turned into deadlines under a weighted completion-time objective — make them NP-complete, by reduction from KNAPSACK. This mission formalizes four of those reductions, parts (b), (c), (e) and (f) of Theorem 4.

Timeline, as far as this mission is concerned:

1955: Jackson — $n|1||L_{\max}$ is solved by sequencing in order of nondecreasing due dates.
1968: Moore — $n|1||\sum U_j$ (unit weights, no release dates) is solvable in polynomial time.
1972: Karp — KNAPSACK (in the subset-sum form used here) is NP-complete; Karp also notes the reduction to $n|1||\sum w_jU_j$ , which the report cites for part (e).
1975: Brucker, Lenstra and Rinnooy Kan — Theorem 4: KNAPSACK reduces to ten scheduling problems, including the four single-machine problems of this mission.

Setting

A single-machine instance consists of $n\ge1$ jobs $J_1,\dots,J_n$ . Job $J_j$ needs $p_{j1}$ units of processing on the machine $M_1$ , has a weight $w_j$ , a release date $r_j$ and a due date $d_j$ ; all data are nonnegative integers. A schedule assigns to each job a starting time $B_j\ge r_j$ such that the occupied intervals $[B_j,B_j+p_{j1})$ of distinct jobs are disjoint. Idle time is allowed; a job with $p_{j1}=0$ occupies an empty interval. The completion time is $C_j=B_j+p_{j1}$ , the lateness is $L_j=C_j-d_j$ (possibly negative), and $U_j$ is $0$ if $C_j\le d_j$ and $1$ otherwise. The criteria are

L_{\max}=\max_j L_j,\qquad \sum w_jC_j=\sum_{j=1}^n w_jC_j,\qquad \sum w_jU_j=\sum_{j=1}^n w_jU_j .

The problem class is written in the $\lambda$ field: by default every $r_j=0$ ; $r_n\ge0$ allows a nonzero release date for the last job $J_n$ only; $w_j=1$ fixes unit weights; $L_{\max}\le0$ admits only schedules that meet every due date. A problem is turned into a yes/no question by asking whether a schedule with value $\le y$ exists.

KNAPSACK (Theorem 2(b) of the report): given positive integers $a_1,\dots,a_t,b$ , is there a subset $S\subseteq T=\{1,\dots,t\}$ with $\sum_{j\in S}a_j=b$ ? Write $A=\sum_{j\in T}a_j$ .

A problem $P'$ is reducible to $P$ , $P'\propto P$ , if every instance of $P'$ can be transformed in polynomial time into an instance of $P$ whose answer is the same.

Formalization targets

Goal: Theorem 4(b), (c), (e), (f)

\mathsf{KNAPSACK}\propto n|1|L_{\max}\le0|\textstyle\sum w_jC_j,\quad \mathsf{KNAPSACK}\propto n|1|r_n\ge0|L_{\max},

\mathsf{KNAPSACK}\propto n|1||\textstyle\sum w_jU_j,\quad \mathsf{KNAPSACK}\propto n|1|r_n\ge0,w_j=1|\textstyle\sum w_jU_j ,

as polynomial-time many-one reductions between languages of binary strings.

Milestones: the four yes-instance equivalences

For positive $a_1,\dots,a_t,b$ with $0<b<A$ , and the paper's constructions:

4(c): $n=t+1$ ; $r_j=0$ , $p_{j1}=a_j$ , $d_j=A+1$ for $j\in T$ ; $r_n=b$ , $p_{n1}=1$ , $d_n=b+1$ . KNAPSACK has a solution iff some schedule has $L_{\max}\le0$ .
4(f): the same instance with unit weights; KNAPSACK has a solution iff some schedule has $\sum U_j\le0$ .
4(e): $n=t$ ; $p_{j1}=w_j=a_j$ , $d_j=b$ . KNAPSACK has a solution iff some schedule has $\sum w_jU_j\le A-b$ .
4(b): $n=t+1$ ; $p_{j1}=w_j=a_j$ , $d_j=A+1$ for $j\in T$ ; $p_{n1}=1$ , $w_n=0$ , $d_n=b+1$ . KNAPSACK has a solution iff some schedule meeting all due dates has

\sum w_jC_j\le y=\sum_{j,k\in T,\ j\le k}a_ja_k+A-b .

Significance

The result. Combined with the NP-completeness of KNAPSACK, the four reductions show that the four problems are NP-hard (in the ordinary sense; they admit pseudo-polynomial algorithms). Part (c) shows that Jackson's rule cannot be extended to a single nonzero release date unless P = NP; part (f) does the same for Moore's algorithm; part (e) explains why weights are essential in the late-jobs problem; part (b) shows that deadlines turn the weighted completion-time problem, solved by Smith's ratio rule without them, into a hard one. These are entries of the complexity tables that every later scheduling classification builds on.

Formalizing it. The reductions are classical and proved on paper, in a few lines each: for (c), (e) and (f) the report gives only the construction and a figure. None of them has a machine-checked proof. A complete formalization supplies the explicit equivalence over all feasible schedules (including schedules with idle time and arbitrary processing order), the handling of the inputs the proof sets aside by "we may assume that $0<b<A$ ", and the polynomial-time computability of the constructions in a Turing-machine model.

Difficulty

Each equivalence has an easy direction: a subset $S$ with sum $b$ gives the schedule "jobs of $S$ , then $J_n$ , then the rest" (Figures 4 and 7 of the report). The other direction must rule out every feasible schedule, not only the idle-free ones in the displayed order. The report gives no argument for this direction in (c), (e) and (f), and for (b) only a computation for idle-free schedules of one shape. The equivalences are false outside $0<b<A$ in some cases (for (c), any $b>A$ makes every schedule on time), so the goal's reduction must treat those inputs separately.

The heavier part is polynomial-time computability: the reduction must be a function on strings, computed by a one-tape Turing machine within a polynomial number of steps, that parses a binary-coded KNAPSACK instance, computes $A$ and the threshold (for (b), a sum of $O(t^2)$ products), and writes the coded scheduling instance — and maps malformed strings outside the target language.

Formalization scope

Model. Jobs are Fin n (0-based; $J_n$ is the last index), with $n>0$ in each target language. Starting times are natural numbers: Section 3 computes them from processing orders on integer data, and since all criteria here are regular and release dates survive left shifts, real starting times give the same yes-instances. Feasibility requires disjoint occupied intervals, including empty intervals when $p_{j1}=0$ . Idle time is allowed. Lateness is an integer.
Problem classes are binding. $r_n\ge0$ means at least one job and release date $0$ for every job except the last; $L_{\max}\le0$ in (b) is a constraint on schedules, not the criterion. Instances outside the class are not in the target language.
Thresholds. $y\in\mathbb N$ in all four languages; for $L_{\max}$ this restricts to nonnegative thresholds, enough for the paper's $y=0$ . " $L_{\max}\le y$ " is stated as " $L_j\le y$ for all $j$ ".
Codes. An instance with threshold $y$ is the list $n$ , then $p_{j1},w_j,r_j,d_j$ per job, then $y$ , each number in binary.
Reducibility. "Reducible" (Section 2) is read as Karp reducibility, CookPvsNP.PolyReducible from the published definition CookPvsNP_defs. The alphabet and binary number codes are those of the published definition ProjSchedTW.Complexity.Encoding (Neumann, Schwindt and Zimmermann); its SUBSET SUM language is not reused because it admits zero sizes, while the paper's KNAPSACK is over positive integers.
Explicit readings of loose phrases. "We may assume that $0<b<A$ " becomes a hypothesis of each milestone and an obligation on the goal's reduction. "Cf. reduction (i) and Figure 4", "Cf. Karp [19] and Figure 7" and "The equivalence follows immediately" become the stated equivalences over all feasible schedules. Reduction (c) does not specify weights; the shared construction uses unit weights.
Not trivializable. The equivalences are stated for the paper's explicit constructions, not for an existentially chosen instance; the target languages enforce the problem class; and the goal demands polynomial-time computability, not only the equivalence.
Infrastructure. A Turing-machine library for arithmetic on binary codes (parsing, addition, multiplication, comparison) is reusable across all seven missions of this series and across every reduction posed in the same framework. Contributions of such general lemmas are welcome.

Parts (a), (d) and (g)–(j) of Theorem 4 are formalized in other missions of this series.

Selected references

P. Brucker, J. K. Lenstra, A. H. G. Rinnooy Kan, Complexity of Machine Scheduling Problems, Mathematisch Centrum, Report BW 43/75, Amsterdam, 1975; journal version: J. K. Lenstra, A. H. G. Rinnooy Kan, P. Brucker, Annals of Discrete Mathematics 1 (1977) 343–362. https://doi.org/10.1016/S0167-5060(08)70743-X
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
S. A. Cook, The complexity of theorem-proving procedures, Proc. 3rd ACM STOC, 1971, 151–158. https://doi.org/10.1145/800157.805047
J. M. Moore, An n job, one machine sequencing algorithm for minimizing the number of late jobs, Management Science 15 (1968) 102–109. https://doi.org/10.1287/mnsc.15.1.102
J. R. Jackson, Scheduling a production line to minimize maximum tardiness, Research Report 43, Management Science Research Project, UCLA, 1955.

11 thms3 active usersReviewed

Complexity Theory Operations Research·Captain: mikedeng1

Complexity of Machine Scheduling Problems 1: PARTITION Reduces to Makespan and to Weighted Completion Time on Two Identical MachinesResearch Paper

Motivation

Deterministic machine scheduling asks how to process a set of jobs on a set of machines so that an overall criterion, such as the time at which the last job finishes, is as small as possible. In the early 1970s many such problems had efficient algorithms (Johnson's rule for the two-machine flow shop, Smith's ratio rule for a single machine, Lawler's rule under precedence constraints), while others resisted every attempt. The report of Brucker, Lenstra and Rinnooy Kan (Mathematisch Centrum, 1975; journal version in Annals of Discrete Mathematics 1, 1977) drew the line between the two groups systematically. It fixed the four-field notation $n|m|\ell,\lambda|k$ that the scheduling literature still uses, and it proved NP-completeness of the "easiest" hard problems by explicit reductions in the sense of Karp.

The first family of reductions in the report, Theorem 3, concerns the simplest machine environment beyond a single machine: two identical machines. It shows that already there, minimizing the makespan and minimizing the total weighted completion time are as hard as PARTITION. These two reductions are simplified versions of reductions given by Bruno, Coffman and Sethi (1974), reference [3] of the report.

Setting

PARTITION. Given positive integers $a_1,\dots,a_t$ , decide whether there is a subset $S$ of $T=\{1,\dots,t\}$ with

\sum_{j\in S}a_j=\sum_{j\in T-S}a_j .

Write $A=\sum_{j\in T}a_j$ for the total.

Two identical machines. There are $n$ jobs $J_1,\dots,J_n$ and two machines $M_1,M_2$ . Job $J_j$ has a processing time $p_j\in\mathbb N$ and a weight $w_j\in\mathbb N$ , and must be processed without interruption on one machine of its choice; all jobs are available at time $0$ . A schedule assigns to every job a machine and a starting time $B_j\in\mathbb N$ ; its completion time is $C_j=B_j+p_j$ . A schedule is feasible if no two jobs on the same machine are processed at the same time, i.e. the intervals $[B_j,B_j+p_j)$ on each machine are pairwise disjoint. Idle time is allowed. Two criteria are considered:

C_{\max}=\max_j C_j,\qquad \sum_j w_jC_j .

The problems $n|2|I|C_{\max}$ and $n|2|I|\sum w_jC_j$ ask for a feasible schedule minimizing the respective criterion.

Reducibility. Following Section 2 of the report, each problem is replaced by its recognition version: given an instance and a threshold $y$ , is there a feasible schedule with value $\le y$ ? A problem $P'$ is reducible to $P$ , written $P'\propto P$ , if every instance of $P'$ can be transformed in polynomial time into an instance of $P$ with the same answer. Instances are written as words over a finite alphabet, with every number in binary.

Formalization targets

Goal: Theorem 3

\text{PARTITION}\propto n|2|I|C_{\max}\qquad\text{and}\qquad \text{PARTITION}\propto n|2|I|\textstyle\sum w_jC_j .

Both reductions use the same instance shape: $n=t$ jobs with $p_j=a_j$ .

Milestones

Theorem 3(a), equivalence. With $p_j=a_j$ and $y=\tfrac12A$ : PARTITION has a solution iff some feasible schedule has $C_{\max}\le y$ .
Ordering independence. With $p_j=w_j=a_j$ , if $S$ is the set of jobs on $M_1$ and each machine works without idle time from $0$ , then $\sum w_jC_j=k(S)$ for every order of the jobs, where

k(S)=\sum_{j,k\in S,\,j\le k}a_ja_k+\sum_{j,k\in T-S,\,j\le k}a_ja_k ;

every feasible schedule with this assignment has value at least $k(S)$ . 3. The identity for $k(S)$ . With $c=\sum_{j\in S}a_j-\tfrac12A$ ,

k(S)=k(T)-\Big(\sum_{j\in S}a_j\Big)\Big(\sum_{j\in T-S}a_j\Big)=\sum_{j,k\in T,\,j\le k}a_ja_k-\big(\tfrac12A+c\big)\big(\tfrac12A-c\big)=y+c^2 .

Theorem 3(b), equivalence. With $p_j=w_j=a_j$ and $y=\sum_{j,k\in T,\,j\le k}a_ja_k-\tfrac14A^2$ : PARTITION has a solution iff some feasible schedule has $\sum w_jC_j\le y$ .

Significance

The result. Since PARTITION is NP-complete (Karp 1972), Theorem 3 shows that both problems are NP-hard with only two machines and a single operation per job; their recognition versions are NP-complete. Together with the single-machine and shop results in the rest of the report, it places the boundary of tractability in deterministic scheduling. The makespan problem $P2\|C_{\max}$ became a standard source problem for later hardness proofs and a standard target for pseudo-polynomial algorithms and approximation schemes. The weighted completion time result contrasts with the single-machine case, which Smith's ratio rule solves in polynomial time.

Formalizing it. The theorem is classical and fully proved on paper; the report prints the constructions and, for (b), a short calculation. To our knowledge no machine-checked proof exists. The mission produces (i) a precise model of nonpreemptive schedules on two identical machines with integer start times and idle time allowed, (ii) the two yes-instance equivalences with the paper's rational thresholds, (iii) the ordering-independence statement for $p_j=w_j$ behind part (b), and (iv) the polynomial-time computability of the reductions in a Turing machine model. Part (iv) is the formal content of "reducible" and is missing from the paper.

Difficulty

For part (a) the mathematics is short. The paper treats it as evident; a formal proof must still handle schedules with idle time and the case of odd $A$ , where $\tfrac12A$ is not an integer.

Part (b) rests on the claim that, when $p_j=w_j$ , the value $\sum w_jC_j$ does not depend on the order of the jobs on a machine. For a single machine without idle time this is a symmetric double sum. A recognition-problem proof also needs the converse direction: no schedule with idle time beats the non-idle one, so every feasible schedule with assignment $S$ has value at least $k(S)$ . The paper cites this rather than proving it.

The step the paper leaves out entirely is polynomiality. The constructions copy the input and compute $\tfrac12A$ or $\sum_{j\le k}a_ja_k-\tfrac14A^2$ , and in a one-tape Turing machine model with an explicit polynomial time bound this needs binary arithmetic (sums, products, a floor) carried out on the tape. It also needs a decoder that rejects malformed words and lists containing a zero. This is routine in principle but long in practice.

Formalization scope

Model. Jobs are Fin n and machines Fin 2 (machine 0 is $M_1$ ). Starting times are natural numbers. Section 3 of the report computes them from processing orders on nonnegative integer data, and both criteria are regular, so real starting times would give the same yes-instances. Processing times may be zero; a zero-length job occupies the empty interval. Schedules may contain idle time.
Criteria. " $C_{\max}\le y$ " is stated as $C_j\le y$ for every job, which equals $\max_jC_j\le y$ for $n\ge1$ and avoids a supremum. $\sum w_jC_j$ is a finite sum in $\mathbb N$ .
Languages. PARTITION is the set of binary codes of lists of positive integers that admit a partition; a code of a list with a zero entry is not in the language. A target word codes $n$ , the processing times (and weights, job by job), and a threshold $y\in\mathbb N$ . The number of machines is fixed by the class and not coded. Every coded instance is in the class, so the language admits nothing outside it.
Reducibility is CookPvsNP.PolyReducible from the published definition CookPvsNP_defs (Cook's one-tape Turing machines, polynomial-time many-one reductions). The alphabet BSym and the binary code encNats are reused from the published ProjSchedTW.Complexity.Encoding (Neumann, Schwindt and Zimmermann). Its PARTITION language is not reused, because it allows zero sizes.
Thresholds. The milestones state the paper's thresholds $\tfrac12A$ and $\sum_{j\le k}a_ja_k-\tfrac14A^2$ as real numbers, exactly as printed. The goal's reduction must write a natural-number threshold; all schedule values are integers, so the floor of the printed threshold gives the same yes-instances.
Explicit readings. The equivalence of (a) is not printed; the report says on p. 14 that such equivalences are "trivial or clear" where not proved. "Only depends on the choice of $S$ " is stated as two facts: equality for non-idle schedules and a lower bound for all feasible schedules. "It is easily seen (cf. Figure 1)" is the three-step identity, one equality per printed step. $k(S)$ is defined by its closed form, and its link to schedules is a milestone.
Ruled out. A target language whose yes-instances are defined through PARTITION, an equivalence for some instance rather than the paper's construction, and a goal that drops polynomial-time computability would all make the goal vacuous or different. The statements here use the constructions as printed and Cook's reducibility.
Welcome contributions. Proofs of the four milestones; a library of polynomial-time Turing machine programs for binary arithmetic and list decoding over BSym, which every mission of this series needs and which is reusable for other reductions on the platform.

Selected references

P. Brucker, J. K. Lenstra, A. H. G. Rinnooy Kan, Complexity of Machine Scheduling Problems, Mathematisch Centrum Report BW 43/75, Amsterdam, 1975. https://ir.cwi.nl/pub/9725/9725D.pdf
J. K. Lenstra, A. H. G. Rinnooy Kan, P. Brucker, Complexity of machine scheduling problems, Annals of Discrete Mathematics 1 (1977) 343–362. https://doi.org/10.1016/S0167-5060(08)70743-X
J. Bruno, E. G. Coffman Jr., R. Sethi, Scheduling independent tasks to reduce mean finishing time, Communications of the ACM 17 (1974) 382–387. https://doi.org/10.1145/361011.361064
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
S. A. Cook, The complexity of theorem-proving procedures, STOC 1971, 151–158. https://doi.org/10.1145/800157.805047
W. E. Smith, Various optimizers for single-stage production, Naval Research Logistics Quarterly 3 (1956) 59–66. https://doi.org/10.1002/nav.3800030106

11 thms3 active usersReviewed

Completed

Combinatorics Operations Research Probability·Captain: mikedeng1

Online Stochastic Matching: Beating 1-1/e 3: No Online Algorithm Beats Expected Approximation Factor 26/27 on a 6-Cycle, and None Reaches 1 − o(1) on Disjoint 6-CyclesResearch Paper

Motivation

Online bipartite matching asks an algorithm to assign arriving requests to resources it cannot reassign later. In display advertising, the requests are page views (impressions) and the resources are advertisers who have bought a fixed number of impressions in advance; each impression must be served immediately or lost. In the adversarial model, Karp, Vazirani and Vazirani (STOC 1990) showed that the RANKING algorithm achieves a $1 - 1/e$ fraction of the optimum in expectation, and that no online algorithm does better. Advertising systems, however, have historical traffic data, which motivates the i.i.d. model: the impression types are drawn independently from a distribution that is known in advance.

Feldman, Mehta, Mirrokni and Muthukrishnan (arXiv:0905.4100, FOCS 2009) were the first to beat $1 - 1/e$ in this model, with an algorithm that achieves $\approx 0.67$ with high probability. Their Section 3 asks the complementary question: how close to $1$ can any online algorithm get when the distribution is known? Their Theorem 3 answers that the expected approximation factor of every online algorithm is bounded strictly away from $1$ , already on a graph with six vertices. Later work in the same model (Manshadi, Oveis Gharan and Saberi, SODA 2011, arXiv:1007.1673) sharpened both the algorithmic and the hardness side.

Setting

An instance consists of a bipartite graph $G = (A, I, E)$ between a finite set $A$ of advertisers and a finite set $I$ of impression types, a distribution $D$ on $I$ , and a number $n$ of arrivals. In this mission $D$ is the uniform distribution on $I$ . Online, $n$ impressions arrive one at a time; their types $\omega(0), \dots, \omega(n-1)$ are independent draws from $D$ . When impression $t$ arrives, the algorithm must immediately either assign it to an advertiser $a$ with $(a, \omega(t)) \in E$ that has not yet been used, or leave it unassigned. Each advertiser can be used at most once, and decisions are final.

A deterministic online algorithm decides what to do with arrival $t$ from the types $\omega(0), \dots, \omega(t)$ seen so far; it knows $G$ , $D$ and $n$ , but not the future. A randomized online algorithm is a probability distribution over deterministic ones. $\mathrm{ALG}(\omega)$ is the number of impressions the algorithm assigns on the arrival sequence $\omega$ . $\mathrm{OPT}(\omega)$ is the size of a maximum matching of the realization graph, which has one node per arrival $t$ , joined to every advertiser adjacent to $\omega(t)$ : the most impressions that could have been assigned with hindsight. The expected approximation factor of an algorithm is

\mathbb E\!\left[\frac{\mathrm{ALG}(\omega)}{\mathrm{OPT}(\omega)}\right],

the expectation taken over the algorithm's randomness and the arrivals.

The 6-cycle instance has $A = \{a, b, c\}$ , $I = \{x, y, z\}$ and $E = \{(x,a),(y,a),(y,b),(z,b),(z,c),(x,c)\}$ , with the uniform distribution and $n = 3$ . The family $\Gamma_k$ consists of $k$ disjoint copies of the 6-cycle, with the uniform distribution on its $3k$ impression types and $n = 3k$ arrivals.

Formalization targets

Goal: Theorem 3

On the 6-cycle, every randomized online algorithm satisfies

\mathbb E\!\left[\frac{\mathrm{ALG}}{\mathrm{OPT}}\right] \le \frac{26}{27},

and there are a constant $c < 1$ and a threshold $K_0$ such that for every $k \ge K_0$ and every randomized online algorithm on $\Gamma_k$ ,

\mathbb E\!\left[\frac{\mathrm{ALG}}{\mathrm{OPT}}\right] \le c .

The second part is the paper's "there exists a family of instances with $n \to \infty$ for which no algorithm can achieve an expected approximation of $1 - o(1)$ ", stated on the paper's own family. It leaves $c$ unspecified: Appendix B estimates $c \approx 0.9898$ through approximate counts, and a sharper constant would not invalidate the goal.

Milestones

The $(x, y, y)$ scenario (§3, p. 4). For every deterministic online algorithm on the 6-cycle and every type $u$ of the first arrival there is a type $v$ with $\mathrm{ALG}(u, v, v) \le 2$ and $\mathrm{OPT}(u, v, v) = 3$ .
Theorem 3, first sentence (p. 4). The bound $26/27$ on the 6-cycle, for every randomized online algorithm.

Significance

Theorem 3 sets the ceiling against which algorithms in the i.i.d. model are measured. It rules out an online algorithm with expected factor arbitrarily close to $1$ , even though the distribution is known and the instance is tiny, so a constant-factor gap between online and offline matching is intrinsic to the model and not an artefact of adversarial arrivals. The paper's positive results ( $1 - 1/e$ for the Suggested Matching algorithm, $\approx 0.67$ for Two Suggested Matchings) sit between $1 - 1/e$ and this ceiling.

The single-instance bound has a short counting proof. The family statement is argued in the paper only in outline: Appendix B approximates the fractions of copies receiving $1$ , $2$ , $3$ or more impressions, assumes the most favourable outcome on each, and reports the resulting ratio as approximately $0.9898$ . A machine-checked proof of the family statement would turn that sketch into a theorem with an explicit constant. To our knowledge neither part has been formalized before.

Difficulty

The single-cycle bound reduces to a finite check, but the paper's "without loss of generality (from the symmetry of the 6-cycle)" hides the cases the algorithm can choose: assigning the first impression to either neighbour, or not assigning it at all. Each case needs its own bad continuation. The passage from deterministic to randomized algorithms is an averaging step.

The family bound is harder. On $\Gamma_k$ the algorithm sees all arrivals in all copies and may coordinate its decisions across copies, so the per-copy loss of the single cycle does not transfer by independence. Moreover the target is the expectation of a ratio, $\mathbb E[\mathrm{ALG}/\mathrm{OPT}]$ , not a ratio of expectations: a bound on the expected loss must be combined with concentration of the number of copies that receive exactly three impressions, and with a lower bound on $\mathrm{OPT}$ that holds with high probability. The approximations " $\simeq 3/e^3$ , $9/(2e^3)$ , $27/(6e^3)$ " of Appendix B have unquantified errors and cannot be used as they stand.

Formalization scope

The model is formalized for general finite $A$ and $I$ with uniform arrivals. Arrival sequences are functions Fin n → I. A deterministic online algorithm is a function that receives the time $t$ , the prefix of the first $t$ types (Fin t → I) and the current type, and returns an advertiser or none; it cannot read later arrivals. A proposal of a non-adjacent or already used advertiser leaves the impression unassigned, so the encoding covers all online algorithms, including ones that skip an impression while a neighbour is free. A randomized online algorithm is a probability distribution (PMF) on the finite type of deterministic algorithms; by Kuhn's theorem this is equivalent to fresh random choices at each step. $\mathrm{OPT}$ is the maximum size of an injective, edge-respecting partial assignment of arrivals to advertisers. The expected approximation factor is a finite average over all $|I|^n$ arrival sequences, weighted by the algorithm distribution.

The explicit instantiations of the paper's asymptotic wording are as follows:

"no algorithm can achieve an expected approximation of $1 - o(1)$ " becomes $\exists\, c < 1,\ \exists K_0,\ \forall k \ge K_0,\ \forall P:\ \mathbb E[\mathrm{ALG}/\mathrm{OPT}] \le c$ on $\Gamma_k$ , with $n = 3k$ tied to $k$ , and with $c$ and $K_0$ chosen before $k$ and before the algorithm.
The paper's constant $0.9898$ is not part of the statement.

Lean's division sets $x/0 = 0$ . A formalization of the form "there is an instance on which every algorithm has expected factor at most $26/27$ " would be satisfied trivially by a graph without edges, where $\mathrm{OPT} = 0$ ; the statements here are on the paper's explicit instances, where every impression type has an adjacent advertiser and $\mathrm{OPT} \ge 1$ on every arrival sequence.

A complete development needs finite case analysis on runs of online algorithms, averaging over mixed strategies, and, for the family, concentration inequalities for occupancy counts (Azuma or McDiarmid, both available on the platform) together with bounds on maximum matchings of disjoint unions. The online-algorithm model and the averaging lemmas are reusable for other lower bounds in the i.i.d. model. Proofs of either milestone, and independent proofs of the family statement with any explicit $c < 1$ , are welcome.

Selected references

J. Feldman, A. Mehta, V. Mirrokni, S. Muthukrishnan, Online Stochastic Matching: Beating 1-1/e, FOCS 2009; arXiv:0905.4100v1. https://arxiv.org/abs/0905.4100
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
V. H. Manshadi, S. Oveis Gharan, A. Saberi, Online Stochastic Matching: Online Actions Based on Offline Statistics, SODA 2011; arXiv:1007.1673. https://arxiv.org/abs/1007.1673

5 thms3 active usersReviewed

Completed

Combinatorics Graph Theory·Captain: mikedeng1

On the Approximability of Single-Machine Scheduling with Precedence Constraints 3: The Incomparable-Pairs Graphs of Canonical Interval Orders Have Unbounded Chromatic NumberResearch Paper

Motivation

Single-machine scheduling with precedence constraints asks for an order in which one machine processes jobs while respecting prescribed comparisons between them. For the objective of minimizing total weighted completion time, the structure of the precedence order can influence the quality of approximation algorithms. Ambühl, Mastrolilli, Mutsanas, and Svensson connect one such approach to coloring a graph built from the order's incomparable pairs. A bounded number of colors would make a certain class of coloring-based guarantees uniform over the class of precedence orders. Their Theorem 4.3 shows that canonical interval orders have no such uniform bound for this particular graph. Ambühl et al., §4.2, p. 658

An interval order is a partial order whose elements can be represented by closed real intervals, with one element strictly before another when the first interval ends before the second begins. Interval orders are a familiar restriction of general precedence systems. The paper distinguishes them from semiorders, represented by intervals of equal length, for which it reports a three-element realizer bound and a corresponding scheduling guarantee. The chromatic obstruction here explains why that particular bounded-color route cannot be extended uniformly from semiorders to all interval orders. It does not assert that every scheduling approach to interval orders fails. Ambühl et al., §§3–4.2, pp. 656–658

Setting

For an integer $n\ge2$ , let $[n]$ be a linearly ordered set with $n$ points. The canonical interval order $I_n$ has one element for every pair of distinct points $a<b$ in $[n]$ , viewed as the closed interval $[a,b]$ . For two such intervals, write $S\le_{I_n}T$ when $S=T$ or the right endpoint of $S$ is strictly less than the left endpoint of $T$ . Thus intervals that touch at an endpoint remain incomparable. The formalization represents each interval by its two-element endpoint set, and its order relation is equivalent to this endpoint rule. Ambühl et al., §4.2, p. 658

For any partial order $P$ on a ground set $N$ , an ordered incomparable pair is $(x,y)$ with neither $x\le_P y$ nor $y\le_P x$ . Both $(x,y)$ and $(y,x)$ are vertices when $x$ and $y$ are incomparable. A linear extension of $P$ is a linear order on the same elements that contains all comparisons of $P$ . It reverses $(x,y)$ if it places $y$ before $x$ . The graph $G_P$ has the ordered incomparable pairs as vertices. Two distinct vertices form an edge when no linear extension reverses both, while each singleton can be reversed by some linear extension. This singleton condition is the minimality clause in the paper's definition through its hypergraph of incomparable pairs. Ambühl et al., §2.1, p. 655, §3, p. 656

A proper $k$ -coloring assigns one of $k$ colors to every vertex of $G_P$ so that endpoints of an edge have different colors. The graph's chromatic number $\chi(G_P)$ is the least positive number of colors that works, when the graph is nonempty. The mission uses the equivalent predicate that no proper map into a fixed $k$ -element color set exists once $n$ is large enough. This also gives a clear interpretation at $k=0$ .

Formalization targets

The goal is Theorem 4.3: for each fixed integer $k$ , all sufficiently large canonical interval orders have incomparable-pairs graphs with chromatic number greater than $k$ . With $k\ge0$ , the Lean target is

\forall k\in\mathbb N,\ \exists n_0\ge2,\ \forall n\ge n_0,\quad G_{I_n}\text{ is not $k$-colorable}.

The paper states $k$ as an integer. Its negative cases are immediate from nonnegativity of chromatic numbers; the target states the substantive range. The threshold $n_0$ may depend on $k$ , while $I_n$ and $G_{I_n}$ are constructed from $n$ rather than supplied as arbitrary objects. Ambühl et al., Theorem 4.3, p. 658

Two assertions from the theorem's proof serve as milestones. First, $\chi(G_{I_n})$ is nondecreasing as $n$ increases. Second, for four endpoints $i<j<\ell<m$ , the vertices $(\{i,j\},\{j,\ell\})$ and $(\{j,\ell\},\{\ell,m\})$ are adjacent in $G_{I_n}$ . They are recorded with their wording and provenance from §4.2. A separately published theorem on hypergraph Ramsey numbers is included as a reference because the source uses that theorem in its large- $n$ argument. Ambühl et al., proof of Theorem 4.3, p. 658

Significance

The result provides a precise structural limitation: across the canonical interval orders, the chromatic numbers of $G_{I_n}$ cannot be bounded by one constant. The graph $G_P$ is a specific graph of ordered incomparable pairs, distinct from other graphs that can be associated with a scheduling instance. Thus the conclusion addresses the bounded-color approach attached to this graph, without asserting an algorithmic impossibility for interval-order scheduling. The paper contrasts this limitation with the bounded-realizer situation for semiorders. Ambühl et al., §§3–4.2, pp. 656–658

The theorem is proved in the 2011 paper. The remaining work in this mission is a machine-checked development of its definition layer, its two stated supporting assertions, and the unbounded-color conclusion. The partial-order property of $I_n$ is already proved in the definition file; the three theorem statements are open proof targets in the proposal. A completed formalization would also give reusable components for finite interval orders, ordered incomparable pairs, and coloring arguments in dimension theory.

Difficulty

A pair of intervals overlapping or touching is easy to recognize as incomparable, but graph adjacency has a stronger meaning: it quantifies over every linear extension of the entire partial order. A local test based only on the four displayed intervals would silently change the graph. Likewise, the fact that two vertices have different endpoint descriptions does not by itself make them adjacent. The formal argument must connect the canonical interval representation to the global extension-based edge condition, then show that a bounded coloring cannot persist as the endpoint set grows. Ambühl et al., proof of Theorem 4.3, p. 658

Formalization scope

The endpoint set is Fin n, hence indexed $0,\ldots,n-1$ rather than the paper's $1,\ldots,n$ ; the shift preserves order. Elements of $I_n$ are exactly two-element subsets of this set. The order relation includes equality and strict separation of endpoint sets and is proved to be a partial order. The graph is defined for an arbitrary binary relation so it can be reused, but every target here applies it to the concrete partial order $I_n$ . Vertices are ordered incomparable pairs, and adjacency retains both singleton reversibility and failure of simultaneous reversibility. Defining adjacency directly from the desired four-point pattern would trivialize the target and is excluded.

Colorable n k means existence of a proper function from all vertices of $G_{I_n}$ to Fin k. For an empty graph, zero-colorability is allowed by this representation. The theorem therefore includes a threshold $n_0\ge2$ and quantifies over every $n\ge n_0$ ; the assertion itself forces the threshold past any empty-graph exceptions. The formal target uses natural $k$ ; the paper's negative integer values need no separate theorem. No asymptotic notation or unspecified constants occur. The source's Ramsey number $R(3:4,\ldots,4)$ is not hard-coded into the goal, because the source asserts existence of a suitable threshold, not that the least threshold equals that value.

The printed adjacency justification names an alternating-cycle pair set different from the two adjacent vertices in the preceding sentence. The milestone formalizes the adjacency assertion itself and records the printed explanation verbatim for review; it does not turn the mismatched pair set into a hypothesis. The mission needs finite order embeddings, linear extensions, graph colorings, and a finite Ramsey theorem. The existing published Ramsey theorem is referenced as a reusable result. No scheduling approximation algorithm, polynomial-time statement, or numerical scheduling guarantee is formalized in this mission.

Selected references

Christoph Ambühl, Monaldo Mastrolilli, Nikolaos Mutsanas, and Ola Svensson, On the Approximability of Single-Machine Scheduling with Precedence Constraints, Mathematics of Operations Research 36(4), 653–669, 2011. DOI: 10.1287/moor.1110.0512

7 thms3 active usersReviewed

Completed

Combinatorics Graph Theory Operations Research·Captain: mikedeng1

On the Approximability of Single-Machine Scheduling with Precedence Constraints 1: A k-Fold Realizer of Size t Yields a Vertex Cover of Expected Weight at Most (2 − 2/(t/k)) Times OptimalResearch Paper

Motivation

Single-machine scheduling with precedence constraints, written $1|\mathrm{prec}|\sum w_jC_j$ in the notation of Graham et al., asks for an order of $n$ weighted jobs on one machine that respects a given partial order and minimizes the weighted sum of completion times. The problem is strongly NP-hard (Lawler 1978; Lenstra and Rinnooy Kan 1978), and closing its approximability gap is listed by Schuurman and Woeginger among ten outstanding open problems in scheduling theory. Several 2-approximation algorithms are known (Schulz 1996; Hall et al. 1997; Chudak and Hochbaum 1999; Chekuri and Motwani 1999; Margot et al. 2003).

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 built from the precedence order. Ambühl, Mastrolilli, Mutsanas and Svensson (Math. Oper. Res. 36(4), 2011) observed that this graph is the graph of incomparable pairs of dimension theory, and used that identification to obtain $(2-2/f)$ -approximations for orders of fractional dimension at most $f$ . This mission formalizes that framework: the identification of the two graphs and the rounding guarantee of the paper's Theorem 5.1.

Setting

An instance $S$ consists of a finite set $N$ of jobs, a partial order $P$ on $N$ (reflexive, antisymmetric, transitive; $(i,j)\in P$ with $i\ne j$ means job $i$ finishes before job $j$ starts), processing times $p_j\ge 0$ and weights $w_j\ge 0$ .

Two jobs $x,y$ are incomparable, $x\parallel y$ , when neither $(x,y)$ nor $(y,x)$ lies in $P$ . The set $\operatorname{inc}(P)$ of incomparable pairs consists of ordered pairs and is closed under swapping. A linear extension of $P$ is a linear order $L\supseteq P$ on $N$ ; it reverses $(x,y)\in\operatorname{inc}(P)$ when $y<x$ in $L$ . A nonempty multiset $L_1,\dots,L_t$ of linear extensions is a $k:t$ -realizer if every incomparable pair is reversed by at least $k$ of them. The fractional dimension $\operatorname{fdim}(P)$ is the least ratio $t/k$ over all $k:t$ -realizers.

The vertex cover graph $G^S_P$ has the incomparable pairs as nodes; 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),(k,j)\in P$ (symmetrically closed). Node $(i,j)$ has weight $w_{(i,j)}=p_iw_j$ , and $w(C)=\sum_{u\in C}w_u$ . $\mathrm{OPT}$ is the minimum weight of a vertex cover of $G^S_P$ . The LP relaxation [CS-LP] asks for $x\in[0,1]^{\operatorname{inc}(P)}$ with $x_u+x_v\ge1$ on every edge, minimizing $\sum_u w_ux_u$ . For a solution $x$ write $V_a=\{u: x_u=a\}$ , and for a linear extension $L$ let $I_{1/2}(L)$ be the pairs of $V_{1/2}$ reversed in $L$ .

The graph of incomparable pairs $G_P$ (Felsner and Trotter 2000) also has the incomparable pairs as vertices; two of them are adjacent when the pair of them is a minimal set of incomparable pairs that no linear extension reverses entirely.

Formalization targets

Goal: Theorem 5.1 (p. 658)

For an instance $S$ , a $k:t$ -realizer $L_1,\dots,L_t$ of $P$ , and a half-integral optimal solution $x$ of [CS-LP], put $C_i=V_1\cup\bigl(V_{1/2}\setminus I_{1/2}(L_i)\bigr)$ . Then every $C_i$ is a vertex cover of $G^S_P$ , and

\frac1t\sum_{i=1}^t w(C_i)\;\le\;\Bigl(2-\frac{2}{t/k}\Bigr)\mathrm{OPT}.

Milestones

Proposition 3.2 (p. 657): $G^S_P=G_P$ .
Footnote 4 (p. 659): the pairs reversed by a linear extension are independent in $G^S_P$ .
Eq. (4): $\frac1t|\{i: L_i\text{ reverses }u\}|\ge k/t$ for every incomparable pair $u$ .
Eq. (5): $\frac1t\sum_i w(I_{1/2}(L_i))\ge \frac kt\,w(V_{1/2})$ .
Hochbaum's observation (§5, p. 659): for half-integral feasible $x$ , $V_1\cup C$ covers $G^S_P$ whenever $C$ covers $G^S_P[V_{1/2}]$ .
Eqs. (6)–(8): $\frac1t\sum_iw(C_i)\le w(V_1)+(1-\frac kt)w(V_{1/2})\le 2(1-\frac kt)(w(V_1)+\frac12w(V_{1/2}))\le(2-\frac2{t/k})\mathrm{OPT}$ when $P$ is not a linear order.

Significance

The result. Combined with the cited Theorem 2.1 (Ambühl–Mastrolilli 2009; Correa–Schulz 2005), which turns an $\alpha$ -approximate vertex cover of $G^S_P$ into an $\alpha$ -approximate schedule, Theorem 5.1 gives a $(2-2/f)$ -approximation for $1|\mathrm{prec}|\sum w_jC_j$ whenever the precedence order has an efficiently samplable realizer with $t/k\le f$ . The paper applies it to interval orders ( $3/2$ ), convex bipartite orders and semiorders ( $4/3$ ), orders of bounded degree and orders of interval dimension two; for the earlier special classes it matched or improved the best known ratios, and for the last two it gave the first results. Proposition 3.2 makes the dimension theory of posets (realizers, critical pairs, fractional dimension) directly available to the vertex cover approach.

Formalizing it. The results are proved in the paper; to the best of current knowledge none of them has a machine-checked proof. The mission produces a Lean development of incomparable pairs, linear extensions, $k$ -fold realizers and the hypergraph of incomparable pairs, which other dimension-theory missions can reuse, and a verified LP-rounding argument for half-integral vertex cover solutions under a distribution of independent sets.

Difficulty

Most of the rounding argument is arithmetic over finite sums. The central nontrivial step is the inclusion $G_P\subseteq G^S_P$ in Proposition 3.2: for two incomparable pairs that are not adjacent under the three-case rule, one must construct a single linear extension reversing both. This needs an extension of $P$ by two new comparabilities whose transitive closure is still antisymmetric, followed by Szpilrajn's theorem; checking that every potential cycle is excluded by the three cases is the actual content. The opposite inclusion, and footnote 4, follow from transitivity and antisymmetry of linear orders. A second point of care is the inequality $t\ge 2k$ used in step (7): it is not part of the definition of a realizer, and follows from each linear extension reversing exactly one of $(x,y)$ and $(y,x)$ .

Formalization scope

Jobs form a finite type N; the precedence order is a relation P : N → N → Prop with IsPartialOrder, carried by the structure Instance. Processing times and weights are nonnegative reals.
$\operatorname{inc}(P)$ is the subtype IncPair P of N × N; a linear extension is a relation with IsLinearOrder containing P; a $k:t$ -realizer is a family Fin t → LinearExtension P with $t>0$ . Reversal of $(x,y)$ means $y<x$ in $L$ throughout; the page's " $y>x$ " in Eq. (4) and " $\mathrm{Prob}[j>i]$ " in Eq. (5) are the same family of inequalities because $\operatorname{inc}(P)$ is symmetric.
$G^S_P$ is the symmetric closure of the printed three-case rule on distinct nodes. $G_P$ is defined through linear extensions and hyperedge minimality, never through the three-case rule, so Proposition 3.2 is a genuine statement and not a definitional equality.
[CS-LP] drops the constant term $\sum_jp_jw_j+\sum_{(i,j)\in P}p_iw_j$ of [CS-IP], which does not affect optimality. $\mathrm{OPT}$ is the minimum weight of a vertex cover of $G^S_P$ , taken over a finite nonempty family.
Not formalized: "efficiently samplable", "polynomial time" and "randomized algorithm". The expectation over a uniformly sampled $L_i$ is stated as the average $\frac1t\sum_{i=1}^t$ , which is equivalent to it and stronger than the existence of one good index. The existence of a half-integral optimal [CS-LP] solution (Nemhauser–Trotter, cited) is a hypothesis on $x$ . The conversion of a vertex cover into a schedule (Theorem 2.1, cited) is not formalized; the goal is stated for vertex covers of $G^S_P$ .
Constants: $2-2/(t/k)$ in real arithmetic; it equals $2-2k/t$ , and equals $2$ when $k=0$ .
The paper assumes $\operatorname{fdim}(P)\ge2$ , i.e. $P$ is not a linear order. Eqs. (6)–(8) carry that hypothesis as the paper does; the goal omits it because for a linear order both sides are $0$ .
Conclusion (a), that each $C_i$ is a vertex cover, is part of the goal and is not assumed.

Contributions welcome: proofs of the milestones in any order, and a reusable Szpilrajn-style lemma producing a linear extension that reverses a prescribed set of compatible incomparable pairs.

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), 2009 (reference [2] of the paper).
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
G. R. Brightwell, E. R. Scheinerman, Fractional dimension of partial orders, Order 9(2):139–158, 1992 (reference [7]).
S. Felsner, W. T. Trotter, Dimension, graph and hypergraph coloring, Order 17(2):167–177, 2000 (reference [13]).
D. S. Hochbaum, Efficient bounds for the stable set, vertex cover and set packing problems, Discrete Appl. Math. 6(3):243–254, 1983 (reference [20]).
G. L. Nemhauser, L. E. Trotter, Vertex packings: structural properties and algorithms, Math. Programming 8(1):232–248, 1975 (reference [29]).

10 thms3 active usersReviewed

Information Theory Quantum Information·Captain: mikedeng1

Shadow Tomography of Quantum States 3: Shadow Tomography Needs Ω(min{D², log M}/ε²) CopiesResearch Paper

Why count copies of a quantum state

A mixed state of a $D$ -dimensional quantum system is a $D\times D$ positive semidefinite matrix $\rho$ of trace $1$ . Writing $\rho$ down takes about $D^2$ real numbers, and $D$ is exponential in the number of qubits, so learning $\rho$ in full is expensive. Holevo's theorem and the random access code bounds of Ambainis, Nayak, Ta-Shma and Vazirani say that an $n$ -qubit state carries far fewer usable classical bits than its $2^n$ amplitudes suggest. Shadow tomography, introduced by S. Aaronson (arXiv:1711.01053), makes this quantitative: given $M$ known two-outcome measurements $E_1,\dots,E_M$ , how many copies of an unknown $\rho$ are needed to estimate every acceptance probability $\operatorname{Tr}(E_i\rho)$ to within $\varepsilon$ ?

Aaronson shows that $\widetilde O(\log^4 M\cdot\log D/\varepsilon^4)$ copies suffice, polylogarithmic in $M$ and $D$ . The question this mission addresses is the converse: how many copies are necessary. Section 6 of the paper proves two lower bounds. Theorem 16 gives $\Omega(\min\{D,\log M\}/\varepsilon^2)$ even when $\rho$ and the $E_i$ are diagonal (a classical distribution). Theorem 19, the goal here, strengthens the dimension term to $D^2$ for genuinely quantum states.

Timeline:

2016: full tomography of a $D$ -dimensional state to trace-distance accuracy $\varepsilon$ needs $\Theta(D^2/\varepsilon^2)$ copies up to logarithmic factors, with upper and lower bounds by O'Donnell and Wright (arXiv:1508.01907) and Haah, Harrow, Ji, Wu and Yu (arXiv:1508.01797).
2017–2018: Aaronson poses shadow tomography (Problem 1), proves the polylogarithmic upper bound (Theorem 2), and proves the lower bounds of Theorems 16 and 19.
2020 onward: classical shadows (Huang, Kueng and Preskill, arXiv:2002.08953) and later shadow-tomography algorithms study the same estimation task with other measurement models and improved upper bounds.

Setting

Fix a dimension $D$ . A two-outcome measurement is a $D\times D$ Hermitian matrix $E$ with $0\preceq E\preceq I$ ; it accepts $\rho$ with probability $\operatorname{Tr}(E\rho)$ . The tensor power $\rho^{\otimes k}$ is the $D^k\times D^k$ matrix of $k$ independent copies. A strategy using $k$ copies is a measurement of $\rho^{\otimes k}$ with finitely many outcomes $\omega\in\Omega$ , given by positive semidefinite matrices $\Pi_\omega$ with $\sum_\omega\Pi_\omega = I$ , together with outputs $b(\omega)=(b_1(\omega),\dots,b_M(\omega))$ . It succeeds on $\rho$ when, with probability at least $2/3$ over $\omega$ , $|b_i(\omega)-\operatorname{Tr}(E_i\rho)|\le\varepsilon$ for every $i\in[M]$ .

The proof works with these further objects, all defined in the mission:

an orthogonal projection $\mathbb P$ onto an $N/2$ -dimensional subspace of $\mathbb C^N$ (Hermitian, idempotent, trace $N/2$ );
$\rho_{\mathbb P} := \tfrac2N\mathbb P$ , the maximally mixed state on that subspace;
$\sigma_{\mathbb P,\varepsilon} := (1-6\varepsilon)\,\mathbb I/N + 6\varepsilon\,\rho_{\mathbb P}$ ;
the von Neumann entropy in bits, $S(\rho) = -\sum_x\lambda_x\log_2\lambda_x$ over the eigenvalues of $\rho$ ;
for states $\sigma_1,\dots,\sigma_K$ and $\zeta := \tfrac1K\sum_i\sigma_i^{\otimes T}$ , the quantum mutual information with the classical index, $I(\zeta;i) := S(\zeta) - \tfrac1K\sum_i S(\sigma_i^{\otimes T})$ .

Formalization targets

Goal: Theorem 19 (p. 23)

There are a universal constant $c>0$ and a threshold $N_0$ such that for all $D\ge N_0$ , all $M$ with $\log_2 M\ge N_0^2$ and all $0<\varepsilon\le\tfrac16$ , some measurements $E_1,\dots,E_M$ on $\mathbb C^D$ force every strategy that succeeds on every mixed state to use

k \;\ge\; c\,\frac{\min\{D^2,\ \log_2 M\}}{\varepsilon^2}

copies. The goal fixes only the shape $\Omega(\min\{D^2,\log M\}/\varepsilon^2)$ , not a constant, so a sharper constant does not invalidate it.

Milestones (pp. 23–24)

The milestones follow the proof, which sets $N:=\lfloor\min\{D,\sqrt{\log_2 M}\}\rfloor$ and $K:=\lfloor c^{N^2}\rfloor$ :

Eq. (2): for some $c\in(1,2)$ and all large even $N$ there are $K$ projections $\mathbb P_i$ of rank $N/2$ with $|\operatorname{Tr}(\mathbb P_i\rho_j)-\tfrac12|\le\tfrac1{12}$ for all $i\ne j$ .
$\operatorname{Tr}(\mathbb P_i\sigma_i) = \tfrac12+3\varepsilon$ .
$|\operatorname{Tr}(\mathbb P_j\sigma_i)-\tfrac12| = 6\varepsilon|\operatorname{Tr}(\mathbb P_j\rho_i)-\tfrac12|\le\tfrac\varepsilon2$ for $i\neq j$ .
The exact entropy $S(\sigma_i) = \log_2 N - [1-h(\tfrac12+3\varepsilon)]$ , with $h$ the binary entropy, and the bound $S(\sigma_i)\ge\log_2 N - C\varepsilon^2$ .
$I(\zeta;i)\le T(\log_2 N - S(\sigma_i))$ when all $\sigma_i$ have equal entropy.

Significance

Theorem 19 shows that the $\log M$ dependence of shadow tomography cannot be removed, and that for $M\ge 2^{D^2}$ shadow tomography is as hard as full tomography: as $M$ grows the bound becomes the $\Omega(D^2/\varepsilon^2)$ tomography lower bound, which it therefore contains. Compared with the classical Theorem 16, it shows that quantum states need quadratically more copies in the dimension term. The $1/\varepsilon^2$ factor matches the upper bound of Proposition 20 for the decision version, so the $\varepsilon$ -dependence of the lower bound is tight in that setting.

The results are proved in the paper; none of them has a machine-checked proof that we know of. Formalizing the argument requires von Neumann entropy and its additivity on tensor products, the bound $S\le\log_2(\text{dimension})$ , a Holevo-plus-Fano step that turns successful estimation into mutual information, and the existence of many nearly orthogonal half-dimensional subspaces. Each is reusable well beyond this mission.

Difficulty

The obvious attempt adapts the classical argument of Theorem 16, which hides $K$ subsets of $[N]$ in a biased distribution. Quantum states allow $\exp(\Omega(N^2))$ hidden subspaces instead of $\exp(\Omega(N))$ subsets, which is where $D^2$ comes from, but two steps change character. First, the hiding family must be shown to exist: Eq. (2) is a concentration statement for random subspaces, and the lemma the paper cites for it (Lemma 18) is misstated, as explained below. Second, the information bound must be carried out for quantum states: the step "learning $i$ from $\zeta$ requires $I(\zeta;i)\ge\log_2 K$ " needs Holevo's bound and Fano's inequality, adjusted for success probability $2/3$ rather than certainty.

Formalization scope

Matrices are Matrix n n ℂ over a finite index type; the goal uses $n=\texttt{Fin } D$ . Conventions committed to:

A mixed state is the published WildeQIT.IsDensityOperator (positive semidefinite, trace $1$ ), reused as a reference item.
A strategy is a finite-outcome POVM on $\rho^{\otimes k}$ , indexed by Fin k → Fin D, with deterministic outputs $b(\omega)\in\mathbb R^M$ ; classical randomness can be absorbed into the outcome set.
Probabilities and traces are real parts of complex traces. Entropies use $\log_2$ ; Lean's $\log_2 0 = 0$ gives $0\log 0=0$ , and vnEntropy returns $0$ on non-Hermitian matrices, which no statement uses.
Added to the goal: the threshold $N_0$ on $D$ and $\sqrt{\log_2 M}$ (for $D=1$ , $k=0$ succeeds) and $\varepsilon\le\tfrac16$ (for $\varepsilon\ge\tfrac12$ , the output $b_i=\tfrac12$ succeeds with $k=0$ ). Problem 1's $b_i\in[0,1]$ is dropped, an equivalent statement under clipping.
The measurements are chosen before the strategy (for every strategy, the same $E$ ), which is the meaning of a lower bound.

A trivializing formalization is ruled out: the goal does not mention $N$ , $K$ , $\mathbb P_i$ , $\sigma_i$ or $\zeta$ , the success condition quantifies over all mixed states rather than a vacuous class, and the measurements are fixed before the strategy.

Not drafted:

Lemma 18 (pp. 22–23) is false as printed. Since $\mathbb E_S[\rho_S] = \mathbb I/N$ , $\operatorname{Tr}(\mathbb P_T\rho_S)$ concentrates at $1/2$ , not $1/4$ . The proof needs only Eq. (2), which is centred correctly and is a milestone.
Eq. (2) is stated as existence, not as "probability $1-o(1)$ over Haar-random subspaces", because Mathlib has no Haar measure on the unitary group or the Grassmannian; existence is what the proof uses.
" $I(\zeta;i)$ must be at least $\log_2 K$ " is not drafted: as stated it is imprecise for success probability $2/3$ , and the correct Holevo–Fano form is left to the solver.
The final combination $I(\zeta;i)=O(T\varepsilon^2)$ , $T=\Omega(N^2/\varepsilon^2)$ is the goal's last step.

Contributions welcome: proofs of the milestones; a Haar-measure version of Eq. (2); von Neumann entropy infrastructure (additivity, the dimension bound, concavity); Holevo's bound and Fano's inequality for finite-dimensional states.

Selected references

S. Aaronson, Shadow Tomography of Quantum States, arXiv:1711.01053v2, 2018; STOC 2018. https://arxiv.org/abs/1711.01053
P. Hayden, D. Leung, A. Winter, Aspects of generic entanglement, Comm. Math. Phys. 265, 2006. https://arxiv.org/abs/quant-ph/0407049
R. O'Donnell, J. Wright, Efficient quantum tomography, STOC 2016. https://arxiv.org/abs/1508.01907
J. Haah, A. W. Harrow, Z. Ji, X. Wu, N. Yu, Sample-optimal tomography of quantum states, IEEE Trans. Inf. Theory 63, 2017. https://arxiv.org/abs/1508.01797
A. Ambainis, A. Nayak, A. Ta-Shma, U. Vazirani, Dense quantum coding and quantum finite automata, J. ACM 49, 2002. https://arxiv.org/abs/quant-ph/9804043
H.-Y. Huang, R. Kueng, J. Preskill, Predicting many properties of a quantum system from very few measurements, Nature Physics 16, 2020. https://arxiv.org/abs/2002.08953

16 thms3 active usersReviewed

Completed

Combinatorics Operations Research Optimization+1·Captain: mikedeng1

A Tight Linear Time (1/2)-Approximation for Unconstrained Submodular Maximization 2: Randomized Double Greedy Achieves 1/2 of the Optimum in ExpectationResearch Paper

Motivation

Many selection problems assign a value to each subset of a finite collection: the coverage supplied by chosen facilities, the influence reached by chosen seeds, or the value of a coalition. A submodular set function has diminishing returns in the precise sense that the combined value of two sets, counting their overlap once, does not exceed the sum of their separate values. When the function is also monotone, taking more elements never hurts. The unconstrained problem studied here permits nonmonotone functions, so both accepting and rejecting an element can matter. The question is what a single pass through the elements can guarantee when the function is available through value queries. Buchbinder et al., FOCS 2012

The randomized algorithm in this mission attains an expected one-half approximation for every nonnegative submodular function. The paper presents this as tight in the value-oracle setting: it recalls the earlier result of Feige, Mirrokni and Vondrák that a fixed improvement beyond one-half requires exponentially many queries. The contribution here is therefore both the guarantee and a short adaptive rule that attains it in a linear number of iterations. The local proposal follows the FOCS 2012 version of the paper; its theorem numbering differs from the later SIAM Journal on Computing article. Buchbinder et al., §I.A and Theorem I.2

Setting

Let $\mathcal N$ be a finite ground set, and let $f:2^{\mathcal N}\to\mathbb R_{\ge0}$ assign a nonnegative real value to every subset. The unconstrained submodular maximization problem asks for the largest value $f(S)$ among all $S\subseteq\mathcal N$ . Write $OPT$ for that value when no confusion arises, and $O$ for a set attaining it. Submodularity means

f(A\cup B)+f(A\cap B)\le f(A)+f(B)\qquad(A,B\subseteq\mathcal N).

There is no monotonicity or normalization assumption: $f(\varnothing)$ and $f(\mathcal N)$ may both be positive. A value oracle returns $f(S)$ for a requested subset $S$ . The paper's complexity claim counts such queries, assuming a query takes constant time. Buchbinder et al., §I and footnotes 1–2

Algorithm 2 visits the elements once in an arbitrary order $u_1,\ldots,u_n$ . It keeps two sets, starting at $X_0=\varnothing$ and $Y_0=\mathcal N$ . At step $i$ , it measures the gain $a_i$ from adding $u_i$ to $X_{i-1}$ and the gain $b_i$ from removing $u_i$ from $Y_{i-1}$ . It clips each gain at zero, giving $a'_i=\max(a_i,0)$ and $b'_i=\max(b_i,0)$ . It adds $u_i$ to $X$ with probability $a'_i/(a'_i+b'_i)$ and otherwise removes it from $Y$ . When both clipped gains vanish, the paper defines the add probability as one. After all elements have been processed, the two sets coincide, and the algorithm returns their common value. The state law is adaptive: its probability at step $i$ depends on the actual pair of sets produced by earlier choices. Buchbinder et al., Algorithm 2

Formalization targets

The main target is Theorem I.2 for this exact algorithm and for every enumeration of the ground set:

\max_{S\subseteq\mathcal N}f(S)\le 2\,\mathbb E[f(X_n)].

The milestone statements retain the paper's key local quantities. For a comparison optimum $O$ , set $OPT_i=(O\cup X_i)\cap Y_i$ . Lemma II.1 asserts $a_i+b_i\ge0$ . The endpoint statement identifies $OPT_0=O$ and $OPT_n=X_n=Y_n$ . Inequality (3) bounds the conditional loss in the positive-gain case; Lemma III.1 compares the expected change of $OPT_i$ with the expected combined change of $X_i$ and $Y_i$ . The telescoped display keeps the initial endpoint values $f(\varnothing)$ and $f(\mathcal N)$ before using nonnegativity. Buchbinder et al., Lemmas II.1 and III.1, inequality (3), proof of Theorem I.2

A companion target is Theorem I.4 via its second proof. For two normalized monotone submodular utilities $f_1,f_2$ , let $g(S)=f_1(S)+f_2(\mathcal N\setminus S)$ . The maximum of $g$ is exactly the optimal welfare of a two-player partition. Algorithm 2 on $g$ is asked to satisfy

3\max_{S\subseteq\mathcal N}g(S)\le4\,\mathbb E[g(X_n)].

This is the paper's three-quarter guarantee in its welfare application. Buchbinder et al., Theorem I.4 and Proof (2)

Significance

The main theorem gives a specific randomized rule whose expected value is at least half the best subset value, even when accepting an element can lower the objective. It applies without restricting the cardinality or shape of the chosen subset. The welfare corollary shows that keeping the initial endpoint values in the analysis yields a stronger guarantee for the objective formed from two monotone players. Buchbinder et al., Theorems I.2 and I.4

This mission formalizes the statement of the algorithm, its intermediate state laws, its comparison set, and the paper's numbered proof targets. The algorithmic guarantee is proved in the source paper; the local Lean theorem files are open statements with sorry and do not yet give machine-checked proofs of these results. A completed development would supply a reusable formal model of an adaptive finite random process over pairs of subsets, as well as the specific submodular inequalities. The published Submodular and OPT definitions from the earlier Feige–Mirrokni–Vondrák formalization are reused here.

Difficulty

The two possible updates cannot be assessed independently. The probability of each choice depends on the current state, and the comparison set $OPT_i$ can gain or lose the processed element in a way that differs from the two algorithm sets. A bound on the expected value of $X_i$ alone does not control the movement of $OPT_i$ . The proof must handle the clipped gains, including the case when both are zero, while preserving the exact joint law of $(X_i,Y_i)$ . Buchbinder et al., proof of Lemma III.1

Formalization scope

The ground set is a finite Lean type; subsets are Finset X, and values are real numbers. An order is a list with no repeated elements that covers the type, including the empty type. The run is an explicit finite mass function on pairs of subsets after every prefix of the list. Expectation is a finite weighted sum, so it has no integrability exception. The transition clips the two real marginal gains and handles $0/0$ by assigning probability one to the add branch, exactly as Algorithm 2 specifies. The optimum is the published maximum over all subsets. No ratio divides by a possibly zero optimum.

The theorem fixes Algorithm 2 itself; an arbitrary process with nested sets or a process defined by its desired approximation property does not satisfy this scope. The Lean goal states the value bound and leaves the paper's linear-time claim outside the formal theorem. The algorithm uses four value evaluations per processed element in its printed rule; the Lean development represents those evaluations, not an implementation cost model. The statement that its two final sets coincide is a separate milestone.

The source's main-text decreasing-returns definition has an overbroad quantifier on the added element. This development uses the equivalent lattice inequality given in the paper's footnote, which permits nonmonotone functions. The proof of Lemma II.1 also has a set-index slip, and the proof of Theorem I.2 prints $F$ for $f$ in one display; neither slip is copied into a formal statement. The one-step inequality (3) is stated for any nested pair with the processed element in $Y\setminus X$ , a generalization of the conditioned reachable states in the paper. Contributions proving the endpoint invariant, conditional inequality, one-step expected estimate, and final bound are all within scope.

Selected references

Niv Buchbinder, Moran Feldman, Joseph Naor and Roy Schwartz, A Tight Linear Time (1/2)-Approximation for Unconstrained Submodular Maximization, Proceedings of the 53rd IEEE Symposium on Foundations of Computer Science, 2012. FOCS version used here.
Niv Buchbinder, Moran Feldman, Joseph Naor and Roy Schwartz, A Tight Linear Time (1/2)-Approximation for Unconstrained Submodular Maximization, SIAM Journal on Computing 44(5), 2015. DOI: 10.1137/130929205. The cited statement indices above refer to the FOCS version.

11 thms3 active usersReviewed

Completed

Combinatorics Graph Theory Operations Research+1·Captain: mikedeng1

Secretary Problems: Weights and Discounts 5: A 3e-Competitive Algorithm for the Graphic Matroid Secretary ProblemResearch Paper

Motivation

In the secretary problem, $n$ items with nonnegative values arrive one at a time in a uniformly random order, and an online algorithm must decide on each arrival, irrevocably, whether to keep it. The classical version keeps one item; the rule that observes a $1/e$ fraction of the arrivals and then takes the first item better than everything seen picks the best item with probability at least $1/e$ (Ferguson 1989).

Babaioff, Immorlica and Kleinberg (SODA 2007; journal version J. ACM 2018) introduced the matroid secretary problem: the kept set must be independent in a known matroid. It models online auctions in which the feasible sets of winners have matroid structure, for example hiring along the edges of a network without closing a cycle. They gave a $16$ -competitive algorithm when the matroid is graphic, i.e. the items are the edges of a graph and a set is feasible when it contains no cycle.

Timeline for graphic matroids:

2007, Babaioff–Immorlica–Kleinberg: $16$ -competitive.
2009, Babaioff–Dinitz–Gupta–Immorlica–Talwar (SODA 2009, Theorem 1.5): $3e\approx 8.15$ -competitive, through a random reduction to partition matroids. This mission formalizes that result.
2009, Korula–Pál (ICALP 2009): $2e$ -competitive, by a different reduction.

Setting

Let $G=(V,E)$ be a finite simple graph. Each edge $e$ has a value $v(e)\ge 0$ . A set $S\subseteq E$ is independent in the graphic matroid of $G$ if the graph $(V,S)$ has no cycle. The offline optimum is

\mathrm{OPT}(G,v)=\max\Big\{\sum_{e\in S}v(e): S\subseteq E\ \text{acyclic}\Big\}.

The edges arrive in a uniformly random order. An algorithm sees each edge and its value on arrival and decides at once whether to select it. The selected set must be acyclic. The algorithm is $\alpha$ -competitive if $\mathrm{OPT}(G,v)\le\alpha\cdot\mathbb E[\text{value of the selected set}]$ for every $G$ and every $v\ge 0$ .

A partition matroid on a subset $U'\subseteq E$ is given by a family $P$ of nonempty, pairwise disjoint parts with union $U'$ : a set is independent when it lies in $U'$ and meets each part at most once. Its max-weight base has value $\mathrm{val}(P,v)=\sum_{p\in P}\max_{e\in p}v(e)$ .

Definition 5.1. A random partition $\mu$ (a probability distribution on such families, chosen from $G$ alone) is an $\alpha$ -partition scheme if every partition in its support has only acyclic independent sets, and for every $v\ge 0$ ,

\mathrm{OPT}(G,v)\le \alpha\cdot\mathbb E_{P\sim\mu}[\mathrm{val}(P,v)].

The random partition of Lemma 5.3. Pick an edge $\{u,w\}$ uniformly at random. With probability $\tfrac12$ colour $u$ red and $w$ blue, otherwise the reverse. Colour every other vertex red or blue independently with probability $\tfrac12$ . Each red vertex $x$ gets a part: the red-blue edges at $x$ . Then repeat on the edges with both endpoints blue, with fresh randomness.

The algorithm. Draw the partition, let the edges arrive, and on each part run the classical secretary rule on that part's arrivals. Output all selected edges.

Formalization targets

Goal: Theorem 1.5

For every finite simple graph $G$ and every $v\ge 0$ :

every possible output of the algorithm is an acyclic set of edges of $G$ ;

\mathrm{OPT}(G,v)\le 3e\cdot\mathbb E[\mathrm{ALG}].

Part 1 is needed for the statement to have content: an algorithm that selects every edge would otherwise satisfy part 2.

Milestones

Section 2, p. 4. On $m\ge1$ arrivals, the classical rule selects the maximum with probability at least $1/e$ .
Theorem 5.4, first clause. For a fixed partition $P$ , the per-part rule outputs a set independent in the partition matroid, and $\mathrm{val}(P,v)\le e\cdot\mathbb E_\pi[\mathrm{ALG}]$ .
Lemma 5.3, independence. Every partition the random construction can produce is a partition matroid on a subset of $E$ , and each of its independent sets is a forest.
Lemma 5.3. The construction is a $3$ -partition scheme.
Section 5, p. 10. Any $\alpha$ -partition scheme for a graphic matroid, combined with the per-part rule, gives a feasible, $e\alpha$ -competitive algorithm.

Significance

The theorem shows that the graphic matroid secretary problem admits a constant-competitive algorithm with a small explicit constant. It does so through a reduction: a random partition matroid that is feasible for the original matroid and loses only a constant factor in expectation. The reduction separates the combinatorics (Lemma 5.3) from the online part (Theorem 5.4). The same framework gives algorithms for uniform and transversal matroids and for the weighted and discounted variants on any matroid with an $\alpha$ -partition property.

The result is proved in the paper; it has not been formalized. The mission contributes a machine-checked version of the reduction, a formal treatment of a recursively defined random partition, and the classical secretary bound in a reusable finite form. The constant $3e$ is not the best known for graphic matroids (Korula–Pál improve it to $2e$ ), so the formal goal is this algorithm's guarantee, not the best possible ratio.

Difficulty

The online half is routine once the classical bound is available: the relative order of the edges in each part is uniform, and the parts are disjoint. The difficulty is Lemma 5.3. The natural idea of using a fixed optimal forest to build the partition is ruled out because the partition must be chosen before the values are seen. The expectation bound must therefore hold for every valuation at once, for a law that depends on the graph only. The construction is recursive and random: its expected value is not a closed-form sum, and any bound has to be carried through the random sequence of blue-blue subgraphs. Feasibility needs an invariant across rounds: the parts created later live inside the blue-blue edges of every earlier round.

Formalization scope

Graph. A SimpleGraph on a Fintype vertex type with decidable adjacency. The edges are G.edgeFinset, and acyclicity of $S$ is (SimpleGraph.fromEdgeSet S).IsAcyclic. Multigraphs are not covered.
Values. Values are a real function v : Sym2 V → ℝ with ∀ e, 0 ≤ v e; only the values on edges matter.
OPT is a Finset.sup' over acyclic subsets of the edge set. A partition is a finite family of nonempty, pairwise disjoint parts inside the edge set. Its max-weight base value is the sum of the part maxima.
Random partition. A PMF defined by well-founded recursion on the number of edges. Empty parts are dropped, and edges with two red endpoints are discarded.
Random order. The edges are numbered by a fixed enumeration. An arrival order is a permutation of the numbers, and expectation over the order is the average over all $|E|!$ permutations.
Classical rule. It samples $\lfloor m/e\rfloor$ arrivals of a part with $m$ edges. Ties are broken by preferring the smaller edge number among equal values.
Constants. Competitiveness is multiplicative ( $\mathrm{OPT}\le 3e\cdot\mathbb E[\mathrm{ALG}]$ ), so a zero expectation is not a loophole.
Ruling out trivial formalizations. In Definition 5.1 the random partition is fixed before the valuation, and the independence requirement holds for every partition in its support. A partition allowed to depend on $v$ would make every matroid $1$ -partitionable.

A complete development needs the classical secretary bound in finite form, the uniformity of induced sub-orders of a uniform permutation, expectations of PMF.bind along a well-founded recursion, and facts about forests in SimpleGraph. The first two, and a general graphic-matroid layer, are reusable beyond this mission. Proofs of any milestone, alternative proofs of Lemma 5.3, and extensions to the uniform and transversal cases of Theorem 5.2 are welcome.

Selected references

M. Babaioff, M. Dinitz, A. Gupta, N. Immorlica, K. Talwar, Secretary Problems: Weights and Discounts, Proc. 20th ACM-SIAM Symposium on Discrete Algorithms (SODA), 2009. https://doi.org/10.1137/1.9781611973068.135
M. Babaioff, N. Immorlica, R. Kleinberg, Matroids, secretary problems, and online mechanisms, SODA 2007, pp. 434–443. https://dl.acm.org/doi/10.5555/1283383.1283429
M. Babaioff, N. Immorlica, D. Kempe, R. Kleinberg, Matroid Secretary Problems, Journal of the ACM 65(6), 2018. https://doi.org/10.1145/3212512
N. Korula, M. Pál, Algorithms for Secretary Problems on Graphs and Hypergraphs, ICALP 2009, LNCS 5556. https://doi.org/10.1007/978-3-642-02930-1_42
T. S. Ferguson, Who solved the secretary problem?, Statistical Science 4(3), 1989. https://doi.org/10.1214/ss/1177012493

10 thms3 active usersReviewed

Completed

Operations Research Optimization·Captain: mikedeng1

A Simple Forward Algorithm to Solve General Dynamic Lot Sizing Models with n Periods in O(n log n) or O(n) Time: Minimal Optimal Predecessor Lists Are Characterized by Strictly Increasing BreakpointsResearch Paper

Motivation

The dynamic lot size model asks when, and how much, to order of a single item over a planning horizon of $n$ periods with known, time-varying demands, setup costs, unit order costs and holding costs. It is the textbook model of production planning and the building block of material requirements planning, multi-item scheduling and many decomposition schemes for larger supply-chain problems.

Wagner and Whitin (1958) showed that some optimal policy orders only when inventory is zero, which turns the problem into a shortest-path recursion with $O(n^2)$ running time. For more than thirty years this was the standard algorithm. In 1991 three groups independently reduced the complexity: Federgruen and Tzur (Management Science 37(8), 1991), Wagelmans, van Hoesel and Kolen (Operations Research 40, 1992) and Aggarwal and Park (Operations Research 41, 1993). Each obtained $O(n \log n)$ in general and $O(n)$ under special cost structures. The Federgruen–Tzur algorithm is a forward algorithm: at iteration $j$ it keeps a short list of periods that could still be the best last setup period for some future horizon, and updates it by local tests on neighbouring entries. This mission formalizes the theorem that justifies those tests.

Setting

For periods $i = 1, 2, \dots$ let $d_i$ be the demand, $K_i$ the setup cost, $c_i$ the variable per unit order cost and $h_i$ the cost of carrying a unit of inventory at the end of period $i$ . Write $D(i) = \sum_{k=1}^{i} d_k$ and $H(i) = \sum_{k=1}^{i} h_k$ , so $D(0) = H(0) = 0$ . For $i < j$ let $c_{ij} = c_i + h_i + \dots + h_{j-1}$ , let $\tilde C(i) = c_i - H(i-1)$ , and let

S(i, j) = \sum_{r=i}^{j-1} h_r\,\bigl(D(j) - D(r)\bigr)

be the carrying cost of an order placed in period $i$ that covers the demands of periods $i, \dots, j$ .

The costs are given by the zero-inventory recursion (2): $F(0) = 0$ and, for $1 \le l \le t$ ,

F(l, t) = F(l-1) + K_l + S(l, t) + c_l\,[D(t) - D(l-1)], \qquad F(t) = \min_{1 \le l \le t} F(l, t).

$F(l, t)$ is the cost of the first $t$ periods when the last setup is in period $l$ .

For two periods $k < l$ the difference $\Delta_{k,l}(t) = F(k,t) - F(l,t)$ is affine in $D(t)$ , with intercept $A(k,l)$ given by (4) and slope $c_{k,l} - c_l = \tilde C(k) - \tilde C(l)$ . Its root $G(k,l)$ is defined by (5): $A(k,l)/(\tilde C(l) - \tilde C(k))$ when the slopes differ, and $+\infty$ or $-\infty$ according to the sign of $A(k,l)$ when they agree. It is extended symmetrically, $G(l,k) = G(k,l)$ .

At iteration $j$ the future demands are unknown, so a future horizon has a potential cumulative demand $x \ge D(j)$ . The $j$ th Minimal Optimal Predecessors list $\Omega(j)$ is the set of periods $l \le j$ that are the lowest-index optimal last setup period, among $\{1, \dots, j\}$ , for every potential cumulative demand in some open interval above $D(j)$ .

Formalization targets

Goal: Theorem 1(a)

Let $j \ge 1$ and let $S = \{i_1, \dots, i_r\}$ with $\Omega(j) \subseteq S \subseteq \{1, \dots, j\}$ , ranked so that $\tilde C(i_1) \ge \dots \ge \tilde C(i_r)$ , with equal $\tilde C$ -values in ascending order of index. Put $g(1) = D(j)$ and $g(l) = G(i_l, i_{l-1})$ for $l = 2, \dots, r$ . Then

S = \Omega(j) \iff g(1) < g(2) < \dots < g(r) < \infty. \tag{6}

Milestones

In attack order:

identity (1a) for the carrying costs;
Lemma 2(a)–(d), the linearity of $\Delta_{k,l}$ and the sign test against its root $G(k,l)$ ;
the claim that $\Omega(j)$ contains an optimal last setup period for the horizon $j$ ;
the strict chains (7)–(8) of the Appendix;
Theorem 1(b), that under (6) the first entry $i_1$ is an optimal last setup period $l(j)$ ;
Theorem 1(c)(i)–(iii), the three elimination rules: $g(2) \le D(j)$ removes $i_1$ , $g(k+1) \le g(k)$ removes $i_k$ , and $g(r) = \infty$ removes $i_r$ .

A supporting item potCost_spec certifies that the potential costs used to define $\Omega(j)$ agree with the paper's $F(l,t)$ , up to a term that does not depend on $l$ .

Significance

Theorem 1 is what makes the forward algorithm correct. Part (a) reduces the minimality of a candidate list to a condition on consecutive pairs of a sorted list. Part (c) says which entry to delete when the condition fails. Part (b) says where to read off the optimal last setup period. With these, $\Omega(j)$ is maintained by deletions at the ends and in the interior of a list ordered by $\tilde C$ , and each period is inserted and deleted at most once; the $O(n \log n)$ bound, and the $O(n)$ bound under the paper's special cost structures, follow from this bookkeeping. The same lower-envelope reasoning appears in the other 1991–1993 algorithms and in later extensions to backlogging and capacitated variants.

The result has a complete published proof. To our knowledge there is no machine-checked development of the Wagner–Whitin recursion or of any of the fast lot-sizing algorithms. This mission produces the model, the breakpoints and the Minimal Optimal Predecessors lists as reusable definitions, and a checked proof of the characterization. It also records two small corrections that a formal reading forces on the printed text (see Formalization scope).

Difficulty

Each piece in isolation is elementary algebra on affine functions. The difficulty is in the combinatorics of the lower envelope with ties. The natural argument "consecutive breakpoints increase, so each line owns an interval" must handle three things:

equal slopes, where $G = \pm\infty$ ;
several lines meeting at one point;
the lowest-index tie-breaking that makes $\Omega(j)$ minimal.

The "only if" direction needs every failure of (6) to be traced to an element that is never the unique lowest-index optimum on an interval. Ties are exactly where the printed definition of $\Omega(j)$ , read literally at a single demand value, breaks the theorem. A proof that ignores ties proves a statement that is false.

Formalization scope

Data and costs. The data are four functions $\mathbb N \to \mathbb R$ bundled in a structure; values at index $0$ are unused, and no sign conditions are imposed. $F$ is defined by the recursion (2) with $F(0) = 0$ . Its identification with the minimum cost over all feasible policies is the paper's Lemma 1 (Wagner–Whitin), which is not part of this mission. The horizon $n$ is not a parameter.
Breakpoints. $G$ and the critical values $g(\cdot)$ take values in EReal, so $\pm\infty$ are kept distinct from every real number. The final " $< \infty$ " of (6) is part of the condition.
Ranked lists. A ranked set is a duplicate-free List ℕ. Lean lists are 0-based, so the paper's $i_{m+1}$ and $g(m+1)$ are entry $m$ and gval j L m.
Disclosed change 1, $\Omega(j)$ . The page asks for a single potential cumulative demand $D \ge D(j)$ at which $l$ is the lowest-index optimum. With that reading, Theorem 1(a) "only if" and Theorem 1(c) fail when two lines tie exactly at a breakpoint (an explicit five-period instance is in the definition's note). The formalization requires $l$ to be the lowest-index optimum on a nondegenerate open interval of potential demands above $D(j)$ . This is the paper's own description of the list on p. 915: "the unique optimal last setup period for any horizon … with potential cumulative demand $g(k) < D < g(k+1)$ ".
Disclosed change 2, Lemma 2(d). The printed hypothesis " $c_{k,l} < c_l$ " duplicates part (c) and is read as " $c_{k,l} = c_l$ ". The equivalence " $\Delta_{k,l} \ge 0$ iff $D(t) \ge G(k,l)$ " is stated under $A(k,l) \ne 0$ , since $A(k,l) = 0$ gives $G = +\infty$ by (5).
Ruling out trivial formalizations. The hypotheses of the goal are satisfiable for every $j \ge 1$ : rank $\{1, \dots, j\}$ itself. $\Omega(j)$ is nonempty (a milestone). $F(t)$ for $t \ge 1$ is a minimum over the nonempty set $\{1, \dots, t\}$ , never a default value. $G$ is never replaced by a real-valued junk value at equal slopes.
Out of scope. Lemma 1, Lemma 3, Corollaries 1–5, Theorem 2, the Algorithm's pseudo-code and its complexity analysis, and the submodularity discussion of §5.
Reusable infrastructure. The model, the recursion (2), $A$ , $G$ and $\Omega(j)$ can be reused for the paper's algorithmic results and for related lot-sizing papers. Proofs of the milestones, in any order, are welcome.

Selected references

A. Federgruen and M. Tzur, A Simple Forward Algorithm to Solve General Dynamic Lot Sizing Models with n Periods in O(n log n) or O(n) Time, Management Science 37(8):909–925, 1991. https://doi.org/10.1287/mnsc.37.8.909
H. M. Wagner and T. M. Whitin, Dynamic Version of the Economic Lot Size Model, Management Science 5(1):89–96, 1958. https://doi.org/10.1287/mnsc.5.1.89
A. Wagelmans, S. van Hoesel and A. Kolen, Economic Lot-Sizing: An O(n log n) Algorithm That Runs in Linear Time in the Wagner-Whitin Case, Operations Research 40(1-supplement-1):S145–S156, 1992. https://doi.org/10.1287/opre.40.1.S145
A. Aggarwal and J. K. Park, Improved Algorithms for Economic Lot Size Problems, Operations Research 41(3):549–571, 1993. https://doi.org/10.1287/opre.41.3.549

16 thms3 active usersReviewed

Completed

Operations Research·Captain: mikedeng1

On the Power of Randomization in On-Line Algorithms 4: Restarting a Bounded-Cost Algorithm Is (1+ε)α-Competitive in Games of Finite DiameterResearch Paper

Motivation

Competitive analysis compares an online algorithm, which must answer each request before seeing the next, with the optimal off-line solution of the same request sequence. Ben-David, Borodin, Karp, Tardos and Wigderson (Algorithmica 11, 1994) set up a general framework, request-answer games, in which paging, the $K$ -server problem and metrical task systems are all instances, and used it to compare the power of randomized algorithms against several kinds of adversaries.

One of their results (Theorem 2.1) says that if a randomized algorithm is $\alpha$ -competitive against every adaptive off-line adversary, then some deterministic algorithm is already $\alpha$ -competitive. The argument is a game-theoretic existence proof: it says nothing about how to compute the deterministic algorithm. Section 4 of the paper, "A Constructive Version of Theorem 2.1", answers the natural follow-up question for a large class of games: under monotonicity, locality and a finite diameter, a deterministic algorithm that loses only a factor $1+\epsilon$ can be assembled from a finite object.

Setting

A request-answer game $F$ has a request set $R$ , a finite answer set $A$ , and cost functions $f_n : R^n \times A^n \to \mathbb{R}$ , $n \ge 0$ ; $f_0$ is the cost of the empty play. The off-line optimum of a request sequence $r$ of length $n$ is $c(r) = \min_{a \in A^n} f_n(r, a)$ . A deterministic online algorithm $G$ answers the $i$ -th request by a function $g_i(r_1, \dots, r_i)$ of the requests so far; its cost on $r$ is $c_G(r) = f_n(r, G(r))$ . It is $\alpha$ -competitive if $c_G(r) \le \alpha(c(r))$ for every $r$ .

The game is monotone if $f_{n+1}(rt, ab) \ge f_n(r, a)$ always, and local if for every $h > 0$ only finitely many request sequences have $c(r) \le h$ . The discrepancy of two request-answer sequences is

\delta((r,a),(r',a')) = f(rr', aa') - f(r,a) - f(r',a'),

and the diameter $D(F)$ is the supremum of $|\delta|$ over all pairs.

For a real $H$ , the set $R_H$ consists of the request sequences all of whose proper prefixes have off-line optimum at most $H$ . Given a deterministic algorithm $A_H$ , the restart algorithm simulates $A_H$ and, as soon as the request sequence leaves $R_H$ , starts over as if it had received no previous requests. This cuts every request sequence into segments $r = r(1)\, r(2) \cdots r(t)$ , each a longest prefix in $R_H$ of what remains.

Formalization targets

Goal: Theorem 4.1 through its construction

Let $F$ be monotone and local, with finite nonempty $R$ and $A$ , $f_0 \ge 0$ , and diameter at most $D$ . Let $\alpha(x) = d\,x$ with $d \ge 1$ , $\epsilon > 0$ , and

H = \frac{(2+\epsilon) D}{\epsilon}.

Then $R_H$ is finite; the restart algorithm depends on $A_H$ only through its values on $R_H$ ; and for every $A_H$ with $c_{A_H}(r) \le \alpha(c(r))$ on $R_H$ ,

c_{\mathrm{Restart}}(r) \le (1+\epsilon)\,\alpha(c(r)) \qquad \text{for all request sequences } r.

Milestones (proof of Theorem 4.1, pp. 17–18)

$R_H$ is finite.
The restart rule produces the greedy decomposition into longest prefixes in $R_H$ .
The restart algorithm answers $A_H(r(1)), A_H(r(2)), \dots, A_H(r(t))$ .
$c(r(i)) \ge H$ for $i = 1, \dots, t-1$ .
$c(r) \ge c(r(1)) + \sum_{i=2}^{t} (c(r(i)) - D(F))$ .
$c_{\mathrm{Restart}}(r) \le \alpha(c(1)) + \sum_{i=2}^{t} (\alpha(c(i)) + D(F))$ .

Significance

Theorem 2.1 shows that, against adaptive off-line adversaries, randomization gives no advantage, but only as an existence statement. Theorem 4.1 turns it into a recipe: a deterministic algorithm need only be good on the finite set $R_H$ , which can be prepared in advance, and restarting extends it to all inputs at a loss of $1+\epsilon$ . The paper illustrates this with $K$ -server problems on finite graphs, where $A_H$ is a finite table and each step of the resulting algorithm costs one dynamic-programming evaluation of an off-line optimum.

The restart construction is of independent use: it is a general way to turn a guarantee on bounded-cost inputs into a guarantee on all inputs when the cost is nearly additive over concatenation.

To our knowledge neither the abstract request-answer game model nor this theorem has a machine-checked proof. The mission produces a formal model of request-answer games with the monotonicity, locality and diameter conditions, the restart algorithm as an explicit definition, and the full chain of inequalities of the proof.

Difficulty

The individual inequalities are elementary; the work lies in the bookkeeping of the construction. The algorithm is defined online, one request at a time, while the analysis is phrased through the decomposition of the whole sequence. Relating the two requires showing that the online rule produces exactly the decomposition into longest prefixes in $R_H$ , and that the answers produced on each segment are those of $A_H$ run from scratch, so that the cost of the whole play can be compared with the costs on the segments. The constants must close exactly: with $H = (2+\epsilon)D/\epsilon$ the additive losses at the $t-1$ cuts, on both the algorithm's side and the optimum's side, must be absorbed by the factor $1+\epsilon$ , and they do so only for ratios $d \ge 1$ .

A tempting shortcut is to conclude Theorem 4.1 from Theorem 2.1 directly: a deterministic $\alpha$ -competitive algorithm is trivially $(1+\epsilon)\alpha$ -competitive when costs are nonnegative. This proves the sentence of the theorem without its point, and is ruled out below.

Formalization scope

Request and answer sequences are Lean Lists, oldest first; $f_n(r,a)$ is F.cost r a with r.length = a.length. Costs are real-valued (the paper allows $+\infty$ ; real costs are a special case).
The answer set is a Fintype and nonempty; in the goal the request set is a Fintype and nonempty.
A deterministic algorithm is one function List R → A. Competitiveness of a deterministic algorithm against adaptive off-line adversaries is stated as competitiveness on every request sequence, which is equivalent for deterministic algorithms (p. 8).
Finite diameter is a real bound $D$ with $|\delta| \le D$ for all pairs, and every statement holds for every such $D$ , in particular $D = D(F)$ ; no real supremum is taken.
$f_0 \ge 0$ is assumed in the goal; with monotonicity it makes every cost nonnegative. It holds in the paper's examples.
$\alpha(x) = d\,x$ with $d \ge 1$ in the goal; the cost bound for the restart algorithm (milestone 6) holds for an arbitrary $\alpha$ .
$H$ is fixed to the paper's value $(2+\epsilon)D/\epsilon$ .
The restart algorithm is a definition (a left fold over the requests), not a hypothesis. The paper's assumption of a randomized algorithm competitive against adaptive off-line adversaries is used only, through Theorem 2.1, to obtain $A_H$ ; the goal quantifies over every $A_H$ that is $\alpha$ -competitive on $R_H$ . "Computable" has no precise meaning for real costs; its content is the finiteness of $R_H$ together with the fact that the restart algorithm reads $A_H$ only on $R_H$ . A formalization that proves only the existence of a deterministic $(1+\epsilon)\alpha$ -competitive algorithm, without the construction, does not meet the goal.
Milestones 5 and 6 are stated for nonempty request sequences, so that $t \ge 1$ ; milestone 5 is stated for every decomposition into consecutive pieces.

Contributions welcome: proofs of the milestones, and a connection to the other missions of this series, where the randomized model and Theorem 2.1 are formalized.

Selected references

S. Ben-David, A. Borodin, R. Karp, G. Tardos, A. Wigderson, On the power of randomization in on-line algorithms, Algorithmica 11 (1994). https://doi.org/10.1007/BF01294260
M. Chrobak, H. Karloff, T. Payne, S. Vishwanathan, New results on server problems, SIAM Journal on Discrete Mathematics 4 (1991), 172–181. https://doi.org/10.1137/0404017

10 thms3 active usersReviewed

Completed

Operations Research Probability·Captain: mikedeng1

On the Power of Randomization in On-Line Algorithms 3: An Augmented Potential Function Yields an Explicit Deterministic α∘β-Competitive AlgorithmResearch Paper

Motivation

Competitive analysis measures an online algorithm, which must answer each request before seeing the next, against the best off-line answer to the whole request sequence. Randomized online algorithms are often much better than deterministic ones against an oblivious adversary, who fixes the requests in advance; the paging problem is the standard example. Against an adaptive adversary, who sees the algorithm's answers before choosing the next request, the advantage can disappear.

Ben-David, Borodin, Karp, Tardos and Wigderson (Algorithmica 11, 1994; preliminary version STOC 1990) made this precise in an abstract framework of request-answer games. Their Corollary 2.1 says: if a game has a randomized algorithm that is $\alpha$ -competitive against adaptive on-line adversaries and one that is $\beta$ -competitive against oblivious adversaries, then it has a deterministic $\alpha\circ\beta$ -competitive algorithm. That proof is non-constructive: it goes through a game-theoretic determinacy argument. Section 3 of the paper gives a constructive version. Most competitive analyses of randomized algorithms against adaptive adversaries are carried out with a potential function, in the style of Manasse, McGeoch and Sleator (J. Algorithms 11, 1990). The paper shows that such a potential function, together with any oblivious-competitive algorithm $H$ , determines an explicit deterministic algorithm $M$ , answer by answer. This mission formalizes that construction and its guarantee.

Setting

A request-answer game has a request set $R$ , a finite answer set $A$ and cost functions $f_n : R^n \times A^n \to \mathbb R$ . The off-line optimum of $r \in R^n$ is $c(r) = \min_{a \in A^n} f_n(r, a)$ . A deterministic online algorithm $M$ is a sequence of maps $m_i : R^i \to A$ ; on $r = (r_1,\dots,r_n)$ it answers $M(r) = (m_1(r_1), m_2(r_1,r_2), \dots, m_n(r))$ , at cost $c_M(r) = f_n(r, M(r))$ . It is $\alpha$ -competitive if $c_M(r) \le \alpha(c(r))$ for all $r$ . Throughout, $\alpha$ and $\beta$ are affine maps $\mathbb R \to \mathbb R$ (the paper's "linear functions").

A randomized online algorithm $H$ is a probability distribution over deterministic algorithms $H_y$ ; it is $\beta$ -competitive against any oblivious adversary if $\mathbb E_y[f_n(r, H_y(r))] \le \beta(c(r))$ for all $r$ . The algorithm $G$ analysed by the potential function is described by its next-answer laws $g_{n+1}(r r_{n+1}, a)$ on $A$ , given the requests so far, the new request and its own past answers. An adaptive on-line adversary $S$ chooses each request from the algorithm's past answers and answers it itself, before the algorithm does, for at most $d_Q$ rounds; a configuration after $n$ rounds is $(r, a, b) \in R^n \times A^n \times A^n$ : requests, algorithm's answers, adversary's answers.

An augmented potential function for $\alpha$ and $G$ (Definition 3.1) is a family $\Phi_n : R^n \times A^n \times A^n \to \mathbb R$ with (1) $\Phi_0 = 0$ ; (2) $\Phi_n(r,a,b) \le \alpha(f_n(r,b)) - f_n(r,a)$ for every configuration; (3) $\mathbb E_{a_{n+1} \sim g_{n+1}(r r_{n+1}, a)}[\Phi_{n+1}(r r_{n+1}, a a_{n+1}, b b_{n+1})] \ge \Phi_n(r,a,b)$ for every configuration, every $r_{n+1} \in R$ and every $b_{n+1} \in A$ .

Formalization targets

Goal: Theorem 3.1 (p. 15)

Let $\Phi$ be an augmented potential function for $\alpha$ and $G$ , and $H$ a $\beta$ -competitive algorithm against oblivious adversaries. Say that $M$ obeys the potential rule if for every $r \in R^n$ and $r' = rt$ ,

\mathbb E_y\big[\Phi_{n+1}(r', M(r)\,m_{n+1}(r'), H_y(r'))\big] \ \ge\ \mathbb E_y\big[\Phi_n(r, M(r), H_y(r))\big].

Then such an $M$ exists, and every such $M$ satisfies

c_M(r) \le \alpha\big(\beta(c(r))\big) \quad \text{for all } r .

Both parts are part of the goal: the rule can be followed, and following it guarantees $\alpha\circ\beta$ -competitiveness.

Milestones

In every play of $G$ against an adaptive on-line adversary, the expected final potential is nonnegative (proof of Lemma 3.1).
Lemma 3.1, "if" direction: an augmented potential function for $\alpha$ and $G$ makes $G$ $\alpha$ -competitive against any adaptive on-line adversary, $\mathbb E[c_G(S)] \le \mathbb E[\alpha(c_S(G))]$ .
For every $r$ , $t$ and every $a \in A^n$ , some $a' \in A$ satisfies $\mathbb E_y[\Phi_{n+1}(rt, aa', H_y(rt))] \ge \mathbb E_y[\Phi_n(r, a, H_y(r))]$ .
If $M$ obeys the rule, $\mathbb E_y[\Phi_n(r, M(r), H_y(r))] \ge 0$ for every $r$ .
If $M$ obeys the rule, $f_n(r, M(r)) \le \mathbb E_y[\alpha(f_n(r, H_y(r)))]$ for every $r$ : $M$ is $\alpha$ -competitive against the randomized adaptive adversary that serves its requests with $H$ .

Significance

The theorem turns two separate analyses into one deterministic algorithm with an explicit description. The potential function certifies $G$ against the strongest on-line adversary; the oblivious algorithm $H$ need not be related to $G$ , and the paper remarks that $H$ may be $G$ itself. The next answer of $M$ is computable whenever the expected potential under $H$ is (Corollary 3.1, stated informally in the paper), and the paper notes that for the potential functions used in the $K$ -server literature this expectation is computable in time polynomial in the number of nodes and $K$ . Read in this light, a potential-function proof for a randomized algorithm doubles as a deterministic algorithm.

The result is proved in the paper. As far as is known, neither this theorem nor the abstract framework of request-answer games with adaptive adversaries has a machine-checked formalization. The mission produces that framework and a checked derandomization principle that applies to every request-answer game with real costs, not to one problem.

Difficulty

The obvious argument for the existence of $m_{n+1}(r')$ averages property (3) of $\Phi$ ; the work is in seeing which configuration to apply it to. The rule compares $M$ 's configuration against $H_y$ 's answers, not against an adversary playing $G$ , and the paper argues through an auxiliary on-line adversary that asks $r'$ and serves it with $H_y$ . Making this rigorous requires interchanging the expectation over $H$ 's coins with the finite expectation over $G$ 's next answer, and checking that the needed expectations are finite.

The second difficulty is the two kinds of randomness. $G$ enters only through its next-answer laws, while $H$ must be a single distribution over deterministic algorithms: the rule evaluates $H_y(r)$ and $H_y(r')$ with the same coins $y$ . Replacing $H$ by a behavioural description breaks the coupling between consecutive rounds.

Formalization scope

Requests and answers are Lean lists, oldest first, and $f_n(r,a)$ is F.cost r a on lists of common length; values on lists of different lengths are never used. Costs are real: the paper allows $f_n = +\infty$ , so every statement here is about the real-valued games. The answer type is finite and nonempty, so the minimum $c(r)$ exists. Affine maps are written $\alpha(x) = c x + d$ . The goal additionally assumes $\alpha$ nondecreasing: the last step of the paper's proof applies $\alpha$ to an inequality, which needs it, and the paper's examples are positive ratios. In Lemma 3.1 and milestone 5 linearity of $\alpha$ is kept as the paper's standing convention, although with $\alpha$ inside the expectation the argument does not use it.

$G$ is a map from (requests, own answers) to a probability mass function on $A$ (behavioural form); its play against an adaptive on-line adversary is a probability mass function on final configurations, with finite support, and its expectations are finite sums. $H$ is a probability measure on a coin space with a deterministic algorithm per coin, each answer measurable in the coins; expectations over $H$ are Bochner integrals of functions with finitely many values. $\alpha$ stays inside expectations, as in the paper's definition of competitiveness against adaptive adversaries. Adversaries stop by returning none and have a uniform depth bound.

The goal cannot be satisfied vacuously: it states the existence of an algorithm obeying the rule alongside the guarantee for every such algorithm, and Definition 3.1 is required at every configuration, not only at reachable ones.

Not formalized: the "only if" direction of Lemma 3.1, which the paper only sketches, and Corollary 3.1, whose notion of computability the paper leaves unspecified. The definitions of request-answer games, online algorithms, adversaries and competitiveness are reusable for the other missions of this paper and for any problem-specific competitive analysis. Contributions welcome: proofs of the milestones, and a lemma relating the mixed and behavioural forms of a randomized algorithm.

Selected references

S. Ben-David, A. Borodin, R. Karp, G. Tardos, A. Wigderson, On the power of randomization in on-line algorithms, Algorithmica 11 (1994), 2–14. https://doi.org/10.1007/BF01294260
M. Manasse, L. McGeoch, D. Sleator, Competitive algorithms for server problems, Journal of Algorithms 11 (1990), 208–230. https://doi.org/10.1016/0196-6774(90)90003-W
D. Sleator, R. Tarjan, Amortized efficiency of list update and paging rules, Communications of the ACM 28 (1985), 202–208. https://doi.org/10.1145/2786.2793
A. Borodin, R. El-Yaniv, Online Computation and Competitive Analysis, Cambridge University Press, 1998. ISBN 0-521-56392-5

9 thms3 active usersReviewed

Completed

Combinatorics Operations Research Optimization·Captain: mikedeng1

A Tight Linear Time (1/2)-Approximation for Unconstrained Submodular Maximization 3: Fractional Double Greedy on the Multilinear Extension Achieves 1/2 of the OptimumResearch Paper

Motivation

Unconstrained submodular maximization (USM) asks for a subset $S$ of a finite ground set $\mathcal N$ maximizing a nonnegative submodular function $f$ . It contains Max-Cut, Max-DiCut and maximum facility location as special cases, and it is the basic subproblem of many constrained submodular maximization algorithms. Because $f$ is given only through a value oracle, the question is how close to the optimum a polynomial number of queries can get.

Timeline of the approximation ratio for USM in the value oracle model:

Feige, Mirrokni and Vondrák (FOCS 2007; SIAM J. Comput. 2011) showed that a uniformly random set achieves $1/4$ , local search achieves $1/3$ and $2/5$ , and that no algorithm making polynomially many queries achieves $1/2 + \varepsilon$ for any fixed $\varepsilon > 0$ .
Oveis Gharan and Vondrák (SODA 2011) reached $0.41$ by simulated annealing; Feldman, Naor and Schwartz (ICALP 2011) reached $0.42$ .
Buchbinder, Feldman, Naor and Schwartz (FOCS 2012) closed the gap with the double greedy algorithms: a deterministic $1/3$ -approximation and a randomized $1/2$ -approximation, both linear in the number of oracle calls. Their Appendix A gives a third, fractional variant, which is the subject of this mission.

This is the third mission on the FOCS 2012 paper; the first two treat the deterministic and the randomized double greedy on sets.

Setting

Let $\mathcal N$ be a finite ground set with $n$ elements and $f : 2^{\mathcal N} \to \mathbb R_{\ge 0}$ . The function $f$ is submodular if

f(A) + f(B) \ge f(A \cup B) + f(A \cap B) \qquad \text{for all } A, B \subseteq \mathcal N .

Write $f(OPT) = \max_{S \subseteq \mathcal N} f(S)$ and let $OPT$ be a maximizing set.

The multilinear extension of $f$ is the function on vectors $x \in [0,1]^{\mathcal N}$

F(x) = \sum_{S \subseteq \mathcal N} f(S) \prod_{u \in S} x_u \prod_{u \notin S} (1 - x_u) = \mathbb E\bigl[f(R(x))\bigr],

where the random set $R(x)$ contains each element $u$ independently with probability $x_u$ . A set is identified with its characteristic vector, so $F$ agrees with $f$ on $\{0,1\}^{\mathcal N}$ , and $\{u\}$ also denotes the unit vector at $u$ . For vectors, $x \vee y$ and $x \wedge y$ are the coordinate-wise maximum and minimum.

Algorithm 4 (MultilinearUSM). Fix an arbitrary order $u_1, \dots, u_n$ of $\mathcal N$ and start from $x_0 = \emptyset$ and $y_0 = \mathcal N$ (the vectors $\mathbf 0$ and $\mathbf 1$ ). In iteration $i = 1, \dots, n$ compute

a_i = F(x_{i-1} + \{u_i\}) - F(x_{i-1}), \qquad b_i = F(y_{i-1} - \{u_i\}) - F(y_{i-1}),

set $a_i' = \max\{a_i, 0\}$ , $b_i' = \max\{b_i, 0\}$ , and update

x_i = x_{i-1} + \frac{a_i'}{a_i' + b_i'} \{u_i\}, \qquad y_i = y_{i-1} - \frac{b_i'}{a_i' + b_i'} \{u_i\},

with the convention that the two fractions are $1$ and $0$ when $a_i' = b_i' = 0$ . The output is the random set $R(x_n)$ . Every choice before the output is deterministic; the algorithm queries $F$ at four points per element.

For the analysis, $OPT_i = (OPT \vee x_i) \wedge y_i$ .

Formalization targets

Goal: Theorem A.1, oracle-access clause

For every nonnegative submodular $f$ and every order of the ground set,

x_n = y_n \qquad\text{and}\qquad f(OPT) \le 2\,F(x_n) = 2\,\mathbb E\bigl[f(R(x_n))\bigr].

Milestones, in the order the proof uses them

$a_i + b_i \ge 0$ at every iteration (proof of Lemma A.2; the page cites Lemma II.1).
Endpoints: $OPT_0 = OPT$ with $F(OPT) = f(OPT)$ , and $OPT_n = x_n = y_n$ .
(4) and (5): if $a_i \ge 0$ and $b_i > 0$ , then $F(x_i) - F(x_{i-1}) = a_i^2/(a_i+b_i)$ and $F(y_i) - F(y_{i-1}) = b_i^2/(a_i+b_i)$ .
(6): in the same case, $F(OPT_{i-1}) - F(OPT_i) \le a_i b_i/(a_i + b_i)$ , whether or not $u_i \in OPT$ .
Lemma A.2: for every $1 \le i \le n$ ,

F(OPT_{i-1}) - F(OPT_i) \le \tfrac12\bigl[F(x_i) - F(x_{i-1}) + F(y_i) - F(y_{i-1})\bigr].

Telescoped display: $F(OPT_0) - F(OPT_n) \le \tfrac12[F(x_n) - F(x_0)] + \tfrac12[F(y_n) - F(y_0)] \le \tfrac12(F(x_n) + F(y_n))$ .

Significance

The result. Theorem A.1 shows that the double greedy analysis survives a change of domain: the factor $1/2$ is obtained by a procedure that never flips a coin until the end, and whose state is a pair of fractional points. The ratio matches the Feige–Mirrokni–Vondrák hardness bound, so it cannot be improved in the value oracle model. Its output is a fractional point together with an independent rounding, which separates the optimization from the rounding step.

Formalizing it. The result is proved on paper; no machine-checked proof of a double greedy guarantee is known. A complete development yields reusable facts about the multilinear extension of a submodular function on a finite type: $F$ is affine in each coordinate, its coordinate increments are antitone in the other coordinates on $[0,1]^{\mathcal N}$ , and $F$ restricted to characteristic vectors is $f$ . These are the standard tools of every continuous-relaxation argument for submodular maximization.

Difficulty

The proof on the page is short, but it relies on two facts it does not prove. First, the page justifies $a_i + b_i \ge 0$ "by Lemma II.1", which is a statement about sets; for vectors it requires that the increment of $F$ along a coordinate decreases as the other coordinates increase, a property of the multilinear extension of a submodular function that must be derived from the sum defining $F$ . Second, inequality (6) is written out only for $u_i \notin OPT$ , and Case 2 of Lemma A.2 is omitted as analogous; the formal statements cover all cases. The main technical work is the bookkeeping of the run: that each coordinate is touched once, that $x_{i-1}(u_i) = 0$ and $y_{i-1}(u_i) = 1$ when it is touched, that $x_i \le OPT_i \le y_i$ , and that every state stays in $[0,1]^{\mathcal N}$ , where the antitonicity applies.

Formalization scope

The ground set is a Fintype $X$ with decidable equality; sets are Finset X; $f$ is real-valued, with nonnegativity a hypothesis ∀ S, 0 ≤ f S wherever the page uses it (the goal and the telescoped display). Submodularity is the published NonmonotoneSubmod.Shared.Submodular, the lattice form $f(S \cup T) + f(S \cap T) \le f(S) + f(T)$ ; $f(OPT)$ is the published NonmonotoneSubmod.Shared.OPT; $F$ is the published NonmonotoneSubmod.Shared.F, the sum above, defined for every $x : X \to \mathbb R$ .
The order $u_1, \dots, u_n$ is a duplicate-free list containing every element; $u_i$ is the entry at index $i-1$ , and $n$ is the list's length. The state after $i$ iterations is obtained by folding one step over the first $i$ entries from $(\mathbf 0, \mathbf 1)$ . Statements hold for every such order.
The footnote's convention $a_i'/(a_i'+b_i') = 1$ , $b_i'/(a_i'+b_i') = 0$ when $a_i' = b_i' = 0$ is an explicit case split; with Lean's $0/0 = 0$ it would otherwise be reversed and the run would no longer end with $x_n = y_n$ .
Corrected slips of the page: lines 3–4 of Algorithm 4 assign $a_i', b_i'$ but define $a_i, b_i$ ; " $f : \mathcal N \to \mathbb R^+$ " means $f : 2^{\mathcal N} \to \mathbb R^+$ ; " $F(x) \triangleq \mathbb E[R(x)]$ " means $\mathbb E[f(R(x))]$ ; "NSM" in Theorem A.1 means USM. The main text's one-line definition of submodularity, read literally, forces monotonicity; the footnote's lattice form is used.
Not formalized: the sampling clause of Theorem A.1 (ratio $(1/2) - o(1)$ without oracle access to $F$ , whose proof the paper refers to Calinescu, Chekuri, Pál and Vondrák) and the running time. The guarantee is stated for the algorithm as printed, so the trivial existence of a $1/2$ -approximation by exhaustive search does not satisfy it. A statement in which $x_n$ is an arbitrary point, or the state any process with $x_i \le y_i$ , would not be this theorem.
Contributions welcome: the multilinear-extension facts above as general lemmas, the run invariants, and proofs of the milestones in any order.

Selected references

N. Buchbinder, M. Feldman, J. Naor, R. Schwartz, A Tight Linear Time (1/2)-Approximation for Unconstrained Submodular Maximization, FOCS 2012, 649–658. https://doi.org/10.1109/FOCS.2012.73 (journal version: SIAM J. Comput. 44(5), 2015, https://doi.org/10.1137/130929205; its numbering differs and is not used here).
U. Feige, V. S. Mirrokni, J. Vondrák, Maximizing Non-monotone Submodular Functions, SIAM J. Comput. 40(4), 2011, 1133–1153. https://doi.org/10.1137/090779346
S. Oveis Gharan, J. Vondrák, Submodular Maximization by Simulated Annealing, SODA 2011, 1098–1117. https://doi.org/10.1137/1.9781611973082.83
M. Feldman, J. Naor, R. Schwartz, Nonmonotone Submodular Maximization via a Structural Continuous Greedy Algorithm, ICALP 2011, 342–353. https://doi.org/10.1007/978-3-642-22006-7_29
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), 2011, 1740–1766. https://doi.org/10.1137/080733991

11 thms3 active usersReviewed

Completed

Operations Research Probability·Captain: mikedeng1

On the Power of Randomization in On-Line Algorithms 1: α-Competitiveness Against Adaptive On-Line and β Against Oblivious Adversaries Give a Deterministic α∘β-Competitive AlgorithmResearch Paper

Why randomization matters in online algorithms

An online algorithm must answer each request before it sees the next one. Its performance is compared with an optimum that may choose all its answers after seeing the complete request string. Randomization can improve an online algorithm's guarantee when the request string is fixed in advance. The comparison changes when an adversary chooses later requests after seeing the algorithm's earlier answers. Ben-David, Borodin, Karp, Tardos and Wigderson studied these choices of adversary in a common request-answer model and proved a general relation between their competitive guarantees (Ben-David et al., 1994, manuscript §§2–3).

The paper distinguishes three adversaries. An oblivious adversary fixes the request string before the algorithm's random choices affect any answer. An adaptive off-line adversary chooses the next request from previous answers but serves the resulting request string optimally after the play. An adaptive on-line adversary also chooses its own answer as each request arrives. The ability to react to answers makes the latter two adversaries materially different from the oblivious one for randomized algorithms (Ben-David et al., 1994, manuscript pp. 7–9).

Request-answer games and competitive cost

A request-answer game has a request set $R$ , a finite nonempty answer set $A$ , and a real cost $f_n(r,a)$ for a request string $r\in R^n$ and an answer string $a\in A^n$ . The off-line optimum for $r$ is $c(r)=\min_{a\in A^n}f_n(r,a)$ . A deterministic online algorithm $D$ returns its $i$ th answer from the first $i$ requests alone; it has no access to the rest of $r$ or to the eventual stopping time. Its cost on $r$ is $c_D(r)=f_n(r,D(r))$ .

A randomized online algorithm is a distribution over deterministic online algorithms. With coins $\omega$ , write $G_\omega$ for the resulting deterministic algorithm. For a fixed request string $r$ , $G$ is $\beta$ -competitive against oblivious adversaries when $\mathbb E_\omega[c_{G_\omega}(r)]\leq\beta(c(r))$ . The paper calls a transformation “linear” when it has the affine form $x\mapsto ux+v$ (Ben-David et al., 1994, manuscript p. 7).

An adaptive off-line adversary $Q$ has a rule from prior answer strings to either the next request or a stop signal, together with a common finite upper bound on play length. Let $r(G_\omega,Q)$ denote its request string and $c_Q(G_\omega)=c(r(G_\omega,Q))$ . Its competitiveness condition places the transformation inside the expectation: $\mathbb E_\omega[c_{G_\omega}(Q)]\leq\mathbb E_\omega[\alpha(c_Q(G_\omega))]$ . An adaptive on-line adversary $S$ has the same request rule and an additional answer rule; its own cost is $c_S(G_\omega)$ , and the corresponding condition uses $\mathbb E_\omega[\alpha(c_S(G_\omega))]$ on the right (Ben-David et al., 1994, manuscript pp. 8–9).

Formalization targets

Randomization against adaptive off-line adversaries

The first target is Theorem 2.1: if some randomized algorithm is $\alpha$ -competitive against every adaptive off-line adversary, a deterministic algorithm has that same guarantee on every request string:

\exists G\;\forall Q,\quad \mathbb E[c_G(Q)]\leq\mathbb E[\alpha(c_Q(G))]\quad\Longrightarrow\quad\exists D\;\forall r,\quad c_D(r)\leq\alpha(c(r)).

Composition of two guarantees

Theorem 2.2 takes an $\alpha$ guarantee for $G$ against adaptive on-line adversaries and a $\beta$ guarantee for another randomized algorithm against oblivious adversaries. It concludes that $G$ has the composed guarantee against adaptive off-line adversaries:

\mathbb E[c_G(Q)]\leq\mathbb E[(\alpha\circ\beta)(c_Q(G))]\qquad\text{for every }Q.

The mission goal is Corollary 2.1, the deterministic consequence of these two results:

\exists D\;\forall r,\qquad c_D(r)\leq(\alpha\circ\beta)(c(r)).

The milestones follow the paper's two theorems and the stated claims in their proofs, including the finite-horizon winning-position formulation and the adversary that simulates a fixed online algorithm (Ben-David et al., 1994, manuscript pp. 9–13).

What the result supplies

The corollary turns the existence of two randomized guarantees under different information rules into the existence of a deterministic online strategy with an explicit composed cost transformation. It is an existence result: it does not say that the deterministic strategy can be computed efficiently from the randomized algorithms. The paper itself notes that such a construction is unavailable in full generality and then examines settings where constructive versions are possible (Ben-David et al., 1994, manuscript p. 13).

The mathematical results were proved in the 1994 paper; this mission asks for machine-checked Lean proofs of the abstract model, the intermediate claims, and Corollary 2.1. The local draft currently contains compiled statements with proof placeholders, so it does not yet provide checked proofs. A completed development would make the adversary distinctions and the exact placement of expectations available for reuse in later online-algorithm formalizations.

Why the proof is difficult

The apparent shortcut is to treat an adaptive request sequence as fixed and apply a guarantee against oblivious adversaries directly. That loses the dependence of later requests on the algorithm's earlier answers. For Theorem 2.1, a winning request strategy must have one finite horizon that works for every answer path; separate finite horizons for each branch do not suffice when the answer set is infinite. For Theorem 2.2, the simulated adversary must make its own answers before the algorithm answers the current request, while still matching a fixed online benchmark along every resulting play. The expectation inequalities must remain valid when the request string itself depends on the algorithm's coins (Ben-David et al., 1994, manuscript pp. 9–11).

Formalization scope

Lean represents requests and answers as oldest-first lists. List index zero is request one in the paper. The general game is a separate definition; the algorithm, adversary, and competitiveness definitions build on it. An off-line adversary's rule returns Option R, where none is the stop signal, and has a uniform finite depth bound. A randomized algorithm consists of a coin probability space and a deterministic prefix algorithm for each coin; its answer events are measurable. Finiteness of $A$ and bounded play depth make the cost of each fixed adversarial play take finitely many values, so its real expectation is an ordinary integrable expectation.

The formal game uses real-valued costs, a deliberate restriction of the paper's $\mathbb R\cup\{\infty\}$ costs. The answer set is finite and nonempty, while the request set may be infinite. The transformations $\alpha$ and $\beta$ are affine. Theorem 2.2 and the goal assume $\alpha$ is monotone: the paper applies $\alpha$ to an inequality in its proof, and its competitive-ratio examples have positive slope. Theorem 2.1 does not need this added assumption. The two randomized algorithms may have different coin spaces, each an arbitrary Lean type at the declaration's universe level. The off-line and on-line adaptive comparisons retain $\alpha$ inside the expectation.

The target ranges over every equal-length request and answer play generated by these rules, including an adversary that stops without a request. It does not allow the deterministic algorithm to see future requests or choose a different policy for each adversary. Reusable contributions include the game interface, bounded adaptive plays, measurable randomized algorithms, and finite-horizon winning positions. The statements of all three principal results, their intervening claims, and proofs of those statements are within scope.

Selected references

S. Ben-David, A. Borodin, R. Karp, G. Tardos and A. Wigderson, On the Power of Randomization in On-Line Algorithms, Algorithmica 11, 1994. DOI: 10.1007/BF01294260. The local source is the authors' 20-page manuscript; citations above use its page numbers.

11 thms3 active usersReviewed

Completed

Operations Research Probability·Captain: mikedeng1

On the Power of Randomization in On-Line Algorithms 2: The Bound α∘β Against Adaptive Off-Line Adversaries Is TightResearch Paper

Motivation

An on-line algorithm must answer each request as it arrives, without knowing the requests to come; paging, caching, the $k$ -server problem and metrical task systems are standard examples. Its quality is measured by competitive analysis: its cost is compared with the cost of an optimal off-line solution that knows the whole request sequence. For randomized on-line algorithms the comparison depends on how much the adversary producing the requests is allowed to see. Ben-David, Borodin, Karp, Tardos and Wigderson (Algorithmica 11, 1994; conference version STOC 1990) introduced the three standard adversaries — oblivious, adaptive on-line and adaptive off-line — and related the competitive ratios achievable against each.

Their Theorem 2.2 (manuscript p. 10) shows that if a randomized algorithm is $\alpha$ -competitive against adaptive on-line adversaries and some randomized algorithm is $\beta$ -competitive against oblivious adversaries, then the first algorithm is $\alpha\beta$ -competitive against adaptive off-line adversaries. This mission formalizes the paper's claim (manuscript p. 11) that this product bound cannot be improved in general, together with the explicit construction on pp. 12–13 that proves it.

Setting

A request-answer game consists of a request set $R$ , a finite answer set $A$ , and cost functions $f_n : R^n \times A^n \to \mathbb R$ . For a request sequence $\underline r \in R^n$ , the off-line optimum is $c(\underline r) = \min_{\underline a \in A^n} f_n(\underline r, \underline a)$ . A deterministic on-line algorithm $G$ answers the $i$ -th request with $a_i = g_i(r_1, \dots, r_i)$ ; a randomized one is a probability distribution over deterministic algorithms $G_x$ , $x$ being the coin tosses.

An adaptive off-line adversary $Q$ chooses each request $r_{i+1} = q_i(a_1, \dots, a_i)$ from the answers given so far, stops after at most $d_Q$ requests, and pays the off-line optimum $c_Q(G) = c(\underline r)$ of the requests it made; the algorithm pays $c_G(Q) = f_n(\underline r, \underline a)$ . An adaptive on-line adversary $S$ must in addition answer each request itself, before the algorithm does, with $b_{i+1} = p_i(a_1, \dots, a_i)$ , and pays $c_S(G) = f_n(\underline r, \underline b)$ . An oblivious adversary fixes $\underline r$ in advance and pays $c(\underline r)$ . A randomized $G$ is $\alpha$ -competitive against oblivious adversaries if $\mathbb E_x[c_{G_x}(\underline r)] \le \alpha\, c(\underline r)$ for all $\underline r$ , and against adaptive on-line adversaries if $\mathbb E_x[c_{G_x}(S)] \le \mathbb E_x[\alpha\, c_S(G_x)]$ for all $S$ .

The construction uses the mates game: $R = A$ is a set of $2t$ elements split into $t$ pairs of mates, and for $n \ge 2$ the cost depends only on the first answer $a_1$ and the second request $r_2$ : it is $1$ if $a_1 = r_2$ , $M$ if $a_1$ is the mate of $r_2$ , and $m$ otherwise. The algorithm $G$ draws $a_1$ uniformly at random. The parameters solve

\beta = \frac{(2t-2)m + M + 1}{2t}, \qquad \alpha = \frac{1 + (2t-1)M}{2 + (2t-2)m}.

Formalization targets

Goal: tightness of Theorem 2.2

For $1 < \beta \le \alpha$ (or $\alpha = \beta = 1$ ) and every $C < \alpha\beta$ , there are a game and a randomized algorithm $G$ such that

G \text{ is } \alpha\text{-competitive against adaptive on-line adversaries}, \qquad G \text{ is } \beta\text{-competitive against oblivious adversaries},

and for every randomized algorithm $K$ some adaptive off-line adversary $Q$ achieves

\mathbb E[c_Q(K)] > 0, \qquad \mathbb E[c_K(Q)] \ge C\cdot \mathbb E[c_Q(K)].

Milestones (pp. 12–13)

The closed forms $m(t)$ , $M(t)$ are the unique solution of the two equations.
$m(t) \to \beta$ and $M(t) \to \alpha\beta$ as $t \to \infty$ .
For all large $t$ : $M(t) \ge \max(m(t)^2, C)$ , $1 \le m(t) \le M(t)$ , $\alpha(m(t)-1) \le M(t) - m(t)$ .
$G$ is $\beta$ -competitive against oblivious adversaries in the mates game.
$G$ is $\alpha$ -competitive against adaptive on-line adversaries in the mates game.
An adaptive off-line adversary makes every algorithm pay $M$ while paying $1$ .

Significance

The result. Together with Theorem 2.2, the claim pins down exactly how much the adaptive off-line adversary can gain over the other two: the product $\alpha\beta$ is an upper bound for every game and is approached by a single game for every admissible pair $(\alpha, \beta)$ . It shows that no general argument relating the three adversary models can give a bound better than the product, so any improvement for a specific problem (paging, $k$ -server) must use the structure of that problem. The paging example cited on p. 11 (RANDOM against the three adversaries) gives one instance of tightness; the mates game gives tightness for every admissible pair.

Formalizing it. The result is proved in the paper, in about one page, with two steps left to the reader ("by inspection of the equations", "a simple case analysis"). No machine-checked proof of this or of any statement about adaptive adversaries is known to us. The formalization makes the model of §2 precise (sequences, stopping, the order in which adversary and algorithm commit, expectations over coins), checks the asymptotics of the parameters, and verifies the case analysis, which on inspection needs an inequality the page does not state. Two printed formulas on p. 12 contain typos; the formal statements carry the correct values.

Difficulty

The construction is explicit, but each competitiveness claim quantifies over all adversaries, which may adapt their requests to the algorithm's random answers, stop at any time, and (for the on-line adversary) commit to their own answers in advance. The algebra of $\alpha$ -competitiveness is tight: the adversary's best expected advantage is exactly zero, so every case of its best reply must be checked with no slack. The page's condition $M \ge m^2$ does not suffice for this: when $a_1$ is neither the adversary's first answer nor its mate, the reply "mate of $a_1$ " beats the reply "the adversary's own answer" only when $\alpha(m-1) \le M - m$ , which holds for the solved parameters but is not implied by $M \ge m^2$ . At $\beta = 1 < \alpha$ the solved parameter $m$ is below $1$ for every $t$ , and the oblivious bound fails.

Formalization scope

All declarations live in OnlineRandomization.Tightness. The conventions:

Costs are real-valued; the paper allows $+\infty$ , so the game class is a special case.
Answer sets are nonempty finite types; request sets are arbitrary types.
Sequences are Lean lists, oldest first; cost r a is $f_n$ on lists of equal length $n$ .
Adversaries return none for "stop" and carry a depth bound $d_Q$ ; an on-line adversary's answer $b_{i+1}$ depends only on $a_1, \dots, a_i$ .
Randomized algorithms are a probability space of coins with a deterministic algorithm per coin and measurable answers; expectations are Bochner integrals, with $\alpha$ applied inside the expectation. In the goal, coin spaces range over Type.
Competitiveness uses the ratio functions $x \mapsto \alpha x$ and $x \mapsto \beta x$ , with no additive constant.
The mates game is on Fin t × Bool, with mate $(i, b) \mapsto (i, \lnot b)$ . The paper leaves the costs of plays with fewer than two requests undefined; the formalization sets $f_0 = 0$ and $f_1 \equiv 1$ (with $f_1 \equiv 0$ the algorithm would not be $\alpha$ -competitive).
Range. The goal assumes $1 < \beta \le \alpha$ or $\alpha = \beta = 1$ ; the page's case $\beta = 1 < \alpha$ is not covered by its construction and is left out. In fact the claim is false there for $1 < C < \alpha$ : an algorithm that is $1$ -competitive against oblivious adversaries answers optimally, almost surely, on every request sequence (its cost is never below the optimum and its expected cost does not exceed it), and an adaptive off-line adversary reaches only finitely many request sequences, so against $K = G$ every adversary has $\mathbb E[c_G(Q)] = \mathbb E[c_Q(G)]$ , a ratio of $1 < C$ .

The positivity requirement $\mathbb E[c_Q(K)] > 0$ in the goal is essential: without it the adversary that asks nothing satisfies $\mathbb E[c_K(Q)] \ge C \cdot 0$ for every $K$ , and the third clause would hold vacuously.

A complete development needs: finite expectations over a uniform coin, the evaluation of the play of an adversary against a constant algorithm, and limit and eventual-inequality arguments for rational functions of $t$ . The model of §2 is shared with the other missions of this series and is reusable for any request-answer formulation of an on-line problem. Proofs of individual milestones are welcome.

Selected references

S. Ben-David, A. Borodin, R. Karp, G. Tardos, A. Wigderson, On the power of randomization in on-line algorithms, Algorithmica 11 (1994) 2–14. https://doi.org/10.1007/BF01294260 (cited from the authors' manuscript, manuscript pp. 7–13).
A. Borodin, R. El-Yaniv, Online Computation and Competitive Analysis, Cambridge University Press, 1998. ISBN 0-521-56392-5.
P. Raghavan, M. Snir, Memory versus randomization in on-line algorithms, IBM Journal of Research and Development 38 (1994) 683–707. https://doi.org/10.1147/rd.386.0683

9 thms3 active usersReviewed

Completed

Operations Research Probability·Captain: mikedeng1

Secretary Problems: Weights and Discounts 3: An O(log n)-Competitive Algorithm for the Discounted Secretary ProblemResearch Paper

Motivation

In the secretary problem, $n$ candidates with arbitrary values arrive one at a time in a uniformly random order, and an online decision maker must accept or reject each candidate on arrival, irrevocably, keeping at most one. The rule that observes the first $n/e$ candidates and then accepts the first one better than everything seen so far selects the best candidate with probability about $1/e$ (Dynkin, 1963). The problem is a basic model of online selection and, read economically, of posted-price mechanisms for agents who arrive in random order: a rule that compares each agent only against a threshold set by earlier agents is truthful.

Babaioff, Dinitz, Gupta, Immorlica and Talwar (SODA 2009) study a variant in which time costs value. Selecting the candidate who arrives at time $t$ earns that candidate's value multiplied by a discount $d(t)$ , for an arbitrary non-negative discount function $d$ known in advance. Earlier work treated only specific discount shapes, such as geometric discounting $d(t)=\beta^t$ (Rasmussen and Pliska, 1976). For a general $d$ the classical rule can fail badly: if all the discount mass sits in the first few time steps, a rule that waits through a sample of size $n/e$ earns nothing. The paper shows that the best competitive ratio for arbitrary discounts lies between $\Omega(\log n/\log\log n)$ (its Theorem 4.3) and $O(\log n)$ (its Theorem 4.4). This mission formalizes the upper bound.

Setting

There are $n\ge1$ elements, indexed $\{0,\dots,n-1\}$ , with values $v(e)\ge 0$ , and $n$ times with discounts $d(t)\ge0$ . A uniformly random permutation $\pi$ fixes the order of arrivals: element $\pi(t)$ arrives at time $t$ . An algorithm knows $d$ but not $v$ ; it sees each value on arrival and may select the current element, irrevocably, earning $d(t)\,v(\pi(t))$ . Expectations over $\pi$ are exact averages over the $n!$ orders.

The offline optimum on order $\pi$ is $\mathsf{OPT}(\pi)=\max_t d(t)\,v(\pi(t))$ ; it is a random variable, and the benchmark is its expectation $\mathbb E_\pi[\mathsf{OPT}]$ (p. 4 of the paper).

Let $d_{\max}=\max_t d(t)$ and $v_{\max}=\max_e v(e)$ . For $c\ge1$ the $c$ -th discount class is the set of times

P_c=\{\,i : 2^{-c}d_{\max}<d(i)\le 2^{-(c-1)}d_{\max}\,\}.

The quantity $\mathsf{OPT}_c$ is the part of $\mathbb E_\pi[\mathsf{OPT}]$ earned when the optimal time (the smallest time attaining the maximum) lies in $P_c$ .

The classical secretary rule on $m$ arrivals observes the first $\lfloor m/e\rfloor$ and then selects the first arrival that ranks above every earlier arrival. Ranks use a fixed tie-break order: larger value first, and smaller element index among equal values.

The algorithm $\mathcal A$ sets $M=3\lceil\log_2 n\rceil+2$ , draws $c\in\{1,\dots,M\}$ uniformly, and runs the classical rule on the subsequence of arrivals at the times of $P_c$ , ignoring all other arrivals.

Formalization targets

Goal: Theorem 4.4 with its explicit constant

\mathbb E_\pi[\mathsf{OPT}]\;\le\;4e\,\bigl(3\lceil\log_2 n\rceil+2\bigr)\;\mathbb E[\mathcal A]\qquad(n\ge1,\ d\ge0,\ v\ge0).

The paper states $\mathbb E[\mathsf{OPT}]/\mathbb E[\mathcal A]\le O(\log n)$ ; the constant $4e$ is the one its proof yields.

Milestones

The classical secretary rule selects the top-ranked of $m\ge1$ elements with probability at least $1/e$ (§2, p. 4).
$\mathsf{OPT}_1\ge v_{\max}d_{\max}/n$ (proof of Theorem 4.4, p. 7).
$\mathsf{OPT}_c\le 2^{-c}\,2n^2d_{\max}v_{\max}$ for every $c\ge1$ (p. 7).
$\sum_{c=1}^{3\lceil\log_2 n\rceil+1}\mathsf{OPT}_c\ge\tfrac12\mathbb E_\pi[\mathsf{OPT}]$ (p. 7).
$\mathbb E[\mathcal A_c]\ge\mathsf{OPT}_c/2e$ for every $c\ge1$ , where $\mathcal A_c$ is the classical rule on $P_c$ (p. 7).

Significance

The theorem shows that a general discount function costs only a logarithmic factor against the offline benchmark, and that one algorithm achieves this without any knowledge of the values. Together with the lower bound of Theorem 4.3 it pins the competitive ratio of the discounted secretary problem between $\log n/\log\log n$ and $\log n$ . The same scale-splitting idea, stated in the paper as Theorem 4.5 without full proof, extends the bound to the weighted discounted problem.

The result is proved in the paper; to our knowledge it has not been formalized. A complete development would also produce a machine-checked proof of the classical secretary guarantee for the rule with sample size exactly $\lfloor m/e\rfloor$ at every finite $m$ , with an explicit tie-break, which is reusable by every secretary-type mission. Milestone 1 is that statement. Sharper constants or a smaller class range are welcome as additional statements but do not replace the goal, which is about this algorithm with this $M$ .

Difficulty

The obvious argument, running the classical rule on all $n$ arrivals, fails because the discounts can be concentrated at times the rule spends sampling. Splitting by discount scale fixes this but creates two problems. First, there are unboundedly many scales, and one has to show that the offline optimum's mass outside the top $O(\log n)$ of them is negligible against $\mathbb E[\mathsf{OPT}]$ , a random quantity rather than a fixed maximum. Second, the classical rule on a class sees only a random subset of the elements, in random order, and the guarantee must be transferred to this subsequence, conditioning on which elements land in $P_c$ . Neither step is deep, but both require careful bookkeeping of permutations, and the classical $1/e$ bound at finite $m$ with a floor in the sample size is itself a nontrivial estimate.

Formalization scope

Elements and times are Fin n, an order is π : Equiv.Perm (Fin n) read as time $\mapsto$ element, and the paper's time $t=1,\dots,n$ is index $t-1$ . Values and discounts are Fin n → ℝ with non-negativity hypotheses. Every expectation is the finite average $\frac1{n!}\sum_\pi$ ; the algorithm's random class is the explicit average $\frac1M\sum_{c=1}^M$ . Maxima are suprema over the finite index set. The logarithm is base 2, $\lceil\log_2 n\rceil$ is Nat.clog 2 n, and the sample size is Nat.floor (m / Real.exp 1). Ties are broken by the order on Lex (ℝ × (Fin n)ᵒᵈ) (larger value, then smaller index); distinct values are not assumed. The optimal time is the smallest maximizing time, so that the $\mathsf{OPT}_c$ add up to $\mathbb E[\mathsf{OPT}]$ . Competitiveness is stated multiplicatively, never as a quotient, so $\mathbb E[\mathcal A]=0$ is not a loophole.

The goal is a statement about the specific algorithm $\mathcal A$ , not "there exists an algorithm": an existential over unrestricted algorithms is witnessed by a clairvoyant rule that reads the values in advance. $\mathcal A$ sees the values only through comparisons among arrivals that have already occurred, and $\mathbb E[\mathsf{OPT}]$ is the expected offline maximum over the same random order, not $d_{\max}v_{\max}$ .

Needed infrastructure: averages over permutations and the fact that the elements landing at a fixed set of times form a uniformly random subset in uniformly random order; the finite- $m$ analysis of the classical rule; and elementary estimates on geometric sums. Contributions of general lemmas about uniform permutations are welcome and reusable.

Selected references

M. Babaioff, M. Dinitz, A. Gupta, N. Immorlica, K. Talwar, Secretary Problems: Weights and Discounts, Proc. 20th ACM-SIAM Symposium on Discrete Algorithms (SODA), 2009. https://doi.org/10.1137/1.9781611973068.139
E. B. Dynkin, The optimum choice of the instant for stopping a Markov process, Soviet Math. Doklady 4, 1963.
T. S. Ferguson, Who solved the secretary problem?, Statistical Science 4(3), 1989. https://doi.org/10.1214/ss/1177012493
L. T. Rasmussen, S. R. Pliska, Choosing the maximum from a sequence with a discount function, Applied Mathematics and Optimization 2, 1976. https://doi.org/10.1007/BF01458209
M. Babaioff, N. Immorlica, R. Kleinberg, Matroids, secretary problems, and online mechanisms, SODA 2007. https://dl.acm.org/doi/10.5555/1283383.1283429

9 thms3 active usersReviewed

Combinatorics Operations Research Probability·Captain: mikedeng1

A Polylogarithmic-Competitive Algorithm for the k-Server Problem: Randomized k-Server Is O(log² k · log³ n · log log n)-Competitive on Every n-Point MetricResearch Paper

Motivation

The k-server problem (Manasse, McGeoch and Sleator, 1990) is the central problem of online computation: $k$ servers sit on points of a metric space, requests arrive one at a time at points of the space, and each request must be served by moving a server to it, at a cost equal to the distance travelled. An online algorithm decides without knowing future requests; its quality is its competitive ratio, the worst-case ratio between its cost and the cost of an optimal offline schedule. Paging (caching) is the special case of a uniform metric, and weighted paging the case of a weighted star.

Timeline of the upper bounds for general metrics:

1990: Manasse, McGeoch and Sleator prove that every deterministic algorithm has ratio at least $k$ and conjecture that $k$ is achievable.
1991: Fiat, Rabani and Ravid give the first ratio depending on $k$ only (exponential in $k$ ).
1995: Koutsoupias and Papadimitriou prove that the work function algorithm is $(2k-1)$ -competitive.
For randomized algorithms against an oblivious adversary, the conjectured answer is $O(\log k)$ , achieved for paging (Fiat et al., 1991), but until 2011 nothing better than the deterministic $2k-1$ was known for general metrics, even when the ratio may depend on the number of points $n$ .
2011: Bansal, Buchbinder, Mądry and Naor give the first polylogarithmic bound, $O(\log^2 k\log^3 n\log\log n)$ (arXiv:1110.1580; J. ACM 62(5), 2015, DOI 10.1145/2783434), the result of this mission.

Setting

Let $(M,\mathrm{dist})$ be a finite metric space with $n$ points and $k$ a number of servers. A configuration $C:\{1,\dots,k\}\to M$ places server $i$ at $C(i)$ . A deterministic online algorithm maps each prefix of the request sequence to a configuration that has a server at the last request; its cost on a sequence $\rho$ is the total distance travelled. $\mathrm{OPT}(C_0,\rho)$ is the least cost of any schedule serving $\rho$ from the initial configuration $C_0$ . A randomized algorithm is a probability distribution over deterministic online algorithms, all starting at $C_0$ ; it is $c$ -competitive if there is a constant $a$ such that its expected cost on every request sequence $\rho$ is at most $c\cdot\mathrm{OPT}(C_0,\rho)+a$ .

The paper works with three auxiliary objects. A σ-HST is a rooted tree whose leaves are the points, in which all edges from a node to its children have one common length, equal to $1/\sigma$ times the length of the edge above that node; the distance between two leaves is the length of the tree path. A weighted σ-HST only requires that the edge above a non-root internal node be at least $\sigma$ times each edge below it. In the fractional k-server problem on a tree, the state is a vector $x$ of server probabilities on the leaves with $0\le x_i\le1$ and $\sum_i x_i=k$ , a request at leaf $i$ forces $x_i=1$ , and moving from $x$ to $x'$ costs $\sum_v W(v)\,|x'_v-x_v|$ , where $x_v$ is the mass below node $v$ and $W(v)$ the length of the edge above $v$ . In the allocation problem on a weighted star with weights $w_i$ , requests carry a location $i^t$ , a monotone cost vector $h^t(0)\ge\dots\ge h^t(k)\ge0$ (the cost of serving with $j$ servers there) and a server quota $\kappa(t)\le k$ .

Formalization targets

Goal: Theorem 1

There is a universal constant $C>0$ such that for all $k\ge2$ , every metric space $M$ with $n\ge3$ points and every initial configuration $C_0$ , some randomized online algorithm starting at $C_0$ is

C\,\log^2 k\,\log^3 n\,\log\log n\text{-competitive.}

Milestones

In the order the proof uses them:

Claim 15: the fix-stage inequality behind the allocation algorithm's analysis.
Theorem 5: for every $0<\varepsilon\le1$ , a fractional allocation algorithm whose hit cost is at most $(1+\varepsilon)(\mathrm{Opt}+w_{\max}g(\kappa))+a$ and whose movement cost is at most $O(\log(k/\varepsilon))(\mathrm{Opt}+w_{\max}g(\kappa))+a$ , where $g(\kappa)=\sum_t|\kappa(t)-\kappa(t-1)|$ .
Theorem 6: given such allocation algorithms, an $O(\ell\log(k\ell))$ -competitive fractional k-server algorithm on every weighted σ-HST of depth $\ell$ with $\sigma=\Omega(\ell\log(k\ell))$ .
Theorem 8: every σ-HST with $n$ leaves becomes a weighted σ-HST of depth $O(\log n)$ on the same leaves, with distances distorted by at most $2\sigma/(\sigma-1)$ .
Lemma 25 and Theorem 24: on a σ-HST with $\sigma>5$ , randomized states consistent with a changing fractional state can be maintained online at cost $O(c_t)$ per step.
Theorem 7: on a σ-HST with $\sigma>5$ , a $c$ -competitive fractional algorithm yields an $O(c)$ -competitive randomized one.

Significance

The theorem broke the exponential gap between the $\Omega(\log k)$ lower bound and the $2k-1$ upper bound for randomized k-server, and showed that randomization helps on every finite metric, not only on uniform or specially structured ones. Its two-level method (a fractional algorithm on trees driven by per-node allocation problems, followed by an online rounding) became the template for later work, including the $O(\log^2 k)$ bound on HSTs of Bubeck, Cohen, Lee, Lee and Mądry (STOC 2018) and Lee's $O(\log^6 k)$ bound on general metrics (FOCS 2018).

The result is proved, in this paper. As far as is known it has no machine-checked proof. Formalizing it means formalizing the analysis of an online algorithm driven by a continuous-time process, a potential-function argument with exact constants, a tree contraction with a distortion bound, and an online randomized rounding against a transportation cost. The allocation, HST and rounding statements are reusable for other online problems on trees (metrical task systems, weighted paging).

Difficulty

For a deterministic or randomized algorithm on a tree, the natural recursion splits the servers of each node among its children. Coté, Meyerson and Poplawski showed that this works if each node solves an allocation problem with a strong guarantee: hit cost within a factor $1+\varepsilon$ of optimal. Integral allocation algorithms cannot achieve this; the integrality gap example of the paper (p. 8) gives a factor $\Omega(k)$ . The fractional relaxation avoids the gap, but then the rounding step must keep a randomized state consistent with a fractional state at constant-factor cost, and the HSTs obtained from general metrics have depth growing with the aspect ratio, which a depth-dependent ratio cannot afford. Each of the three reductions (allocation to fractional k-server, deep HST to shallow weighted HST, fractional to randomized) loses only polylogarithmic or constant factors, and the main theorem needs all three at once.

Formalization scope

The k-server model, randomized algorithms and competitiveness are the published definitions KServer_model and KServer_randomized; competitiveness carries an additive constant fixed before the request sequence. Trees are finite rooted trees with a parent map, a depth function and positive edge lengths; points of the k-server problem are the leaves, and the theorems take an arbitrary finite metric space together with a bijection to the leaves and the hypothesis that the distance equals the tree distance. Fractional k-server states have exactly $k$ units of mass, each leaf at most $1$ , and fractional algorithms are measured against the integral offline optimum. The allocation optimum is the integral optimum; cost vectors are finite, non-negative and non-increasing; the diameter of the star is $w_{\max}=\max_i w_i$ . The cost of changing a randomized state is the transportation cost over couplings, with minimum-matching cost between configurations. Every $O(\cdot)$ is an explicit constant quantified before the instance, except that in Theorems 7 and 24 and Lemma 25 it may depend on $\sigma$ .

Formalizations that make the targets trivial are excluded: the fractional state must place a full server on every request and stay in $[0,1]$ , the benchmark is the integral optimum (not the algorithm's own or the fractional cost), and no constant may depend on $k$ , $n$ , the metric or the tree, since otherwise Theorem 1 would follow from the $2k-1$ bound.

The proof of Theorem 1 also uses the embedding of Fakcharoenphol, Rao and Talwar [18] of a finite metric into a distribution over σ-HSTs with expected distortion $O(\sigma\log_\sigma n)$ . It is an external ingredient, not a result of this paper, and is not a milestone; contributions formalizing it (or Bartal's earlier embedding) are welcome, as are formalizations of the integral optimum's properties on trees (Lemmas 21–22 of the paper), which are not stated here.

Selected references

N. Bansal, N. Buchbinder, A. Mądry, J. Naor, A Polylogarithmic-Competitive Algorithm for the k-Server Problem, arXiv:1110.1580v1, 2011; J. ACM 62(5), 2015. https://arxiv.org/abs/1110.1580, https://doi.org/10.1145/2783434
M. Manasse, L. McGeoch, D. Sleator, Competitive algorithms for server problems, J. Algorithms 11, 1990. https://doi.org/10.1016/0196-6774(90)90003-W
E. Koutsoupias, C. Papadimitriou, On the k-server conjecture, J. ACM 42(5), 1995. https://doi.org/10.1145/210118.210128
A. Fiat, R. Karp, M. Luby, L. McGeoch, D. Sleator, N. Young, Competitive paging algorithms, J. Algorithms 12, 1991. https://doi.org/10.1016/0196-6774(91)90041-V
J. Fakcharoenphol, S. Rao, K. Talwar, A tight bound on approximating arbitrary metrics by tree metrics, J. Comput. Syst. Sci. 69(3), 2004. https://doi.org/10.1016/j.jcss.2004.04.011
A. Coté, A. Meyerson, L. Poplawski, Randomized k-server on hierarchical binary trees, STOC 2008. https://doi.org/10.1145/1374376.1374474

14 thms3 active usersReviewed

Completed

Combinatorics Operations Research Optimization·Captain: mikedeng1

Online Scheduling of a Single Machine to Minimize Total Weighted Completion Time: Delayed SWPT Has Competitive Ratio 2Research Paper

Motivation

A single machine must process $n$ jobs that arrive over time. Job $j$ is released at time $r_j$ , needs $p_j$ units of uninterrupted processing, and has weight $w_j > 0$ ; the goal is to minimize the total weighted completion time $\sum_j w_j C_j$ . Offline, with all release dates equal to zero, Smith's rule (sequence by nondecreasing $p_j/w_j$ ) is optimal (Smith 1956); with arbitrary release dates the problem $1\,|\,r_j\,|\,\sum w_j C_j$ is strongly NP-hard (Lenstra, Rinnooy Kan and Brucker 1977).

In the online version the scheduler learns of job $j$ only at time $r_j$ , and at each moment must either start a released job or keep the machine idle. Its quality is measured by its competitive ratio: the worst case, over all instances, of the ratio between the online schedule's cost and the offline optimum. Release-date scheduling is one of the basic test cases of online optimization.

Timeline:

1996. Hoogeveen and Vestjens show that no online algorithm has competitive ratio below 2, even with equal weights, and give the 2-competitive algorithm Delayed SPT for equal weights.
1997. Hall, Schulz, Shmoys and Wein give a $(3+\varepsilon)$ -competitive algorithm for arbitrary weights, based on geometric intervals and linear programming.
1998. Phillips, Stein and Wein give another 2-competitive algorithm for equal weights, which does not extend to arbitrary weights.
2002. Goemans, Queyranne, Schulz, Skutella and Wang obtain a $(1+\sqrt2)$ -competitive deterministic algorithm from an LP relaxation.
2004. Anderson and Potts show that Delayed SWPT has competitive ratio exactly 2 for arbitrary positive weights, matching the lower bound.

Setting

An instance has jobs $j \in J = \{1,\dots,n\}$ with integer release dates $r_j \ge 0$ , integer processing times $p_j \ge 1$ and real weights $w_j > 0$ . A schedule assigns each job an integer start time $S_j$ . It is feasible if $S_j \ge r_j$ for every $j$ and no two intervals $[S_j, S_j + p_j)$ overlap; idle time is allowed. Its cost is $C(S) = \sum_j w_j (S_j + p_j)$ .

Delayed SWPT runs over unit time slots $[t, t+1)$ . When the machine is available at time $t$ , it looks at the jobs released by $t$ and not yet started, and selects one with the smallest ratio $p_j/w_j$ . Ties go to the smaller $p_j$ , then to the smaller index. If $p_j \le t$ , it starts $j$ at $t$ and the machine is busy until $t + p_j$ . Otherwise the machine stays idle and the rule is applied again at $t+1$ . The resulting schedule is written $\pi$ , or dswpt I in Lean. In particular no job starts before time $p_j$ .

The proof uses three auxiliary problems:

the doubled problem (2P), with data $(2r_j, 2p_j, w_j)$ ;
the extended problem (E), with release dates $r'_j = \max\{p_j, f(r_j)\}$ , where $f(t)$ is the first time at or after $t$ at which $\pi$ leaves the machine free;
one unit-length gap job $g_t$ for each slot $[t,t+1)$ in which Delayed SWPT idles although a job $j$ is available. The gap job has release date $f(r_j)$ and weight $w_j/p_j$ .

The schedule $\pi_E$ of (E) runs the original jobs as in $\pi$ and each $g_t$ in $[t,t+1)$ .

Formalization targets

Goal: Theorem 8

\min\Bigl\{\rho \;:\; \sum_j w_j C_j(\pi) \le \rho \sum_j w_j C_j(S)\ \text{for every instance and every feasible schedule } S\Bigr\} = 2.

Lean: IsLeast {ρ | ∀ n I S, IsFeasible I.r I.p S → cost I.w I.p (dswpt I) ≤ ρ * cost I.w I.p S} 2. Both halves are required: the upper bound $2$ and the fact that no smaller constant is valid for this algorithm.

Milestones

$\pi_j \ge p_j$ for every job (§2) and $r'_j \le \max\{2r_j, p_j\}$ (§3.2).
$\pi_E$ is feasible for (E) (§3.2).
Lemma 1. If $\pi^*$ and $\mu^*$ are optimal for (P) and (2P), then $C(\mu^*) = 2\,C(\pi^*)$ .
Lemma 2. $\pi_E$ is optimal for (E).
Lemma 3. If $\mu^*$ is optimal for (2P) and a feasible $\sigma_E$ for (E) satisfies

\sum_{j\in J} w_j C_j(\sigma_E) + \sum_{g\in G} w_g C_g(\sigma_E) \le \sum_{j\in J} w_j C_j(\mu^*) + \sum_{g\in G} w_g C_g(\pi_E), \tag{1}

then $C(\pi) \le 2\,C(S)$ for every feasible $S$ . 6. Inequality (1) holds for some feasible $\sigma_E$ , for every optimal $\mu^*$ of (2P) (§§3.4–3.6).

Significance

The theorem shows that a deterministic online algorithm can match the lower bound of Hoogeveen and Vestjens for arbitrary positive weights. This settles the best competitive ratio for deterministic online algorithms for $1\,|\,r_j\,|\,\sum w_j C_j$ . The algorithm needs no linear program. The analysis also does not compare the algorithm with a lower bound on the optimum. Instead it shows that the online schedule is optimal for a modified problem (E), and it converts an optimal schedule of (2P) into a schedule of (E).

The result was proved on paper in 2004. Neither Mathlib nor the Prove2Me catalog contains a machine-checked proof of it, or of any competitive ratio for online scheduling with release dates. This mission provides several reusable pieces:

an executable, verified-terminating definition of an online scheduling rule;
the doubling lemma for release-date problems;
the optimality criterion behind Lemma 2;
the block-by-block exchange argument of §§3.3–3.6.

Difficulty

The obvious argument fails at Lemma 2. Delayed SWPT is far from optimal for (P) itself, and its idle time is unbounded in relative terms. The proof therefore has to show that the inserted gap jobs make every idle slot "justified", so that a preemptive best-available argument becomes valid for (E). That argument rests on an optimality criterion of Belouadah, Posner and Potts (1992), which is not in Mathlib.

The second difficulty is inequality (1). Once $\mu^*$ is doubled and the gap jobs are inserted, nongap jobs must be shifted, and the gain of each gap-generating job must be charged against the delay of the gap jobs in its block. That accounting (Lemmas 4–7 of the paper) is an induction over blocks with signed differences of completion times.

The natural first idea, plain online SWPT (start the available job with the smallest $p_j/w_j$ whenever the machine is free), has no finite competitive ratio (Example 1 of the paper), so the delay $\pi_j \ge p_j$ is essential to the bound and must be tracked through the whole argument.

Formalization scope

Conventions committed to in Lean:

Data. Jobs are Fin n (0-based, so "smallest index" is the order of Fin n). Times are natural numbers, the paper's standing integer-data assumption (p. 688), and weights are real. Every instance carries $p_j \ge 1$ and $w_j > 0$ .
Schedules and optimality. Schedules are integer start times. Feasibility, cost and optimality are defined for any finite job type, so (E), with job type Fin n ⊕ gapTimes I, uses the same notions. "Optimal" means optimal among all feasible nonpreemptive schedules with integer start times.
The algorithm. Delayed SWPT is a def: a unit-time simulation that compares ratios by cross-multiplication and re-applies the rule at every slot. It runs to the horizon $\sum_j (r_j + 2p_j) + 1$ . A sorry-free check (not uploaded) shows that every job has started by then, and that the simulation reproduces Examples 3 and 4 of the paper, including the gap times $0,2,3,4,5,6$ of Table 2.
Completion times. In (2P) the completion time is $\mu^*_j + 2p_j$ , and gap jobs have unit length.

The goal quantifies over every feasible schedule of every instance. It cannot be met by restricting the competitor to schedules without idle time or to list schedules, by dropping release-date feasibility, or by leaving jobs unscheduled.

Out of scope:

The general lower bound "no online algorithm beats 2" (Example 2 of the paper, due to Hoogeveen and Vestjens) is not part of the mission. The lower half of the goal concerns Delayed SWPT only.
The Belouadah–Posner–Potts optimality criterion is an external ingredient of Lemma 2. Solvers may formalize it as a supporting theorem.

Infrastructure that a complete development needs:

simulation invariants for the algorithm;
exchange and left-shift arguments for single-machine schedules;
the job-splitting relaxation behind the best-available criterion.

The schedule vocabulary and the criterion are reusable for other release-date scheduling results. Contributions toward the block lemmas of §§3.3–3.6 (Lemmas 4–7, the bound (9)) are welcome as supporting theorems.

Selected references

E. J. Anderson and C. N. Potts, Online Scheduling of a Single Machine to Minimize Total Weighted Completion Time, Mathematics of Operations Research 29(3), 686–697, 2004. https://doi.org/10.1287/moor.1040.0092
J. A. Hoogeveen and A. P. A. Vestjens, Optimal On-Line Algorithms for Single-Machine Scheduling, IPCO 1996, LNCS 1084, 404–414. https://doi.org/10.1007/3-540-61310-2_30
L. A. Hall, A. S. Schulz, D. B. Shmoys and J. Wein, Scheduling to Minimize Average Completion Time: Off-line and On-line Approximation Algorithms, Mathematics of Operations Research 22(3), 513–544, 1997. https://doi.org/10.1287/moor.22.3.513
C. Phillips, C. Stein and J. Wein, Minimizing Average Completion Time in the Presence of Release Dates, Mathematical Programming 82, 199–223, 1998. https://doi.org/10.1007/BF01585872
M. X. Goemans, M. Queyranne, A. S. Schulz, M. Skutella and Y. Wang, Single Machine Scheduling with Release Dates, SIAM Journal on Discrete Mathematics 15(2), 165–192, 2002. https://doi.org/10.1137/S089548019936223X
H. Belouadah, M. E. Posner and C. N. Potts, Scheduling with Release Dates on a Single Machine to Minimize Total Weighted Completion Time, Discrete Applied Mathematics 36(3), 213–231, 1992. https://doi.org/10.1016/0166-218X(92)90255-9
J. K. Lenstra, A. H. G. Rinnooy Kan and P. Brucker, Complexity of Machine Scheduling Problems, Annals of Discrete Mathematics 1, 343–362, 1977. https://doi.org/10.1016/S0167-5060(08)70743-X
W. E. Smith, Various Optimizers for Single-Stage Production, Naval Research Logistics Quarterly 3, 59–66, 1956. https://doi.org/10.1002/nav.3800030106

11 thms3 active usersReviewed

Complexity Theory Operations Research Optimization·Captain: mikedeng1

Project Scheduling with Time Windows and Scarce Resources IX: Deciding Feasibility with Cumulative Resources Is NP-Complete Even for Acyclic Project NetworksTextbook

Motivation

Project scheduling with cumulative resources models production and logistics projects in which activities fill and empty storage: an activity withdraws material from an inventory when it starts and deposits its output when it completes, and every inventory must stay between a safety stock and a storage capacity. Neumann, Schwindt and Zimmermann treat this model in §2.12 of Project Scheduling with Time Windows and Scarce Resources (2nd ed., Springer 2003, doi:10.1007/978-3-540-24800-2) and use it in their process-industry applications.

Before any optimization, a scheduler must know whether a feasible schedule exists at all. Theorem 2.12.1 of the book answers the complexity of this question: it is NP-complete, and it stays NP-complete when the project network has no cycles. The contrast with renewable resources (machines, workers) is the point of the theorem: with renewable resources, the feasibility problem is NP-complete as well (Theorem 2.3.13, after Bartusch, Möhring and Radermacher, 1988), but an acyclic network always admits a feasible schedule when every requirement is within capacity.

The mission also collects the two other reductions the book proves in full: Proposition 2.5.4 (recognizing whether an activity lies in some minimal delaying alternative, the branching object of the book's branch-and-bound procedures, is NP-complete) and Proposition 3.4.2 (maximizing weighted start-time deviations, a resource-levelling objective, is NP-hard without any resource constraints).

Setting

A project has activities $V=\{0,1,\dots,n+1\}$ with $n\ge1$ ; activity $0$ is the project beginning and $n+1$ the project completion. Activity $i$ has a duration $p_i\in\mathbb N$ , with $p_0=p_{n+1}=0$ . The project network $N$ has arc set $E$ ; an arc $\langle i,j\rangle$ with integer weight $\delta_{ij}$ imposes the temporal constraint $S_j-S_i\ge\delta_{ij}$ on the start times. A schedule is a real vector $S=(S_i)_{i\in V}$ with $S_0=0$ and $S_i\ge0$ ; it is time-feasible if it meets every temporal constraint.

Cumulative resources $k\in\mathcal R^\gamma$ carry integer demands $r_{ik}$ : $r_{ik}<0$ depletes $-r_{ik}$ units at the start $S_i$ , $r_{ik}>0$ replenishes $r_{ik}$ units at the completion $S_i+p_i$ , and $r_{0k}$ is the initial stock. The inventory at time $t$ is

r_k(S,t)=\sum_{i:\ r_{ik}<0,\ S_i\le t} r_{ik}+\sum_{i:\ r_{ik}>0,\ S_i+p_i\le t} r_{ik}.

With safety stock $\underline R_k$ and storage capacity $\overline R_k$ (integers, $\underline R_k\le\sum_{i\in V}r_{ik}\le\overline R_k$ by (2.12.1)), $S$ is feasible if it is time-feasible and $\underline R_k\le r_k(S,t)\le\overline R_k$ for every $k$ and every $t\ge0$ . The decision problem of $PSc|temp|C_{\max}$ asks whether a feasible schedule exists.

For renewable resources $k\in\mathcal R$ with capacities $R_k$ and requirements $r_{ik}\in\mathbb N$ , a set $F\subseteq V$ is forbidden if $\sum_{i\in F}r_{ik}>R_k$ for some $k$ . A delaying alternative for $F$ is a set $B\subseteq F$ such that $F\setminus B$ is not forbidden; it is minimal if no proper subset of $B$ is one.

In $PS\infty|temp,\bar d|f$ there are no resources, schedules must also satisfy $S_{n+1}\le\bar d$ , and the objective here is $f(S)=-\sum_{i\in V}\sum_{j>i}w_{ij}|S_j-S_i|$ with weights $w_{ij}\ge0$ .

NP and NP-completeness are taken in the sense of Cook's Turing-machine formulation, with instances written in binary.

Formalization targets

Goal: Theorem 2.12.1

Assuming PARTITION is NP-complete,

L=\{\text{codes of instances of }PSc|temp|C_{\max}\text{ with a feasible schedule}\}\ \text{ and }\ L_{\mathrm{acyc}}=L\cap\{N\text{ acyclic}\}

are both NP-complete.

Milestones

Membership (proof of Theorem 2.12.1): $L\in\mathrm{NP}$ and $L_{\mathrm{acyc}}\in\mathrm{NP}$ .
Reduction correctness (proof of Theorem 2.12.1): for sizes $s(1),\dots,s(\nu)$ with even sum, the project with $r_0=r_{n+1}=-\sum s(i)/2$ , $r_i=s(i)$ , $\underline R=\overline R=0$ , $d^{\min}_{0,n+1}=1$ has an acyclic network, and it has a feasible schedule iff the sizes split into two parts of equal sum.
Polynomial transformation: $\mathrm{PARTITION}\le_p L_{\mathrm{acyc}}$ .
Proof of Proposition 2.5.4, one resource: for $j^*\in B\subseteq F$ , $B$ is a minimal delaying alternative iff $R-\min_{j\in B}r_j<\sum_{i\in F\setminus B}r_i\le R$ .
Proof of Proposition 2.5.4, with $r_{j^*}=1$ : a minimal delaying alternative contains $j^*$ iff some $A\subseteq F\setminus\{j^*\}$ has $\sum_{i\in A}r_i=R$ .
Proposition 2.5.4: assuming SUBSET SUM is NP-complete, deciding whether some minimal delaying alternative for a forbidden set $F$ contains $j^*\in F$ is NP-complete.
Proof of Proposition 3.4.2: a graph has a cut of at least $M$ edges iff the constructed instance has a schedule with $S_i\in\{0,1\}$ and $\sum_{i<j}w_{ij}|S_j-S_i|\ge M$ .
Proposition 3.4.2: assuming SIMPLE MAX CUT is NP-complete, the decision version of $PS\infty|temp,\bar d|-\sum\sum w_{ij}|S_j-S_i|$ is NP-hard.

The goal follows from milestones 1 and 3 together with the transfer of NP-completeness along $\le_p$ (on the platform as CookPvsNP.npComplete_of_polyReducible).

Significance

The result. Theorem 2.12.1 explains why the book's methods for cumulative resources enumerate precedence relations between depleting and replenishing activities (minimal surplus and shortage sets, Theorem 2.12.4) instead of relying on a constructive feasibility test: unless P = NP, no polynomial algorithm decides feasibility, even for acyclic networks, where the renewable-resource case is trivial. Proposition 2.5.4 does the same for the branching scheme of §2.5, and Proposition 3.4.2 places the resource-levelling objectives of Chapter 3 among the hard ones.

Formalizing it. The three results are proved in the book, as short reductions whose delicate steps are left implicit: the polynomial size of a certificate for real-valued schedules, the handling of instances outside the construction (odd sums, empty index sets, oversized items), and the passage from an optimization problem to its decision version. None of the three reductions is machine-checked anywhere known. The mission states them against a single Turing-machine model and a single binary encoding, reusing the published definitions CookPvsNP_defs, so that the reductions compose with the Cook–Levin development already on the platform.

Difficulty

The mathematical content of the reductions is short; the difficulty is in the complexity-theoretic layer. Two steps resist the obvious argument.

First, NP membership. The book's certificate is a schedule, and a schedule is a real vector: it is not a string. A verifier needs a finite certificate of polynomial length, and it is not immediate that a feasible instance has a feasible schedule with small rational (or integer) start times, since the inventory constraints involve strict orderings between event times.

Second, polynomial-time computability in a concrete Turing-machine model. The transformation must compute, on a one-tape machine, binary codes of sums and halves of the input sizes, an arc list of quadratic length, and must map malformed strings to fixed no-instances. Informal "clearly polynomial" arguments have to become explicit machine constructions or a reusable library of closure properties.

Formalization scope

The Lean development fixes the following conventions.

Activities are Fin (n + 2), with the completion Fin.last (n + 1); resources are Fin m. Start times are real.
The inventory constraints hold for every $t\ge0$ , not only for $0\le t\le\bar d$ as (2.12.2) is printed; the book's proofs use this reading.
Real activities may have duration $0$ in $PSc|temp|C_{\max}$ : the reduction of Theorem 2.12.1 uses only such activities.
Instances are coded as lists of integers written in binary over the alphabet $\{0,1,-,\#\}$ ; arc weights are listed for every ordered pair of activities together with an arc indicator. Well-formedness (standing assumptions such as $n\ge1$ , $p_0=p_{n+1}=0$ , no loops, (2.12.1), $r_{ik}\le R_k$ ) is part of each language.
"Acyclic" means the nodes admit a numbering increasing along every arc.
The NP-completeness of PARTITION, SUBSET SUM and SIMPLE MAX CUT (Karp, 1972) enters as a hypothesis of the corresponding theorem; these are not results of the book.
Proposition 3.4.2 is stated for the decision version of the optimization problem, with natural-number weights and threshold.

A trivializing formalization is ruled out: the languages contain only codes of well-formed instances, the encoding is injective, and the hypotheses on the source problems are true theorems, so the goal cannot hold vacuously or by a degenerate encoding.

A complete development needs closure properties of polynomial-time computable functions in Cook's model (composition, binary arithmetic, list manipulation), transitivity of $\le_p$ , and a small-certificate lemma for systems of difference constraints with strict and non-strict inequalities. These are reusable for every NP-hardness proof stated in the same framework. Contributions to any of them, to the instance-level milestones 2, 4, 5 and 7, or to the NP-completeness of PARTITION, SUBSET SUM and SIMPLE MAX CUT in this model, are welcome.

Selected references

K. Neumann, C. Schwindt, J. Zimmermann, Project Scheduling with Time Windows and Scarce Resources, 2nd ed., Springer, 2003. doi:10.1007/978-3-540-24800-2
M. Bartusch, R. H. Möhring, F. J. Radermacher, Scheduling project networks with resource constraints and time windows, Annals of Operations Research 16, 1988.
M. R. Garey, D. S. Johnson, Computers and Intractability: A Guide to the Theory of NP-Completeness, W. H. Freeman, 1979.
R. M. Karp, Reducibility among combinatorial problems, in Complexity of Computer Computations, Plenum, 1972. doi:10.1007/978-1-4684-2001-2_9
S. Cook, The P versus NP Problem, Clay Mathematics Institute problem description. claymath.org

14 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

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

Theoretical Computer Science

Missions

Complexity of Machine Scheduling Problems 6: DIRECTED HAMILTON PATH Reduces to No-Wait Flow Shop Makespan and Total Completion TimeResearch Paper

Motivation

Setting

Formalization targets

Goal (Theorem 5)

Milestones, in the order the proof uses them

Significance

Difficulty

Formalization scope

Selected references

Complexity of Machine Scheduling Problems 3: KNAPSACK Reduces to Single-Machine Total Weighted TardinessResearch Paper

Motivation

Setting

Formalization targets

Goal: Theorem 4(d)

The equivalence and its claims

Significance

Difficulty

Formalization scope

Selected references

Complexity of Machine Scheduling Problems 2: KNAPSACK Reduces to Single-Machine Maximum Lateness, Weighted Number of Late Jobs, and Weighted Completion Time with DeadlinesResearch Paper

Motivation

Setting

Formalization targets

Goal: Theorem 4(b), (c), (e), (f)

Milestones: the four yes-instance equivalences

Significance

Difficulty

Formalization scope

Selected references

Complexity of Machine Scheduling Problems 1: PARTITION Reduces to Makespan and to Weighted Completion Time on Two Identical MachinesResearch Paper

Motivation

Setting

Formalization targets

Goal: Theorem 3

Milestones

Significance

Difficulty

Formalization scope

Selected references

Online Stochastic Matching: Beating 1-1/e 3: No Online Algorithm Beats Expected Approximation Factor 26/27 on a 6-Cycle, and None Reaches 1 − o(1) on Disjoint 6-CyclesResearch Paper

Motivation

Setting

Formalization targets

Goal: Theorem 3

Milestones

Significance

Difficulty

Formalization scope

Selected references

On the Approximability of Single-Machine Scheduling with Precedence Constraints 3: The Incomparable-Pairs Graphs of Canonical Interval Orders Have Unbounded Chromatic NumberResearch Paper

Motivation

Setting

Formalization targets

Significance

Difficulty

Formalization scope

Selected references

On the Approximability of Single-Machine Scheduling with Precedence Constraints 1: A k-Fold Realizer of Size t Yields a Vertex Cover of Expected Weight at Most (2 − 2/(t/k)) Times OptimalResearch Paper

Motivation

Setting

Formalization targets

Goal: Theorem 5.1 (p. 658)

Milestones

Significance

Difficulty

Formalization scope

Selected references

Shadow Tomography of Quantum States 3: Shadow Tomography Needs Ω(min{D², log M}/ε²) CopiesResearch Paper

Why count copies of a quantum state

Setting

Formalization targets

Goal: Theorem 19 (p. 23)

Milestones (pp. 23–24)

Significance

Difficulty

Formalization scope

Selected references