← back to the atlas

d4-conf-atal-2014-0061 (d4-conf-atal-2014-0061)

Answer: Polynomial-time solvable: in \(\mathrm{P}\), with running time polynomial in \(m,\tau,L\).

The anchor (named result in the paper)

Theorem 3 — class: hardness

PDF text-layer excerpt — equations and symbol order may be approximater-DV-2 is NP-complete for every constant r ≥3.

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

The continuous mirror question, as graded

Given candidates \(C \cup \{p\}\), a common order \(L\), fixed \(r \ge 3\), and \(\tau\) ranking types that are 2-peaked with respect to \(L\), each with rational mass \(\mu_t \ge 0\) and \(\sum_t \mu_t = 1\), plus a rational deletion budget \(\rho\), does there exist deleted mass \(x_t \in [0,\mu_t]\) with \(\sum_t x_t \le \rho\) such that \(p\) is the unique \(r\)-approval winner among the remaining mass; that is, \(\sum_t (\mu_t-x_t)a_{t,p} > \sum_t (\mu_t-x_t)a_{t,c}\) for every \(c \in C\), where \(a_{t,c}\) indicates whether type \(t\) ranks \(c\) in its top \(r\)?

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

Let \(A=C\cup\{p\}\), with \(p\notin C\), \(m=|A|\ge r\), and fixed integer \(r\ge3\). The input includes a common linear order \(\ell\) of \(A\).
A strict ranking is 2-peaked with respect to \(\ell\) if \(\ell\) can be partitioned into at most two nonempty contiguous blocks, on each of which the restricted ranking is single-peaked; the partition may depend on the ranking.
A society is given by its support: a list of \(\tau\) distinct such ranking types, each with positive binary rational mass \(\mu_t\), where \(\sum_{t=1}^{\tau}\mu_t=1\). Here \(\tau\) is the support size, not the number of possible rankings.
The deletion budget is a binary rational \(\rho\in[0,1]\). Write \(a_{t,c}\) for the indicator that type \(t\) ranks candidate \(c\) among its top \(r\) positions.
A feasible deletion chooses real masses \(x_t\in[0,\mu_t]\) with \(\sum_{t=1}^{\tau}x_t\le\rho\). Candidate scores are \(s_x(c)=\sum_{t=1}^{\tau}(\mu_t-x_t)a_{t,c}\); ties do not make \(p\) a unique winner.
The decision problem asks whether a feasible deletion satisfies \(s_x(p)>s_x(c)\) for every \(c\in C\).

For each fixed \(r\ge3\), is this continuous deletion problem in \(\mathrm{P}\), with running time polynomial in \(m,\tau,L\), or is it \(\mathrm{NP}\)-hard, where \(L\) is the total input bit length?

Discrete deletion of at most a prescribed number of whole votes is \(\mathrm{NP}\)-complete for every fixed \(r\ge3\), even for 2-peaked rankings with the common order supplied ([Yang–Guo](https://arxiv.org/pdf/1304.4471)).
No result settling this exact continuous deletion problem was identified in the literature search.

Modeling choices made when packaging the task

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

Result

The problem is in \(\mathrm{P}\) for every fixed \(r\ge3\). In fact, the same algorithm works for arbitrary explicitly listed rankings and for variable \(r\). The crucial feature is that deletion masses may be fractional.

1. A linear program for the winning margin

Define the retained mass of type \(t\) by \(y_t=\mu_t-x_t\). The deletion constraints become
\[ 0\le y_t\le\mu_t \quad\text{and}\quad \sum_{t=1}^{\tau}y_t\ge1-\rho, \]
because \(\sum_t\mu_t=1\). Conversely, every such retained-mass vector gives a feasible deletion through \(x_t=\mu_t-y_t\).

For each opponent \(c\in C\), define \(b_{t,c}=a_{t,p}-a_{t,c}\in\{-1,0,1\}\). The score difference is
\[ s_x(p)-s_x(c)=\sum_{t=1}^{\tau}b_{t,c}y_t. \]

Consider the following rational linear program, with variables \(y_1,\ldots,y_\tau,\delta\):
\[ \begin{aligned} \text{maximize}\quad &\delta\\ \text{subject to}\quad &0\le y_t\le\mu_t &&(1\le t\le\tau),\\ &\sum_{t=1}^{\tau}y_t\ge1-\rho,\\ &\sum_{t=1}^{\tau}b_{t,c}y_t\ge\delta &&(c\in C),\\ &-1\le\delta\le1. \end{aligned} \]

The margin bounds are legitimate: every feasible retained-mass vector satisfies \(\sum_t y_t\le1\), so every candidate score lies in \([0,1]\) and every score difference lies in \([-1,1]\).

This program is nonempty: take \(y_t=\mu_t\) and \(\delta=-1\). Its feasible set is closed and bounded, hence compact, so an optimal value \(\delta^\star\) exists.

2. Equivalence with strict victory

Claim. A successful deletion exists if and only if \(\delta^\star>0\).

Proof. Suppose a feasible deletion makes \(p\) the unique winner. For its retained-mass vector \(y\), every quantity \(\sum_t b_{t,c}y_t\) is positive. Since \(C\) is finite and nonempty, their minimum
\[ \eta=\min_{c\in C}\sum_{t=1}^{\tau}b_{t,c}y_t \]
is positive. It is at most \(1\), so \((y,\eta)\) is feasible for the linear program. Thus \(\delta^\star\ge\eta>0\).

Conversely, if \(\delta^\star>0\), let \((y^\star,\delta^\star)\) be an optimum and set \(x_t=\mu_t-y_t^\star\). The retained-mass constraints ensure that \(x\) is a feasible deletion. For every opponent,
\[ s_x(p)-s_x(c)=\sum_t b_{t,c}y_t^\star\ge\delta^\star>0. \]
Hence \(p\) is the unique winner. This proves the claim.

3. Polynomial bit complexity and exact positivity

The standard polynomial-time theorem for rational linear programming states that feasibility and optimization are solvable in time polynomial in the dimensions and binary encoding length of the rational data. See [Adler–Beling, introduction](https://adler.ieor.berkeley.edu/ilans_pubs/lp_algebraic_stoc_1992.pdf).

Here there are \(\tau+1\) variables and \(2\tau+m+2\) inequalities. All constraint-matrix entries belong to \(\{-1,0,1\}\); the right-hand sides are input masses, \(1-\rho\), and small integers. The indicators can be constructed by scanning the supplied rankings. Consequently, the program has encoding length polynomial in \(m,\tau,L\), and it can be constructed in polynomial time.

For completeness, strict positivity also has an explicit rational separation bound. Put \(n=\tau+1\), and let \(D\) be the product of the denominators appearing in the input masses and budget. Its binary length is at most \(L+1\), and every right-hand side of the program becomes integral after multiplication by \(D\).

A linear objective on a nonempty bounded polytope attains its optimum at a vertex. At such a vertex, the active constraint normals span the full variable space: otherwise a sufficiently small perturbation in a direction orthogonal to all active normals would give two distinct feasible points whose midpoint is the vertex. Thus one can select \(n\) independent active constraints, giving
\[ Mz=v/D, \]
where \(M\) is a nonsingular integer matrix with entries in \(\{-1,0,1\}\), and \(v\) is integral.

By Cramer’s rule, the margin coordinate has the form
\[ \delta^\star=\frac{k}{D\det M} \]
for an integer \(k\). The determinant expansion gives \(|\det M|\le n!\). Therefore,
\[ \delta^\star>0 \quad\Longrightarrow\quad \delta^\star\ge\frac{1}{Dn!}. \]

The number \(1/(Dn!)\) has polynomial binary encoding length. Thus one may alternatively decide the problem by a single rational LP feasibility test, adding the constraint \(\delta\ge1/(Dn!)\). The proved separation bound makes this test exactly equivalent to strict victory, including rejection when the best margin is zero.

4. Scope of the conclusion

The proof uses neither the common order nor the two-peaked restriction. It applies to every explicitly supplied finite support.

The stated hardness of whole-vote deletion concerns an integrality requirement. The present problem allows every real mass in the specified intervals, so its feasible set is a rational polytope and the linear-programming argument settles the continuous version.

⟨structured verdict parsed — rendered above⟩

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

The prover’s output resolves the assigned problem correctly. The continuous deletion problem is in \(\mathrm{P}\), with running time polynomial in \(m,\tau,L\). No major or minor mathematical issues were found.

The substitution \(y_t=\mu_t-x_t\) gives a bijection between the original feasible deletions and vectors satisfying
\[ 0\le y_t\le\mu_t,\qquad \sum_t y_t\ge1-\rho. \]
Both directions use the stated normalization \(\sum_t\mu_t=1\). The budget inequality has the correct direction, and the reformulation preserves permission to delete less than the budget.

The score-difference identity is also correct:
\[ s_x(p)-s_x(c)=\sum_t(a_{t,p}-a_{t,c})y_t. \]
Every coefficient \(b_{t,c}\) belongs to \(\{-1,0,1\}\).

Since \(0\le y_t\le\mu_t\), every feasible retained-mass vector has total mass at most \(1\). Thus every score is in \([0,1]\), and every score difference is in \([-1,1]\). The bounds on \(\delta\) therefore preserve all possible positive winning margins.

The proposed feasible point \(y_t=\mu_t,\delta=-1\) satisfies every constraint, including the retention constraint because \(\rho\ge0\). The feasible region is closed and bounded in finite-dimensional space, and the objective is continuous. Consequently, an optimum exists.

The forward implication correctly takes the minimum of the finitely many positive score differences. The opponent set is nonempty: the task assumes \(m\ge r\ge3\), so \(|C|=m-1\ge2\). Hence the minimum is well-defined and strictly positive. Its upper bound of \(1\) follows from the already established score bounds.

The reverse implication correctly converts an optimal retained-mass vector into a feasible deletion and uses each margin constraint to obtain strict superiority over every opponent.

This establishes existence equivalence for real deletion masses; it does not presuppose that the successful deletion supplied in the forward implication is rational.

There are \(\tau+1\) variables. The inequality count is
\[ 2\tau+1+(m-1)+2=2\tau+m+2. \]
These terms correspond to retained-mass bounds, the retention constraint, opponent constraints, and margin bounds.

After writing all constraints in a common inequality orientation, every matrix coefficient remains in \(\{-1,0,1\}\). The right-hand sides are rational numbers obtained from the supplied masses, budget, and small integers. Computing \(1-\rho\) requires only polynomial bit complexity.

Scanning explicitly supplied rankings constructs the indicators in polynomial time. Even a dense LP encoding has size polynomial in \(m,\tau,L\).

The prover states the required theorem: rational LP feasibility and optimization admit algorithms polynomial in the dimensions and binary encoding length of the data. The cited [Adler–Beling introduction](https://adler.ieor.berkeley.edu/ilans_pubs/lp_algebraic_stoc_1992.pdf) confirms polynomial-time solvability for rational-coefficient LPs in this bit model.

The constructed program has rational data of polynomial encoding length and a finite attained optimum. Its hypotheses therefore satisfy the theorem as used. The separate separation-bound argument also supplies an exact feasibility formulation, avoiding any reliance on numerical tolerance when deciding positivity.

The product \(D\) of the input denominators is a positive integer with polynomial binary length. It clears all right-hand-side denominators, including that of \(1-\rho\).

The invoked vertex-attainment theorem applies to the nonempty bounded polytope. The argument that active normals at a vertex span the full variable space is valid: otherwise sufficiently small perturbations in both directions orthogonal to those normals preserve feasibility and contradict extremality. This argument also covers a polytope of lower affine dimension.

Selecting \(n=\tau+1\) independent active constraints therefore gives the stated nonsingular integer system. Cramer’s rule yields
\[ \delta^\star=\frac{k}{D\det M}. \]
Each term in the determinant expansion has absolute value at most \(1\), so \(|\det M|\le n!\). Whenever \(\delta^\star>0\), its absolute numerator is at least \(1\), giving
\[ \delta^\star\ge\frac{1}{Dn!}. \]
The denominator has polynomial binary length because \(\log_2(n!)\le n\log_2 n\). Thus the additional rational feasibility constraint has polynomial encoding length and distinguishes positive margin from zero exactly.

The proof remains valid for \(\rho=0\) and \(\rho=1\). In particular, zero retained mass produces zero score differences and cannot be accepted as strict victory. When \(m=r\), all rankings approve every candidate, so the LP correctly rejects.

Neither the order nor the two-peaked promise is needed for the argument. Explicit support and fractional deletion suffice. The whole-vote hardness statement imposes an integrality constraint absent from this LP and creates no inconsistency.

No additional clarification or mathematical 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.