Answer: Polynomial-time solvable for binary-encoded rational inputs.
Theorem 3.1 — class: hardness
PDF text-layer excerpt — equations and symbol order may be approximatePROP-CFD is NP-complete even if G is a path.
statement extracted from the paper’s text layer; consult the paper for the exact wording
Given a path \(P=(V,E)\), complete valuation types \(T\), rational masses \(\mu_t\) with \(\sum_t\mu_t=1\), and replicated per-capita supply, decide whether there are variables \(x_{t,I}\ge 0\) for integral intervals \(I\subseteq V\) such that \(\sum_I x_{t,I}=\mu_t\), \(\sum_{t,I\ni v}x_{t,I}\le\beta_v\), and \(x_{t,I}>0\Rightarrow u_t(I)\ge\rho\). In the uniform replication of a finite \(n_0\)-agent instance, take \(K\) path copies and \(K\) population copies, scale item utilities by \(1/K\), and set \(\beta_v=\rho=1/n_0\), so the finite quota \(1/(Kn_0)\) becomes the mass-limit quota \(\rho\).
Given a path \(P=(V,E)\), rational per-item supplies \(\beta_v\), a threshold \(\rho\), and finitely many valuation types \(T\) with rational masses \(\mu_t\ge 0\), \(\sum_{t\in T}\mu_t=1\), each type \(t\) has an additive rational valuation \(u_t\) on subsets of \(V\). An integral interval is a connected subset of \(P\). Decide whether there are \(x_{t,I}\ge0\) such that \(\sum_I x_{t,I}=\mu_t\) for every \(t\), \(\sum_{t,I\ni v}x_{t,I}\le\beta_v\) for every \(v\), and \(x_{t,I}>0\Rightarrow u_t(I)\ge\rho\).
Target: Is this continuous proportional connected-allocation problem on paths solvable in polynomial time, or is it NP-hard?
Nearest known results: For indivisible items with normalized additive utilities, deciding whether agents can receive pairwise disjoint connected path intervals each worth at least \(1/n\) is NP-complete. No result for the continuous mass-allocation problem above was verified.
The problem is solvable in polynomial time, under the standard assumption that the threshold \(\rho\), like the other numerical inputs, is rational and encoded in binary.
The key fact is that a path has only quadratically many connected subsets. Thus the stated problem can be written explicitly as a rational linear-programming feasibility problem of polynomial size.
Write the vertices in path order as \(v_1,\ldots,v_n\), and let \(k=|T|\). Every nonempty connected subset is uniquely an interval
\[
I_{i,j}=\{v_i,v_{i+1},\ldots,v_j\},
\qquad 1\le i\le j\le n.
\]
There are exactly \(n(n+1)/2\) such intervals.
For each type \(t\), write \(a_{t,\ell}=u_t(\{v_\ell\})\). Additivity gives
\[
u_t(I_{i,j})=\sum_{\ell=i}^{j}a_{t,\ell}.
\]
Compute the set of eligible intervals
\[
A_t=\left\{(i,j):1\le i\le j\le n,\
\sum_{\ell=i}^{j}a_{t,\ell}\ge\rho\right\}.
\]
Introduce one real variable \(y_{t,i,j}\) for each \(t\in T\) and \((i,j)\in A_t\). Test feasibility of the following linear system:
\[
y_{t,i,j}\ge 0
\qquad
(t\in T,\ (i,j)\in A_t),
\]
\[
\sum_{(i,j)\in A_t}y_{t,i,j}=\mu_t
\qquad (t\in T),
\]
\[
\sum_{t\in T}
\sum_{\substack{(i,j)\in A_t\\ i\le \ell\le j}}
y_{t,i,j}\le\beta_{v_\ell}
\qquad (1\le\ell\le n).
\]
An empty sum is zero. In particular, a type with positive mass and no eligible interval makes the system infeasible.
Suppose first that the original allocation variables \(x_{t,I}\) are feasible. If \(u_t(I)<\rho\), the implication in the question rules out \(x_{t,I}>0\). Since \(x_{t,I}\ge0\), necessarily \(x_{t,I}=0\).
Consequently, setting \(y_{t,i,j}=x_{t,I_{i,j}}\) for eligible intervals preserves every type’s total mass and every vertex’s total consumption. These variables satisfy the constructed linear system.
Conversely, suppose the constructed system has a feasible solution. Set \(x_{t,I_{i,j}}=y_{t,i,j}\) for eligible intervals and set \(x_{t,I_{i,j}}=0\) for all other intervals. The linear constraints give the required mass equalities and supply inequalities. Every positive variable corresponds to an eligible interval, so its value is at least \(\rho\). Thus the original allocation is feasible.
The two feasibility questions are therefore equivalent.
Let \(L\) be the total binary input length. Each interval value is a sum of at most \(n\) input rationals. Such a sum has polynomial encoding length: using the product of the denominators as a common denominator yields numerator and denominator bit lengths bounded by \(O(nL+\log n)\). Exact comparisons with rational \(\rho\) therefore take polynomial time. Enumerating and testing all \(k n(n+1)/2\) type–interval pairs is polynomial.
The resulting linear system has at most \(k n(n+1)/2\) variables, \(k\) mass equalities, and \(n\) supply inequalities, in addition to nonnegativity. All matrix entries are zero or one, and the right-hand sides are input rationals. Even a dense encoding of this system has polynomial length.
The polynomial-time theorem for rational linear programming states that feasibility of a finite system of linear equalities and inequalities with binary-encoded rational coefficients can be decided in time polynomial in its encoding length. All its hypotheses hold here. Applying that theorem gives an exact polynomial-time decision algorithm.
This reasoning does not require nonnegative valuations or normalization. If the empty set is also permitted as an interval, adding one eligible empty-interval variable per type when \(0\ge\rho\) preserves the same conclusion.
The cited indivisible problem imposes discrete choices and pairwise disjointness. Here each type’s mass may be divided among eligible intervals, and vertex usage is constrained by linear inequalities. The explicit linear program above fully captures those continuous requirements, so hardness of the indivisible variant does not establish hardness of this problem.
⟨structured verdict parsed — rendered above⟩
The prover’s polynomial-time conclusion is correct for explicitly represented rational inputs, including a binary-encoded rational threshold. The argument fully resolves that formulation of the task. No substantive gaps or errors were found.
The prover explicitly assumes that \(\rho\) is rational and binary encoded. This is appropriate for the stated rational-input complexity problem. Since USER_TASK does not explicitly specify the threshold’s encoding, the conclusion should be understood under this declared assumption. An arbitrarily represented real threshold would require a computational model that USER_TASK does not provide.
For a path with \(n\) vertices, every nonempty connected vertex subset is uniquely a consecutive interval \(I_{i,j}\), with \(1\le i\le j\le n\). The count \(n(n+1)/2\) is correct. Finding a path order from an explicitly supplied path takes polynomial time and presents no missing mathematical step.
Additivity justifies computing each interval’s value by summing its singleton values. The condition defining \(A_t\) uses the required weak inequality, so intervals valued exactly at \(\rho\) are correctly included. Negative singleton values cause no difficulty: the argument enumerates all intervals and makes no monotonicity assumption.
The variables represent exactly the eligible type–interval pairs. The mass equations and supply inequalities reproduce the original constraints, including the fact that interval mass consumes that amount of supply at every vertex in the interval. There are no discrete choices or additional consistency conditions in USER_TASK that the construction omits.
For an ineligible interval, the original implication and nonnegativity force \(x_{t,I}=0\). Removing those variables therefore preserves all mass equalities and supply inequalities. The proposed restriction to eligible variables is valid.
Extending a feasible linear-program solution by assigning zero to every ineligible interval preserves all required linear constraints. Every positive allocation variable then belongs to an interval whose valuation meets the threshold. This establishes the reverse implication.
The sentence “Every positive variable corresponds to an eligible interval, so its value is at least \(\rho\)” is understood as referring to the interval’s valuation. The surrounding definition makes this meaning clear; the argument does not require the allocation variable itself to exceed \(\rho\).
Each interval value sums at most \(n\) input rationals. The stated bound \(O(nL+\log n)\) on numerator and denominator bit lengths is valid, although loose. Products of denominators and the corresponding numerator sums have polynomial bit length, so exact threshold comparisons take polynomial time.
For explicitly represented vertices and types, both \(n\) and \(k\) are bounded polynomially by the input length. Consequently, enumerating the \(kn(n+1)/2\) candidate pairs is polynomial.
The claimed variable and constraint counts are correct. The displayed coefficient matrix has entries in \(\{0,1\}\), and its right-hand sides are input rationals. Nonnegativity can be represented as variable bounds or additional rational inequalities. Even a dense representation has polynomial encoding length.
The prover states the relevant theorem precisely enough: feasibility of a finite rational linear system can be decided in time polynomial in its binary encoding length. The constructed system satisfies its hypotheses. Equalities, unrestricted signs of right-hand sides, and possible infeasibility are all covered. The theorem supplies an exact decision procedure, so numerical approximation is not an unresolved issue.
Empty eligible sets are handled explicitly. Positive mass then makes the relevant equation infeasible, while zero mass is compatible with an empty sum. Zero supplies and negative valuations require no modifications. The optional empty interval is also handled correctly: its additive valuation is zero, and it consumes no vertex supply. This covers the possible convention concerning whether empty intervals are allowed.
The distinction is sound. USER_TASK allows continuous splitting of each type’s mass and imposes aggregate supply inequalities. The cited indivisible hardness result therefore does not contradict the polynomial-size linear-program formulation.
The proof establishes an exact polynomial-time algorithm for the intended rational-input problem. No repair is necessary. The rational encoding assumption for the threshold should remain explicit whenever the conclusion is restated.
⟨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.