Motivation

Scheduling work on several identical processors creates a plausible expectation: completing tasks sooner, removing constraints, or adding a processor should not delay the overall finish. A fixed priority-list rule defeats that expectation. When a task becomes ready earlier, it can occupy a processor that would otherwise have run another task; that decision changes later availability. Graham gives explicit schedules in which changing only the list raises the finishing time from 12 to 14, removing two precedence constraints raises it to 16, shortening every task raises it to 13, or adding one processor raises it to 15. These examples establish that the effect is a property of the scheduling rule, rather than of a change in the total set of tasks. See Graham, §2, pp. 417–419.

This mission concerns the upper limit of that effect. An operations researcher comparing a list schedule before and after a change in available processors or task data needs a bound that survives all four changes at once. The result is also a compact benchmark for formalizing algorithms whose behavior depends on changing availability: the model must describe when tasks become ready, when processors are idle, and which ready task a processor takes next. Graham's Theorem 1, proved in the 1969 paper, supplies the bound.

Setting

There are $r$ tasks $T_1,\ldots,T_r$ and $n$ identical processors. Each task $T_j$ has a positive processing time $\mu(T_j)$. A strict precedence order $\prec$ specifies tasks that must be completed first: $T_i\prec T_j$ means $T_j$ cannot start before $T_i$ ends. A priority list $L$ orders all tasks once each. It may place a successor before a predecessor, because the processor skips any task that is not ready. These conventions are those of Graham's system in §2, p. 416.

A schedule gives each task a processor and a start time $S_j\ge0$. Once started, the task occupies that processor continuously on $[S_j,S_j+\mu(T_j))$. Two tasks on one processor cannot overlap, while tasks may meet at an endpoint. Precedence means $S_i+\mu(T_i)\le S_j$ whenever $T_i\prec T_j$. The finishing time $\omega$ is the largest completion time $S_j+\mu(T_j)$. The paper's list rule starts the first currently ready task in $L$ whenever a processor can take a task. A ready task that has not started cannot coexist with an idle processor. If one task starts while another ready task waits, the started task is earlier in $L$.

The same task set is run a second time, with processing times $\mu'$, order $\prec'$, list $L'$, processor count $n'$, and finishing time $\omega'$. The data satisfy $\mu'(T_j)\le\mu(T_j)$ for every $j$ and $\prec'\subseteq\prec$. Thus the second run may have shorter tasks and fewer precedence relations; both lists may differ arbitrarily. Both runs obey the same list-scheduling rule Graham, §3, p. 419.

Formalization targets

General anomaly bound

For $r,n,n'\ge1$, positive processing times in both runs, and the two list schedules just described, the target is Graham's Theorem 1:

$$\frac{\omega'}{\omega}\le 1+\frac{n-1}{n'}.$$

The numerator and denominator refer to the actual runs, with potentially different lists and processor counts. The conclusion does not require the new schedule to finish earlier. Its factor permits the anomalies shown in §2 while preventing an arbitrarily large increase for fixed $n,n'$. The supporting targets follow the proof's numbered displays: a precedence chain covering idle times in the second run (1), an idle-time estimate for that chain (2), a comparison of its length with the first run (3)–(4), and the work-volume bound used in (5) Graham, pp. 419–420.

Significance

The theorem places a quantitative limit on the damage caused by a list rule after simultaneous changes in task durations, precedence, ordering, and capacity. When $n'=n$, the factor is $2-1/n$; when the first run has one processor, it is $1$. The statement applies to every finite task set and every pair of lists, so it can be reused when a scheduling method produces a list without additional structural guarantees. Graham states that the bound is best possible, citing earlier examples; this mission formalizes the inequality in this paper and does not claim to formalize those external examples Graham, p. 420.

The result is proved in the source paper. The work here is to give its objects precise Lean definitions and to supply machine-checked proofs of the bound and its supporting claims. A formal development needs to account for continuous real start times, processor assignments, half-open execution intervals, and the behavior of the list rule when several tasks or processors become available together. The resulting model of a nonpreemptive list schedule and the basic volume and chain estimates can serve later formalizations of parallel scheduling. The present proposal contains statements and definitions; its theorem bodies are open proof obligations.

Difficulty

Total work alone does not control the anomaly: processors can be idle while precedence keeps available work from starting, and changing precedence can alter which tasks occupy the processors later. A direct comparison of corresponding task completion times between the two runs also fails in Graham's §2 examples. The central difficulty is expressing the second run's idle periods through work on a single precedence chain and then relating that chain to the first run's finishing time. In Lean, the chain and the time intervals must be represented without silently changing endpoint conventions or treating a ready but unstarted task as running.

Formalization scope

Tasks are Fin r and processors are Fin n, with zero-based Lean indices corresponding to Graham's one-based subscripts. Processing times and start times are real. A priority list is a bijection between positions and tasks, so it contains every task exactly once and need not respect precedence. The order is strict. Feasible schedules are nonpreemptive and use half-open running intervals. The finishing time is a finite maximum of completion times; for no tasks it is defined as zero, while the ratio theorem assumes $r>0$ so its denominator is positive. Both processor counts are positive. The strict positivity of both time functions is inherited from the paper's $\mu:T\to(0,\infty)$ convention.

The model captures Graham's rule by no unforced idleness and list priority. It does not encode the smaller-index tie rule for identical processors, since the tie affects only processor labels and not start times or $\omega$. The covering-chain milestone represents Graham's set $B$ as times before $\omega'$ when not all processors are busy; all-idle times before the finish cannot occur under the list rule. The idle-time milestone writes the total duration of empty tasks as $n'\omega'-\sum_j\mu'(T_j)$ using display (5). Natural-number subtraction is not used in the constants: $n-1$ and $n'-1$ are real differences. The companion existence statement and a concrete two-task sanity check rule out a vacuous list-schedule predicate. Contributions can address that existence theorem, the chain construction, interval accounting, the volume bound, and the final ratio.

Selected references

• R. L. Graham, Bounds on Multiprocessing Timing Anomalies, SIAM Journal on Applied Mathematics 17(2), 416–429, 1969. DOI: 10.1137/0117039.

Motivation

Parallel processing poses a basic allocation question: given tasks of known lengths and several identical processors, how much time is lost when tasks are assigned by a simple list rule instead of an optimal allocation? The finishing time is the moment the last processor completes its work. For independent tasks, a list rule starts each next task on a processor that becomes free first. Such a rule is easy to execute, but the resulting allocation can be worse than the best partition of tasks among processors. Graham's 1969 paper studies precise worst-case ratios for this model. Its Theorem 3 asks what guarantee follows when the first $k$ tasks of the list are chosen among the longest and scheduled optimally before the remaining tasks are appended.

The paper also notes two endpoints of this family. With $k=0$, the rule is ordinary list scheduling and has ratio at most $2-1/n$. With $k=n$, the $n$ longest tasks can start one per processor, giving ratio at most $3/2-1/(2n)$. Theorem 3 expresses these as instances of one bound, including the integer jump at each multiple of $n$ Graham, pp. 427–428.

Setting

There are $r>0$ independent tasks, indexed by $jin\{0,\ldots,r-1\}$, and $n>0$ identical processors, indexed by $p\in\{0,\ldots,n-1\}$. Task $j$ takes a strictly positive time $\mu_j$. A priority list $L$ contains every task exactly once. Its first $k$ tasks are $k$ of the longest tasks; equal lengths may be ordered either way. As a processor becomes available, it takes the next task in the list. Once started, a task runs without interruption. With no precedence constraints, every unstarted task is ready, so a processor runs its assigned tasks consecutively from time zero.

An assignment $\sigma$ records the processor that executes each task. The load $\ell_p(\sigma)$ of processor $p$ is the sum of its assigned task lengths. The finishing time is the largest load, $\omega(k)=\max_p\ell_p(\sigma)$. For a list assignment, each task is assigned to a processor whose load from earlier list tasks is smallest at that step. If two processors are tied, either can be selected without changing the finishing time. For any assignment $\tau$, let $\omega_k(\tau)$ be the largest load contributed by only the first $k$ list tasks. The algorithm requires its own first $k$ assignments to minimize $\omega_k(\tau)$ over all assignments $\tau$; the remaining tasks may occur in any list order.

Write $\omega_0$ for the smallest finishing time achievable for all $r$ tasks. The paper introduces it as the minimum over possible lists and later describes the same problem as minimizing the largest part sum over partitions of the task lengths Graham, pp. 421, 428. The formalization uses the partition or assignment form of $\omega_0$.

Formalization targets

Theorem 3

For $0\le k\le r$, when the first $k$ longest tasks have an optimal prefix schedule, Graham's bound is

$$\frac{\omega(k)}{\omega_0} \le 1+\frac{1-1/n}{1+\lfloor k/n\rfloor}.$$

Here $\lfloor k/n\rfloor$ is the greatest integer at most $k/n$. The theorem also says the bound is best possible when $k$ is divisible by $n$ Graham, Theorem 3, p. 427. The equality examples are a separate companion statement in this mission.

Source milestones

The milestones state the finite-volume lower bound on $\omega_0$, the case in which completing all tasks takes no longer than completing the first $k$, and the paper's numbered inequalities (14), (15), and (16). They use $\alpha^*$ for the greatest task length after the first $k$ positions. These are individual mathematical claims from the proof on p. 427, with their original wording and formulas recorded alongside the formal statements.

Significance

The theorem gives a quantitative tradeoff between work spent optimizing a prefix and the worst-case finishing time of the full list. Its denominator is $1+\lfloor k/n\rfloor$, so the guarantee improves when the optimized prefix contains another full processor's worth of long tasks. The example at multiples of $n$ shows that the stated coefficient cannot be uniformly reduced for the algorithm as specified Graham, p. 427.

The result is proved in the paper. This mission's remaining work is a machine-checked proof of its exact statement and the source's intermediate inequalities. The published identical-machine makespan definition is reused, while the list-assignment rule, optimal prefix, and longest-remaining-task quantity are made explicit here. Those definitions can also support later work on list scheduling without precedence constraints. No machine-checked proof of Theorem 3 is claimed by this proposal.

Difficulty

An optimal schedule for the first $k$ long tasks does not make the entire list optimal: short tasks appended later can affect which processor finishes last. A bound based only on average total work ignores this final imbalance; a bound based only on the largest remaining task ignores how many long tasks every assignment must place together. The proof must relate both constraints to one finishing time while preserving the floor $\lfloor k/n\rfloor$. Replacing that floor with the real quotient changes the claim, and allowing an arbitrary prefix arrangement loses the algorithm's required optimality.

Formalization scope

Tasks and processors are finite indexed sets Fin r and Fin n; their zero-based indices correspond to the paper's one-based $T_j$ and $P_i$. Task lengths are positive real numbers, and both $r$ and $n$ are positive. The list is a permutation, not merely a sequence that might omit or repeat a task. The condition $k\le r$ is explicit because choosing $k$ tasks from $r$ requires it; the paper treats $r>k$ inside the proof and the case $k=r$ is covered by the theorem. There is no precedence relation in this mission.

The list rule is a predicate on assignments: each next task goes to a processor with least current load. It omits the paper's smaller-index tie convention, since tied identical processors can be interchanged without changing the finishing time. The first $k$ positions must contain $k$ longest tasks, and their assignment must minimize the prefix finishing time among all assignments of those tasks. Those conditions are part of the goal; the inequalities (14)–(16) are conclusions to establish, not assumptions of the goal. A separate existence statement and a checked concrete instance ensure the list predicate is satisfiable.

All maxima and minima range over finite nonempty processor or assignment sets. The optimum is a minimum over assignments, equivalent to the paper's minimum over lists in the independent-task model. The quantity $\alpha^*$ is the largest duration outside the prefix when $k<r$, and is defined as zero when none remains; statements using it require $k<r$. Division is by $n>0$ and by $\omega_0>0$. Lean's natural-number quotient represents $\lfloor k/n\rfloor$; real subtraction is used for coefficients such as $n-1$. Contributions toward the finite load identities, the optimum-over-lists equivalence, and proofs of the listed bounds are within scope.

Selected references

• R. L. Graham, Bounds on Multiprocessing Timing Anomalies, SIAM Journal on Applied Mathematics 17(2), 416–429, 1969. DOI: 10.1137/0117039.

3SUM asks whether three distinct positions in a list of integers contain values summing to zero. It is a central problem in fine-grained complexity.

This mission formalizes a deterministic $O(n^{1.9992})$ algorithm for 3SUM on $n$ polynomially bounded integers, on a word RAM with $O(\log n)$-bit words. Alman and Vassilevska Williams's 2026 breakthrough gives a truly subquadratic bound, refuting the integer 3SUM hypothesis in this model.

The mission uses the accompanying Lean specification and shares the Exact Triangle milestone with Truly Subcubic APSP on a Word RAM.

References

1. Josh Alman and Virginia Vassilevska Williams, Truly Subquadratic 3SUM and Truly Subcubic APSP via Triangles in Sparse Lopsided Graphs, 2026, Theorem 22.
2. Anthropic, formal-math / 3sum-apsp: accompanying Lean formalization, Theorem_22_3SUM.

Why priority queues with cheap decrease key matter

Many network optimization algorithms spend most of their time in a heap (priority queue): a set of items with real keys that supports inserting an item, finding and deleting an item of minimum key, melding two heaps, decreasing the key of an item, and deleting an arbitrary item. Dijkstra's shortest-path algorithm performs at most one delete min per vertex and may perform a decrease key for each edge, so on a graph with $n$ vertices and $m$ edges its running time is governed by how cheap decrease key is. Binomial queues support the heap operations in $O(\log n)$ worst-case time.

Fredman and Tarjan (J. ACM 34 (1987)) introduced Fibonacci heaps (F-heaps), in which delete min and delete take $O(\log n)$ amortized time and every other operation, decrease key included, takes $O(1)$ amortized time. This brings Dijkstra's algorithm to $O(n \log n + m)$ and improves the best bounds then known for all-pairs shortest paths, weighted bipartite matching (the assignment problem) and minimum spanning trees. F-heaps descend from the binomial queues of Vuillemin (1978) and use the potential technique of amortized analysis of Sleator and Tarjan. This mission formalizes the paper's §2 analysis, culminating in THEOREM 1 on p. 604.

Setting

An F-heap is a list of heap-ordered rooted trees: every child's key is at least its parent's key. Each node holds an item, the item's real key and a mark bit; the children of a node are kept in the order in which they were linked to it, earliest first. The rank $r(x)$ of a node is its number of children. A collection is a list of heaps, named by position; a run starts with no heaps.

Linking two trees with roots $x$ and $y$ makes $y$ the last child of $x$ if the key of $x$ is smaller, and otherwise makes $x$ the last child of $y$; the root that becomes a child is unmarked. The operations act as follows:

• make heap adds an empty heap; find min acts on a nonempty heap and returns a root of minimum key; insert adds a one-node tree for a new item; meld concatenates two root lists.
• delete min removes a root $x$ of minimum key, adds the children of $x$ to the roots, then repeats the linking step, "find any two trees whose roots have the same rank, and link them", in any order, until all root ranks are distinct.
• decrease key $(\Delta, i, h)$, $\Delta \ge 0$, lowers the key of $i$ and, if the node $x$ of $i$ is not a root, cuts $x$ from its parent, making its subtree a new tree. delete $(i, h)$ cuts $x$ the same way, destroys it and adds its children to the roots; a minimum root is deleted as in delete min.
• After every cut of a child of $p$, if $p$ is not a root it is marked if unmarked and cut from its own parent if marked: a cascading cut, which may repeat upwards.

The actual time of an operation is one unit, plus one per linking step, plus one per cut, plus for delete min the scan of the rank array (the largest rank involved). The potential $\Phi$ of a collection is the number of trees plus twice the number of marked nonroot nodes, and the amortized time of an operation is its actual time plus the increase of $\Phi$.

Formalization targets

Goal: THEOREM 1 (p. 604)

There is an absolute constant $C > 0$ such that for every sequence of $T$ operations started from no heaps, with $n_t$ the number of items in the heap that operation $t$ acts on, just before it acts,

$$\sum_{t<T} \mathrm{cost}_t \;\le\; \sum_{t<T} b_t, \qquad b_t = \begin{cases} C(\log_2 n_t + 1) & \text{delete min or delete},\\ C & \text{otherwise.}\end{cases}$$

The paper's wording is "the total time is at most the total amortized time, where the amortized time is $O(\log n)$ for each delete min or delete operation and $O(1)$ for each of the other operations"; the goal pins the $O(\cdot)$ to one constant and does not name the potential.

Milestones

1. LEMMA 1: the $i$th child of a node, in linking order, has rank at least $i - 2$.
2. $F_{k+2} \ge \varphi^k$, with $F_k$ the Fibonacci numbers and $\varphi = (1+\sqrt5)/2$.
3. COROLLARY 1: a node of rank $k$ has at least $F_{k+2} \ge \varphi^k$ descendants, itself included.
4. A node of rank $k$ in an $n$-item heap has $\varphi^k \le n$, hence $k \le \log n / \log\varphi$.
5. make heap, find min and meld leave $\Phi$ unchanged; insert raises it by one.
6. delete min raises $\Phi$ by at most $\log n / \log \varphi$ minus the number of linking steps.
7. decrease key raises $\Phi$ by at most three minus the number of cascading cuts.
8. From no heaps, the total amortized time bounds the total actual time.

Significance

THEOREM 1 is the data-structure fact behind the paper's algorithmic results: Dijkstra's algorithm in $O(n\log n + m)$, all-pairs shortest paths and the assignment problem in $O(n^2 \log n + nm)$, and minimum spanning trees in $O(m\,\beta(m,n))$.

The result has been proved since 1987. What the mission adds is a machine-checked version of the paper's own analysis on an operational model with arbitrary linking order, unmarking on link, marking or cascading on every cut, and the paper's unit costs. The proposal states the theorem and its supporting claims; their proofs remain to be formalized.

Difficulty

The obvious argument, that every tree is a binomial tree and so every rank is at most $\log_2 n$, fails as soon as cuts are allowed: decrease key and delete remove subtrees arbitrarily, and the trees of an F-heap need not be binomial. The rank bound has to come from an invariant of the whole history (LEMMA 1), which only holds because a node loses at most one child before it is cut itself; without cascading cuts a node of rank $k$ can be left with only $k+1$ descendants, and no logarithmic rank bound holds. A second difficulty is that the actual cost of one decrease key is unbounded, since a single operation may trigger arbitrarily many cascading cuts; a per-operation worst-case argument cannot give THEOREM 1, and the bound holds only for whole sequences started from no heaps.

Formalization scope

All declarations sit in the namespace FibHeap.Amort. Trees are a nested inductive FTree with item ℕ, key ℝ, a mark bit and a list of children in linking order; a heap is List FTree (its roots) and a collection is List Heap. Operations are a step relation Step s op s' d whose data d records linking steps, cuts, cascading cuts and the scan, so that cost d = 1 + links + cuts + scan is determined by what the operation did. The linking loop allows every order of linking; a link tie makes the first root a child of the second, while delete min may choose any minimum-key root. Runs start from no heaps; reachable collections consist of heap-ordered trees with each item in at most one heap. LEMMA 1, COROLLARY 1 and the delete-min bound are stated for reachable collections only, as the paper's "a node in an F-heap" intends. The paper's standing assumption that an item is in only one heap at a time is enforced by the precondition of insert and is not a hypothesis. The minimum pointer and returned items are not stored in the step relation; find min is a state-preserving step charged one unit. A heap destroyed by meld remains as an empty heap at its index.

Logarithms in the goal are base 2 (footnote 1, p. 600), with a $+1$ so that one-item heaps have positive budget. The paper's constant "$\le 1.4404 \log n$" on p. 604 is a rounding slip ($1/\log_2 \varphi = 1.44042\ldots$); milestones use the exact $\log_\varphi n$.

The goal is not trivialized: the cost counts every linking step and every cut as fixed by the step relation, $C$ is quantified before the run, and a companion theorem (step_exists) shows that every valid operation can be performed, so runs containing delete min, decrease key and cascading cuts exist. A further supporting statement gives an explicit form of the delete potential bound. A complete development needs facts about the nested inductive (sizes, subtree lists, marked counts under list edits), an invariant for LEMMA 1 recording when each child was linked, and the Fibonacci inequality; contributions of any of these as separate lemmas are welcome.

Selected references

• M. L. Fredman and R. E. Tarjan, Fibonacci heaps and their uses in improved network optimization algorithms, J. ACM 34(3):596–615, 1987. https://doi.org/10.1145/28869.28874
• J. Vuillemin, A data structure for manipulating priority queues, Comm. ACM 21(4):309–315, 1978. https://doi.org/10.1145/359460.359478
• R. E. Tarjan, Amortized computational complexity, SIAM J. Algebraic Discrete Methods 6(2):306–318, 1985. https://doi.org/10.1137/0606031
• E. W. Dijkstra, A note on two problems in connexion with graphs, Numer. Math. 1:269–271, 1959. https://doi.org/10.1007/BF01386390

All-pairs shortest paths (APSP) computes the shortest distance between every pair of vertices in a weighted graph. It is a fundamental problem in graph algorithms and a fundamental problem in fine-grained complexity.

This mission formalizes a deterministic $O(n^{2.99942})$ algorithm for APSP on directed $n$-vertex graphs with polynomially bounded integer edge weights and no negative cycles, on a word RAM with $O(\log n)$-bit words. This is a truly subcubic bound and refutes the integer-weight APSP hypothesis in this model.

References:

1. Josh Alman and Virginia Vassilevska Williams, Truly Subquadratic 3SUM and Truly Subcubic APSP via Triangles in Sparse Lopsided Graphs, 2026, Theorem 22.
2. Anthropic, formal-math / 3sum-apsp: accompanying Lean formalization, Theorem_22_APSP.

Motivation

Minimum makespan scheduling on unrelated parallel machines, written $R\,||\,C_{\max}$, is one of the basic models of scheduling theory: $n$ jobs must each be run on one of $m$ machines, and the time a job takes depends arbitrarily on the machine. Lenstra, Shmoys and Tardos (CWI Report OS-R8714, 1987; journal version Math. Programming 46, 1990) gave a polynomial 2-approximation algorithm for this problem and, in the same paper, a matching limit from below: no polynomial algorithm can guarantee a factor smaller than $3/2$ unless $P = NP$ (their Corollary 2).

The two bounds have stood for more than three decades. Closing the gap between $3/2$ and $2$ for $R\,||\,C_{\max}$ is listed among the central open problems of approximation algorithms (Williamson and Shmoys, The Design of Approximation Algorithms, 2011, open problem on unrelated machines; Schuurman and Woeginger, Polynomial time approximation algorithms for machine scheduling: ten open problems, J. Scheduling 1999). The lower bound of $3/2$ is the subject of this mission.

Timeline:

• 1979: Graham, Lawler, Lenstra and Rinnooy Kan introduce the classification $R\,||\,C_{\max}$.
• 1987/1990: Lenstra, Shmoys and Tardos prove NP-completeness of deciding makespan at most 3 (Theorem 4, giving the bound $4/3$) and at most 2 (Theorem 5, giving $3/2$), both by reduction from 3-dimensional matching.
• Since then: the $3/2$ hardness bound has not been improved for general $R\,||\,C_{\max}$; progress has concentrated on special cases such as the restricted-assignment problem.

Setting

3-dimensional matching. There are three disjoint sets $A = \{a_1,\dots,a_n\}$, $B = \{b_1,\dots,b_n\}$, $C = \{c_1,\dots,c_n\}$ and a family $F = \{T_1,\dots,T_m\}$ of triples, each with one element of $A$, one of $B$ and one of $C$. A matching is a subfamily $F'$ with $|F'| = n$ whose union is $A \cup B \cup C$. In Lean an instance is a map $T : \mathrm{Fin}\,m \to \mathrm{Fin}\,n \times \mathrm{Fin}\,n \times \mathrm{Fin}\,n$, and HasMatching T says that a matching exists.

The scheduling model. Machines are $\mathrm{Fin}\,m$, jobs are $\mathrm{Fin}\,N$, and $p_{ij}$ is the positive integer processing time of job $j$ on machine $i$. A schedule $\sigma$ assigns each job to one machine; the load of machine $i$ is $\sum_{j:\sigma(j)=i} p_{ij}$ and the makespan $C_{\max}(\sigma)$ is the largest load. These are the published definitions MatousekLP.Scheduling.load and makespan.

The instance of Theorem 5. The triples containing $a_j$ are the triples of type $j$; let $t_j$ be their number. From $T$ the paper builds a scheduling instance with $m$ machines, machine $i$ corresponding to $T_i$, and with

1. $2n$ element jobs, one for each $b_k$ and each $c_l$;
2. $t_j - 1$ dummy jobs of type $j$, for each $j$.

If $T_i = (a_j, b_k, c_l)$, machine $i$ processes the element jobs of $b_k$ and $c_l$ in time $1$, each dummy job of type $j$ in time $2$, and every other job in time $3$. In Lean the processing-time matrix is P T.

A $\rho$-approximate schedule of an instance is a schedule $\sigma$ with $C_{\max}(\sigma) \le \rho\, C_{\max}(\tau)$ for every schedule $\tau$ of the same instance.

Formalization targets

Goal: Corollary 2 (p. 8)

For every instance $T$, every $\rho < 3/2$, and every $\rho$-approximate schedule $\sigma$ of the instance of Theorem 5 built from $T$,

$$C_{\max}(\sigma) \le 2 \iff T \text{ has a matching}.$$

This is the mathematical content of "for every $\rho < 3/2$ there is no polynomial $\rho$-approximation algorithm unless $P = NP$": a $\rho$-approximate answer on the reduced instance decides 3-dimensional matching.

Theorem 5 (p. 7)

For every instance $T$,

$$\exists\,\sigma:\ C_{\max}(\sigma) \le 2 \iff T \text{ has a matching}.$$

Milestones from the proof of Theorem 5 (pp. 7–8)

1. If every $t_j \ge 1$, then $\sum_j (t_j - 1) + n = m$: there are $m - n$ dummy jobs.
2. A matching yields a schedule with makespan at most $2$.
3. A schedule with makespan at most $2$ yields a matching.

Significance

The result. Theorem 5 shows that $R\,||\,C_{\max}$ is NP-hard already when every processing time lies in $\{1,2,3\}$ and the target makespan is $2$. Corollary 2 turns this into the best known inapproximability bound for the problem, $3/2$, which sits opposite the paper's own factor-2 algorithm. The same reduction pattern (machines as triples, dummy jobs that pin machines down) is reused in many later hardness proofs for scheduling and assignment problems.

Formalizing it. The result is proved on paper; no machine-checked version is known to exist. A formal proof requires the full combinatorial argument behind the reduction, including the counting of machines per type and the case where some element of $A$ lies in no triple, which the paper does not discuss. Together with mission 1 of this series (the factor-2 algorithm), it fixes both ends of the $[3/2, 2]$ gap in one formal library.

Difficulty

The construction is short, but the converse direction carries the weight: from an arbitrary schedule with makespan at most $2$ one must recover a matching, although nothing in the schedule singles out the triples that form it. The obvious first idea, to read the matching off the machines that receive unit-time jobs, fails as it stands: a machine may receive one unit-time job or none, and the argument must exclude this for every schedule, including the degenerate instances in which some $a_j$ lies in no triple or triples repeat. For Corollary 2, the passage from the real-valued approximation guarantee to the threshold $2$ depends on the strict inequality $\rho < 3/2$; at $\rho = 3/2$ the statement is no longer implied by Theorem 5.

Formalization scope

• Machines are Fin m; 3DM elements are Fin n; a 3DM instance is T : Fin m → Fin n × Fin n × Fin n, so a triple may repeat. A matching is a set of $n$ triple indices covering every $a_j$, $b_k$, $c_l$ (the covering form of the paper's definition, which forces disjointness).
• The jobs of the reduced instance are the sum type $\mathrm{Fin}\,n \oplus \mathrm{Fin}\,n \oplus \Sigma_j\,\mathrm{Fin}(t_j - 1)$. They are enumerated by a fixed bijection with $\mathrm{Fin}\,N$ so that the published MatousekLP.Scheduling.makespan applies. All statements quantify over every schedule, so the choice of bijection is irrelevant.
• $t_j - 1$ is natural-number subtraction. When some $t_j = 0$ (a case the paper leaves aside), type $j$ has no dummy job; the reduced instance then has neither a matching nor a schedule of makespan at most $2$, so Theorem 5 and Corollary 2 hold as stated, with no hypothesis $t_j \ge 1$. Only the dummy-count milestone assumes $t_j \ge 1$.
• Processing times are natural numbers cast to $\mathbb R$; makespans are real.
• Not formalized: "polynomial" (running time of an algorithm and of the reduction), membership in NP, "NP-complete" and "unless $P = NP$". Theorem 5 is stated as the reduction's equivalence; Corollary 2 is stated as the fact that any $\rho$-approximate schedule of the reduced instance, $\rho < 3/2$, decides 3-dimensional matching. The reduction is evidently polynomial, but this is not stated.
• The approximation hypothesis compares $\sigma$ with every schedule $\tau$ of the same reduced instance; a goal in which $\sigma$ is an arbitrary schedule, or is bounded against an unrelated quantity, would be a different statement. The strict inequality $\rho < 3/2$ is essential and kept.
• Contributions welcome: proofs of the three milestones, of Theorem 5 from them, and of Corollary 2; reusable lemmas about integer-valued makespans and about sum-type job sets.

Selected references

• J. K. Lenstra, D. B. Shmoys, É. Tardos, Approximation algorithms for scheduling unrelated parallel machines, CWI Report OS-R8714, Centre for Mathematics and Computer Science, Amsterdam, 1987 (FOCS 1987); the version cited for every theorem number in this mission.
• J. K. Lenstra, D. B. Shmoys, É. Tardos, Approximation algorithms for scheduling unrelated parallel machines, Mathematical Programming 46 (1990) 259–271. https://doi.org/10.1007/BF01585745
• R. L. Graham, E. L. Lawler, J. K. Lenstra, A. H. G. Rinnooy Kan, Optimization and approximation in deterministic sequencing and scheduling: a survey, Annals of Discrete Mathematics 5 (1979) 287–326. https://doi.org/10.1016/S0167-5060(08)70356-X
• M. R. Garey, D. S. Johnson, Computers and Intractability: A Guide to the Theory of NP-Completeness, Freeman, 1979 (3-dimensional matching, problem [SP1]).
• P. Schuurman, G. J. Woeginger, Polynomial time approximation algorithms for machine scheduling: ten open problems, Journal of Scheduling 2 (1999) 203–213. https://doi.org/10.1002/(SICI)1099-1425(199909/10)2:5<203::AID-JOS26>3.0.CO;2-5
• D. P. Williamson, D. B. Shmoys, The Design of Approximation Algorithms, Cambridge University Press, 2011. https://doi.org/10.1017/CBO9780511921735

Motivation

Minimum makespan scheduling on unrelated parallel machines asks for an assignment of $n$ jobs to $m$ machines, where job $j$ takes $p_{ij}$ time units on machine $i$, so that the largest machine load is as small as possible. In the three-field notation of Graham, Lawler, Lenstra and Rinnooy Kan (1979) it is $R\,\|\,C_{\max}$. It models load balancing across heterogeneous processors, workers or production lines, and it is a standard test case for linear-programming rounding.

Lenstra, Shmoys and Tardos (FOCS 1987; CWI Report OS-R8714; Mathematical Programming 46, 1990) gave a polynomial 2-approximation algorithm for $R\,\|\,C_{\max}$ and showed that no polynomial algorithm achieves a ratio below $3/2$ unless P = NP. They also asked which restrictions on the processing times keep the problem hard. Their Section 5 answers this when only two distinct processing times occur:

• all $p_{ij}=1$: trivial;
• all $p_{ij}\in\{1,\infty\}$: bipartite cardinality matching;
• all $p_{ij}\in\{1,2\}$: polynomial by matching techniques (Theorem 6);
• all $p_{ij}\in\{p,q\}$ with $p<q$, $2p\ne q$: NP-hard (Theorem 7).

Theorem 7 is the paper's last result and closes this classification. Its proof generalizes the reduction of Theorem 4, which handles the case $\{1,3\}$, from 3-dimensional matching to $q$-dimensional matching.

Setting

Machines are indexed by $i\in\{1,\dots,m\}$ and jobs by $j$. A schedule $\sigma$ assigns every job to exactly one machine. The load of machine $i$ is $\sum_{j:\sigma(j)=i}p_{ij}$, and the makespan $C_{\max}(\sigma)$ is the largest load.

$q$-dimensional matching. An instance is a ground set $U$ of $qn$ elements and a family $S_1,\dots,S_m$ of $q$-element subsets of $U$. A matching is a subfamily $F'\subseteq\{1,\dots,m\}$ with $|F'|=n$ and $\bigcup_{i\in F'}S_i=U$; its members are then pairwise disjoint.

The instance of Theorem 7. Fix natural numbers $0<p<q$ that are relatively prime. Build a scheduling instance with $m$ machines, machine $i$ corresponding to $S_i$, and two kinds of jobs:

• $qn$ element jobs, one per $u\in U$, with $p_{iu}=p$ if $u\in S_i$ and $p_{iu}=q$ otherwise;
• $p(m-n)$ dummy jobs, each taking $q$ time units on every machine.

Every processing time lies in $\{p,q\}$.

The instance of Theorem 4. For disjoint sets $A=\{a_1,\dots,a_n\}$, $B$, $C$ of the same size and triples $T_i=(a_j,b_k,c_l)$, $i=1,\dots,m$, there are $3n$ element jobs, one per element of $A\cup B\cup C$, and $m-n$ dummy jobs. Machine $i$ processes the element jobs of $a_j$, $b_k$, $c_l$ in one time unit and every other job in three time units. A 3-dimensional matching is a subfamily of $n$ triples covering $A\cup B\cup C$.

Formalization targets

Goal: Theorem 7 (p. 8; proof pp. 8–9)

For relatively prime $0<p<q$ and a family of $q$-subsets $S_1,\dots,S_m$ of a $qn$-element set, the instance above has all processing times in $\{p,q\}$, and

$$\exists\,\sigma:\ C_{\max}(\sigma)\le pq \quad\Longleftrightarrow\quad \exists\,F'\subseteq\{1,\dots,m\}:\ |F'|=n,\ \bigcup_{i\in F'}S_i=U .$$

Milestones

1. Theorem 4 (p. 7): on the 3-dimensional matching instance with times in $\{1,3\}$, a schedule with makespan at most $3$ exists iff a matching exists.
2. Matching gives a schedule (pp. 8–9): if $S$ has a matching, some schedule has $C_{\max}\le pq$.
3. No idle time, two kinds of machine (p. 9): in every schedule with $C_{\max}\le pq$, three things hold. Every load equals $pq$. Every element job runs at length $p$, on a machine whose tuple contains it. Each machine processes either exactly $q$ element jobs and no dummy job, or exactly $p$ dummy jobs and no element job.

Significance

The result. Theorems 6 and 7 together say exactly which two-valued restrictions of $R\,\|\,C_{\max}$ are tractable. Up to scaling, the polynomial case is $\{1,2\}$, and every other pair $\{p,q\}$ with $p<q$ is NP-hard. Theorem 4 is the base case. It also yields Corollary 1 of the paper: no polynomial $\rho$-approximation with $\rho<4/3$ exists unless P = NP. Reductions of this "no idle time" kind are a standard template for hardness of restricted-assignment and two-value scheduling, a line still active in the study of the restricted assignment problem and of the "graph balancing" special case.

Formalizing it. The result is proved, in two short paragraphs. The proof leaves to the reader the construction of the schedule from a matching and the "easy number theoretic argument" behind the converse, and both become explicit here. The development also produces reusable pieces: a $q$-dimensional matching definition over an arbitrary family of $q$-sets, and two reduction instances built on the published load and makespan of MatousekLP.Scheduling.Schedule. To our knowledge no machine-checked proof of these reductions exists.

Difficulty

The forward direction is a direct construction. The converse is where care is needed. A schedule with makespan at most $pq$ may a priori place an element job on a machine whose tuple does not contain it, at length $q$, and may mix element and dummy jobs on one machine. Looking at one machine at a time does not exclude either: a single machine can carry such a mixed load below $pq$. What excludes them is a property of the whole schedule together with the arithmetic of $p$ and $q$. The hypotheses are sharp for this step: for $p>q$ element jobs are cheaper on foreign machines, and for $\gcd(p,q)>1$ a load $ap+bq=pq$ with $a,b>0$ becomes possible.

Formalization scope

• Model. Machines are Fin m. Schedules are maps from jobs to machines. Load and makespan are those of the published MatousekLP.Scheduling.Schedule, with natural-number processing times cast to $\mathbb R$. The jobs are enumerated as Fin (q * n + p * (m - n)) (Theorem 7) and Fin (3 * n + (m - n)) (Theorem 4), element jobs first, through finSumFinEquiv.
• Ground set and family. The ground set is Fin (q * n) and the family is indexed by machines, so repeated tuples are allowed. The $q$-partite structure of $q$-dimensional matching is not imposed: the reduction does not use it, and statements over all families of $q$-sets contain the $q$-partite case. Theorem 4 keeps the tripartite structure, with triples of indices in Fin n × Fin n × Fin n.
• Threshold. The thresholds are exactly $pq$ and $3$, with "makespan at most".
• Complexity wording not formalized. "NP-hard" (Theorem 7) and "NP-complete" (Theorem 4) are not formalized: membership in NP, polynomial size of the reductions, and the hardness of the matching problems are not stated. What is stated is the equivalence each reduction establishes.
• Hypotheses. Theorem 7's goal assumes $0<p<q$, $\gcd(p,q)=1$ and $|S_i|=q$. The paper's general case $\gcd(p,q)=g>1$ is its stated "without loss of generality": divide all times by $g$, which divides every makespan by $g$. It is not part of the formal statement. The paper's hypothesis $2p\ne q$ is dropped because the reduction does not use it. With coprime $p<q$ it excludes only $(p,q)=(1,2)$, where the equivalence still holds but the source problem is bipartite matching. The formal goal is therefore stronger than the paper's.
• Edge cases. For $m<n$, natural-number subtraction gives no dummy jobs; both sides of each equivalence are false when $n\ge1$. This stands in for the paper's "trivial 'no' instance". For $n=0$ the empty family is a matching and the dummy jobs fill the machines exactly.
• No trivialization. The goal is an equivalence about a constructed instance whose processing times are given by explicit definitions. Neither side is assumed, the schedule is quantified over all maps from jobs to machines, and the instance is not a free parameter pinned by hypotheses.
• Welcome contributions. Besides the milestones: counting lemmas relating a machine's load to the numbers of jobs of each length on it, and lemmas on the makespan of MatousekLP.Scheduling.Schedule (it bounds every load; it is attained when $m\ge1$), which are reusable across scheduling reductions.

Selected references

• J. K. Lenstra, D. B. Shmoys, É. Tardos, Approximation algorithms for scheduling unrelated parallel machines, CWI Report OS-R8714, Amsterdam, 1987 (the version formalized here); journal version in Mathematical Programming 46 (1990) 259–271. https://doi.org/10.1007/BF01585745
• M. R. Garey, D. S. Johnson, Computers and Intractability: A Guide to the Theory of NP-Completeness, Freeman, 1979 (3-dimensional matching, problem SP1).
• R. L. Graham, E. L. Lawler, J. K. Lenstra, A. H. G. Rinnooy Kan, Optimization and approximation in deterministic sequencing and scheduling: a survey, Annals of Discrete Mathematics 5 (1979) 287–326. https://doi.org/10.1016/S0167-5060(08)70356-X
• J. Matoušek, B. Gärtner, Understanding and Using Linear Programming, Springer, 2007, §8.3 (the schedule, load and makespan definitions reused here). https://doi.org/10.1007/978-3-540-30717-4

Motivation

A retailer or an airline chooses which products to offer, and customers choose among what is offered, or buy nothing. Choosing the offer set that maximizes expected revenue is the assortment problem, central to revenue management (Talluri and van Ryzin, 2004). It is NP-hard even for simple mixtures of logit models, so practice relies on heuristics. The most common one is the revenue-ordered assortments strategy: offer the products whose price is above a threshold, and pick the best threshold.

Berbeglia and Joret (arXiv:1606.01371) analyse this heuristic under every regular choice model, the broad class in which enlarging the offer set never raises the probability of choosing any given alternative, including not buying. They prove three approximation guarantees, then show that none of the three can be improved. This mission formalizes that last result, Theorem 3.4.

Timeline:

• Talluri and van Ryzin (2004) showed that revenue-ordered assortments are optimal under the multinomial logit model.
• Rusmevichientong, Shmoys, Tong and Topaloglu (2014) showed the problem NP-hard under a mixture of two logit models, and proved that revenue-ordered assortments earn at least $\mathrm{OPT}/(e(1+\ln(r_k/r_1)))$ under mixed logit.
• Aouad, Farias, Levi and Segev (2018) proved an $\Omega(1/\ln(r_k/r_1))$ guarantee under random utility models, and that the assortment problem there is NP-hard to approximate within $\Omega(1/n^{1-\epsilon})$ and $\Omega(1/\log^{1-\epsilon}(r_k/r_1))$.
• Berbeglia and Joret (2016–2020, Algorithmica) proved the guarantees $1/k$, $1/\sum_{i}(r_i-r_{i-1})/r_i\ge1/(1+\ln(r_k/r_1))$ and a purchase-probability bound under any regular model, and an instance on which all three, in their sum forms, are attained in the limit.

Setting

The products form a finite set $\mathcal C$. A system of choice probabilities gives, for every offer set $S\subseteq\mathcal C$ and product $x$, the probability $\mathcal P(x,S)$ that a customer buys $x$. The no-purchase probability is $\mathcal P(0,S)=1-\sum_{x\in S}\mathcal P(x,S)$. The model is regular if

1. $\mathcal P(x,S)\ge0$ for $x\in\mathcal C\cup\{0\}$;
2. $\mathcal P(x,S)=0$ for $x\notin S$;
3. $\sum_{x\in S}\mathcal P(x,S)\le1$;
4. $\mathcal P(x,S)\ge\mathcal P(x,S')$ for $S\subseteq S'$ and every $x\in S\cup\{0\}$.

Each product has a revenue $r(x)>0$. Offering $S$ earns $\mathrm{rev}(S)=\sum_{x\in S}\mathcal P(x,S)\,r(x)$, and $\mathrm{OPT}=\max_{S\subseteq\mathcal C}\mathrm{rev}(S)$.

Let $r_1<\dots<r_k$ be the distinct revenues, with $r_0:=0$, and $S_i=\{x: r(x)\ge r_i\}$. The heuristic earns

$$\mathrm{RO}=\max_{i\in[k]}\mathrm{rev}(S_i).$$

For an optimal $S^*$ let $N_i=\sum_{x\in S^*,\,r(x)\ge r_i}\mathcal P(x,S^*)$, $N_{k+1}=0$, and $\ell$ the largest index with $N_\ell>0$. Section 3 of the paper proves

• (A) $\mathrm{OPT}\le k\cdot\mathrm{RO}$ (Theorem 3.1);
• (B) $\mathrm{OPT}\le D_r\cdot\mathrm{RO}$, with $D_r=\sum_{i=1}^{k}\frac{r_i-r_{i-1}}{r_i}\le 1+\ln(r_k/r_1)$ (Theorem 3.2);
• (C) $\mathrm{OPT}\le D_N(S^*)\cdot\mathrm{RO}$, with $D_N(S^*)=\sum_{i=1}^{\ell}\frac{N_i-N_{i+1}}{N_i}\le 1+\ln(N_1/N_\ell)$ (Theorem 3.3).

Formalization targets

Goal: Theorem 3.4

For every $k\ge1$ and every $\delta>0$ there are a finite nonempty product set, a regular $\mathcal P$, revenues $r>0$ with exactly $k$ distinct values, and an optimal $S^*$ with $N_1>0$, such that

$$k\cdot\mathrm{RO}<(1+\delta)\,\mathrm{OPT},\qquad D_r\cdot\mathrm{RO}<(1+\delta)\,\mathrm{OPT},\qquad D_N(S^*)\cdot\mathrm{RO}<(1+\delta)\,\mathrm{OPT}.$$

So none of the bounds (A), (B), (C) stays true when multiplied by $1+\delta$, for any number $k$ of distinct revenues.

The tight instance (milestones)

The paper's witness has products $(i,j)$ with $i\in[k]$ and $j\in[i]$. Product $(i,j)$ has revenue $\varepsilon^{-j}$, and $\mathcal P((i,j),S)=\varepsilon^i$ when $(i,j)\in S$ and $(i,1),\dots,(i,j-1)\notin S$, and $0$ otherwise, for $0<\varepsilon\le\tfrac12$. The milestones follow the proof on pp. 10–11:

• the axiom (iii) bound;
• (7);
• (8);
• (9);
• regularity;
• the distinct revenues $r_i=\varepsilon^{-i}$;
• $\mathrm{RO}=\mathrm{rev}(\mathcal C)<1/(1-\varepsilon)$;
• $\mathrm{OPT}=k$, attained by $\{(i,i)\}$;
• the limits $\mathrm{OPT}/\mathrm{RO}\to k$ and $D_r\to k$;
• $N_i=\varepsilon^i+\dots+\varepsilon^k$ and $D_N\to k$ as $\varepsilon\to0^+$.

Significance

With Theorems 3.1–3.3, Theorem 3.4 closes the analysis: in terms of the parameters $k$, $D_r$ and $D_N$, revenue-ordered assortments are understood exactly under regular choice. It complements the hardness results of Aouad et al., which already show that no efficient strategy can do much better than (A) and (B) in general; Theorem 3.4 shows that the analysis of this particular heuristic is exact. The instance is also a concrete regular choice model in which the optimal offer set is far from every nested one.

On the formal side, the mission produces a reusable formal definition of regular discrete choice models, revenue-ordered assortments and the three bound quantities. These are shared, under other sub-namespaces, with the companion missions on Theorems 3.2 and 3.3. The result is proved in the paper. As far as is known it has not been machine-checked anywhere; the remaining work is formalizing the paper's proof, including the steps it leaves to the reader.

Difficulty

The proof is a construction, and the paper verifies most of it in a sentence each. The work lies in those sentences:

• the regularity of the instance at the no-purchase option, (9), which needs the row decomposition (8);
• the claim that $\{(i,i)\}$ is optimal among all $2^{k(k+1)/2}$ offer sets, asserted without proof;
• the claim that the full set is the best threshold set;
• the evaluation of $D_N(S^*)$, which needs $\ell=k$.

The naive witness, one instance per bound, does not help: the goal asks for one instance with exactly $k$ revenues on which all three bounds are nearly attained, for every $k$.

Formalization scope

• Products are an arbitrary finite type C. The no-purchase option is not a product: $\mathcal P(0,S)$ is the derived quantity noPurchase P S. Offer sets are Finset C.
• IsRegular carries axioms (i)–(iv), with (i) and (iv) stated both for products and for the no-purchase option. Regularity at $x=0$ is essential: without it the guarantees fail.
• $\mathrm{OPT}$ is Finset.sup' over all subsets, including $\emptyset$. $\mathrm{RO}$ is Finset.sup' over the $k$ threshold sets only, and needs Nonempty C.
• The distinct revenues are the sorted image of r, indexed by Fin k from $0$: the Lean index $i$ is the paper's $i+1$, and $r_0=0$ is a separate case. $\ell$ lives in WithBot (Fin k).
• Bounds are multiplicative ($\mathrm{OPT}\le D\cdot\mathrm{RO}$); there is no ratio $\mathrm{RO}/\mathrm{OPT}$ in the goal. Limits are along 𝓝[>] 0.
• The tight instance keeps the paper's 1-based pairs $(i,j)$ as a subtype of Fin (k+1) × Fin (k+1). Its regularity is a theorem to prove, never a field assumed.

Ruled out:

• a fixed $k$, since "for every $k$" is the content;
• tightness of the logarithmic forms $1/(1+\ln(r_k/r_1))$ and $1/(1+\ln\nu)$, which this instance does not show (there $1+\ln(r_k/r_1)\to\infty$ while $\mathrm{OPT}/\mathrm{RO}\to k$), so only the sum forms are claimed tight;
• an instance whose regularity is assumed;
• a heuristic maximizing over all subsets.

Contributions welcome: proofs of the milestones, especially (8), (9) and the optimality of $\{(i,i)\}$, and general lemmas on sorted distinct values of a finite function.

Selected references

• G. Berbeglia and G. Joret, Assortment Optimisation Under a General Discrete Choice Model: A Tight Analysis of Revenue-Ordered Assortments, arXiv:1606.01371v3, 2019; published in Algorithmica, 2020. https://arxiv.org/abs/1606.01371
• K. Talluri and G. van Ryzin, Revenue Management Under a General Discrete Choice Model of Consumer Behavior, Management Science 50(1), 2004. https://doi.org/10.1287/mnsc.1030.0147
• P. Rusmevichientong, D. Shmoys, C. Tong and H. Topaloglu, Assortment Optimization under the Multinomial Logit Model with Random Choice Parameters, Production and Operations Management 23(11), 2014. https://doi.org/10.1111/poms.12191
• A. Aouad, V. Farias, R. Levi and D. Segev, The Approximability of Assortment Optimization Under Ranking Preferences, Operations Research 66(6), 2018. https://doi.org/10.1287/opre.2018.1724

Motivation

A retailer that can display only some of its products must choose an assortment: the set of products offered to an arriving customer. Customers substitute: whether a given product is bought depends on what else is on the shelf. The assortment problem asks for the offer set that maximises expected revenue under a model of this substitution behaviour. It is a core problem of revenue management (Talluri and van Ryzin, Management Science 2004), and it is NP-hard already for a mixture of two multinomial logit models (Rusmevichientong, Shmoys, Tong and Topaloglu, POMS 2014).

The heuristic used most widely in practice is revenue-ordered assortments: sort the products by price and offer, for some threshold, every product priced at least that threshold. It is optimal under the multinomial logit model (Talluri and van Ryzin 2004) but not in general. Berbeglia and Joret (arXiv:1606.01371v3, 2019; Algorithmica 2020) give a tight analysis of its approximation ratio for every regular discrete choice model, a class that includes all random utility models. They prove three incomparable guarantees. This mission formalizes the third, Theorem 3.3, whose ratio depends on the purchase behaviour of an optimal assortment rather than on the prices. Companion missions in this series cover the price-ratio bound (Theorem 3.2) and the tightness of all three bounds (Theorem 3.4).

Setting

Let $\mathcal C$ be a finite nonempty set of products. A system of choice probabilities gives, for every offer set $S\subseteq\mathcal C$ and product $x$, the probability $\mathcal P(x,S)$ that a customer offered $S$ buys $x$. Buying nothing is the option $0$, with $\mathcal P(0,S)=1-\sum_{x\in S}\mathcal P(x,S)$. The model is regular when

1. $\mathcal P(x,S)\ge0$ for products and for $x=0$;
2. $\mathcal P(x,S)=0$ for $x\notin S$;
3. $\sum_{x\in S}\mathcal P(x,S)\le1$;
4. $\mathcal P(x,S)\ge\mathcal P(x,S')$ whenever $S\subseteq S'$ and $x\in S\cup\{0\}$.

Axiom 4 at $x=0$ says that enlarging the offer set never makes buying nothing more likely.

Prices are a function $r:\mathcal C\to\mathbb R_{>0}$. Offering $S$ earns $\mathrm{rev}(S)=\sum_{x\in S}\mathcal P(x,S)\,r(x)$, and $\mathrm{OPT}=\max_{S\subseteq\mathcal C}\mathrm{rev}(S)$. Let $r_1<\dots<r_k$ be the distinct values of $r$, and let $S_i=\{x:r(x)\ge r_i\}$ for $i\in[k]$. The revenue-ordered strategy earns

$$\mathrm{RO}=\max_{1\le i\le k}\mathrm{rev}(S_i).$$

For an assortment $S^*$, the purchase profile is

$$N_i=\sum_{x\in S^*,\ r(x)\ge r_i}\mathcal P(x,S^*)\qquad(i\in[k]),\qquad N_{k+1}:=0,$$

the probability that a customer offered $S^*$ buys something priced at least $r_i$. It is non-increasing in $i$.

Formalization targets

Goal: Theorem 3.3 (p. 9)

Let $S^*$ be optimal, $\mathrm{rev}(S^*)=\mathrm{OPT}$, suppose $N_1>0$, and let $\ell\in[k]$ be maximum with $N_\ell>0$. Then

$$\mathrm{OPT}\le\Big(\sum_{i=1}^{\ell}\frac{N_i-N_{i+1}}{N_i}\Big)\mathrm{RO} \qquad\text{and}\qquad \sum_{i=1}^{\ell}\frac{N_i-N_{i+1}}{N_i}\le1+\ln\nu,\quad\nu=\frac{N_1}{N_\ell}.$$

The first inequality is the paper's sum-form factor, the bound that Theorem 3.4 shows to be tight. The second is the closed form $1/(1+\ln\nu)$.

Milestones (in proof order)

• Lemma 2.1 (p. 6): $\sum_{x\in S}\mathcal P(x,S)\le\sum_{x\in S'}\mathcal P(x,S')$ for $S\subseteq S'$.
• First observation of the proof (p. 9): $N_i\le\sum_{x\in S_i}\mathcal P(x,S_i)$ and $N_ir_i\le\sum_{x\in S_i}\mathcal P(x,S_i)r_i$.
• Inequality (6) (p. 9): $N_ir_i\le\mathrm{RO}$ for every $i\in[k]$.
• Revenue identity (p. 9): $\mathrm{rev}(S^*)=\sum_{i=1}^{\ell}(N_i-N_{i+1})r_i=\sum_{i=1}^{\ell}\frac{N_i-N_{i+1}}{N_i}N_ir_i$.
• Logarithmic step (p. 9, the comparison $1/\sum\ge1/(1+\ln\nu)$ in Theorem 3.3, used in the last inequality of the proof): for $N_1\ge\dots\ge N_\ell>0$ and $N_{\ell+1}=0$, $\sum_{i=1}^{\ell}(N_i-N_{i+1})/N_i\le1+\ln(N_1/N_\ell)$. The paper states this step without proof.

Significance

Theorem 3.3 gives a guarantee that is independent of prices. The bound $1+\ln(r_k/r_1)$ of Theorem 3.2 grows when prices are spread out. The bound $1+\ln\nu$ is small whenever an optimal assortment sells its expensive products with probability comparable to its overall purchase probability. In §4 the paper combines it with a reduction from unit-demand pricing to derive, for example, the $1/(1+\ln m)$ guarantee of uniform pricing for the unit-demand min-pricing problem (Corollary 4.8, originally due to Aggarwal et al.). Together with Theorems 3.1 and 3.2, it describes the performance of the most common assortment heuristic over the whole class of regular models, with no parametric assumption on customer behaviour.

The theorem is proved on paper. To our knowledge it has no machine-checked proof, and no regular choice model has been formalized on the platform. This mission produces the regular model as a reusable definition, a statement of Theorem 3.3 in which every hypothesis is explicit, and formal versions of the proof's identities and inequalities. The logarithmic step is asserted without proof in the source, so a formal proof of it completes the paper's argument.

Difficulty

Each step is elementary. The difficulty is bookkeeping. The revenue of $S^*$ has to be regrouped by distinct price levels rather than by products: several products may share a price, and $k$ counts values. The regrouping uses an Abel-type rearrangement with the boundary convention $N_{k+1}=0$. Comparing $N_i$ with the purchase probability of $S_i$ needs regularity twice. First, axiom 4 for products passes from $S^*$ to $S^*\cap S_i$. Then the no-purchase case passes from $S^*\cap S_i$ to $S_i$. A proof that uses axiom 4 only for products fails at the second step, and the claim is false without it.

Formalization scope

• Products form a finite type C with [Fintype C] [DecidableEq C]. The goal adds [Nonempty C], the paper's $k\ge1$. Offer sets are Finset C, and $\mathcal P$ is P : C → Finset C → ℝ. The no-purchase option is not a product: $\mathcal P(0,S)$ is the derived quantity noPurchase P S. IsRegular P carries axioms 1–4, including both no-purchase cases.
• $\mathrm{OPT}$ is Finset.sup' over all subsets. $\mathrm{RO}$ is Finset.sup' over the indices $1,\dots,k$ of the threshold sets only.
• Indices are 1-based natural numbers. level r i is $r_i$ for $1\le i\le k$. purchaseProfile P r S i is $N_i$ for $1\le i\le k$ and $0$ otherwise, which builds in $N_{k+1}=0$.
• Optimality is the hypothesis $\mathrm{rev}(S^*)=\mathrm{OPT}$. The index $\ell$ is a variable with hypotheses $1\le\ell\le k$, $N_\ell>0$, and $N_i\not>0$ for $\ell<i\le k$. $N_1>0$ is kept as in the paper.
• The approximation factor is stated in product form, $\mathrm{OPT}\le D\cdot\mathrm{RO}$, never as a ratio. Both the sum form and the logarithmic form are stated. $\ln$ is Real.log, applied to $\nu\ge1$.
• The milestones other than the goal are stated for an arbitrary $S^*$, because the proof does not use optimality there.

The following statements are trivial or false and are not this mission: a maximum over all subsets in place of $\mathrm{RO}$; regularity without its no-purchase case; a purchase profile taken from a non-optimal set while $\mathrm{rev}(S^*)$ is still called the optimum; the logarithmic form alone; a specific choice model (MNL, Markov chain) in place of an arbitrary regular $\mathcal P$.

A complete development needs finite sums regrouped by the values of a function and an elementary logarithm inequality. The regular choice model and the revenue-ordered sets are shared with the other missions of this series and are reusable for any analysis of assortment heuristics. Proofs of any milestone are welcome. So are alternative arguments for the logarithmic step and a proof that $N$ is non-increasing.

Selected references

• G. Berbeglia and G. Joret, Assortment Optimisation Under a General Discrete Choice Model: A Tight Analysis of Revenue-Ordered Assortments, arXiv:1606.01371v3, 2019; Algorithmica 82, 2020. https://arxiv.org/abs/1606.01371v3
• K. Talluri and G. van Ryzin, Revenue Management Under a General Discrete Choice Model of Consumer Behavior, Management Science 50(1), 2004. https://doi.org/10.1287/mnsc.1030.0147
• P. Rusmevichientong, D. Shmoys, C. Tong and H. Topaloglu, Assortment Optimization under the Multinomial Logit Model with Random Choice Parameters, Production and Operations Management 23(11), 2014. https://doi.org/10.1111/poms.12191

Motivation

Consensus asks $N$ processors, each holding an initial value, to agree on one value despite some of them failing. It underlies replicated databases, atomic commit and state-machine replication. Its solvability depends on the timing assumptions. With fully synchronous processors and communication, $t$ fail-stop faults can be tolerated for any $t < N$. With fully asynchronous communication, Fischer, Lynch and Paterson showed that no deterministic protocol tolerates even one fail-stop fault (JACM 1985).

Dwork, Lynch and Stockmeyer (JACM 1988) introduced partial synchrony, a model between these two extremes. Message delays have an upper bound $\Delta$, but either the bound is unknown to the protocol, or it holds only from an unknown time on. For each fault type they found the exact number of faults that can be tolerated. This mission formalizes the lower bound for fail-stop faults: when the processors are synchronous and communication is partially synchronous, no consensus protocol tolerates $t$ faults once $N \le 2t$.

Timeline. 1985: Fischer, Lynch, Paterson, impossibility of consensus with one fail-stop fault under asynchrony. 1987: Dolev, Dwork, Stockmeyer, which combinations of synchrony assumptions admit consensus (JACM 1987). 1988: Dwork, Lynch, Stockmeyer, partial synchrony, with matching upper and lower bounds on resiliency for fail-stop, omission, authenticated Byzantine and Byzantine faults. The global stabilization time of the 1988 paper became a common liveness assumption for later fault-tolerant agreement protocols.

Setting

There are $N$ processors $p_1, \dots, p_N$. Each processor holds an initial value $v_i \in \{0, 1\}$. Each runs a deterministic protocol: a transition diagram over a possibly infinite set of states. In each state the next instruction is either $\mathrm{Send}(m, p_j)$, which puts message $m$ in $p_j$'s buffer, or $\mathrm{Receive}(p_i)$, which removes a set $S$ of messages from $p_i$'s buffer and delivers it. The next state depends on the current state and, for a Receive, on $S$. A step never both sends and receives. Each state may record a decision, and the first decision a processor records is final.

Real time is the ticks $1, 2, 3, \dots$. A run fixes the initial values and, at each tick, which processors take a step and which messages each Receive delivers. A message is delivered only after the tick at which it was sent, only to its addressee, and at most once.

• Synchronous processors ($\Phi = 1$): every correct processor takes a step at every tick.
• Fail-stop faults: a faulty processor follows the protocol until it stops, and it never restarts. A processor that stops at time $0$ is initially dead.
• $\Delta$ holds in $[T, \infty)$: a message sent at a tick $s_1 \ge T$ is delivered no later than any Receive of its addressee at a tick $s_2 \ge s_1 + \Delta$.
• Delta holds eventually: $\Delta$ is a fixed positive integer known to the protocol. In every run, $\Delta$ holds in $[T, \infty)$ for some unknown global stabilization time $T$. Messages sent before $T$ may be delayed arbitrarily or lost.
• Delta is unknown: the protocol is fixed first. In every run, some positive $\Delta$ holds in $[1, \infty)$.

A protocol is a $t$-resilient consensus protocol achieving weak unanimity if the following holds for every set $C$ of at least $N - t$ processors and every allowed run in which the processors of $C$ are correct and the others fail-stop. No two processors of $C$ decide differently (consistency). Every processor of $C$ decides (termination). If all initial values are $v$ and no processor is faulty, every decision is $v$ (weak unanimity).

Formalization targets

Goal: Theorem 4.3

For integers $t \le N$ with

$$2 \le N \le 2t,$$

there is no $t$-resilient consensus protocol achieving weak unanimity for binary values with fail-stop faults and synchronous processors. This holds for every positive $\Delta$ when $\Delta$ holds eventually, and when delta is unknown.

Milestones: the three scenarios of the proof

Split the processors into groups $P$ and $Q$ with $1 \le |P|, |Q| \le t$.

• Scenario A: all inputs $0$ and $Q$ initially dead. The processors of $P$ decide by some time $T_A$, and they decide $0$.
• Scenario B: all inputs $1$ and $P$ initially dead. The processors of $Q$ decide $1$ by some time $T_B$.
• Scenario C: all processors alive, $P$ starting with $0$ and $Q$ with $1$, and messages between the groups held back past a time $T$. Up to time $T$, every processor of $P$ is in the same state as in Scenario A, and every processor of $Q$ in the same state as in Scenario B.

Significance

The result. Theorem 4.3 shows that the resiliency $N \ge 2t + 1$ of the paper's fail-stop and omission protocols (Theorems 4.1 and 4.2) is optimal. It holds even under three restrictions: binary values, weak unanimity, and processors in perfect lock-step. Partial synchrony costs a majority of correct processors, whereas full synchrony costs nothing. The same scenarios give the authenticated Byzantine bound $N \ge 3t + 1$ (Theorem 4.4). The halting remark of Section 4.2 rests on an argument of the same kind.

The formalization. The theorem is proved in the paper, and its proof is short. It is not machine-checked anywhere known to the mission. No message-passing model is on the platform. This mission supplies one: a step-level model with buffers, per-message timing, fail-stop faults and both partially synchronous communication models. It also gives a machine-checked impossibility on top of that model. FLP, Theorem 4.4 and the lower bounds of Section 6 are natural follow-ups on the same definitions.

Difficulty

The informal proof is an indistinguishability argument. Making it formal means comparing different runs of the same deterministic protocol. Two points need care.

First, the scenarios must be allowed runs. Scenario C holds messages between the groups back past $\max(T_A, T_B)$. With delta unknown, this needs a $\Delta$ larger than that delay. When $\Delta$ holds eventually, $\Delta$ is fixed before the protocol, and the protocol fixes $T_A$ and $T_B$. So the delay is legal only for messages sent before the global stabilization time, which must therefore be placed after $\max(T_A, T_B)$. Read literally, "every message between the groups takes more than $\max(T_A, T_B)$ steps" is not an allowed run in this model.

Second, "the processors of $P$ act exactly as they do in Scenario A" is a claim about whole runs. Two runs must agree on states, on which messages are in which buffer, and on when each message is delivered, tick by tick up to $T$. With one-to-one sends and atomic steps, "delivered in exactly time 1" also needs a reading: a processor that sends at the next tick cannot receive at that tick.

Formalization scope

All declarations live in the namespace DLSConsensus.LowerBound. Processor $p_i$ is the index $i - 1$ of Fin N. Values are Bool. The protocol's state type and message type are arbitrary types in Type, finite or infinite. R.state i n is the state after tick $n$. A message instance is identified in the run by its sender and send tick. A Receive hands the protocol each delivered message as (sender, content); the absolute send tick is not exposed.

Explicit readings and conventions:

• "Fail-stop or omission faults": the goal is the fail-stop impossibility. It implies the omission case, because a fail-stop processor looks to the others like one whose sends are all omitted. The omission case is not a separate item.
• A fail-stop processor may skip ticks before its final stop. The processor timing bound $\Phi = 1$ applies to correct processors.
• "Decides": the first state that records a decision. Irreversibility therefore holds by definition.
• "Delivered in exactly time 1": the message is delivered no later than the addressee's first Receive at least one tick after the send.
• "Within time $T_A$" and "for some finite $T_B$": an explicit $\exists$ before the decision bound.
• "Messages between the groups take more than $\max(T_A, T_B)$ steps": no message between the groups is delivered at a tick $\le T$, for any given $T$.
• "Act exactly as they do": equal local states at every tick $n \le T$.
• Quantifier order: when $\Delta$ holds eventually, $\Delta$ is chosen first, then the protocol, then the run with its stabilization time. When delta is unknown, the protocol is chosen first and each run carries its own $\Delta$. In both models $\Delta > 0$.

Trivializing formalizations are ruled out. The model has allowed runs for every protocol, so Resilient is never vacuously true. Correct processors step at every tick, so termination does not fail for the wrong reason. Unanimity is the weak form, applied only when no processor is faulty.

Contributions welcome: a general simulation lemma (equal inputs up to a tick give equal states up to that tick), the construction of runs from a delivery schedule, and proofs of the scenarios. These parts are reusable for the other lower bounds of the paper.

Selected references

• C. Dwork, N. Lynch, L. Stockmeyer, Consensus in the presence of partial synchrony, Journal of the ACM 35(2), 1988, 288–323. https://doi.org/10.1145/42282.42283
• M. J. Fischer, N. A. Lynch, M. S. Paterson, Impossibility of distributed consensus with one faulty process, Journal of the ACM 32(2), 1985, 374–382. https://doi.org/10.1145/3149.214121
• D. Dolev, C. Dwork, L. Stockmeyer, On the minimal synchronism needed for distributed consensus, Journal of the ACM 34(1), 1987, 77–97. https://doi.org/10.1145/7531.7533