Prove that subset sum is NP-complete by reducing the existing 3-SAT language, to it. Given a list of positive integers and a nonnegative target, decide whether some selection of entries sums exactly to the target. Integers are encoded in binary.

References:

• Richard M. Karp. Reducibility Among Combinatorial Problems. Complexity of Computer Computations, 85–103, 1972. Binary encoding convention, p. 89; Main Theorem, problem 18, pp. 94–95; original Exact Cover reduction, p. 100.

Prove that $k$-SAT is NP-complete for every fixed $k\ge3$, with at most $k$ literal occurrences per clause.

Construct the reductions and certificate verifier using the existing WordRAM definitions. We reuse proved polynomial backend and Cook–Levin SAT completeness.

References:

• Richard M. Karp. Reducibility Among Combinatorial Problems. Complexity of Computer Computations, 85–103, 1972. Main Theorem, problem 11; reduction, p. 98.
• Stephen A. Cook and Robert A. Reckhow. Time Bounded Random Access Machines. Journal of Computer and System Sciences 7(4), 354–375, 1973.
• Torben Hagerup. Sorting and Searching on the Word RAM. STACS 1998, 366–398.

Motivation

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

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

Timeline:

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

Setting

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

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

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

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

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

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

Formalization targets

Goal: Theorem 13

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

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

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

Milestones

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

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

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

Significance

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

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

Difficulty

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

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

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

Formalization scope

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

Selected references

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

Motivation

In a shared-memory multiprocessor, each processor keeps copies of memory blocks in its own cache, and all caches listen ("snoop") on a common bus. Every bus cycle spent keeping these copies consistent is a cycle not available for useful work, so the protocol that decides when a block is shared by several caches and when it is private to one cache directly controls bus traffic. The decision has to be made on-line, without knowing which processor will touch the block next.

Karlin, Manasse, Rudolph and Sleator (Algorithmica 1988) introduced competitive analysis for this problem and gave a deterministic algorithm with competitive ratio $2$, which is optimal among deterministic algorithms. Karlin, Manasse, McGeoch and Owicki (Algorithmica 1994) showed that randomization helps: against an oblivious adversary the optimal ratio for block snoopy caching is $e_p/(e_p-1)$, where $p$ is the cost of transferring a block. The same paper develops a general method for "nonuniform" problems, in which some state transitions are much more expensive than others, and the snoopy-caching result is its first application.

Setting

Fix $n$ processors and one memory block $B$ holding $p-1$ variables; transferring $B$ over the bus costs $p$ bus cycles. The block is in one of $n+1$ states: shared between all caches, or private to the cache of processor $i$.

A request is a read $\mathrm{R}_i$ or a write $\mathrm{W}_i$ by processor $i$. Moving from a private state to any other state costs $p$; moving from the shared state is free. A read $\mathrm{R}_i$ costs $0$ if $B$ is shared or private to $i$ and $+\infty$ otherwise. A write $\mathrm{W}_i$ costs $0$ if $B$ is private to $i$, $1$ if $B$ is shared (one bus cycle broadcasts the new value), and $+\infty$ otherwise.

Before request $j$ the system is in state $s_{j-1}$. A read is a look-ahead-one request: the algorithm may change state at the moment of the request, after seeing it. A write is a look-ahead-zero request: it is served in whatever state the system is in. After either kind, the algorithm may move again. The cost of a request is the cost of the move to the serving state, plus the task cost there, plus the cost of the move afterwards. Every write is preceded by a read to the same block, so in an admissible sequence each write $\mathrm{W}_i$ directly follows $\mathrm{R}_i$ or $\mathrm{W}_i$.

The off-line optimum $C_{opt}(s_0,\sigma)$ is the least total cost of serving $\sigma$ from the initial state $s_0$ with full knowledge of $\sigma$. A randomized on-line algorithm $A$ is a probability distribution over deterministic on-line algorithms; its expected cost on $\sigma$ is $\mathbf{E}C_A(\sigma)$. $A$ is $c$-competitive against an oblivious adversary from $s_0$ if there is a constant $a$ with

$$\mathbf{E}C_A(\sigma)\le c\cdot C_{opt}(s_0,\sigma)+a$$

for every admissible $\sigma$. Put

$$e_p=\left(1+\frac1p\right)^p .$$

Formalization targets

Goal: Theorem 4

For $n\ge 2$, $p\ge 1$ and every initial state $s_0$:

$$\Big(\forall A\ \forall c:\ A \text{ is } c\text{-competitive from } s_0 \Rightarrow c\ge \tfrac{e_p}{e_p-1}\Big)\ \wedge\ \exists A:\ A \text{ is } \tfrac{e_p}{e_p-1}\text{-competitive from } s_0 .$$

The two conjuncts are milestones of their own: the lower bound (Theorem 4, first claim) and attainment (Theorem 4, second claim).

The phase linear program (§3.2, pp. 552–554)

For $p\ge1$, real $\pi_1,\dots,\pi_{p+1}$ with $\pi_{p+1}=1$, and real $\alpha$ with

$$\pi_{k+1}p+\sum_{i=1}^{k}(1-\pi_i)\le\alpha k\qquad(k=0,\dots,p),$$

one has $\alpha\ge e_p/(e_p-1)$. Conversely, at $\alpha=e_p/(e_p-1)$ the choice $\pi_k=(\alpha-1)\big(((p+1)/p)^{k-1}-1\big)$ satisfies $\pi_{p+1}=1$, $0\le\pi_1\le\dots\le\pi_{p+1}$, and makes every constraint an equality.

Significance

The theorem settles the randomized competitive ratio of block snoopy caching exactly: $2$ at $p=1$, $9/5$ at $p=2$, decreasing to $e/(e-1)\approx1.582$ as $p\to\infty$, against the deterministic optimum $2$. The same ratio $e/(e-1)$ is the randomized optimum for the continuous ski-rental and spin-block problems treated later in the paper, and the snoopy-caching case is its discrete counterpart with ratio $e_p/(e_p-1)$. The phase-LP method used here recurs in the paper's two-server results.

The result is proved in the paper; to our knowledge it has no machine-checked proof. This mission produces a formal model of the snoopy-caching task system with look-ahead-zero requests, of randomized algorithms against an oblivious adversary with infinite task costs allowed, and of the off-line optimum, together with the exact optimal ratio. The platform's fractional ski-rental result (PrimalDualOnline.SkiRental.fractional_competitive) proves an $e_B/(e_B-1)$ bound for a different model: one deterministic fractional algorithm, with no lower bound over randomized algorithms. It is related work, not a special case.

Difficulty

The linear program is elementary. The gap is between the LP and the algorithms. The paper's lower bound reduces arbitrary randomized algorithms to phase-based ones, whose state distribution at the end of each phase agrees with the optimal algorithm's known state, and whose behaviour inside a phase depends only on the number of writes so far. This reduction (Theorems 1 and 3 of the paper, pp. 545–549) is where the argument is not routine. An algorithm may keep the block private to a processor that is not the active one, may randomize over histories rather than over phase lengths, and the off-line optimum is not a sum of per-phase costs at the ends of the sequence. The obvious approach, bounding a single adversarial phase, does not suffice, because an algorithm may pay more in one phase and recover it in the next; the additive constant $a$ and the infinite horizon have to be handled. For attainment, the mixture of threshold algorithms must be written as a genuine distribution over on-line algorithms, with the initial phase from a private state absorbed into the additive constant.

Formalization scope

Everything lives in the namespace NonuniformCompetitive.Snoopy. States are Option (Fin n) (none = shared). Costs are in ℝ≥0∞; $+\infty$ is a genuine outcome, so an algorithm that ever pays $+\infty$ with positive probability on an admissible sequence is not competitive. A deterministic on-line algorithm is a pair of functions of the request prefix (the state at the moment of the last request, and the state after it), with the look-ahead-zero rule as a field. Moves "immediately before" a request are made without knowledge of it and are recorded as moves after the previous request. A randomized algorithm is a probability space with a measurable cost on every sequence, and its expected cost is a lower Lebesgue integral. The off-line optimum is an infimum in ℝ≥0∞ over schedules starting in $s_0$; it is finite on admissible sequences.

Conventions added to the printed statement, all from the paper's setting: (i) $n\ge2$, since with one processor the block can stay private for free; (ii) one block, since the proof of Theorem 4 splits a multi-block system into independent blocks (p. 551); (iii) admissibility in the form "each write of $i$ directly follows a read or write of $i$", the reading of "every write is preceded by a read to the same block" that the proof uses; without it every algorithm is defeated by a write from a processor whose block copy was invalidated; (iv) $p\in\mathbb{N}$, $p\ge1$; (v) both claims from every initial state, with an additive constant depending on $n$, $p$, $s_0$.

The lower bound is over all randomized algorithms, not over phase-based or deterministic ones; a statement restricted to phase-based algorithms, or the LP alone in place of the goal, would not be Theorem 4. The LP variables are free, as in the paper.

Welcome contributions: a formal version of the phase reduction (Theorems 1 and 3 of the paper) for this task system, which is reusable for the paper's other nonuniform problems; the threshold algorithms and their mixture; and a proof that the off-line optimum decomposes by write runs up to a bounded error.

Selected references

• A. R. Karlin, M. S. Manasse, L. A. McGeoch, S. Owicki, Competitive Randomized Algorithms for Nonuniform Problems, Algorithmica 11 (1994), 542–571. https://doi.org/10.1007/BF01189993
• A. R. Karlin, M. S. Manasse, L. Rudolph, D. D. Sleator, Competitive Snoopy Caching, Algorithmica 3 (1988), 79–119. https://doi.org/10.1007/BF01762111
• A. Borodin, R. El-Yaniv, Online Computation and Competitive Analysis, Cambridge University Press, 1998.

Motivation

Many equivalence problems on finite structures reduce to computing the coarsest partition of a finite set that is compatible with a relation. Deciding whether two states of a finite labelled transition system are bisimilar, testing congruence of finite-state processes in Milner's calculus of communicating systems (CCS), and minimizing a deterministic finite automaton are all instances. Kanellakis and Smolka studied the relational version in connection with CCS equivalence and gave an $O(mn)$-time algorithm, conjecturing that $O(m \log n)$ was possible. Paige and Tarjan's 1987 paper answers that conjecture with an algorithm that has since become the standard method for bisimulation minimization in model checkers and process-algebra tools.

Timeline:

• 1971 — Hopcroft gives an $O(n \log n)$ algorithm for minimizing deterministic finite automata, i.e. for the coarsest partition stable with respect to one or more functions, using the rule "process the smaller half".
• 1983/1990 — Kanellakis and Smolka give an $O(mn)$-time, $O(m + n)$-space algorithm for the relational problem, and $O(c^2 n \log n)$ when every element has at most $c$ successors; they conjecture an $O(m \log n)$ algorithm.
• 1987 — Paige and Tarjan combine Hopcroft's smaller-half strategy with refinement by unions of blocks and obtain $O(m \log n)$ time and $O(m + n)$ space for the relational problem.

Setting

Let $U$ be a finite set with $n = |U|$ elements and let $E \subseteq U \times U$ be a binary relation on $U$; write $xEy$ for $(x, y) \in E$ and $m = |E|$. For $S \subseteq U$ the preimage of $S$ is

$$E^{-1}(S) = \{x \in U \mid \exists y \in S,\ xEy\}.$$

A partition of $U$ is a family of nonempty, pairwise disjoint subsets of $U$, its blocks, whose union is $U$. A partition $R$ is a refinement of a partition $P$ if every block of $R$ lies inside a block of $P$.

A set $B \subseteq U$ is stable with respect to $S \subseteq U$ if $B \subseteq E^{-1}(S)$ or $B \cap E^{-1}(S) = \emptyset$: either every element of $B$ has an $E$-successor in $S$, or none does. A partition is stable with respect to $S$ if all its blocks are, and a partition is stable if it is stable with respect to each of its own blocks.

Given $E$ and an initial partition $P$, the coarsest stable refinement of $P$ is a stable partition $Q$ refining $P$ such that every stable partition refining $P$ is a refinement of $Q$. The relational coarsest partition problem asks for it.

The algorithms refine by the operation $\mathrm{split}(S, Q)$, which replaces each block $B$ of $Q$ that meets both $E^{-1}(S)$ and its complement by the two blocks $B \cap E^{-1}(S)$ and $B - E^{-1}(S)$. The set $S$ is a splitter of $Q$ if $\mathrm{split}(S, Q) \neq Q$.

• The naïve algorithm starts from $Q = P$ and, while possible, picks a splitter $S$ of $Q$ that is a union of blocks of $Q$ and replaces $Q$ by $\mathrm{split}(S, Q)$.
• The improved algorithm also maintains a partition $X$, initially $\{U\}$, of which $Q$ is a refinement. While $Q \neq X$, it picks a block $S \in X$ that is not a block of $Q$ and a block $B \in Q$ with $B \subseteq S$ and $|B| \le |S|/2$, replaces $S$ in $X$ by $B$ and $S - B$, and replaces $Q$ by $\mathrm{split}(S - B, \mathrm{split}(B, Q))$.

The improved algorithm is analysed under the standing assumption $|E(\{x\})| \ge 1$ for all $x \in U$: every element has at least one successor. (The paper reduces the general case to this one by a preprocessing step.)

Formalization targets

Goal: the improved algorithm

For every run $(Q_0, X_0) = (P, \{U\}), \dots, (Q_K, X_K)$ of the improved algorithm with refining blocks $B_0, \dots, B_{K-1}$:

1. at every stage $Q_j$ and $X_j$ are partitions, $Q_j$ refines $X_j$, and $Q_j$ is stable with respect to every block of $X_j$;
2. if $Q_K = X_K$, then $Q_K$ is the coarsest stable refinement of $P$;
3. if $Q_K \neq X_K$, another step applies;
4. $K \le n - 1$;
5. every $x \in U$ satisfies

$$\#\{\, j < K \mid x \in B_j \,\} \le \log_2 n + 1.$$

Items 1–4 are the correctness of the improved algorithm, which the paper deduces from that of the naïve one. Item 5 is the counting fact on which the $O(m \log n)$ bound rests.

Milestones

• §3, p. 978: $S$ is a splitter of $Q$ if and only if $Q$ is unstable with respect to $S$.
• Properties (1)–(3), p. 978: stability is inherited under refinement and under union; $\mathrm{split}$ is monotone in its second argument.
• §3, p. 979: a stable partition is stable with respect to every union of its blocks.
• Lemma 2, p. 979: every stable refinement of $P$ refines each partition produced by the naïve algorithm.
• Theorem 2, p. 979: the naïve algorithm stops after at most $n - 1$ steps at the unique coarsest stable refinement.
• Property (4), p. 978: $\mathrm{split}$ is commutative, and $\mathrm{split}(S, \mathrm{split}(Q, P))$ is the coarsest refinement of $P$ stable with respect to both $S$ and $Q$.
• Lemma 3, p. 980: the three-way split of a block $D$ into $D_{11}$, $D_{12}$ and $D_2$, including $D_{12} = D_1 \cap (E^{-1}(B) - E^{-1}(S - B))$.

Significance

The coarsest stable refinement of the partition of states by their labels is the bisimilarity relation of a finite transition system, so the goal certifies, for any sequence of choices, the correctness of the refinement loop at the core of bisimulation minimization. The halving count is the combinatorial half of the $O(m \log n)$ bound: once the implementation charges $O(|B| + \sum_{y \in B} |E^{-1}(\{y\})|)$ per refining block $B$, the count bounds the total work.

The results are proved in the paper, some by one-line arguments and the elementary properties (1)–(4) not at all ("stated without proof"). No machine-checked proof of the Paige–Tarjan algorithm's correctness or of its halving count is known to be available in Lean or Mathlib. The mission produces a checked account of the invariant, the final correctness and the counting argument for every run, not only for a particular implementation.

Difficulty

The correctness of the improved algorithm is not a special case of the naïve one read off directly. An improved step refines by $B$ and by $S - B$, and $S - B$ is a union of blocks of $Q$ only because $Q$ refines $X$. The invariant that $Q$ is stable with respect to every block of $X$ is what makes $Q = X$ a stopping condition, and it holds initially only under the standing assumption. The naive idea of reusing Hopcroft's argument fails: for relations, stability with respect to $S$ and $B$ does not imply stability with respect to $S - B$, which is why both refinements are performed. For the halving count, the refining blocks that contain a fixed element must be shown to be nested across steps, which requires tracking how blocks of $X$ are replaced.

Formalization scope

• $U$ is a Fintype with decidable equality, $E$ a decidable relation U → U → Prop. Partitions are Finset (Finset U) with an explicit predicate IsPartition (nonempty, pairwise disjoint blocks covering $U$); blocks are required to be nonempty, which the paper leaves implicit.
• "Coarsest" means: every stable partition refining $P$ refines it. The paper's "every other stable partition" is read this way, since a stable partition that does not refine $P$ need not refine the answer.
• Algorithms are step relations; a run is a finite sequence of states indexed by Fin (K + 1), with the choices $S_j, B_j$ recorded. Every statement holds for every run, so no choice rule is fixed.
• Added hypotheses: $U$ nonempty (so $\{U\}$ is a partition and "at most $n - 1$ steps" is meaningful); the standing assumption $\forall x\, \exists y,\ xEy$ for the goal only. Lemma 2 is stated for every stable refinement of $P$, which is what its proof gives and what Theorem 2 uses; it implies the printed form.
• Explicit forms: $|B| \le |S|/2$ is 2 * B.card ≤ S.card, $K \le n - 1$ is K + 1 ≤ n, $\log_2$ is Real.logb 2 of $n$ cast to $\mathbb{R}$. The termination bound for the improved algorithm is not printed in the paper and is derived as in the proof of Theorem 2. Running times ($O(mn)$, $O(m \log n)$) and the data structures of the implementation are out of scope.
• A trivializing reading is ruled out: the goal quantifies over all runs from $(P, \{U\})$ with every side condition of the step (in particular $S \notin Q$ and the half-size condition), and the conclusion is a full correctness statement, not the existence of some stable partition; the discrete partition is stable but is not the answer in general.
• Reusable beyond this mission: preimage, stability, $\mathrm{split}$ and its algebra (properties (1)–(4)), which apply to Hopcroft's algorithm and to bisimulation minimization in general. Contributions proving the elementary properties first, then Lemma 2 and Theorem 2, are the natural attack order.

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
• P. C. Kanellakis, S. A. Smolka, CCS expressions, finite state processes, and three problems of equivalence, Information and Computation 86(1):43–68, 1990. https://doi.org/10.1016/0890-5401(90)90025-D
• J. E. Hopcroft, An n log n algorithm for minimizing states in a finite automaton, in Theory of Machines and Computations, Academic Press, 1971, pp. 189–196. https://doi.org/10.1016/B978-0-12-417750-5.50022-1
• A. V. Aho, J. E. Hopcroft, J. D. Ullman, The Design and Analysis of Computer Algorithms, Addison-Wesley, 1974.

Motivation

Paging is the problem of managing a two-level memory: a fast cache holds $k$ pages out of an address space of $n$ pages, requests to pages arrive one at a time, and a request to a page outside the cache (a page fault) forces the algorithm to bring that page in and, when the cache is full, to evict another. The cost is the number of faults. An on-line algorithm decides which page to evict without knowing future requests. The comparison of paging policies with the optimal off-line policy is where competitive analysis began.

Sleator and Tarjan showed that LRU and FIFO are within a factor $k$ of the off-line optimum and that no deterministic on-line algorithm does better than $k$ (Sleator–Tarjan 1985). Randomization changes the picture: Fiat, Karp, Luby, McGeoch, Sleator and Young introduced the marking algorithm and proved that its expected cost is within a factor $2H_k$ of the optimum, where $H_k = 1 + \frac12 + \dots + \frac1k \approx \ln k$ (arXiv:cs/0205038).

Timeline.

• 1985: Sleator and Tarjan: LRU and FIFO are $k$-competitive; no deterministic algorithm beats $k$.
• 1988: Karlin, Manasse, Rudolph and Sleator coin "competitive" and analyse flush-when-full (Algorithmica 3).
• 1990: Manasse, McGeoch and Sleator introduce the $k$-server problem and define competitiveness for randomized algorithms (J. Algorithms 11).
• 1991: Fiat et al.: the marking algorithm is $2H_k$-competitive, and $H_{n-1}$-competitive when $k = n-1$; no randomized paging algorithm beats $H_k$.
• 1991: McGeoch and Sleator give an $H_k$-competitive randomized paging algorithm (Algorithmica 6).
• 2000: Achlioptas, Chrobak and Noga determine the exact competitive ratio of the marking algorithm, $2H_k - 1$ (Theoret. Comput. Sci. 234).

Setting

The paper works in the uniform $k$-server problem, which is isomorphic to paging. There is a set $M$ of $n$ vertices, enumerated $e(0), \dots, e(n-1)$, and moving a server between two distinct vertices costs $1$. There are $k$ servers, $1 \le k \le n$. A request is a vertex, and after each request some server must be on it. Cached pages are covered vertices; a fault is a server move.

The marking algorithm starts with its servers on $e(0), \dots, e(k-1)$ and keeps a set of marked vertices, initially the covered ones. On a request to $r$:

1. Marking. $r$ is marked; the moment $k+1$ vertices are marked, all marks except the one on $r$ are erased.
2. Serving. If $r$ is covered, nothing moves. Otherwise a server is chosen uniformly at random among the covered unmarked vertices and moved to $r$.

The marks are updated before the server is chosen. For a finite request sequence $\sigma$, $C_M(\sigma)$ is the algorithm's expected number of server moves. $\mathrm{OPT}(\sigma)$ is the least number of moves with which $k$ servers, starting from the same configuration $C_0$ and knowing $\sigma$ in advance, can serve $\sigma$.

A randomized algorithm is $c$-competitive if there is a constant $a$ such that $C_M(\sigma) \le c \cdot C_B(\sigma) + a$ for every request sequence $\sigma$ and every algorithm $B$.

The marks divide $\sigma$ into phases. A new phase begins at the request that would make $k+1$ vertices marked. A vertex is clean in a phase if it was not requested in the previous phase and not yet in this one, and stale if it was requested in the previous phase but not yet in this one.

Formalization targets

Goal: Theorem 1

$$\exists\, a \in \mathbb R\ \ \forall \sigma:\qquad C_M(\sigma) \;\le\; 2H_k \cdot \mathrm{OPT}(\sigma) + a .$$

The constant $a$ may depend on $n$, $k$ and the enumeration, never on $\sigma$.

Milestones (proof of Theorem 1, pp. 4–5)

1. Without loss of generality the adversary is lazy: no move on a covered request, exactly one move otherwise (reference item, already proved on the platform).
2. At the start of every phase the marked vertices are exactly the covered ones, and the first request of a phase is unmarked.
3. In a phase with $l$ clean requests, a lazy adversary pays $C_A \ge l - d$, where $d$ counts its servers off the marking algorithm's servers at the start of the phase.
4. It also pays $C_A \ge d'$, where $d'$ counts its servers off the final marked set at the end of the phase.
5. Hence $C_A \ge \max(l-d, d') \ge \tfrac12(l - d + d')$.
6. A request to a stale vertex is a fault with probability $c/s$ ($c$ clean vertices requested so far, $s$ stale vertices left).
7. The marking algorithm's expected cost in a phase is at most $l(H_k - H_l + 1) \le lH_k$.

Companions

• Theorem 2: for $k = n-1$, $C_M(\sigma) \le H_{n-1} \cdot \mathrm{OPT}(\sigma) + a$.
• Tightness remark (pp. 5–6): for $k = 2$, $n = 4$ there is no $a$ with $C_M(\sigma) \le H_2 \cdot \mathrm{OPT}(\sigma) + a$ for all $\sigma$.

Significance

The result. Theorem 1 was the first proof that randomization beats the deterministic barrier $k$ for paging, bringing the ratio down to $O(\log k)$. Together with the paper's lower bound $H_k$ for every randomized algorithm, it determines the randomized competitive ratio of paging up to a factor $2$. Its phase and clean/stale accounting is reused throughout the analysis of randomized caching.

Formalizing it. The theorem is proved (1991). As far as is known it has no machine-checked proof. Formalizing it requires a probabilistic model of a randomized on-line algorithm, an off-line optimum, and a phase decomposition with an exchangeability argument, and these are the first such objects in this library. Theorem 2 and the $k = 2$, $n = 4$ example use the same definitions and also check that the formal algorithm is the paper's. The sharp ratio $2H_k - 1$ is a natural follow-up.

Difficulty

The comparison is between a random process and a deterministic adversary, and each side has its own obstacle.

On the algorithm's side, the configuration inside a phase is random, and the fault probability of a stale request depends on the whole history of the phase. The claim that the $c$ uncovered stale vertices form a uniformly random subset of the $s$ stale ones is an exchangeability property of the process, and must be established from the step-by-step uniform choice. The worst-case ordering of the requests within a phase then has to be justified as a bound, not assumed.

On the adversary's side, the per-phase bound $\max(l-d, d')$ does not sum directly. The $d$ and $d'$ terms telescope across phases only because the configuration of the marking algorithm at each phase boundary is deterministic. The first phase, which begins after an initial run of requests to $e(0), \dots, e(k-1)$, and the last, incomplete phase have to be absorbed into the additive constant.

Formalization scope

The vertex set is an abstract metric space $M$ with $e : \mathrm{Fin}\,n \simeq M$ and $\mathrm{dist}(x,y) = 1$ for $x \ne y$. The natural metric $|i - j|$ on $\mathrm{Fin}\,n$ is deliberately not used. The configurations and the off-line optimum $\mathrm{OPT}$ are the published KServer definitions (KServer.Config, KServer.offlineCost), with $\mathrm{OPT}$ taken from the marking algorithm's initial configuration. An off-line algorithm starting elsewhere changes the cost by at most $k$, which is absorbed into $a$.

The marking algorithm is a Markov chain on pairs (covered set, marked set). Each step is a PMF, with the eviction drawn by PMF.uniformOfFinset from the covered unmarked vertices. The expected cost is the sum over requests of the probability that the request is not covered, which is exact because the algorithm moves exactly one server per fault. Harmonic numbers are Mathlib's harmonic, cast to $\mathbb R$. Phases, clean counts and lazy off-line schedules are defined once, in the mission's definition file, and all milestones use them.

A trivializing formalization is ruled out as follows. The additive constant is quantified before $\sigma$, so a per-sequence constant cannot be used. The comparison is with the optimum over all off-line schedules, not a particular one. The random choice is among the covered unmarked vertices, with marks updated first. The hypothesis $1 \le k \le n$ excludes the degenerate case $k = 0$, where $H_0 = 0$.

Proofs of individual milestones are welcome. The laziness reduction for off-line schedules, the exchangeability lemma for the uniform eviction process, and the harmonic-sum identity $\sum_{j=l+1}^{k} l/j = l(H_k - H_l)$ are reusable beyond this mission.

Selected references

• A. Fiat, R. M. Karp, M. Luby, L. A. McGeoch, D. D. Sleator, N. E. Young, Competitive Paging Algorithms, J. Algorithms 12(4):685–699, 1991; arXiv:cs/0205038v1. https://arxiv.org/abs/cs/0205038
• D. D. Sleator, R. E. Tarjan, Amortized Efficiency of List Update and Paging Rules, Comm. ACM 28(2):202–208, 1985. https://doi.org/10.1145/2786.2793
• A. R. Karlin, M. S. Manasse, L. Rudolph, D. D. Sleator, Competitive Snoopy Caching, Algorithmica 3:79–119, 1988. https://doi.org/10.1007/BF01762111
• M. S. Manasse, L. A. McGeoch, D. D. Sleator, Competitive Algorithms for Server Problems, J. Algorithms 11(2):208–230, 1990. https://doi.org/10.1016/0196-6774(90)90003-W
• L. A. McGeoch, D. D. Sleator, A Strongly Competitive Randomized Paging Algorithm, Algorithmica 6:816–825, 1991. https://doi.org/10.1007/BF01759073
• D. Achlioptas, M. Chrobak, J. Noga, Competitive Analysis of Randomized Paging Algorithms, Theoret. Comput. Sci. 234:203–218, 2000. https://doi.org/10.1016/S0304-3975(98)00116-9

Motivation

The traveling salesman problem with the triangle inequality asks for a shortest closed tour through $n$ points whose distances form a metric. It is NP-hard, so in practice tours are built by fast construction heuristics, and the natural question is how far such a tour can be from optimal in the worst case. Rosenkrantz, Stearns and Lewis (SIAM J. Comput. 6(3), 1977) gave the first systematic worst-case analysis of the standard heuristics. Their results are reproduced in textbooks on approximation algorithms and combinatorial optimization, and they are the reference point against which later guarantees (Christofides' $3/2$ algorithm, the double-tree $2$-approximation) are compared.

The simplest heuristic studied is the nearest neighbor algorithm (Bellmore and Nemhauser, 1968; the "next best method" of Gavett, 1965): from the current node, always move to the closest node not yet visited, and return to the start at the end. The paper shows that this greedy rule is never worse than logarithmic (Theorem 1) and that the logarithm cannot be removed (Theorem 2). This mission is about Theorem 2, the lower bound.

Setting

A traveling salesman graph on $n$ nodes is a complete graph with a distance $d(a,b)\in\mathbb R$ that is symmetric, $d(a,b)=d(b,a)$, nonnegative, $d(a,b)\ge 0$, and satisfies the triangle inequality $d(a,c)\le d(a,b)+d(b,c)$. A tour lists the nodes in a visiting order $\tau(0),\dots,\tau(n-1)$ and returns to $\tau(0)$; its length is the sum of the $n$ distances along it. OPTIMAL is the least length of a tour.

The nearest neighbor algorithm starts at an arbitrary node $\tau(0)$; having reached $\tau(k)$, it moves to a node $\tau(k+1)$ that minimizes $d(\tau(k),\cdot)$ over the nodes not yet visited, breaking ties arbitrarily; after the last node it returns to $\tau(0)$. The length of the resulting tour is written NEARNEIBER. Because the start node and the ties are free, one instance has in general several nearest-neighbor tours. A lower bound needs only one of them; an upper bound must hold for all.

The instances of the proof are built from a recursive family of weighted graphs. With $l_i=\frac16(4\cdot 2^i-(-1)^i+3)$ (so $l_1,l_2,l_3,l_4=2,3,6,11$), the graph $F_1$ is a triangle with unit weights, and $F_{i+1}$ consists of two copies of $F_i$ joined through one new node by two edges of length $1$ and two edges of length $l_i$. Each $F_i$ has $2^{i+1}-1$ nodes and a path $P_i$ from its start node to its middle node through every node, of length $L_i$ with $L_1=2$, $L_{i+1}=2L_i+2l_i$. The graph $G_i$ adds two closing edges to $F_i$, and $\bar G_i$ is the complete graph on the same nodes whose distance is the shortest-path distance of $G_i$.

Formalization targets

Goal: Theorem 2 (p. 566)

For each $m>3$ there is a traveling salesman graph with $n=2^m-1$ nodes and a nearest-neighbor tour on it such that

$$\frac{\mathrm{NEARNEIBER}}{\mathrm{OPTIMAL}}>\frac13\lg(n+1)+\frac49 .$$

The statement is existential in both the instance and the run of the algorithm, exactly as in the paper.

Milestones, in the order the proof uses them

1. (2.12): the difference equation $L_{i+1}=2L_i+2l_i$, $L_1=2$, has the solution $L_i=\frac19(6\,i\,2^i+8\cdot2^i+(-1)^i-9)$.
2. $\bar G_i$ is a traveling salesman graph: the shortest-path distance of $G_i$ is symmetric, nonnegative and satisfies the triangle inequality.
3. (2.13)–(2.17): the shortest-path distances in $F_{i+1}$ between the seven named nodes $A,\dots,G$ of Fig. 1, e.g. $\overline{AG}=l_{i+2}-2$.
4. Property a): every edge of $G_i$ is a shortest path between its endpoints.
5. Property b): the nearest neighbor algorithm started at the start node of $\bar G_i$ can follow $P_i$ and return along the edge of length $l_i-1$.
6. The optimal tour: $\mathrm{OPTIMAL}(\bar G_i)=2^{i+1}-1$.
7. The exact ratio: the tour along $P_i$ has length $L_i+l_i-1$, so its ratio is $(L_i+l_i-1)/n$.
8. The inequality: $(L_i+l_i-1)/n>\frac13\lg(n+1)+\frac49$ for $i\ge3$.

The instance for $m$ is $\bar G_{m-1}$.

Significance

Theorem 1 of the same paper shows $\mathrm{NEARNEIBER}/\mathrm{OPTIMAL}\le\frac12\lceil\lg n\rceil+\frac12$ for every nearest-neighbor tour on every traveling salesman graph. Theorem 2 shows that this bound has the right order: no constant-factor guarantee holds for the nearest neighbor rule, and the gap between the two constants ($\frac13$ against $\frac12$) is all that remains. This separates the nearest neighbor rule from the insertion rules analysed later in the same paper, of which nearest and cheapest insertion are within a factor $2$ of optimal. It is the standard example of a natural greedy heuristic whose approximation ratio grows with $n$.

The upper bound, Theorem 1, is already on Prove2Me with a machine-checked proof (SupplyChainTheory.nearest_neighbor_bound); its statement notes that the lower-bound instances are not formalized there. This mission supplies them: an explicit recursive family of metric instances, the shortest-path computations that certify it, and the arithmetic of its ratio. The result is proved in the paper; to our knowledge it has not been formalized in any proof assistant. The construction (a recursively defined weighted graph with a closed-form shortest-path table) is also a reusable pattern for other worst-case lower bounds of greedy heuristics.

Difficulty

The arithmetic ((2.12) and the final inequality) is routine. The content is in properties a) and b). A shortest-path distance is an infimum over all walks, and property a) asks that no detour through the recursive structure is shorter than the direct edge, at every level of the recursion. The paper handles this by an induction on (2.13)–(2.17) that tracks only seven nodes per level, and argues that distances inside a copy of $F_i$ are not shortened by embedding it into $F_{i+1}$. Property b) then needs that at each step of $P_i$ the chosen node is at least as close as every unvisited node, including nodes in the other copy and nodes reached through the start or right nodes; ties occur, and the claim is only that some resolution of them follows $P_i$. Checking small cases by computer does not give either property for all $i$.

Formalization scope

Nodes of an instance are Fin n, a tour is a permutation of Fin n, the tour length is the sum over consecutive pairs including the closing edge, and OPTIMAL is a minimum over the finite set of permutations. The model is the paper's: symmetric, nonnegative distances with the triangle inequality. The distance structure also carries $d(a,a)=0$, a normalization not in the paper; the diagonal never enters a tour length. A nearest-neighbor tour is a permutation in which each step goes to a node at least as close as every unvisited node, from an arbitrary start with arbitrary ties.

Ratios are multiplied out: the goal is $(\frac13\log_2(n+1)+\frac49)\cdot\mathrm{OPTIMAL}<\mathrm{NEARNEIBER}$ together with $\mathrm{OPTIMAL}>0$, the paper's standing assumption (1.1). $\lg(n+1)$ is Real.logb 2 of $n+1$, as printed. Because of the strict inequality and the conjunct $\mathrm{OPTIMAL}>0$, the all-zero distance does not satisfy the goal, so the statement cannot be met by a degenerate instance.

In the construction the nodes of $F_i$, $G_i$, $\bar G_i$ are numbered $0,\dots,2^{i+1}-2$ from left to right (start node $0$, middle node $2^i-1$, right node $2^{i+1}-2$); in $F_{i+1}$ the left copy comes first, then the new node, then the right copy. Graphs are edge lists with real weights and $l_i$ is defined in $\mathbb R$ exactly as in (2.11). The shortest-path distance is the infimum of walk weights over an inductive walk predicate; it would be $0$ for two nodes with no connecting walk, a case that does not arise because every $G_i$ and $F_i$ is connected. $L_i$ is defined by its difference equation; its identification with the length of the tour along $P_i$ is milestone 7. All construction statements assume $i\ge1$.

A complete development needs a small library for shortest-path distances of finite weighted edge lists (symmetry, triangle inequality, attainment, behaviour under relabelling and under gluing two graphs at a few nodes); this part is reusable beyond the mission. Contributions welcome: proofs of any milestone, and such general shortest-path lemmas as separate theorems. Theorem 1 is not part of this mission.

Selected references

• D. J. Rosenkrantz, R. E. Stearns, P. M. Lewis II, An Analysis of Several Heuristics for the Traveling Salesman Problem, SIAM J. Comput. 6(3):563–581, 1977. https://doi.org/10.1137/0206041
• M. Bellmore, G. L. Nemhauser, The Traveling Salesman Problem: A Survey, Operations Research 16(3):538–558, 1968. https://doi.org/10.1287/opre.16.3.538
• J. W. Gavett, Three Heuristic Rules for Sequencing Jobs to a Single Production Facility, Management Science 11(8):B166–B176, 1965. https://doi.org/10.1287/mnsc.11.8.B166
• N. Christofides, Worst-Case Analysis of a New Heuristic for the Travelling Salesman Problem, Report 388, Graduate School of Industrial Administration, Carnegie Mellon University, 1976.

Motivation

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

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

Timeline:

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

Setting

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

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

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

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

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

Formalization targets

Goal: Theorem 4.1

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

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

Milestones

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

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

Significance

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

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

Difficulty

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

Formalization scope

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

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

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

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

Selected references

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

Motivation

Bin packing asks for the fewest unit-capacity bins that hold a given list of item sizes. It models cutting stock, memory allocation, file placement and the loading of trucks, and it is NP-hard, so in practice lists are packed by simple rules that look at one item at a time. The two most widely used rules are First-Fit and Best-Fit, and the question that Johnson, Demers, Ullman, Garey and Graham answered in 1974 is how far from optimal they can be in the worst case.

Their headline answer is that both rules use at most about $\tfrac{17}{10}$ times the optimal number of bins, and that $\tfrac{17}{10}$ is asymptotically attained. The lists that force this ratio use items larger than $\tfrac12$. When all items are known to be small, which is typical of memory and storage applications, the guarantee is much better, and this mission is about that refinement: the paper's Theorem 2.3 and its corollary, which determine the asymptotic worst-case ratio of First-Fit and Best-Fit exactly as a function of the largest allowed item size $\alpha\le\tfrac12$.

Timeline. Ullman (1971) introduced the worst-case analysis of First-Fit with a $\tfrac{17}{10}L^*+3$ bound. Garey, Graham and Ullman (1972) and Johnson's thesis (MIT, 1973) extended it to Best-Fit and to the decreasing variants. The 1974 SIAM paper collects these results; Theorem 2.3 there is the parametric bound for items of size at most $\alpha$. The additive constants in the unrestricted $\tfrac{17}{10}$ bound were sharpened over the following four decades, culminating in Dósa and Sgall's proof (2013) that $FF(L)\le\lfloor\tfrac{17}{10}L^*\rfloor$.

Setting

A list is a finite sequence $L=(a_1,\dots,a_n)$ of real numbers in $(0,1]$. Its optimum $L^*$ is the least number of bins into which the elements of $L$ can be placed so that no bin contains numbers whose sum exceeds $1$. The level of a bin is the sum of the numbers in it. For a real $\alpha>0$, write $L\subseteq(0,\alpha]$ when every element of $L$ is at most $\alpha$.

First-Fit ($FF$) considers bins $B_1,B_2,\dots$, all initially empty, and places $a_1,a_2,\dots,a_n$ in that order: $a_i$ goes into the bin $B_j$ of least index whose level $\beta$ satisfies $\beta\le 1-a_i$. Best-Fit ($BF$) is the same except that, among the bins with $\beta\le 1-a_i$, it chooses one of largest level $\beta$ (least index among ties). $FF(L)$ and $BF(L)$ denote the numbers of nonempty bins at the end.

The restricted worst-case ratios are

$$R^\alpha_{FF}(k)=\max\Big\{\frac{FF(L)}{L^*}: L\subseteq(0,\alpha],\ L^*=k\Big\},\qquad R^\alpha_{BF}(k)=\max\Big\{\frac{BF(L)}{L^*}: L\subseteq(0,\alpha],\ L^*=k\Big\}.$$

Throughout, $0<\alpha\le\tfrac12$ and $m=\lfloor\alpha^{-1}\rfloor$, an integer with $m\ge 2$ and $\tfrac1{m+1}<\alpha\le\tfrac1m$.

Formalization targets

Goal: the asymptotic ratio (Corollary of Theorem 2.3, p. 308)

$$\lim_{k\to\infty}R^\alpha_{FF}(k)=\lim_{k\to\infty}R^\alpha_{BF}(k)=1+\frac{1}{\lfloor\alpha^{-1}\rfloor}.$$

The goal is stated as a limit, which is the stable form of the result: it is unaffected by any improvement of the additive constants below.

Theorem 2.3(i): the lower bound (p. 307)

For each $k\ge1$ there is a list $L\subseteq(0,\alpha]$ with $L^*=k$ and $FF(L)\ge\frac{m+1}{m}L^*-\frac1m$; likewise for $BF$.

Two steps of the First-Fit upper bound (p. 308)

If no element of $L$ exceeds $\frac1m$, then in the First-Fit packing every bin except possibly the last contains at least $m$ elements, and all but at most two bins have level at least $\frac{m}{m+1}$.

Theorem 2.3(ii): the upper bounds (p. 307)

For every list $L\subseteq(0,\alpha]$,

$$FF(L)\le\frac{m+1}{m}L^*+2,\qquad BF(L)\le\frac{m+1}{m}L^*+2.$$

Significance

The theorem gives an exact, parametric description of how the worst case of the two greedy rules improves as items shrink: the asymptotic ratio is $\tfrac32$ when items are at most $\tfrac12$, $\tfrac43$ when at most $\tfrac13$, and tends to $1$ as the maximum item size tends to $0$. Combined with the $\tfrac{17}{10}$ bound for unrestricted lists, it shows that the bad behaviour of First-Fit is caused entirely by items larger than $\tfrac12$. Such parametric bounds are the standard way bin-packing heuristics are compared in the literature on online and semi-online packing, and the construction in part (i) is a reusable template for lower-bound lists.

The paper proves the First-Fit upper bound and the lower bound (the verification of the lower-bound construction is left to the reader). The Best-Fit upper bound is stated but not proved: the paper says only that "a similar, but slightly more complicated, argument can be used". A formal proof of the goal therefore requires supplying that argument. None of these results is known to have a machine-checked proof; Mathlib contains no bin-packing development.

Difficulty

For First-Fit the upper bound is a counting argument, but it rests on a property of the run, not of the final packing: an item that went into a later bin did not fit into an earlier bin at the moment it was placed. Turning that into a statement about the final levels requires an invariant maintained through the whole sequence of placements.

The Best-Fit upper bound is harder because that property fails: Best-Fit may put a small item into a fuller, later bin while an earlier, lighter bin still has room, so a light early bin and a light later bin can coexist longer than under First-Fit. The paper gives no argument for this case.

The lower bound requires computing the exact behaviour of both algorithms on a specific interleaved list with item sizes perturbed by powers of $m$, and computing $L^*$ exactly for that list, which needs a matching lower bound on the optimum.

Formalization scope

A list is L : List ℝ with the hypothesis IsList L (every element in $(0,1]$); $L\subseteq(0,\alpha]$ is the additional hypothesis ∀ a ∈ L, a ≤ α. $L^*$ is optBins L, a sInf in ℕ over numbers of bins admitting a feasible assignment; the hypothesis IsList makes the set nonempty. The runs ffPack L and bfPack L are folds over the list that keep the nonempty bins in the order they were opened, each with its contents; an item that fits nowhere opens a new bin at the end, which is the paper's "least $j$" over infinitely many empty bins. Comparisons are exact (classical decidability on ℝ), and $FF(L)$, $BF(L)$ are the lengths of the final bin lists. $m$ is Nat.floor α⁻¹, cast before any division.

The ratios $R^\alpha_{FF}(k)$, $R^\alpha_{BF}(k)$ are suprema taken in ℝ≥0∞: an unbounded family would give $+\infty$, never a default value, and at $k=0$ the only admissible list is empty and the value is $0$. The goal is a Tendsto … atTop (𝓝 (1 + (⌊α⁻¹⌋₊)⁻¹)) statement in ℝ≥0∞. A real-valued sSup would have returned $0$ on an unbounded family and made a false bound look provable; that encoding is ruled out. The upper bounds keep the additive constant $2$ and the lower bound the subtractive $\frac1m$ exactly as printed.

The two proof steps are stated under the proof's own hypothesis "no element exceeding $1/m$", which is weaker than $L\subseteq(0,\alpha]$.

A complete development needs invariants of the First-Fit and Best-Fit folds, a lower bound $L^*\ge\sum_i a_i$, and exact evaluation of both runs on the construction of part (i). Lemmas about the fold encoding of First-Fit and Best-Fit and about $L^*$ are reusable in the companion missions on the $\tfrac{17}{10}$, $\tfrac{11}{9}$ and $\tfrac{71}{60}$ bounds of the same paper. Contributions on the Best-Fit upper bound are especially welcome, since the source gives no proof.

Selected references

• D. S. Johnson, A. Demers, J. D. Ullman, M. R. Garey, R. L. Graham, Worst-Case Performance Bounds for Simple One-Dimensional Packing Algorithms, SIAM Journal on Computing 3(4):299–325, 1974. https://doi.org/10.1137/0203025
• J. D. Ullman, The Performance of a Memory Allocation Algorithm, Technical Report 100, Princeton University, 1971.
• M. R. Garey, R. L. Graham, J. D. Ullman, Worst-Case Analysis of Memory Allocation Algorithms, Proc. 4th ACM Symposium on Theory of Computing, 143–150, 1972. https://doi.org/10.1145/800152.804907
• D. S. Johnson, Near-Optimal Bin Packing Algorithms, PhD thesis, Massachusetts Institute of Technology, 1973. http://hdl.handle.net/1721.1/57819
• G. Dósa, J. Sgall, First Fit Bin Packing: A Tight Analysis, Proc. 30th STACS, LIPIcs 20:538–549, 2013. https://doi.org/10.4230/LIPIcs.STACS.2013.538