← back to the atlas

d4-conf-atal-2018-0323 (d4-conf-atal-2018-0323)

Answer: Polynomial-time solvable: the decision problem is in \(\mathrm{P}\).

The anchor (named result in the paper)

Theorem 5.5 — class: algorithmic

PDF text-layer excerpt — equations and symbol order may be approximateThe dynamic target rule is optimal for replacement cost among all Pareto efficient social choice functions. Formally, for any Pareto efficient (possibly not online) social choice function f , any N ⊆N and any θ ∈ΘN , RC(τ,θ) ≤RC(f ,θ).

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

The continuous mirror question, as graded

Given an initial setting \(\alpha\) and a finite-support distribution of rational masses over types \(z=(x_z,A_z)\), where \(x_z\in[0,1]\) and \(A_z\subseteq[H]\), find a schedule \(y_1,\ldots,y_H\) minimizing \(\sum_{t=1}^{H}|y_t-y_{t-1}|\), with \(y_0=\alpha\), subject to \(\min_{z:t\in A_z,\,\mu_z>0}x_z\le y_t\le\max_{z:t\in A_z,\,\mu_z>0}x_z\) for every period with active positive mass; periods with none impose no constraint.

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

Given a positive integer horizon \(H\), let \([H]=\{1,\ldots,H\}\). The facility domain is \([0,1]\), with spatial dimension \(m=1\), and the initial location is a binary rational \(\alpha\in[0,1]\).
A society is given by its support: a list of \(\tau\) types \(z=(x_z,A_z)\) with positive binary rational masses \(\mu_z\) summing to \(1\). Here \(x_z\in[0,1]\) is a binary rational and \(A_z\subseteq[H]\) is encoded by an \(H\)-bit vector; active sets may be empty or nonconsecutive. The parameter \(\tau\) is the support size, not the number of possible types.
A feasible schedule has \(y_0=\alpha\) and \(y_t\in[0,1]\) for every \(t\in[H]\). Whenever \(S_t=\{z:t\in A_z\}\) is nonempty, require \(\min_{z\in S_t}x_z\le y_t\le\max_{z\in S_t}x_z\); an empty \(S_t\) imposes no additional constraint.
Minimize the replacement cost \(\sum_{t=1}^{H}|y_t-y_{t-1}|\). Any minimizing schedule is acceptable; there is no terminal-location requirement. Let \(L\) be the total input bit length, including a binary rational threshold \(B\ge0\), and state running times in \(m,\tau,H,L\).

Is deciding whether a feasible schedule has replacement cost at most \(B\) in \(\mathrm{P}\), or is it \(\mathrm{NP}\)-hard?

For finite populations, an online rule computable in polynomial time minimizes replacement cost over all schedules satisfying these periodwise interval constraints, including offline schedules. [Wada et al., 2018](https://www.ifaamas.org/Proceedings/aamas2018/pdfs/p336.pdf).
No result explicitly addressing the stated distribution input was identified in the literature search.

Modeling choices made when packaging the task

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

Conclusion

The decision problem is in \(\mathrm{P}\). An optimal schedule is obtained by projecting the previous location onto the current feasible interval. This works directly on the support list, regardless of the masses or the shape of the active sets.

The rule agrees with the dynamic target rule of [Wada et al. (2018)](https://www.ifaamas.org/Proceedings/aamas2018/pdfs/p336.pdf). The proof below establishes its optimality for the precise input and constraints in the question.

Algorithm

For each \(t\in[H]\), define the nonempty closed interval
\[ I_t=[\ell_t,u_t] = \begin{cases} [\min_{z\in S_t}x_z,\max_{z\in S_t}x_z],&S_t\ne\varnothing,\\ [0,1],&S_t=\varnothing. \end{cases} \]

Set \(g_0=\alpha\), and recursively compute
\[ g_t=\min\{u_t,\max\{\ell_t,g_{t-1}\}\}. \]

Thus \(g_t\) is the projection of \(g_{t-1}\) onto \(I_t\). In particular, \(g_t\in I_t\), so the resulting schedule is feasible. Return yes precisely when
\[ G_H:=\sum_{t=1}^{H}|g_t-g_{t-1}|\le B. \]

The masses do not enter this computation: the stated constraints depend only on which support types are active and their locations.

Proof of optimality

Projection identity. Let \(I=[\ell,u]\), let \(a\in\mathbb R\), and let \(p=\min\{u,\max\{\ell,a\}\}\). For every \(b\in I\),
\[ |a-b|=|a-p|+|p-b|. \]

Indeed, if \(a\in I\), then \(p=a\). If \(a<\ell\), then \(a<p=\ell\le b\); if \(a>u\), then \(b\le p=u<a\). In each case, the displayed equality follows by adding distances between ordered points.

Now fix an arbitrary feasible schedule \(y_0=\alpha,y_1,\ldots,y_H\), whose locations may be real. Define its prefix cost by
\[ C_t=\sum_{s=1}^{t}|y_s-y_{s-1}|, \qquad G_t=\sum_{s=1}^{t}|g_s-g_{s-1}|. \]

We prove by induction that, for every \(t\in\{0,\ldots,H\}\),
\[ C_t\ge G_t+|y_t-g_t|. \]

For \(t=0\), both costs are zero and \(y_0=g_0=\alpha\).

Suppose the inequality holds at \(t-1\). The induction hypothesis and the triangle inequality give
\[ \begin{aligned} C_t &=C_{t-1}+|y_t-y_{t-1}|\\ &\ge G_{t-1}+|y_{t-1}-g_{t-1}|+|y_t-y_{t-1}|\\ &\ge G_{t-1}+|y_t-g_{t-1}|. \end{aligned} \]

Because \(y_t\in I_t\) and \(g_t\) is the projection of \(g_{t-1}\) onto \(I_t\), the projection identity yields
\[ |y_t-g_{t-1}| = |g_t-g_{t-1}|+|y_t-g_t|. \]

Substitution proves the induction step. At \(t=H\), consequently,
\[ C_H\ge G_H+|y_H-g_H|\ge G_H. \]

The greedy schedule itself has cost \(G_H\), so it attains the global minimum. No terminal-location assumption or advance knowledge of future intervals was used.

Exact arithmetic and running time

For the stated dimension \(m=1\), computing all interval endpoints requires \(O(\tau H)\) location comparisons; constructing the schedule requires \(O(H)\) further operations.

To bound bit complexity, write each of \(\alpha,x_1,\ldots,x_\tau,B\) as a ratio of binary integers with positive denominator. Let \(D\) be the product of these denominators. Their total encoding length is at most \(L\), so \(D\) has \(O(L)\) bits. Scale these rational numbers by \(D\); every scaled value is an integer with \(O(L)\) bits. Ordinary integer multiplication and division perform this preprocessing in \(O((\tau+1)L^2)\) bit operations.

Every greedy location is either \(\alpha\) or an interval endpoint, so all scaled locations remain integers in \([0,D]\). The scaled accumulated cost is at most \(HD\), requiring \(O(L+\log H)\) bits. Endpoint comparisons, projections, cost accumulation, and the final comparison can therefore all be performed exactly.

Since the input contains an \(H\)-bit active-set vector for each of the \(\tau\ge1\) types, \(\tau H\le L\), and hence \(H\le L\). A valid overall bound is
\[ O\bigl((\tau+1)L^2+\tau H L\bigr) \qquad\text{for }m=1, \]
which is \(O(L^3)\). The algorithm never expands the masses into a finite population or enumerates possible types.

Thus the stated decision problem is polynomial-time solvable.

⟨structured verdict parsed — rendered above⟩

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

Verification report

The prover resolves the stated decision problem. The optimality proof is correct for arbitrary real feasible schedules, and the exact-arithmetic analysis establishes polynomial running time for the specified support-list encoding. No major or minor mathematical issues were found.

1. Input model and feasibility

The intervals \(I_t\) exactly represent the task’s constraints. When \(S_t\) is nonempty, its minimum and maximum exist because the support list is finite. When \(S_t\) is empty, setting \(I_t=[0,1]\) correctly retains only the facility-domain constraint.

Every interval is nonempty, including singleton intervals. The projection formula therefore defines \(g_t\) at every period and guarantees \(g_t\in I_t\). Together with \(g_0=\alpha\), this proves feasibility.

Ignoring masses is justified: neither the objective nor the periodwise constraints use their magnitudes. Empty and nonconsecutive active sets are handled directly by their bit vectors.

2. Projection identity

The identity is correctly stated for every real \(a\), every nonempty closed interval \(I=[\ell,u]\), and every \(b\in I\).

The three cases given cover all possibilities. In each case, the projected point \(p\) lies between \(a\) and \(b\), so the equality follows from additivity of distance along ordered points. Endpoint equality and singleton intervals introduce no exceptions.

3. Inductive optimality argument

The competitor schedule is arbitrary and may have real coordinates. Thus the proof does not restrict the optimization problem to rational schedules.

The base case holds because both prefix costs vanish and \(y_0=g_0=\alpha\).

The induction step is valid:

At the final period, this implies \(C_H\ge G_H\) for every feasible schedule. Since the constructed feasible schedule attains \(G_H\), the claimed global minimum follows. The proof uses no terminal constraint and no knowledge of future intervals.

4. Decision correctness

Returning yes exactly when \(G_H\le B\) is correct in both directions. A yes answer has the constructed schedule as a witness. A no answer follows from the lower bound on every feasible schedule. Equality with the threshold is handled correctly.

5. Exact arithmetic and running time

The bit-complexity argument is sound.

The product \(D\) of the input denominators has \(O(L)\) bits because their combined encoding length is at most \(L\). Scaling each relevant rational by \(D\) produces an integer of \(O(L)\) bits, including the threshold even when \(B>1\). Ordinary multiplication and exact division support the stated preprocessing bound \(O((\tau+1)L^2)\).

Every greedy location is either \(\alpha\) or an interval endpoint. For an empty period, projection onto \([0,1]\) preserves the previous location. Consequently, scaled locations remain integers between zero and \(D\).

Each scaled movement is at most \(D\), so the accumulated cost is at most \(HD\) and has \(O(L+\log H)\) bits. Exact comparisons and accumulation therefore have the claimed polynomial cost.

Positive masses summing to one imply \(\tau\ge1\). The explicitly encoded active-set vectors imply \(\tau H\le L\), hence \(H\le L\). The stated overall bound

\(O((\tau+1)L^2+\tau H L)\), for \(m=1\),

is valid and implies \(O(L^3)\). The task fixes the dimension, so no bound for variable \(m\) is required.

6. Literature attribution

The stated correspondence with the dynamic target rule is supported by the paper’s description: it retains the previous location when feasible and otherwise chooses the closest feasible location. [Wada et al. (2018), Section 5.2](https://www.ifaamas.org/Proceedings/aamas2018/pdfs/p336.pdf).

The prover’s optimality argument is self-contained; it does not depend on applying an external theorem to the distribution encoding.

Repair feedback

No additional lemma, clarification, or mathematical repair is required. The output establishes polynomial-time solvability for the precise input model.

⟨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.