← back to the atlas

Truthful and Welfare-maximizing Resource Scheduling with Application to Electric Vehicles (aamas25-00021)

Answer: Polynomial-time solvable.

The anchor (named result in the paper)

Theorem 1 — class: hardness

PDF text-layer excerpt — equations and symbol order may be approximateFor monotone valuations and for a given 𝐾, the de- cision problem of whether the optimal allocation to the EV charging problem has a social welfare of at least 𝐾 is NP-complete even when the number of outlets |𝑀| = 1. Given the above result, the VCG mechanism is intractable for our setup. Thus, we focus on providing mechanisms that maximize social welfare approximately. In particular, we provide randomized mechanisms that ensure DSIC and IR, and approximate the social welfare to within a factor of 𝑂( √︁ |𝑆|) for multiple outlets and to within a factor of 2 for the single outlet case.

statement extracted from the paper’s text layer; consult the paper for the exact wording

The continuous mirror question, as graded

Given a finite set of complete valuation types \(\mathcal T\), rational masses \(\mu_t\) with \(\sum_{t\in\mathcal T}\mu_t=1\), rational normalized capacities \(\kappa_{jk}\), and monotone rational valuations \(\theta_t:B\to\mathbb Q_{\ge 0}\), where \(B\) is the paper's set of contiguous single-outlet bundles, compute a mass allocation \(x_{t,b}\ge 0\) maximizing \(W(x)=\sum_{t\in\mathcal T}\sum_{b\in B}\theta_t(b)x_{t,b}\), subject to \(\sum_{b\in B}x_{t,b}\le\mu_t\) and \(\sum_{t\in\mathcal T}\sum_{b\in B_{jk}}x_{t,b}\le\kappa_{jk}\) for every slot–outlet pair \((j,k)\); equivalently, decide whether the optimum is at least \(K\), with \(|M|=1\) as the Theorem 1 restriction.

Packaged proof task (what the prover saw — nothing else)

Let \(S=\{1,\ldots,s\}\), with \(s\ge1\), be ordered time slots and \(M=\{1\}\) the single outlet; write \(m=|M|=1\). A bundle is either \(\varnothing\) or \(([a,c],1)\), occupying all slots \(a,\ldots,c\), where \(1\le a\le c\le s\). Let \(B\) contain these bundles and \(B_{j1}\) contain those occupying slot \(j\).
A society is given by its support: the list of the \(\tau\) types with positive mass, each with its mass as a binary rational. Here \(\tau\) is the support size, not the number of possible types, and \(\sum_t\mu_t=1\).
Each type explicitly lists its complete valuation table \(\theta_t:B\to\mathbb Q_{\ge0}\), with \(\theta_t(\varnothing)=0\) and \(\theta_t(b')\le\theta_t(b)\) whenever \(b'\subseteq b\). Inputs also include binary rational capacities \(\kappa_{j1}\in[0,1]\) and threshold \(K\in\mathbb Q\); let \(L\) be the total input bit length.
An allocation consists of divisible masses \(x_{t,b}\ge0\), with \(\sum_{b\in B}x_{t,b}\le\mu_t\) for every type and \(\sum_t\sum_{b\in B_{j1}}x_{t,b}\le\kappa_{j1}\) for every slot. Unallocated mass is permitted. Its welfare is \(W(x)=\sum_t\sum_{b\in B}\theta_t(b)x_{t,b}\).

Is deciding whether \(\max_x W(x)\ge K\) solvable in polynomial time, or is it NP-hard? State running times in \(m,\tau,s,L\).

For discrete agents, welfare-threshold decision with monotone valuations is NP-complete even with one outlet. [Source](https://www.cse.iitb.ac.in/~swaprava/papers/welfareEV.pdf).
For fractional allocations with every agent bound and slot capacity equal to one, polynomial-time welfare maximization is established; this differs from the arbitrary rational mass and capacity inputs above. [Source](https://www.cse.iitb.ac.in/~swaprava/papers/welfareEV.pdf).

Modeling choices made when packaging the task

Prover output (gpt-6.1-sol / high, Bolzano prover prompt)

Result

The decision problem is polynomial-time solvable. Arbitrary binary rational masses and capacities remain valid right-hand sides of a polynomial-size rational linear program.

For the stated case \(m=1\), the running time is
\(\operatorname{poly}(\tau s^2,\tau+s,L)\) bit operations, hence polynomial in \(L\). More generally, with \(m\) outlets and bundles consisting of an interval at one outlet, the same argument gives
\(\operatorname{poly}(\tau m s^2,\tau+ms,L)\).

1. An exact linear formulation

Index the explicitly listed support types by \(t\in\{1,\ldots,\tau\}\). There are exactly
\(q=s(s+1)/2\) nonempty bundles.

We may set \(x_{t,\varnothing}=0\) for every type: doing so preserves welfare, because \(\theta_t(\varnothing)=0\), and can only relax the type constraints. Conversely, an allocation on nonempty bundles extends to an allocation in the original model by assigning zero mass to the empty bundle.

Write \(y_{t,a,c}=x_{t,([a,c],1)}\) and \(v_{t,a,c}=\theta_t(([a,c],1))\). Consider the following rational linear feasibility problem:

\( \begin{aligned} y_{t,a,c}&\ge 0 &&\text{for all }t,\ 1\le a\le c\le s,\\ \sum_{1\le a\le c\le s}y_{t,a,c}&\le\mu_t &&\text{for all }t,\\ \sum_{t=1}^{\tau}\ \sum_{1\le a\le j\le c\le s}y_{t,a,c}&\le\kappa_{j1} &&\text{for all }j\in\{1,\ldots,s\},\\ \sum_{t=1}^{\tau}\ \sum_{1\le a\le c\le s}v_{t,a,c}y_{t,a,c}&\ge K. \end{aligned} \)

The first three families are exactly the allocation constraints after removing the empty bundle. The last inequality is exactly the requested welfare threshold.

To justify the use of a maximum, let \(P\) denote the feasible set defined by the first three families. It is nonempty because the zero allocation belongs to it. It is closed, being the intersection of finitely many closed half-spaces. Furthermore, nonnegativity and the type constraints imply \(0\le y_{t,a,c}\le\mu_t\), so \(P\) is bounded. Consequently, \(P\) is compact, and its continuous linear welfare function attains its maximum.

It follows that the displayed system is feasible if and only if \(\max_x W(x)\ge K\).

2. Polynomial bit complexity

We use the standard rational linear programming theorem: feasibility of a finite system of linear inequalities with binary rational coefficients can be decided exactly in time polynomial in its dimensions and total binary encoding length. This is the polynomial-time feasibility result underlying [Khachiyan’s linear programming algorithm](https://www.mathnet.ru/eng/dan42319).

Here its hypotheses hold:

A dense encoding of these \(r\) rows has length \(O(nr+L)\), up to harmless encoding overhead. If nonnegativity is also represented as explicit rows, it adds \(O(n^2)\) bits. Thus the entire system has polynomial encoding length and can be constructed in polynomial time.

Applying exact rational feasibility therefore gives the bound
\(\operatorname{poly}(\tau s^2,\tau+s,L)\) bit operations. In particular, it resolves equality at the threshold; an approximate optimum is unnecessary.

Because each type explicitly supplies all \(q\) nonempty-bundle valuations, the input length satisfies \(L=\Omega(\tau q)\). The capacities are also explicitly listed. Hence all the dimensions above are polynomially bounded in \(L\), establishing polynomial-time solvability in the ordinary binary input model.

For the analogous \(m\)-outlet model, there are \(mq\) nonempty bundles, \(n=\tau mq\) variables, and \(r=\tau+ms+1\) inequalities apart from nonnegativity. The same encoding and theorem give
\(\operatorname{poly}(\tau m s^2,\tau+ms,L)\) bit operations.

3. Why the cited hardness does not apply

The cited paper distinguishes discrete allocations from their fractional relaxation and explicitly solves the latter by a polynomial-size linear program; see its Equation (3) and accompanying discussion. [Source](https://www.cse.iitb.ac.in/~swaprava/papers/welfareEV.pdf)

The present model directly permits nonnegative fractional masses. Replacing unit bounds by the rational values \(\mu_t\) and \(\kappa_{j1}\) changes only the right-hand sides of that linear formulation. Rational linear programming does not require those bounds to equal one.

The proof requires neither integrality nor monotonicity of valuations. It therefore establishes the result for all inputs in the question, including the stipulated monotone valuations.

⟨structured verdict parsed — rendered above⟩

Adversarial review (gpt-6.1-sol / medium, Bolzano verifier prompt)

The prover resolves the assigned problem correctly. The reduction to exact rational linear feasibility is valid, and the stated running times are polynomial in the explicit input size. No major or minor issues were found.

For each start slot \(a\), there are \(s-a+1\) possible end slots. Thus the stated count \(q=s(s+1)/2\) is correct.

Setting \(x_{t,\varnothing}=0\) preserves welfare because \(\theta_t(\varnothing)=0\), decreases or preserves each type’s allocated mass, and does not affect slot occupancy. Conversely, assigning zero to the empty bundle extends every feasible allocation on nonempty bundles to the original model. This establishes equivalence for the welfare-threshold question.

The variables \(y_{t,a,c}\) index precisely the nonempty bundles for every explicitly listed support type.

The type inequality sums over all bundles available to that type and uses the correct bound \(\mu_t\). The slot inequality sums exactly those intervals satisfying \(a\le j\le c\), with capacity \(\kappa_{j1}\). Nonnegativity and the welfare inequality also match the task exactly.

In particular, the formulation permits splitting a type’s mass among multiple bundles and leaving mass unallocated, as required. It imposes no discrete allocation restriction.

The zero allocation is feasible because all masses and capacities are nonnegative. The feasible set is closed, and each coordinate satisfies \(0\le y_{t,a,c}\le\mu_t\), so it is bounded. Compactness and continuity therefore justify attainment of the maximum.

Consequently, feasibility of the system including the welfare inequality is equivalent to \(\max_x W(x)\ge K\). This remains valid at equality; no approximation argument is used.

The prover states the required theorem precisely enough: feasibility of an explicitly encoded finite system of binary rational linear inequalities is decidable exactly in polynomial bit complexity.

Its hypotheses are satisfied. Every coefficient and right-hand side is rational; the system is finite and explicitly constructible; and the input supplies every welfare coefficient. The theorem does not require integral bounds, unit capacities, strict feasibility, or a full-dimensional feasible region.

The attribution to [Khachiyan’s polynomial linear programming result](https://www.mathnet.ru/eng/dan42319) is appropriate. No stronger or specialized theorem is needed.

The counts \(n=\tau s(s+1)/2\) and \(r=\tau+s+1\), excluding nonnegativity inequalities, are correct.

A dense representation requires polynomial space: allocation coefficients contribute \(O(nr)\) constant-size entries, while valuation coefficients and right-hand sides are supplied by the input. Explicit nonnegativity rows add \(O(n^2)\) entries. Routine encoding overhead does not change polynomiality.

The complete valuation tables give \(L=\Omega(\tau q)\). Also, \(\tau\ge1\) follows from positive support masses summing to one, and \(q\ge s\) for \(s\ge1\). Thus the dimensions and the constructed system’s encoding length are polynomially bounded in \(L\).

The resulting bound \(\operatorname{poly}(\tau s^2,\tau+s,L)\) bit operations is justified. For the explicitly described extension to \(m\) outlets, the counts \(\tau mq\) variables and \(\tau+ms+1\) allocation and threshold inequalities likewise justify \(\operatorname{poly}(\tau ms^2,\tau+ms,L)\).

The argument covers \(s=1\), zero capacities, zero valuations, and arbitrary rational thresholds, including negative thresholds. None creates an omitted case.

Equation (3) of the [cited scheduling paper](https://www.cse.iitb.ac.in/~swaprava/papers/welfareEV.pdf) indeed gives a fractional LP with unit agent bounds and slot capacities and discusses polynomial-time solution. The prover correctly explains that arbitrary rational masses and capacities change only the right-hand sides.

Monotonicity is unnecessary for this LP argument, so its absence from the proof’s deductions is legitimate. The discrete hardness result does not undermine the continuous classification.

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.