Operations Research

Motivation

In multi-agent scheduling, several decision makers share one processing resource, and each one cares only about the completion of its own jobs. Agnetis, Mirchandani, Pacciarelli and Pacifici (Oper. Res. 52(2), 2004) set up the two-agent version of this problem and classified its complexity for most combinations of classical objectives. Typical settings are a manufacturing cell that serves an internal and an external customer, or two departments that negotiate access to a shared machine. Most of the paper treats a single machine. Its §10 asks what happens when the shared resource is a small shop: two machines that every job must visit.

The answer is that even the simplest two-machine case is hard. In the classical single-agent setting, the two-machine flow shop makespan problem is solved by Johnson's rule (Johnson 1954) and the two-machine open shop makespan problem by Gonzalez and Sahni (1976), both in polynomial time. As soon as two agents each want their own jobs finished early, both problems become NP-hard.

Setting

There are two agents, A and B. Agent A owns jobs $J^A_1,\dots,J^A_{n_A}$ and agent B owns jobs $J^B_1,\dots,J^B_{n_B}$. Every job consists of one operation on machine $M_1$ and one on machine $M_2$, and $p^X_{ih}\ge 0$ is the processing time of job $J^X_i$ on machine $M_h$. A schedule gives every operation a start time. It is feasible when no operation starts before time $0$, each machine processes at most one operation at a time, and the two operations of one job do not overlap in time. Processing is nonpreemptive.

• In the flow shop $F2$ every job is processed first on $M_1$ and then on $M_2$.
• In the open shop $O2$ the two operations of a job may be processed in either order.

The makespan of agent $X$, $C^X_{\max}$, is the latest completion time of an operation of one of its jobs. The recognition problem $F2\|C^A_{\max}\le Q_A,\ C^B_{\max}\le Q_B$ asks, for given thresholds $Q_A, Q_B$, whether some feasible flow shop schedule has $C^A_{\max}\le Q_A$ and $C^B_{\max}\le Q_B$. The problem $O2\|C^A_{\max}\le Q_A,\ C^B_{\max}\le Q_B$ is the same question for the open shop.

PARTITION (Problem 9.1 of the paper) asks whether a finite list of nonnegative integers $p_1,\dots,p_k$ can be split into two parts of equal sum $P/2$, where $P=\sum_i p_i$.

Formalization targets

Goal: Theorems 10.1 and 10.2

$$\text{PARTITION}\ \le_p\ F2\,\|\,C^A_{\max}\le Q_A,\ C^B_{\max}\le Q_B \qquad\text{and}\qquad \text{PARTITION}\ \le_p\ O2\,\|\,C^A_{\max}\le Q_A,\ C^B_{\max}\le Q_B,$$

with $\le_p$ polynomial-time many-one reducibility between binary-coded languages. This is how the paper proves "$F2\|C^A_{\max}:C^B_{\max}$ is NP-hard" (Theorem 10.1, p. 238) and "$O2\|C^A_{\max}:C^B_{\max}$ is NP-hard" (Theorem 10.2, p. 239).

Milestones: the two constructions

For Theorem 10.1, with $\varepsilon=1/(k+1)$, the paper builds the instance with $k$ A-jobs of times $(\varepsilon, p_i)$, one B-job of times $(P/2-(k-1)\varepsilon,\ P/2)$, and thresholds $Q_A = 3P/2+\varepsilon$, $Q_B = P+\varepsilon$. The milestones are:

1. under $C^B_{\max}\le Q_B$ the B-job starts on $M_2$ by $P/2+\varepsilon$, and the A-jobs before it on $M_2$ total at most $P/2$;
2. for even $P$, PARTITION has a solution if and only if this instance meets both thresholds.

For Theorem 10.2 the instance has $k$ A-jobs of time $p_i$ on both machines, one B-job of time $P/2$ on both machines, and thresholds $Q_A=3P/2$, $Q_B=P$. The milestones are:

3. under $C^B_{\max}\le Q_B$ the B-job starts at $0$ on one machine and at $P/2$ on the other;
4. PARTITION has a solution if and only if this instance meets both thresholds.

Significance

The two theorems mark the boundary of tractability of §10. The single-agent problems $F2\|C_{\max}$ and $O2\|C_{\max}$ are polynomial. Giving the second agent a single job and a deadline is already enough to make the problems NP-hard, so no extension of Johnson's rule or of the Gonzalez–Sahni algorithm solves the two-agent versions unless P = NP. The paper also observes that any other combination of the objectives it considers is NP-hard in these shops.

The theorems are proved in the paper by short reductions. As far as we know none of them is machine-checked. This mission produces checked statements of both reductions on a general two-machine shop model with real start times. It also corrects the flow shop equivalence, which as printed does not hold for odd $P$.

Difficulty

The hard direction of each equivalence goes from a feasible schedule to a partition. A schedule is a set of real start times, not a permutation. Nothing forces the jobs into a fixed order or rules out idle time. The proof has to extract a combinatorial split from interval packing: which A-jobs fit into the gap before the B-job on one machine and which fit into the gap after it. The sum of lengths of pairwise disjoint intervals inside a window must be bounded by the window's length.

In the flow shop the gap after the B-job has length $P/2+k\varepsilon$, which is not $P/2$. Integrality of the A-lengths is what closes the gap, and it only works when $P/2$ is an integer. In the open shop, the same argument has to cover both orders of the B-job's operations. Both reductions output rational data, so the goal also needs a scaling to integer data and a polynomial-time bound on the code map.

Formalization scope

• Model. Jobs are numbered Fin (n_A + n_B), the A-jobs first. Start times are real numbers, and idle time and different job orders on the two machines are allowed. Flow shop feasibility is the published JohnsonFlowShop.TwoStage.IsFeasible from the Johnson (1954) series. Open shop feasibility is the definition IsOpenFeasible of this mission: no machine overlap between distinct jobs, and no time overlap between the two operations of a job. "$C^X_{\max}\le Q_X$" is stated as "every operation of every $X$-job ends by $Q_X$", so no maximum over a possibly empty set is taken.
• Languages. The target languages hold the binary codes of instances with natural-number processing times and thresholds that have a feasible schedule meeting both thresholds. PARTITION is the published ProjSchedTW.Complexity.partitionLang (nonnegative sizes, zero allowed), and reducibility is CookPvsNP.PolyReducible. Both come from published definitions of the Neumann–Schwindt–Zimmermann and Cook series. NP-membership is not formalized.
• Constructions. They are defined over $\mathbb R$ exactly as printed. A reduction to the $\mathbb N$-coded languages has to rescale (for example by $2(k+1)$). That rescaling is the solver's to choose and is not a milestone.
• Corrections. The printed flow shop equivalence uses $\lfloor P/2+k\varepsilon\rfloor = P/2$ and fails for odd $P$: $p=(1)$ gives a yes-instance of the scheduling problem but has no partition. It also fails for $P=0$ and $k\ge 2$, where the printed $p^B_{11}$ is negative. Milestone 2 therefore assumes $P$ even and ($P\ge2$ or $k\le1$). The goal is unaffected, because odd $P$ is a PARTITION no-instance. In the open shop proof, the printed identity "$\sum p^A_i+\sum p^B_i = 2P$" is read as "each machine carries $3P/2$ of work", and the statement is unchanged.
• No trivialization. The flow shop and open shop languages are not restricted to the instances the constructions produce, so they cannot be decided by reading off the construction. A schedule must satisfy the machine and job non-overlap constraints, including in the open shop, where a definition without the job constraint would let a job run on both machines at once.
• Welcome contributions. Interval-packing lemmas on $\mathbb R$, a polynomial-time bound for list arithmetic over encNats, and a scaling lemma for shop schedules are reusable beyond this mission.

Selected references

• A. Agnetis, P. B. Mirchandani, D. Pacciarelli, A. Pacifici, Scheduling Problems with Two Competing Agents, Operations Research 52(2) (2004) 229–242. https://doi.org/10.1287/opre.1030.0092
• S. M. Johnson, Optimal two- and three-stage production schedules with setup times included, Naval Research Logistics Quarterly 1 (1954) 61–68. https://doi.org/10.1002/nav.3800010110
• T. Gonzalez, S. Sahni, Open shop scheduling to minimize finish time, Journal of the ACM 23(4) (1976) 665–679. https://doi.org/10.1145/321978.321985
• M. R. Garey, D. S. Johnson, Computers and Intractability: A Guide to the Theory of NP-Completeness, W. H. Freeman, 1979.

Two agents sharing one machine

In many production and service settings a single resource is shared by parties with different goals: two departments sending orders to the same machine, two customers of a contract manufacturer, or two classes of requests on one processor. Multi-agent scheduling models this directly. Each agent owns its own jobs and its own objective, and a schedule is judged by the pair of objective values it gives the two agents rather than by a single combined criterion.

Agnetis, Mirchandani, Pacciarelli and Pacifici (Oper. Res. 52(2), 2004, pp. 229–242) set up the systematic study of the two-agent single-machine problem. For each pair of classical objectives they ask how hard it is to optimise one agent's objective while the other agent's objective stays within a given bound. This mission formalises their §9, the case in which both agents minimise their own total completion time. With a single agent, minimising the total completion time is solved by sorting the jobs by length (the shortest-processing-time rule of Smith, 1956). §9 shows that two agents, each with this easiest of objectives, already give an NP-hard problem (Theorem 9.2), and that the problem is solved in pseudopolynomial time by a dynamic program (Theorem 9.3).

Setting

There are two agents, A and B. Agent A owns jobs $J^A_1,\dots,J^A_{n_A}$ with processing times $p^A_h\in\mathbb N$; agent B owns jobs $J^B_1,\dots,J^B_{n_B}$ with processing times $p^B_k\in\mathbb N$. All jobs are available at time $0$ and are processed on one machine, one at a time, without interruption. Since both objectives are nondecreasing in the completion times, a schedule $\sigma$ is a sequence of all $n_A+n_B$ jobs processed back to back from time $0$. The completion time $C_j(\sigma)$ of a job is the total processing time of the job and of all jobs before it. Agent A's cost is $\sum_hC^A_h(\sigma)$ and agent B's cost is $\sum_kC^B_k(\sigma)$.

The recognition problem $1\|\sum C^A_i\le Q_A,\ \sum C^B_i\le Q_B$ asks, for thresholds $Q_A,Q_B$, whether some schedule has

$$\sum_{h=1}^{n_A}C^A_h(\sigma)\le Q_A\qquad\text{and}\qquad\sum_{k=1}^{n_B}C^B_k(\sigma)\le Q_B .$$

The source problem is PARTITION (Problem 9.1): given integers $p_1,\dots,p_k$ with $P=\sum_ip_i$, is there a set $S\subseteq\{1,\dots,k\}$ with $\sum_{i\in S}p_i=\sum_{i\notin S}p_i=P/2$?

The paper's reduction numbers the integers so that $p_1\le\dots\le p_k$ and gives both agents identical job sets, $k$ jobs of lengths $p_1,\dots,p_k$, with thresholds $Q_A=Q_B=T/2$, where

$$T=3P+4\sum_{i=1}^k(k-i)p_i .$$

Writing $J[i]$ for the pair $J^A_i,J^B_i$, an SPT schedule processes $J[1],\dots,J[k]$ in order, each pair in either internal order; $x$ denotes the total length of the pairs in which B goes first.

Formalization targets

Goal: Theorem 9.2

$$\text{PARTITION}\ \le_p\ 1\|\textstyle\sum C^A_i\le Q_A,\ \sum C^B_i\le Q_B$$

Here $\le_p$ is polynomial-time many-one reducibility between languages of binary codes: a polynomial-time Turing-machine-computable map on strings that sends codes of PARTITION yes-instances, and only those, to codes of yes-instances of the recognition problem. Together with the NP-completeness of PARTITION (Karp 1972) this is the statement "$1\|\sum C^A_i : \sum C^B_i$ is binary NP-hard".

Milestones of the proof

1. Every SPT schedule has $\sum C^A_i+\sum C^B_i=T$, and $Q_A=Q_B=T/2$.
2. Eqs. (5) and (6): in an SPT schedule, $\sum C^A_i=P+2\sum_i(k-i)p_i+x$ and $\sum C^B_i=P+2\sum_i(k-i)p_i+(P-x)$.
3. A schedule with $\sum C^A_i\le T/2$ and $\sum C^B_i\le T/2$ processes the jobs in nondecreasing order of length.
4. For pairwise distinct $p_1<\dots<p_k$: PARTITION has a solution iff some schedule meets $T/2$ for both agents.

Further result: Theorem 9.3 with recursion (7)

With each agent's jobs numbered by nondecreasing length and $P(i,j)$ the total length of $J^A_1,\dots,J^A_i,J^B_1,\dots,J^B_j$, the recursion

$$F(i,j,q)=\min\bigl\{F(i-1,j,q)+P(i-1,j)+p^A_i;\ F(i,j-1,q-P(i,j))\bigr\}$$

with $F(0,0,q)=0$ for $q\ge0$ and $F=+\infty$ for $q<0$ yields $F(n_A,n_B,Q)=\min\{\sum C^A_i:\sum C^B_i\le Q\}$, and $+\infty$ when no schedule meets the bound.

Significance

Theorem 9.2 fills one cell of the paper's complexity table: even when both agents use the objective that is trivial for one agent, sharing the machine makes the constrained problem NP-hard. Together with Theorem 9.3 it places $1\|\sum C^A_i:\sum C^B_i$ exactly: NP-hard under binary encoding, solvable in pseudopolynomial time, hence not strongly NP-hard unless P = NP. The later literature on two-agent and multi-agent scheduling (for example the monograph of Agnetis, Billaut, Gawiejnowicz, Pacciarelli and Soukhal, Multiagent Scheduling, Springer 2014) cites this classification.

Neither result has a machine-checked proof that we know of. The mission adds a formal record of the reduction and of the dynamic program, reusable definitions for the two-agent total-completion-time problem, and a correction of the printed proof: the equivalence between PARTITION and the constructed instance, as printed, holds only when the integers are pairwise distinct. For $p=(1,1,1,1,10)$ PARTITION has no solution, yet a schedule meets $T/2=41$ for both agents. Theorem 9.2 itself is not affected, since PARTITION remains NP-hard, but a complete formal proof needs a reduction that is correct on every input.

Difficulty

The equivalence for distinct integers rests on two facts: the overall total $\sum C^A_i+\sum C^B_i$ is at least $T$ for every schedule, with equality only for sequences in nondecreasing order of length; and, with distinct lengths, such a sequence is made of consecutive pairs, whose split is controlled by $x$. The naive formal argument stops at the second fact, which is false with repeated lengths: a block of equal-length jobs can be shared between the agents in ways no sequence of pairs realises. The goal adds the encoding layer: the reduction must be computable in polynomial time on a Turing machine, must handle repeated and zero sizes and odd $P$ (where $T/2$ is not an integer and the language's thresholds are), and must send strings that do not code a PARTITION instance outside the target language. For Theorem 9.3, the dynamic program is correct only because some optimal schedule orders each agent's jobs by length, and the constraint makes this exchange argument less direct than for a single agent.

Formalization scope

Jobs are Fin nA ⊕ Fin nB (Sum.inl h is $J^A_{h+1}$, Sum.inr k is $J^B_{k+1}$, 0-based). Schedules, completion times and the idle-free sequence model are the published MooreLateJobs.Shared.completionTime (Moore 1968 series): a schedule is a duplicate-free list containing every job once, and completion times are real numbers. Processing times and thresholds of the language are natural numbers. Reducibility is the published CookPvsNP.PolyReducible, and PARTITION, the alphabet and the binary codes are the published ProjSchedTW.Complexity.Encoding (partitionLang, whose sizes are natural numbers including $0$). The target language allows any job counts and any processing times; identical job sets are a property of the construction only.

The following readings are explicit:

• An SPT schedule of the construction is given by a choice $x:\mathrm{Fin}\,k\to\mathrm{Bool}$ of the first agent in each pair; "feasible implies SPT" is stated as "lengths are nondecreasing along the sequence", which is what the paper's exchange argument proves.
• The milestones take the integers already sorted, as a hypothesis; the paper's thresholds $T/2$ are real numbers in the milestones.
• The equivalence milestone assumes $p_1<\dots<p_k$; the printed version with $\le$ is false, as shown above.
• In recursion (7), the terms $F(-1,j,q)$ and $F(i,-1,q)$ that the paper leaves undefined are $+\infty$.
• The running time $O(n_An_BQ)$ of Theorem 9.3 is not formalised; only the correctness of (7) is. Membership in NP is not formalised.

The goal cannot be met by a trivial reduction: PolyReducible requires the map to be computed by a polynomial-time Turing machine and to be correct on every string, and the target language contains every two-agent instance, not only those with identical job sets. Contributions welcome: the exchange lemmas for total completion time on the shared sequence model, the SPT formulas, and Turing-machine constructions for list sorting and arithmetic on binary codes, which other reductions of this series reuse.

Selected references

• A. Agnetis, P. B. Mirchandani, D. Pacciarelli, A. Pacifici, Scheduling Problems with Two Competing Agents, Operations Research 52(2) (2004) 229–242. https://doi.org/10.1287/opre.1030.0092
• R. M. Karp, Reducibility among Combinatorial Problems, in Complexity of Computer Computations, Plenum (1972) 85–103. https://doi.org/10.1007/978-1-4684-2001-2_9
• W. E. Smith, Various Optimizers for Single-Stage Production, Naval Research Logistics Quarterly 3 (1956) 59–66. https://doi.org/10.1002/nav.3800030106
• J. M. Moore, An n Job, One Machine Sequencing Algorithm for Minimizing the Number of Late Jobs, Management Science 15(1) (1968) 102–109. https://doi.org/10.1287/mnsc.15.1.102
• S. Cook, The P versus NP Problem, Clay Mathematics Institute Millennium Problems (2000). https://www.claymath.org/wp-content/uploads/2022/06/pvsnp.pdf
• A. Agnetis, J.-C. Billaut, S. Gawiejnowicz, D. Pacciarelli, A. Soukhal, Multiagent Scheduling: Models and Algorithms, Springer (2014). https://doi.org/10.1007/978-3-642-41880-8

Two agents sharing one machine

In many production and logistics settings a single resource is shared by parties with different goals: two departments of a plant that send orders to the same machine, two customers of a contract manufacturer, or two classes of traffic on one processor. Multi-agent scheduling models this directly. Each agent owns its own jobs and its own objective, and a schedule is judged by the pair of objective values it gives the two agents rather than by one combined criterion.

Agnetis, Mirchandani, Pacciarelli and Pacifici (Oper. Res. 52(2), 2004, pp. 229–242) set up the systematic study of the two-agent single-machine problem. For each pair of classical objectives they ask how hard it is to optimise one agent's objective while the other agent's objective stays within a given bound. Their Table 1 lists the outcome for each pair. This mission formalises one entry, Theorem 5.2: when agent A minimises its total weighted completion time and agent B only requires its makespan to stay below a bound, the problem is NP-hard under binary encoding of the numbers. The corresponding single-agent bicriteria problem had been shown NP-hard in the strong sense by Lenstra, Rinnooy Kan and Brucker (1977); the two-agent version differs because only B's jobs are constrained.

Setting

There are two agents, A and B. Agent A owns jobs $J^A_1,\dots,J^A_{n_A}$; job $J^A_h$ has a processing time $p^A_h\in\mathbb N$ and a weight $w^A_h\in\mathbb N$. Agent B owns jobs $J^B_1,\dots,J^B_{n_B}$ with processing times $p^B_k\in\mathbb N$. All jobs are available at time $0$ and are processed on one machine, one at a time, without interruption.

Because both objectives are nondecreasing in the completion times, there is no reason to leave the machine idle, so a schedule $\sigma$ is a sequence of all $n_A+n_B$ jobs processed back to back from time $0$. The completion time $C_j(\sigma)$ of a job $j$ is the total processing time of $j$ and of all jobs sequenced before it. Agent A's cost is $\sum_{h}w^A_hC^A_h(\sigma)$; agent B's cost is its makespan $C^B_{\max}(\sigma)=\max_kC^B_k(\sigma)$.

The paper's recognition problem $1\|\sum w_iC^A_i\le Q_A,\ C^B_{\max}\le Q_B$ asks, for given thresholds $Q_A,Q_B$, whether some schedule has

$$\sum_{h=1}^{n_A}w^A_hC^A_h(\sigma)\le Q_A\qquad\text{and}\qquad C^B_k(\sigma)\le Q_B\ \text{ for all }k .$$

The source problem is KNAPSACK (Problem 5.1): given nonnegative integers $u_1,\dots,u_n$, $w_1,\dots,w_n$ and integers $b,W$, is there $S\subseteq\{1,\dots,n\}$ with $\sum_{i\in S}u_i\le b$ and $\sum_{i\in S}w_i\ge W$?

Formalization targets

Goal: Theorem 5.2

$$\text{KNAPSACK}\ \le_p\ 1\|\textstyle\sum w_iC^A_i\le Q_A,\ C^B_{\max}\le Q_B$$

Here $\le_p$ is polynomial-time many-one reducibility between languages of binary codes: a Turing-machine-computable, polynomial-time map on strings sending codes of KNAPSACK yes-instances, and only those, to codes of yes-instances of the recognition problem. Together with the NP-completeness of KNAPSACK (Garey and Johnson 1979) this is the statement "$1\|\sum w_iC^A_i : C^B_{\max}$ is binary NP-hard".

Milestones

The paper's reduction builds, from a KNAPSACK instance, the two-agent instance with $p^A_i=u_i$, $w^A_i=w_i$, a single B-job of length $p^B_1=\hat w\hat u$ (where $\hat u=\sum_iu_i$, $\hat w=\sum_iw_i$), and thresholds $Q_B=b+p^B_1$, $Q_A=\hat w\hat u+(\hat w-W)p^B_1$. The milestones are the two directions of the proof and their combination:

1. Eq. (1): if $S$ solves KNAPSACK, every sequence with exactly the A-jobs of $S$ before the B-job meets both thresholds.
2. Eq. (2): if $\sum_iw_iu_i>0$ and a sequence meets both thresholds, the A-jobs before the B-job solve KNAPSACK.
3. Equivalence: under $\sum_iw_iu_i>0$, KNAPSACK is a yes-instance iff the constructed instance is.
4. §8: with every B-job given due date $Q$ and $Q'=0$, a sequence meets $\sum U^B_i\le Q'$ (and A's bound) iff it meets $C^B_{\max}\le Q$, which carries the hardness over to $1\|\sum w_iC^A_i:\sum U^B_i$.

Significance

Theorem 5.2 fixes the complexity of one cell of the two-agent classification. It shows that the polynomial algorithm for the unweighted case $1\|\sum C^A_i:f^B_{\max}$ (Theorem 5.5 of the same paper) cannot be extended to arbitrary weights unless P = NP. Through §8 it also settles $1\|\sum w_iC^A_i:\sum U^B_i$. The hardness is binary, not strong: the reduction produces numbers of size about $\hat w\hat u$, so pseudo-polynomial algorithms are not ruled out, which is consistent with the dynamic programs studied in later two-agent literature.

The result is proved in the paper; no machine-checked proof is known to exist. Formalizing it produces a complete reduction from a two-constraint knapsack problem to a scheduling recognition problem, with the encoding, the degenerate instances and the polynomial running time all made explicit. The model and the KNAPSACK language are reusable by other two-agent reductions (Theorems 9.2, 10.1 and 10.2 of the paper reduce from PARTITION in the same frame).

Difficulty

The two directions of the equivalence are short computations with completion times. The printed argument, however, is not correct as written in two places. The bounds "smaller than $\hat w\hat u$" and "smaller than $(\hat w-W)p^B_1$" in the derivation of (1) hold only with equality allowed. The strict inequalities in (2) fail when $\sum_iw_iu_i=0$, and then the reduction itself fails: with all $u_i=0$ and $W>\hat w$ the KNAPSACK instance is a no-instance while the constructed instance has $Q_A=Q_B=0$ and every schedule meets both thresholds. A complete reduction must recognise such instances and treat them separately.

The construction also produces integer thresholds that can be negative ($b<-p^B_1$, or $W>\hat w+1$), while instances of the target are coded with natural numbers. Finally, the reduction must be a polynomial-time Turing machine computation over binary codes, including the decoding of arbitrary strings and the binary multiplication $\hat w\hat u$; that is where most of the formal work lies.

Formalization scope

• Model. Jobs are Fin nA ⊕ Fin nB (0-based: Sum.inl h is $J^A_{h+1}$, Sum.inr k is $J^B_{k+1}$). Schedules and completion times are the published MooreLateJobs.Shared sequence model (IsSchedule, completionTime) of the Moore (1968) series: a duplicate-free list of all jobs, processed without idle time from time $0$. Integer processing times are cast to $\mathbb R$.
• Makespan bound. $C^B_{\max}\le Q_B$ is written as $C^B_k\le Q_B$ for every B-job; no nonemptiness of B's job set is assumed.
• Languages. Polynomial-time reducibility is the published CookPvsNP.PolyReducible (Cook's Definition 3, one-tape Turing machines). Codes use the published binary encoding ProjSchedTW.Complexity.Encoding (alphabet BSym, encNat, encInt) of the Neumann–Schwindt–Zimmermann series. A KNAPSACK instance is coded as the integers $n,u_1,\dots,u_n,w_1,\dots,w_n,b,W$; a target instance as the natural numbers $n_A,n_B$, the processing times and weights, and $Q_A,Q_B$. The target language allows any $n_A,n_B\ge0$; the reduction uses $n_B=1$.
• Readings of the paper. "Binary NP-hard" is formalised as the reduction from KNAPSACK, without the NP-completeness of KNAPSACK and without membership in NP. The milestone Eq. (2) and the equivalence carry the added hypothesis $\sum_iw_iu_i>0$; the inequalities "smaller than" in (1) are read as $\le$. Eq. (1) is stated for every order of the jobs inside $S$ and inside its complement. The §8 result is stated as the encoding-free equivalence of feasible solutions, not as a reduction between languages.
• Ruled out. The goal cannot be met by a reduction that ignores the input: the equivalence must hold for every string, and the target language is exactly the codes of yes-instances of the two-agent recognition problem with B's objective the makespan. KNAPSACK here is the two-constraint problem of Problem 5.1, not subset sum.

Contributions welcome: proofs of the two directions, of the equivalence, the treatment of the degenerate instances, and the Turing machine for the reduction, which would also serve the other binary-coded reductions on the platform.

Selected references

• A. Agnetis, P. B. Mirchandani, D. Pacciarelli, A. Pacifici, Scheduling Problems with Two Competing Agents, Operations Research 52(2) (2004) 229–242. https://doi.org/10.1287/opre.1030.0092
• M. R. Garey, D. S. Johnson, Computers and Intractability: A Guide to the Theory of NP-Completeness, W. H. Freeman, 1979.
• J. K. Lenstra, A. H. G. Rinnooy Kan, P. Brucker, Complexity of Machine Scheduling Problems, Annals of Discrete Mathematics 1 (1977) 343–362. https://doi.org/10.1016/S0167-5060(08)70743-X
• S. Cook, The P versus NP Problem, Clay Mathematics Institute Millennium Problem description. https://www.claymath.org/wp-content/uploads/2022/06/pvsnp.pdf
• J. M. Moore, An n Job, One Machine Sequencing Algorithm for Minimizing the Number of Late Jobs, Management Science 15(1) (1968) 102–109. https://doi.org/10.1287/mnsc.15.1.102

Motivation

That noncooperative play usually wastes something is part of the folklore of game theory, with the Prisoner's Dilemma as its emblem: each player's best reply leads to an outcome that both would trade for another. Pradeep Dubey's paper turns this folklore into a theorem about smooth games. For games whose payoffs are twice continuously differentiable, and for all payoffs outside a negligible (closed, nowhere dense) set, Nash equilibria are finite in number and are Pareto-inefficient unless some player sits at a vertex of his strategy set. The same conclusion applies to Nash's mixed extensions of finite games (Nash 1951), where a vertex is a pure strategy.

The question is basic to welfare analysis of strategic interaction: market games, oligopoly, public goods and trading mechanisms (Shapley and Shubik 1977) all ask whether equilibrium outcomes can be efficient. Dubey's answer is that efficiency of an equilibrium is non-generic, so a model that delivers it is exploiting special structure.

Timeline. Nash (1951) introduced equilibrium points and multi-matrix games. Smale (1973, "Optimizing several functions") gave the first-order condition for Pareto optimality of several smooth functions: at an efficient interior point the gradients are linearly dependent. Harsanyi (1973, IJGT 2:235–250) proved that generic finite games have finitely many, indeed an odd number of, mixed equilibria. Dubey's Cowles Foundation Discussion Paper 508R (1978) stated finiteness and inefficiency; the version formalized here is the rewrite IIASA WP-83-74 (1983), published as Mathematics of Operations Research 11(1):1–8 (1986).

Setting

There are $n\ge2$ players $N=\{1,\dots,n\}$. Player $i$'s strategy set is the unit simplex

$$S^i=\Big\{x\in\mathbb R^{k(i)}_+ : \sum_{j=1}^{k(i)}x_j\le1\Big\},\qquad k(i)\ge1,$$

whose vertices (extreme points) are the origin and the unit vectors. Profiles $s=(s^1,\dots,s^n)$ range over $S=S^1\times\dots\times S^n\subset\mathbb R^{r(n)}$, $r(n)=\sum_i k(i)$.

Fix open neighbourhoods $V^i\supseteq S^i$ and $V=V^1\times\dots\times V^n$. The space $U$ consists of the $C^2$ functions $f:V\to\mathbb R$ with finite $C^2$-norm $\|f\|=\sup\{\|f(s)\|,\|Df(s)\|,\|D^2f(s)\|: s\in V\}$. A game is $u=(u^1,\dots,u^n)\in(U)^n$. For $T\subseteq N$, $(s|e)$ replaces $s^i$ by $e^i$ for $i\in T$. A profile $s\in S$ is $T$-efficient if no $e\in\times_{i\in T}S^i$ gives $u^i(s|e)\ge u^i(s)$ for all $i\in T$ with strict inequality for some $j\in T$. It is a Nash equilibrium if it is $\{i\}$-efficient for each $i$, efficient if it is $N$-efficient, and a strong Nash equilibrium if it is $T$-efficient for every $T$. The three sets are $N(u)$, $E(u)$, $G(u)$.

In the proof, $D_u(s)$ is the $n\times r(n)$ matrix with rows $Du^i(s)$; $N^*$ is the subspace of matrices whose $i$-th row vanishes on player $i$'s block of columns; $E^*$ is the set of matrices with linearly dependent rows.

Formalization targets

Goal: the Theorem (p. 3)

There is an open dense set $U_0\subseteq(U)^n$ such that for $u\in U_0$:

$$\text{(a) } N(u)\text{ is finite};\quad \text{(b) } s\in N(u)\cap E(u)\Rightarrow \exists j,\ s^j\text{ is a vertex};\quad \text{(c) } s\in G(u)\Rightarrow \text{at most one } s^j \text{ is not a vertex}.$$

Milestones (pp. 4–6)

For interior profiles ($s^i\in\operatorname{Int}S^i$ for all $i$):

$$\text{(i) } s\in N(u)\Rightarrow D_u(s)\in N^*,\qquad \text{(ii) } s\in E(u)\Rightarrow D_u(s)\in E^*,$$

$\operatorname{codim}N^*=r(n)$; the linear perturbation $u_t^i(x)=u_0^i(x)+t\sum_j y_{ij}x_j$ satisfies $\frac{d}{dt}D(u_t,s_0)|_{t=0}=y$ (the computation behind (**)); claim (*) for $M=N^*$: for an open dense set of games $D_u$ is transverse to $N^*$ on a compact neighbourhood $\underline V$ of $S$; under that transversality $S\cap D_u^{-1}(N^*)$ is finite; and the Theorem restricted to interior profiles.

Companions

The Theorem (Multi-Matrix) (p. 14): for an open dense set of payoff vectors $a\in(\mathbb R^K)^n$, the mixed Nash equilibria of $\Pi_a$ are finite, an efficient one has a player using a pure strategy, and a strong one is pure. From the example of §3: every game $(P,Q)$ on $[0,1]^2$ with payoffs $u_P(x,y)=-[(x-a)^2+(y-b)^2]$ has a unique Nash equilibrium (p. 9); Lemma 1, $E(P,Q)=r_X(L(P,Q))$ (p. 9); Lemma 2(a), an interior equilibrium is efficient iff $a=c$ or $b=d$ (p. 10).

Significance

The theorem gives the generic structure of equilibrium sets in smooth games: isolated and finitely many equilibria, and a sharp location of the only places where efficient equilibria can survive, namely the vertices. It explains why efficiency results for noncooperative models need boundary solutions or non-generic structure, and in its multi-matrix form it shows that strong equilibria of generic finite games are in pure strategies. It also supplies the finiteness of equilibria used in comparative-statics and index arguments.

On the formalization side, the result is proved on paper but has no machine-checked version. A complete development would give Lean its first generic-finiteness theorem for Nash equilibria of smooth games, a first-order Pareto condition in the form of Smale's lemma, and a parametric transversality argument in finite dimensions. The multi-matrix companion connects to the published vocabulary of finite games (agt_games), and the example of §3 is an elementary, fully explicit check of the general picture.

Difficulty

The interior case reduces, by (i) and (ii), to a dimension count: $D_u^{-1}(N^*)$ should be zero-dimensional and $D_u^{-1}(N^*\cap E^*)$ empty. Neither holds for every game: they hold only when $D_u$ is transverse to $N^*$ and to the strata of $N^*\cap E^*$, and the step that requires work is showing that transversality is an open and dense condition in the $C^2$ topology. Density is not obtained by adding linear functions to the payoffs: a linear function has finite $C^2$-norm on $V$ only when $V$ is bounded, so perturbations must be localized. The step from interior profiles to the whole of $S$ is a second difficulty. It requires repeating the argument on every product of faces of the simplices and on every subgame, and then intersecting finitely many open dense sets. Efficiency at a boundary point is not $T$-efficiency in a subgame, so the reduction has to be made with care.

Formalization scope

Players are Fin n with 2 ≤ n; block sizes k : Fin n → ℕ with 1 ≤ k i; profiles are ∀ i, Fin (k i) → ℝ. The simplex is the paper's corner simplex {x ≥ 0, ∑ x ≤ 1}, not the probability simplex; "vertex" is Set.extremePoints. The neighbourhoods $V^i$ are taken open, and the goal is stated for every such choice, not assuming $V$ bounded or convex. Payoffs are total functions; a game is ContDiffOn ℝ 2 on $V$ with finite $C^2$-norm, which takes values in $[0,\infty]$, so no junk real supremum enters. "Open dense in $(U)^n$" is written in $\varepsilon$-form for the product of $C^2$-norm topologies; Lean's sup-type norms are equivalent to the Euclidean ones, so the open dense sets are the same. Deviations range over all strategies in $\times_{i\in T}S^i$, not only pure or vertex deviations.

Added hypotheses, all disclosed in the items: openness of $V^i$; interiority of every $s^i$ on milestones (i), (ii) and the finiteness step (the proof's standing case assumption); $M=N^*$ in claim (*). The printed "By (i), $N(u)\subset S\cap D_u^{-1}(N^*)$" is stated for interior equilibria, which is where (i) applies.

A trivializing formalization is ruled out: the open dense set must contain games arbitrarily close to every game (the zero game is a game, so it is never empty), interiority appears only in the milestones and not in the goal, and efficiency is with respect to all deviations in $S$.

Not stated: (*) for a general submanifold $M$, and the decomposition of $N^*\cap E^*$ into submanifolds of codimension $\ge r(n)+1$, both of which need embedded submanifolds of $\mathbb R^N$; Remarks 1–4 (Remark 4's openness claim for strictly concave payoffs is false as printed); Lemma 2(b); §5, which the author leaves as a conjecture. Contributions welcome: a finite-dimensional parametric transversality theorem, Smale's first-order Pareto condition, and the face-by-face reduction.

Selected references

• P. Dubey, Inefficiency of Nash Equilibria, IIASA Working Paper WP-83-74, 1983; Mathematics of Operations Research 11(1):1–8, 1986. https://doi.org/10.1287/moor.11.1.1
• J. F. Nash, Non-Cooperative Games, Annals of Mathematics 54:286–295, 1951. https://doi.org/10.2307/1969529
• J. C. Harsanyi, Oddness of the Number of Equilibrium Points: A New Proof, International Journal of Game Theory 2:235–250, 1973. https://doi.org/10.1007/BF01737572
• S. Smale, Optimizing Several Functions, Manifolds — Tokyo 1973, Proceedings of the International Conference on Manifolds, University of Tokyo Press, 1975.
• R. Abraham and J. Robbin, Transversal Mappings and Flows, W. A. Benjamin, New York, 1967.
• L. S. Shapley and M. Shubik, Trade Using One Commodity as a Means of Payment, Journal of Political Economy 85:937–968, 1977. https://doi.org/10.1086/260617

Motivation

A retailer deciding which variants of a product to stock trades off two effects. A deeper assortment captures consumers whose favourite variant would otherwise be missing, but it splits demand among more variants, each of which then carries its operational costs (shelf space, handling, inventory) at a smaller, less efficient scale. Van Ryzin and Mahajan (Management Science 1999) showed that under multinomial-logit (MNL) demand the optimal assortment consists of the most popular variants, which reduces the search over $2^n$ assortments to $n$ candidates.

Cachon, Terwiesch and Xu (working paper, 2002; published in MSOM 2005) add consumer search: a consumer who finds nothing good enough in the store may leave to look elsewhere, and a deeper assortment makes that less likely. In their independent-assortment model the search threshold does not depend on the store's assortment, but the fraction of consumers who stay does. This mission formalizes their Theorem 5: even with this extra dependence, the profit change from adding a variant is quasi-convex in that variant's preference.

Setting

There are $n$ variants. Variant $i$ has a preference $v_i>0$ and the no-purchase option has preference $v_0>0$ (in the paper $v_i=\exp((u_i-p_i)/\mu)$, with $u_i-p_i$ the net utility and $\mu>0$ the Gumbel scale). For an assortment $S\subseteq\{1,\dots,n\}$ the MNL purchase probability without search is

$$q_i^m(S)=\frac{v_i}{\sum_{k\in S}v_k+v_0},\qquad i\in S .$$

A consumer searches when her best alternative in the store, including no purchase, falls below a threshold $\bar U$. With Euler's constant $\gamma$ and $\lambda=\exp[-(\bar U/\mu+\gamma)]>0$, this happens with probability $H(\bar U,S)=\exp\bigl(-\lambda(v_0+\sum_{k\in S}v_k)\bigr)$, and by the paper's Theorem 1 the independent-assortment demand is

$$q_i^{si}(S)=q_i^m(S)\bigl(1-H(\bar U,S)\bigr).$$

Each variant sold earns a margin $m$, and stocking a variant with demand $q$ costs $c(q)$, where the cost function $c$ is concave and increasing on $[0,1]$ (economies of scale). Variant $i$'s profit is $\pi_i^{si}(S)=m\,q_i^{si}(S)-c(q_i^{si}(S))$. Write $V_S=v_0+\sum_{i\in S}v_i$.

Fix $S$ and a variant $j\notin S$, and treat $j$'s preference $v_j\ge 0$ as a variable. Let $\pi_i^{si}(v_j)$ be variant $i$'s profit in $S_j=S\cup\{j\}$; its demand carries the factor $1-e^{-\lambda(v_j+V_S)}$, not $1-e^{-\lambda V_S}$. The cannibalization loss and the profit change are

$$L^{si}(v_j)=\sum_{i\in S}\pi_i^{si}(S)-\sum_{i\in S}\pi_i^{si}(v_j),\qquad h^{si}(v_j)=\pi_j^{si}(v_j)-L^{si}(v_j).$$

Formalization targets

Goal: Theorem 5 (common margin)

$$h^{si}\ \text{is quasi-convex on }[0,\infty):\qquad h^{si}(t)\le\max\{h^{si}(a),h^{si}(b)\}\quad(0\le a\le t\le b).$$

Milestones (the steps of the paper's proof)

1. Display (7): $h^{si\prime}(v_j)=J(v_j)f(v_j)+N(v_j)g(v_j)$ for $v_j>0$, with the paper's functions $J,f,N,g$.
2. $J(v_j)>0$ and $N(v_j)<0$ for $v_j>0$.
3. $f$ is nondecreasing and $g$ is nonincreasing on $(0,\infty)$.
4. Display (8), corrected: $h^{si\prime}(v_j)=\dfrac{e^{-\lambda(v_j+V_S)}}{(v_j+V_S)^2}\bigl[V_S D(v_j)f(v_j)-K(v_j)g(v_j)\bigr]$.
5. $D$ and $K$ are positive and strictly increasing on $[0,\infty)$, and so is $K/D$.
6. Display (12): $2-2e^{-t}-te^{-t}-t<0$ for $t=\lambda(v_j+V_S)>0$.

Significance

Quasi-convexity of $h^{si}$ says that a variant is worth adding, if at all, at an extreme of its popularity. The paper uses it to conclude that, as without search, the optimal assortment under independent-assortment search lies among the popular assortments, the sets of the $k$ most preferred variants. This reduces assortment optimization to $n$ candidates. The paper also shows that the conclusion fails in its overlapping-assortment model, so the independent-assortment case marks where this structural result survives the addition of search.

The result is proved in the paper; none of it has a machine-checked proof. The paper's proof contains gaps that a formalization must close: several sign and monotonicity facts are asserted without proof ("It can be shown", "by a similar argument as in Theorem 4"), display (8) is printed without a factor $V_S$, and the step from (10) to (11) rests on an inequality asserted without the full expression. A complete formal proof of Theorem 5 therefore also fixes the argument.

Difficulty

The no-search analogue (Theorem 4) is easy: the numerator of $h^{m\prime}$ is increasing, so $h^{m\prime}$ changes sign at most once. Here the search factor $1-e^{-\lambda(v_j+V_S)}$ depends on $v_j$, and the derivative splits as $Jf+Ng$ with $J>0$, $N<0$, $f$ nondecreasing and $g$ nonincreasing, but neither $J$ nor $N$ is monotone. So the argument used for Theorem 4 no longer applies, and when $f\ge 0$ and $g\ge 0$ the derivative cannot be written as a positive factor times a monotone one. The proof needs a separate second-order argument at critical points in that case. Showing only that $h^{si\prime}$ has at most one zero is also not enough: it must change sign from negative to positive.

Formalization scope

• Variants are Fin n (0-based); the no-purchase option is a separate real v0 > 0, not an element of Fin n. All preferences are positive. The MNL probability is the published RetailVariety.Structure.share, referenced, not redefined.
• One margin $m\in\mathbb R$ for every variant, including $j$. The paper's model allows per-variant margins, but its proof of Theorem 5 writes a single $m$ throughout. With unequal margins the statement is false: one variant $i\in S$ with $v_i=0.76202736$, $v_0=0.021273423$, $c(q)=0.38165308\,q^{0.59833805}$, $m_j=5.4080321$, $m_i=6.1078441$, $\lambda=2.6494844$ gives an $h^{si}$ that rises to about $0.246$ near $v_j\approx1.0$, falls to about $0.152$ near $v_j\approx15.9$, and rises again.
• $c:\mathbb R\to\mathbb R$ is concave and monotone on $[0,1]$ (all demands lie in $[0,1)$) and, in addition to the paper's assumptions, twice continuously differentiable on $(0,1)$, because the proof uses $c'$ and $c''$. The milestones use only differentiability where they need it. $c'$ is Mathlib's deriv c. The value $c(0)$ is unconstrained; $h^{si}(0)=-c(0)$.
• $\lambda>0$ is a free parameter; $\mu$, $\gamma$ and $\bar U$ enter only through it.
• Adding $j$ with preference $x$ is Function.update v j x on insert j S, with $j\notin S$. Quasi-convexity is Mathlib's QuasiconvexOn ℝ (Set.Ici 0).
• The following formalizations would trivialize or change the theorem and are ruled out: demand without the factor $1-H$ (that is Theorem 4); evaluating $H$ at $S$ instead of $S_j$ inside $\pi_i^{si}(v_j)$; convexity in place of quasi-convexity; a specific cost function such as $\nu q^\beta$ or a linear cost.
• The definitions (search-adjusted MNL demand, profit-change function) are reusable for the paper's other results. Proofs of the asserted lemmas (milestones 2, 3, 5) and of the corrected (8) are welcome independently of the goal.

Selected references

• G. P. Cachon, C. Terwiesch, Y. Xu, Retail Assortment Planning in the Presence of Consumer Search, Wharton working paper, December 20, 2002. UPenn repository. Published version: Manufacturing & Service Operations Management 7(4), 2005, 330–346. doi:10.1287/msom.1050.0088
• G. van Ryzin, S. Mahajan, On the Relationship Between Inventory Costs and Variety Benefits in Retail Assortments, Management Science 45(11), 1999, 1496–1509. doi:10.1287/mnsc.45.11.1496
• D. McFadden, Conditional Logit Analysis of Qualitative Choice Behavior, in P. Zarembka (ed.), Frontiers in Econometrics, Academic Press, 1974, 105–142.