Answer: Polynomial-time solvable in \(m,\tau,L\), with an exact rational optimal allocation and welfare.
Theorem 3 — class: hardness
PDF text-layer excerpt — equations and symbol order may be approximateMIA is NP-complete. However, it is possible to find an approximately efficient allocation in polynomial time that is truthful and individually rational.
statement extracted from the paper’s text layer; consult the paper for the exact wording
Given \(m\) slots, a rational distribution \(\mu\) over \(\tau\) supported complete job types \(t=(\ell_t,v_{t1},\ldots,v_{tm})\), and rational per-capita slot capacity \(\kappa\), choose nonnegative masses \(x_{tj}\), for \(1\le j\le m-\ell_t+1\), maximizing \(\sum_t\sum_{j=1}^{m-\ell_t+1}v_{tj}x_{tj}\), subject to \(\sum_j x_{tj}\le\mu_t\) for every \(t\) and \(\sum_t\sum_{j:\,j\le s\le j+\ell_t-1}x_{tj}\le\kappa\) for every slot \(s\). Each scheduled unit of mass receives one whole contiguous job block; unscheduled mass is allowed.
A society is given by its support: a list of \(\tau\ge1\) complete job types \(t=(\ell_t,v_{t1},\ldots,v_{tm})\), each with positive binary rational mass \(\mu_t\), with \(\sum_t\mu_t=1\). Here \(\tau\) is the support size, not the number of possible types.
There are \(m\ge1\) slots, positive rational per-capita capacity \(\kappa\), positive integer lengths \(\ell_t\), and nonnegative rational valuations. Let \(J_t=\{j\in\mathbb Z:1\le j\le m-\ell_t+1\}\); valuations at starts outside \(J_t\) are zero.
An allocation chooses real masses \(x_{tj}\ge0\) for \(j\in J_t\). Each scheduled unit receives exactly one whole contiguous block of length \(\ell_t\); a type's mass may be split among different starts. Unscheduled mass has value zero.
Maximize \(\sum_t\sum_{j\in J_t}v_{tj}x_{tj}\), subject to \(\sum_{j\in J_t}x_{tj}\le\mu_t\) for every type and \(\sum_t\sum_{j\in J_t:\,j\le s\le j+\ell_t-1}x_{tj}\le\kappa\) for every slot \(s\). Empty sums are zero.
Let \(L\) be the total binary input bit length; state running times in \(m,\tau,L\).
Is exact welfare maximization for this continuous allocation problem solvable in polynomial time in \(m,\tau,L\), or is it NP-hard?
The discrete counterpart, with individual jobs and integer slot capacity, is reported as NP-complete in [Social Distancing via Social Scheduling](https://www.cse.iitb.ac.in/~swaprava/papers/social_distancing_AAMAS23.pdf). The checked source does not establish a complexity result for this distribution-over-types version.
Exact welfare maximization is solvable in polynomial time in \(m,\tau,L\). An algorithm can output both an optimal allocation and its welfare as exact rational numbers.
The essential point is that the permitted splitting of type mass makes the stated problem itself a rational linear program.
Define the set of valid type–start pairs by
\(I=\{(t,j):1\le t\le\tau,\ j\in J_t\}\),
and let
\(N=|I|=\sum_{t=1}^{\tau}\max\{0,m-\ell_t+1\}\le\tau m\).
If \(N=0\), no type fits within the horizon, and the empty allocation has optimal welfare zero. Henceforth assume \(N>0\).
Introduce one real variable \(x_{tj}\) for each \((t,j)\in I\). Define a matrix \(A\) with \(\tau+m\) rows and \(N\) columns. Its type rows have entries
\(A_{t,(u,j)}=\mathbf{1}_{\{t=u\}}\),
and its slot rows have entries
\(A_{\tau+s,(u,j)}=\mathbf{1}_{\{j\le s\le j+\ell_u-1\}}\).
Let
\(b=(\mu_1,\ldots,\mu_\tau,\underbrace{\kappa,\ldots,\kappa}_{m\text{ entries}})\),
and let \(c_{(t,j)}=v_{tj}\). The linear program is
\(\displaystyle \max\{c^{\mathsf T}x:Ax\le b,\ x\ge0\}.\)
This formulation is exact:
Thus every allocation in the question gives a feasible vector with identical welfare, and every feasible vector specifies an allocation permitted by the question. In particular, splitting mass among starts does not split any scheduled unit’s block: each variable already corresponds to one whole contiguous block.
There are \(N\le\tau m\) variables, \(\tau+m\) resource inequalities, and \(N\) nonnegativity inequalities.
Every constraint coefficient belongs to \(\{-1,0,1\}\), when nonnegativity is written explicitly. Every other coefficient is a rational number appearing in the input. Consequently, a conservative bound on the total binary encoding length \(B\) of a dense LP representation is
\(\displaystyle B=O\bigl((m+\tau+N)(N+L+1)\bigr).\)
Indeed, the constraint matrix has at most \((m+\tau+N)N\) constant-size entries; the right-hand side and objective have at most \(m+\tau+2N\) rational entries, each of bit length at most \(L\). Dimension information also fits within this bound.
The matrix can be constructed in polynomial time by testing the defining type and interval conditions. Lengths exceeding \(m\) produce no variables; their binary magnitudes do not require iteration up to those lengths.
The standard rational linear-programming theorem gives an algorithm that, for a binary-encoded rational LP, detects infeasibility or unboundedness, or returns an exact rational optimum, in a number of bit operations polynomial in its encoding length. Exact polynomial-time algorithms are discussed explicitly in Section 1.3 of [*Linear Programming using Limited-Precision Oracles*](https://optimization-online.org/wp-content/uploads/2019/12/7507.pdf).
Applying this theorem gives running time
\(\displaystyle \operatorname{poly}\bigl((m+\tau+\tau m)(\tau m+L+1)\bigr)=(m+\tau+L)^{O(1)}.\)
This is a polynomial bound in the requested parameters.
The theorem’s hypotheses hold: the LP is explicit and all its coefficients are rational.
Its feasible region is nonempty because \(x=0\) satisfies every constraint. Moreover, nonnegativity and the type constraint imply
\(\displaystyle 0\le x_{tj}\le\sum_{j'\in J_t}x_{tj'}\le\mu_t\le1.\)
The feasible region is therefore closed and bounded, hence compact. The linear objective attains a finite maximum.
An optimal vertex exists by the standard vertex theorem for linear programming. Its coordinates are rational: a vertex is uniquely determined by a full-rank collection of active constraints, and solving that rational linear system yields rational coordinates. The exact LP algorithm returns an optimal rational vector with polynomial encoding length. Evaluating \(c^{\mathsf T}x\) using rational arithmetic then gives the exact optimal welfare in polynomial time.
The discrete formulation in [*Social Distancing via Social Scheduling*, Equation (5)](https://www.cse.iitb.ac.in/~swaprava/papers/social_distancing_AAMAS23.pdf) requires binary allocation variables. The present formulation permits real masses and imposes no corresponding integrality restriction.
Polynomial-time solvability here follows directly from those continuous allocation rules. It requires no claim that the LP’s optimal allocation is integral, and the reported discrete complexity result does not change this conclusion.
⟨structured verdict parsed — rendered above⟩
The prover resolves the assigned continuous problem correctly. The LP represents exactly the permitted allocations, has polynomial encoding length, and admits an exact rational optimum computable in polynomial time. No major or minor mathematical issues were found.
The index set \(I\) includes exactly the permitted type–start pairs. Because each length is a positive integer, the number of valid starts for type \(t\) is \(\max\{0,m-\ell_t+1\}\), so the stated bound \(N\le\tau m\) is correct.
The case \(N=0\) is handled correctly: there are no permitted allocation variables, and welfare is zero. Types with \(\ell_t>m\) contribute no variables even when other types fit.
Each type row sums precisely the scheduled mass of that type. Each slot row sums precisely the masses assigned to blocks covering that slot. The right-hand sides match the type masses and per-capita capacity in the task.
The objective contains exactly the specified valuations at valid starts. Nonnegativity and the type inequalities permit unscheduled mass and splitting among starts.
Both directions of the claimed correspondence hold. An allocation gives a feasible LP vector with the same welfare, and a feasible vector gives an allocation allowed by the task. Each variable represents mass receiving a whole block; allowing real variable values does not introduce partial blocks.
The counts of variables, resource inequalities, and nonnegativity inequalities are correct. With nonnegativity written explicitly, all matrix entries belong to \(\{-1,0,1\}\).
The dense matrix contains at most \((m+\tau+N)N\) entries. The stated count of right-hand-side and objective entries is a valid conservative bound. Repeating \(\kappa\) for every slot is accounted for by bounding each rational entry’s bit length by \(L\).
Consequently,
\(B=O((m+\tau+N)(N+L+1))\)
is valid. Dimension metadata also fits within this bound.
Construction requires only polynomially many tests on binary-encoded indices and lengths. The argument correctly avoids iteration up to a length exceeding \(m\). It therefore establishes polynomial construction time in \(m,\tau,L\).
The prover states the relevant theorem with its input condition, possible outcomes, exactness guarantee, and bit-complexity guarantee. Its application is valid: the constructed LP is explicit, finite-dimensional, and rational.
The cited Section 1.3 does discuss exact polynomial-time algorithms for rational LPs, including recovery of exact rational solutions. The citation supports the exact-output claim, rather than merely approximate optimization. [*Linear Programming using Limited-Precision Oracles*, Section 1.3](https://optimization-online.org/wp-content/uploads/2019/12/7507.pdf).
Substituting \(N\le\tau m\) into the encoding bound yields the claimed polynomial running time. The expression \((m+\tau+L)^{O(1)}\) is a valid summary. No strongly polynomial running-time claim is made or needed.
The zero vector is feasible because every resource bound is positive.
For every existing variable, nonnegativity and its type constraint imply
\(0\le x_{tj}\le\sum_{j'\in J_t}x_{tj'}\le\mu_t\le1\).
The final inequality follows from the positive masses summing to one.
The feasible region is an intersection of finitely many closed halfspaces and is bounded by these coordinate bounds. Thus the compactness and attainment claims are correct. This reasoning also covers zero valuations, redundant constraints, and arbitrary positive rational capacities.
The vertex theorem applies to the nonempty bounded polyhedron established in the preceding paragraph: a linear objective attains its maximum at a vertex. No full-dimensionality assumption is required.
The characterization of a vertex by a full-rank collection of active constraints is correct. All active equations have rational coefficients, so the uniquely determined coordinates are rational.
Polynomial output length follows from the invoked exact polynomial-time algorithm. Computing the objective from the resulting polynomial-length rational vector takes polynomial-time rational arithmetic. The output claim therefore includes both an exact optimal allocation and exact welfare.
Equation (5) of the cited scheduling paper explicitly requires binary allocation variables. The prover’s comparison accurately identifies the integrality restriction absent from the continuous task. [*Social Distancing via Social Scheduling*, Equation (5)](https://www.cse.iitb.ac.in/~swaprava/papers/social_distancing_AAMAS23.pdf).
The continuous conclusion does not depend on the correctness of the reported discrete hardness result or on integrality of an LP optimum.
No repair or additional clarification is needed.
⟨structured verdict parsed — rendered above⟩
Tier: machine-proved, adversarially reviewed by an independent model. No human has checked this proof. Generated from pipeline artifacts by tools/atlas_build.py.