Answer: Polynomial-time solvable; a rational EF1 allocation can be constructed whenever one exists.
Theorem 4.3 — class: algorithmic
PDF text-layer excerpt — equations and symbol order may be approximateThe moving-knife protocol finds an EF1 allocation for three agents and runs in $O(m)$ time, when $G$ is a path.
statement extracted from the paper’s text layer; consult the paper for the exact wording
Given a path \(P=(v_1,\ldots,v_m)\), three complete monotone valuation types \(t\in T\), rational masses \(\mu_t\) with \(\sum_t\mu_t=1\), and rational per-capita supplies \(q_v\), decide whether there exists \(x_{t,B}\ge0\) assigning mass of each type to integral connected intervals \(B\), satisfying \(\sum_B x_{t,B}=\mu_t\), \(\sum_{t,B\ni v}x_{t,B}=q_v\), and \(u_t(B)\ge u_t^-(B')\) whenever \(x_{t,B}>0\) and \(B'\) has positive occupied mass; construct such an allocation when one exists.
Definitions. Let \(P=(v_1,\ldots,v_m)\) be a path and let \(T=\{1,2,3\}\). Each type \(t\) has a monotone valuation \(u_t\), given by a rational table on all nonempty intervals \(B\) of \(P\), with \(u_t(\varnothing)=0\). Define \(u_t^-(B)=\min\{u_t(B\setminus\{v\}):v\text{ is an endpoint of }B\}\).
Given rational masses \(\mu_t\geq0\) with \(\sum_t\mu_t=1\) and rational supplies \(q_v\geq0\), an allocation consists of \(x_{t,B}\geq0\) satisfying \(\sum_Bx_{t,B}=\mu_t\) and \(\sum_{t,B\ni v}x_{t,B}=q_v\). It is EF1 if \(u_t(B)\geq u_t^-(B')\) whenever \(x_{t,B}>0\) and \(\sum_s x_{s,B'}>0\).
Target. Is this decision-and-construction problem solvable in polynomial time, or is it NP-hard?
Nearest known result. For the discrete analogue on a path with three agents and monotone valuations, a connected EF1 allocation can be computed in \(O(m)\) time. The stated mass-distribution formulation permits a type's mass to be split among multiple intervals.
Result. The decision-and-construction problem is solvable in polynomial time. The key is that, with three types, one can enumerate all possible triples of maximum reduced valuations among supported bundles. For each triple, feasibility reduces to a rational linear program.
Definitions for the algorithm. Let \(\mathcal I\) be the set of nonempty intervals of the path, and put \(N=|\mathcal I|=m(m+1)/2\). For each type \(t\) and interval \(B\), write \(d_t(B)=u_t^-(B)\). These numbers are computed directly from the input table; for a singleton interval, \(d_t(B)=0\).
For an allocation \(x\), define its global support by
\[
\mathcal S(x)=\left\{B\in\mathcal I:\sum_{s\in T}x_{s,B}>0\right\}.
\]
Because the masses sum to one, every feasible allocation has nonempty global support. Consequently, the three quantities
\[
r_t(x)=\max_{B\in\mathcal S(x)}d_t(B),\qquad t\in T,
\]
are well-defined.
The EF1 condition is equivalent to the following statement: for every type \(t\) and every interval \(B\) with \(x_{t,B}>0\), one has \(u_t(B)\geq r_t(x)\). Indeed, this single inequality is equivalent to all the inequalities \(u_t(B)\geq d_t(B')\) for \(B'\in\mathcal S(x)\).
Algorithm. For each type, form the finite candidate set \(D_t=\{d_t(B):B\in\mathcal I\}\). Enumerate every triple \(r\in D_1\times D_2\times D_3\).
For a fixed triple \(r\), define the globally permitted intervals by
\[
\mathcal G(r)=\{B\in\mathcal I:d_s(B)\leq r_s\text{ for every }s\in T\},
\]
and the permitted type–interval pairs by
\[
\mathcal A(r)=\{(t,B):B\in\mathcal G(r),\ u_t(B)\geq r_t\}.
\]
Test feasibility of the following linear system, whose variables are \(x_{t,B}\) for \((t,B)\in\mathcal A(r)\):
\[
x_{t,B}\geq0\qquad ((t,B)\in\mathcal A(r)),
\]
\[
\sum_{B:(t,B)\in\mathcal A(r)}x_{t,B}=\mu_t
\qquad(t\in T),
\]
\[
\sum_{(t,B)\in\mathcal A(r):v\in B}x_{t,B}=q_v
\qquad(v\in P).
\]
All omitted variables are set to zero. If a system is feasible, return a rational feasible solution. If every system is infeasible, report that no EF1 allocation exists.
Soundness. Suppose the system for a triple \(r\) is feasible, and extend its solution by zero on all omitted pairs. Its equations give exactly the required mass and supply constraints.
Fix any \(t,B,B'\) with \(x_{t,B}>0\) and \(\sum_sx_{s,B'}>0\). The first condition implies \((t,B)\in\mathcal A(r)\), so \(u_t(B)\geq r_t\). The second condition implies that some permitted pair uses \(B'\), hence \(B'\in\mathcal G(r)\). Therefore \(d_t(B')\leq r_t\). Combining these inequalities gives
\[
u_t(B)\geq r_t\geq d_t(B')=u_t^-(B').
\]
Thus the returned allocation is EF1. In particular, the algorithm does not need to enforce that its guessed thresholds are attained.
Completeness. Suppose an EF1 allocation \(x^*\) exists. Set \(r_t=r_t(x^*)\). Each maximum is attained at a supported interval, so \(r_t\in D_t\); the algorithm therefore examines this triple.
Every supported interval \(B\) satisfies \(d_s(B)\leq r_s\) for every type \(s\), and hence belongs to \(\mathcal G(r)\). If \(x^*_{t,B}>0\), EF1 and the characterization above also give \(u_t(B)\geq r_t\). Thus every positive variable of \(x^*\) belongs to \(\mathcal A(r)\). Its coordinates consequently satisfy the linear system for this triple, which must be feasible.
This argument also covers types of mass zero: nonnegativity and their mass equations force all their variables to zero, so no additional envy condition is imposed on them.
Polynomial running time and construction. Each candidate set has at most \(N\) elements, so there are at most \(N^3=O(m^6)\) triples. Each associated linear program has at most \(3N\) variables, \(m+3\) equality constraints, and nonnegativity constraints. Its matrix entries are zero or one, and its right-hand sides are the input rationals \(\mu_t\) and \(q_v\).
We use the standard polynomial-time theorem for rational linear programming: feasibility can be decided, and a rational feasible point produced when one exists, in time polynomial in the binary encoding length of the system. Its hypotheses hold here because every system is explicitly represented, has polynomial dimensions, and has rational data of polynomial encoding length. Computing candidate values and permitted pairs requires only polynomially many comparisons of input rationals. Hence the entire enumeration and construction take polynomial time in the input length.
If the path has no vertices, there are no nonempty intervals, and the mass equations are infeasible because the total mass is one; this degenerate case is handled directly.
The fixed number of types is essential to this running-time argument: with \(k\) types, the same method enumerates up to \(N^k\) threshold vectors.
⟨structured verdict parsed — rendered above⟩
Verdict: proved. The threshold enumeration and linear programming algorithm correctly decides feasibility and constructs a rational EF1 allocation in polynomial time for three types, with bundles taken to be the nonempty intervals specified in the write-up. No mathematical gaps or false steps were found.
A path with \(m\) vertices has exactly \(N=m(m+1)/2\) nonempty intervals. Removing an endpoint leaves either another interval or, for a singleton, the empty set. Thus every \(d_t(B)\) is computable from the supplied table and \(u_t(\varnothing)=0\). The singleton value \(d_t(B)=0\) is correct.
Each candidate value is either zero or a value already present in the input table, so its binary encoding length is polynomially bounded by the input length.
For any feasible allocation, the mass equations imply
\[
\sum_{t\in T}\sum_{B\in\mathcal I}x_{t,B}=1.
\]
Nonnegativity therefore guarantees at least one positive coordinate and hence nonempty global support. Because the interval family is finite, every maximum \(r_t(x)\) exists and is attained.
This reasoning applies when the interval family is nonempty; the prover separately handles the empty path.
For each fixed positive coordinate \(x_{t,B}\), EF1 requires \(u_t(B)\geq d_t(B')\) for every globally supported \(B'\). This is exactly equivalent to
\[
u_t(B)\geq\max_{B'\in\mathcal S(x)}d_t(B')=r_t(x).
\]
The support is global, as required by the original condition. The reformulation preserves the quantifiers, including the restriction to positive coordinates of the comparing type.
The permitted pairs impose both conditions needed for the argument: every interval used has reduced valuation at most \(r_s\) for every type \(s\), and a type may receive positive mass only on an interval valued at least \(r_t\).
Setting omitted variables to zero makes the displayed equations precisely the original mass and supply equations. Empty sums cause no difficulty: they either equal a zero right-hand side or certify infeasibility.
If \(x_{t,B}>0\), then the pair is permitted and \(u_t(B)\geq r_t\). If \(B'\) is globally supported, nonnegativity ensures that some positive coordinate uses \(B'\), so \(B'\in\mathcal G(r)\) and \(d_t(B')\leq r_t\). Consequently,
\[
u_t(B)\geq r_t\geq d_t(B').
\]
This proves every required EF1 inequality.
The observation that guessed thresholds need not be attained is correct: soundness uses only these inequalities, not equality with the actual support maxima.
Given any feasible EF1 allocation, its actual support maxima belong to the candidate sets because they are attained at intervals. For this enumerated triple, every supported interval is globally permitted, and every positive type–interval coordinate satisfies the additional valuation threshold by EF1.
Therefore restricting the allocation to the permitted coordinates preserves all its positive coordinates and all mass and supply equations. The corresponding linear system is feasible. This also establishes completeness if the original feasible allocation has irrational coordinates; rational construction follows from the stated linear programming theorem.
A zero-mass type has every coordinate zero by nonnegativity, so EF1 imposes no comparisons originating from that type. Its presence in the global threshold restrictions does not invalidate completeness, since the actual support maxima still supply an admissible threshold.
Zero supplies and singleton intervals are handled by the same equations and definitions. For an empty path, there are no variables, and the mass equations cannot hold when total mass is one. The prover’s treatment is correct for the nonempty-bundle domain.
There are at most \(N^3\) threshold triples. Each system has at most \(3N\) variables and \(m+3\) equality constraints, together with nonnegativity. The asserted zero–one coefficient structure and rational right-hand sides are correct.
The invoked theorem is stated adequately: rational linear programming feasibility and production of a rational feasible point are polynomial-time operations in the binary encoding length. Its hypotheses are verified for these explicitly represented systems. Forming the systems, comparing valuation thresholds, and enumerating the triples also require polynomial time under the stipulated explicit interval-table encoding.
The final comment about variable numbers of types correctly limits this enumeration argument: its \(N^k\) bound does not itself provide a polynomial-time algorithm when \(k\) varies.
None. The proof establishes both decision and construction, and no additional lemma, clarification, or repair 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.