← back to the atlas

d4-conf-atal-2017-0359 (d4-conf-atal-2017-0359)

Answer: Polynomial-time solvable: the problem is in \(\mathrm{P}\), with running time polynomial in \(m,\tau,L\), even without single-peakedness.

The anchor (named result in the paper)

Theorem 1 — class: hardness

The continuous mirror question, as graded

Given candidates \(C\), a common axis, a target \(p\), registered masses \(\mu_t\), eligible capacities \(a_t\), and a budget \(\rho\), where every type \(t\) is a complete ranking single-peaked on the axis, decide whether there are additions \(0 \le x_t \le a_t\) with \(\sum_t x_t \le \rho\) such that \(\sum_t (\mu_t+x_t)(s(t,p)-s(t,c)) \ge 0\) for every \(c \in C\), where \(s(t,c)\) is the Borda score of \(c\) in type \(t\).

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

Given a candidate set \(C\) with \(m=|C|\ge 2\), a common single-peaked axis, and a target \(p\in C\), each type is a strict complete ranking single-peaked on that axis. Write \(s(t,c)\) for its standard Borda score for \(c\).
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 the support is the combined registered and eligible pool: type \(t\) has registered mass \(\mu_t\ge 0\) and eligible capacity \(a_t\ge 0\), with \(\mu_t+a_t>0\). Thus \(\tau\) is the support size, not the number of possible rankings. Masses need not sum to one.
The budget \(\rho\ge 0\) is a binary rational; \(L\) is the total input bit length, including rankings, masses, capacities, and budget. Initially \(p\) is not a Borda co-winner.
Decide whether real additions \(0\le x_t\le a_t\), costing one unit per unit of mass and satisfying \(\sum_t x_t\le\rho\), can make \(p\) a co-winner: \(\sum_t(\mu_t+x_t)(s(t,p)-s(t,c))\ge 0\) for every \(c\in C\). Ties count as wins.

Is this continuous constructive control problem in \(\mathrm{P}\), with running time polynomial in \(m,\tau,L\), or is it NP-hard?

Discrete constructive control by adding unweighted votes for Borda is NP-hard even when all registered and eligible rankings share a single-peaked axis, under both co-winner and unique-winner conventions. [Yang, 2017](https://aamas.csc.liv.ac.uk/Proceedings/aamas2017/pdfs/p1178.pdf)
No result for this exact divisible-mass formulation 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}\), with running time polynomial in \(m,\tau,L\). In fact, the proof applies to arbitrary strict complete rankings; single-peakedness is unnecessary.

1. Exact linear-programming formulation

Index the explicitly listed support types by \(t\in\{1,\ldots,\tau\}\). If \(r_t(c)\) is the position of candidate \(c\) in type \(t\), standard Borda gives \(s(t,c)=m-r_t(c)\). Define

\(d_{t,c}=s(t,p)-s(t,c)=r_t(c)-r_t(p)\),

so \(d_{t,c}\) is an integer with \(|d_{t,c}|\le m-1\). For each rival \(c\ne p\), define the registered deficit

\(b_c=-\sum_{t=1}^{\tau}\mu_t d_{t,c}\).

Construct the following linear feasibility problem with real variables \(x_1,\ldots,x_\tau\):

There are exactly \(\tau\) variables and \(2\tau+m\) inequalities.

Equivalence. The first two groups express precisely the permitted additions and their budget. For each rival, the last inequality is equivalent to

\(\sum_{t=1}^{\tau}(\mu_t+x_t)(s(t,p)-s(t,c))\ge 0\),

because \(b_c=-\sum_t\mu_t d_{t,c}\). This is exactly the requirement that the final Borda score of \(p\) be at least that of \(c\). The comparison with \(p\) itself is identically zero and can be omitted.

Thus, permitted additions making \(p\) a co-winner exist if and only if this linear program is feasible over the reals.

2. Polynomial encoding length

It remains to verify polynomial *bit* complexity, since the masses and budget can have large binary encodings.

Write each input rational using its binary numerator and positive denominator. Let \(Q\) be the product of all denominators appearing in the masses, capacities, and budget. Since their total encoding length is at most \(L\), the binary length of \(Q\) is \(O(L)\).

Multiply every inequality above by \(Q>0\). This preserves its solutions and produces integer coefficients and right-hand sides. In particular, writing \(\mu_t=u_t/v_t\), we obtain

\(Qb_c=-\sum_{t=1}^{\tau}(Q/v_t)u_t d_{t,c}\),

which is an integer.

Every input rational has absolute value at most \(2^{O(L)}\), and \(Q\le 2^{O(L)}\). Consequently,

\(|Qb_c|\le Q\tau(m-1)\max_t\mu_t\le\tau(m-1)2^{O(L)}\).

Hence each \(Qb_c\) has \(O(L+\log(\tau+1)+\log m)\) bits. The same bound holds for the other coefficients and right-hand sides: \(Qd_{t,c}\), \(Q\), \(Qa_t\), and \(Q\rho\).

The integer system therefore has total encoding length polynomial in \(m,\tau,L\). It can also be constructed in polynomial time: scan the rankings to compute positions, multiply the input denominators to obtain \(Q\), and compute the displayed integer sums. All these operations involve polynomially many integers of polynomial bit length.

Crucially, only the \(\tau\) explicitly supplied types are used. No enumeration of other rankings is required.

3. Exact polynomial-time decision

Apply the standard polynomial-time linear-programming feasibility theorem:

Given an explicitly encoded integer matrix \(A\) and integer vector \(b\), feasibility of \(Ax\ge b\) over real variables is decidable in time polynomial in their binary encoding length.

The ellipsoid-method theorem includes arbitrary feasible polyhedra, including those of lower dimension; see [MIT’s lecture on the ellipsoid method, Sections 3.11–3.12](https://ocw.mit.edu/courses/6-251j-introduction-to-mathematical-programming-fall-2009/e13f5e6650f7be1e21101a2e7bd0d5b8_MIT6_251JF09_lec18.pdf).

Our constructed system satisfies the theorem’s hypotheses: it is explicit, finite, and has integer data of polynomial encoding length. Therefore its feasibility, and hence the requested control decision, is decidable in time polynomial in \(m,\tau,L\). This is an exact feasibility decision, so it correctly handles ties and zero capacities without any positive-margin assumption.

4. Relation to discrete hardness

[Yang’s discrete hardness result](https://aamas.csc.liv.ac.uk/Proceedings/aamas2017/pdfs/p1178.pdf) concerns adding whole unweighted votes. Aggregating those votes by type imposes integer constraints on the addition variables. The present problem expressly permits real additions, so its feasible set is given entirely by linear inequalities. Feasibility of that continuous relaxation does not establish feasibility under integer restrictions.

Thus the discrete hardness result is consistent with the polynomial-time algorithm proved here.

⟨structured verdict parsed — rendered above⟩

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

The prover resolves the assigned problem correctly. The LP formulation is exactly equivalent to the permitted continuous additions, its encoding has polynomial bit length, and the stated polynomial-time feasibility theorem applies. No major or minor issues were found.

1. Borda coefficients and registered deficits

For a strict complete ranking with positions numbered from \(1\) to \(m\), standard Borda assigns \(m-r_t(c)\) points. Hence the calculation

\[ d_{t,c}=s(t,p)-s(t,c)=r_t(c)-r_t(p) \]

is correct, including its sign. Since both positions lie between \(1\) and \(m\), the bound \(|d_{t,c}|\le m-1\) holds.

The definition

\[ b_c=-\sum_{t=1}^{\tau}\mu_t d_{t,c} \]

correctly gives the amount that the additions must supply in the comparison against \(c\). The terminology “deficit” does not require \(b_c\) to be positive: rivals already behind \(p\) may have nonpositive \(b_c\), and the formulation handles them correctly.

2. Equivalence of the feasibility system

Each constraint corresponds exactly to a requirement in the task:

Substituting the definition of \(b_c\) into the last constraint gives exactly

\[ \sum_t(\mu_t+x_t)(s(t,p)-s(t,c))\ge 0. \]

This establishes both directions of the claimed equivalence. The comparison with \(p\) itself is identically zero, so omitting it is valid.

The inequality count is also correct: \(2\tau\) bounds, one budget constraint, and \(m-1\) rival comparisons give \(2\tau+m\) inequalities.

No normalization of masses or integrality of additions is assumed. Single-peakedness is unused, which justifies the claimed extension to arbitrary strict complete rankings.

3. Polynomial encoding and construction

The denominator-clearing argument is sound. All input denominators are positive integers, and their total binary encoding length is at most \(L\). Their product \(Q\) therefore has \(O(L)\) bits. Multiplication by \(Q>0\) preserves every inequality and its solution set.

For each rival,

\[ Qb_c=-\sum_t(Q/v_t)u_t d_{t,c} \]

is an integer because each \(v_t\) divides \(Q\). The stated magnitude bound follows from nonnegative registered masses and \(|d_{t,c}|\le m-1\):

\[ |Qb_c|\le Q\tau(m-1)\max_t\mu_t. \]

Consequently, its binary length is \(O(L+\log(\tau+1)+\log m)\). The same bound covers the other listed coefficients and right-hand sides. Zero entries require only constant encoding space.

There are polynomially many matrix entries, so polynomial bit length per entry yields polynomial total encoding length. Computing positions, multiplying denominators, taking exact quotients, and forming the sums requires polynomially many arithmetic operations on integers of polynomial bit length. Thus the construction-time claim is justified.

Only explicitly supplied support types are used; there is no hidden enumeration of possible rankings.

4. Application of polynomial-time LP feasibility

The prover states the required theorem precisely: feasibility of an explicitly encoded integer system \(Ax\ge b\), over real variables, is decidable in time polynomial in its binary encoding length.

The cited [MIT lecture, Sections 3.11–3.12](https://ocw.mit.edu/courses/6-251j-introduction-to-mathematical-programming-fall-2009/e13f5e6650f7be1e21101a2e7bd0d5b8_MIT6_251JF09_lec18.pdf), explicitly addresses lower-dimensional polyhedra and states polynomial-time feasibility for integer data, including polynomial bounds on numerical precision.

All hypotheses are satisfied here. The system is finite, explicit, and has integer data of polynomial encoding length. Inequalities written with \(\le\) can be converted to the theorem’s orientation by negation without changing encoding complexity.

The theorem gives an exact decision. Thus equality in a score comparison counts as feasibility, as required for co-winners; no strict-margin assumption is introduced.

5. Edge cases and discrete hardness

Zero capacities, zero registered masses, and zero budget are all represented directly by the constraints. Lower-dimensional feasible sets are covered by the cited theorem.

The initial non-co-winner assumption is not needed for the algorithm, so its omission from the construction causes no gap. An empty support would give every candidate score zero and therefore contradict that assumption.

The discussion of discrete hardness is consistent with [Yang’s result](https://aamas.csc.liv.ac.uk/Proceedings/aamas2017/pdfs/p1178.pdf). Whole-vote additions impose integer restrictions after aggregation by type. The present task permits real additions, so discrete hardness does not invalidate the LP decision procedure.

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.