← back to the atlas

Worst-Case Voting When the Stakes Are High (aaai22-20443)

Answer: An exact minimax lottery is computable in polynomial time in \(m\), \(\tau\), and \(L\).

The anchor (named result in the paper)

Theorem 3.12 — class: algorithmic

PDF text-layer excerpt — equations and symbol order may be approximateFor any profile σ, Algorithm 1 computes the distribution over A which minimizes (expected) additive dis- tortion in polynomial time.

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

The continuous mirror question, as graded

Given candidates \(C\), a finite set \(T\subseteq S_C\) of complete ranking types, rational masses \(\mu_t\ge0\) summing to \(1\), and unit-capped utilities consistent with each type, compute a lottery \(p^\star\in\Delta(C)\) minimizing \(\max_{(u_t)}[\max_{a\in C}W(a)-\sum_{b\in C}p_bW(b)]\), where \(W(c)=\sum_{t\in T}\mu_tu_t(c)\), equivalently solving the paper's exact LP with \(q_b^a(\mu)=\sum_{t\in T}\mu_t\mathbf{1}[b\succeq_t a]/\operatorname{rk}_t(a)\).

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

Let \(C\) be a nonempty candidate set with \(m=|C|\). A society is given by its support: a list \(T\) of \(\tau\) distinct strict complete ranking types with positive binary rational masses \(\mu_t\) summing to \(1\). Here \(\tau\) is the support size, not the number of possible rankings; let \(L\) be the total input bit length.
For each type \(t\), the unknown utility vector belongs to \(\mathcal U_t=\{u_t\in\mathbb R_{\ge0}^{C}:\sum_{c\in C}u_t(c)\le1,\ a\succ_t b\Rightarrow u_t(a)\ge u_t(b)\}\). Thus utilities may tie despite strict rankings, and the cap applies to total utility.
For \(W_u(c)=\sum_{t\in T}\mu_tu_t(c)\), define \(R(p)=\max_{u\in\prod_{t\in T}\mathcal U_t}[\max_{a\in C}W_u(a)-\sum_{b\in C}p_bW_u(b)]\). The computational problem is to output an exact rational lottery \(p^\star\in\arg\min_{p\in\Delta(C)}R(p)\).

Is computing such an exact minimax lottery polynomial-time solvable in \(m\), \(\tau\), and \(L\), or is it NP-hard?

For an explicit finite list of voters with these utility constraints, an exact instance-optimal lottery is computable in polynomial time. That discrete guarantee measures input size using the explicit voters, whereas this question uses support size and binary rational masses.

Modeling choices made when packaging the task

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

Result

An exact minimax lottery is computable in polynomial time in \(m\), \(\tau\), and \(L\). We construct a rational linear program with \(m+m\tau+1\) variables and \(O(m^2\tau)\) constraints whose optimal solutions yield precisely the required lotteries.

1. Decomposing the feasible utilities

For each type \(t\), write its ranking as \(c_{t,1}\succ_t\cdots\succ_t c_{t,m}\), and define the prefix \(P_{t,k}=\{c_{t,1},\ldots,c_{t,k}\}\).

Let \(v_{t,k}\) assign utility \(1/k\) to every candidate in \(P_{t,k}\) and zero elsewhere. We claim that

\(\displaystyle \mathcal U_t=\operatorname{conv}\{0,v_{t,1},\ldots,v_{t,m}\}.\)

Each listed vector satisfies the nonnegativity, ranking, and total-utility constraints. Since these constraints define a convex set, their convex hull is contained in \(\mathcal U_t\).

For the reverse containment, take any \(u_t\in\mathcal U_t\), put \(x_i=u_t(c_{t,i})\), and set \(x_{m+1}=0\). Define \(\lambda_k=k(x_k-x_{k+1})\). Ranking consistency gives \(\lambda_k\geq0\), and telescoping gives

\(\displaystyle \sum_{k=1}^m\lambda_k=\sum_{k=1}^m k(x_k-x_{k+1})=\sum_{i=1}^m x_i\leq1.\)

Moreover, for every \(i\),

\(\displaystyle \sum_{k=1}^m\lambda_kv_{t,k}(c_{t,i})=\sum_{k=i}^m(x_k-x_{k+1})=x_i.\)

Thus \(u_t=\sum_{k=1}^m\lambda_kv_{t,k}\), with the remaining convex-combination weight assigned to zero. This proves the claim.

2. An exact formula for regret

For \(p\in\Delta(C)\), define \(p(P)=\sum_{b\in P}p_b\) and

\(\displaystyle h_{a,t}(p)=\max_{u_t\in\mathcal U_t}\left[u_t(a)-\sum_{b\in C}p_bu_t(b)\right].\)

The decomposition above shows that

\(\displaystyle h_{a,t}(p)=\max\left\{0,\max_{1\leq k\leq m}\frac{\mathbf1_{\{a\in P_{t,k}\}}-p(P_{t,k})}{k}\right\}.\)

Indeed, the maximized expression is linear in \(u_t\), so its maximum over the convex hull equals its maximum over the listed vectors. At \(k=m\), the displayed fraction is zero because \(P_{t,m}=C\) and \(p(C)=1\). Consequently,

\[\displaystyle h_{a,t}(p)=\max_{1\leq k\leq m}\frac{\mathbf1_{\{a\in P_{t,k}\}}-p(P_{t,k})}{k}.\tag{1}\]

In particular, \(0\leq h_{a,t}(p)\leq1\).

Each utility set is nonempty and compact, so all maxima below are attained. Expanding the welfare expression and exchanging the two maxima gives

\(\displaystyle R(p)=\max_{a\in C}\max_{u\in\prod_t\mathcal U_t}\sum_{t\in T}\mu_t\left[u_t(a)-\sum_{b\in C}p_bu_t(b)\right].\)

For fixed \(a\), each summand depends only on \(u_t\). Choosing a maximizing utility independently for every type is permitted by the Cartesian-product feasible set. Since every \(\mu_t\) is positive, this proves

\[\displaystyle R(p)=\max_{a\in C}\sum_{t\in T}\mu_t h_{a,t}(p).\tag{2}\]

3. A polynomial-size linear program

Introduce variables \(p_b\) for candidates, \(z_{a,t}\) for candidate–type pairs, and \(r\). Minimize \(r\) subject to

\(\displaystyle \sum_{b\in C}p_b=1,\qquad p_b\geq0\quad(b\in C),\)

\(\displaystyle 0\leq z_{a,t}\leq1\quad(a\in C,\ t\in T),\qquad 0\leq r\leq1,\)

\[\displaystyle kz_{a,t}+\sum_{b\in P_{t,k}}p_b\geq\mathbf1_{\{a\in P_{t,k}\}}\quad(a\in C,\ t\in T,\ 1\leq k\leq m),\tag{3}\]

and

\[\displaystyle \sum_{t\in T}\mu_tz_{a,t}\leq r\quad(a\in C).\tag{4}\]

We verify exact equivalence.

For any feasible solution, dividing (3) by the positive integer \(k\) and taking the maximum over \(k\) yields \(z_{a,t}\geq h_{a,t}(p)\), by (1). Equations (2) and (4), together with positivity of the masses, then give \(R(p)\leq r\). Hence the linear program’s optimum is at least \(\min_{p\in\Delta(C)}R(p)\).

Conversely, for any lottery \(p\), set \(z_{a,t}=h_{a,t}(p)\) and \(r=R(p)\). Equations (1) and (2) imply (3) and (4). The bounds hold because \(0\leq h_{a,t}(p)\leq1\) and the masses sum to one, so \(0\leq R(p)\leq1\). Thus these choices form a feasible solution.

The two optimal values therefore coincide. If \((p^\star,z^\star,r^\star)\) is an optimal linear-program solution, then

\(\displaystyle \min_{p\in\Delta(C)}R(p)\leq R(p^\star)\leq r^\star=\min_{p\in\Delta(C)}R(p).\)

Accordingly, \(p^\star\) is an exact minimax lottery.

4. Exact rational output and bit complexity

The program has \(m+m\tau+1\) variables and \(O(m^2\tau)\) constraints. Its coefficients are integers of magnitude at most \(m\), together with the input rational masses. Its total binary encoding length is therefore polynomial in \(m\), \(\tau\), and \(L\), and it can be constructed within that bound.

The feasible region is nonempty: choose any lottery, set every \(z_{a,t}=1\), and set \(r=1\). It is also bounded by the explicit variable bounds and the lottery constraints.

We now apply the standard exact rational linear-programming theorem: a linear program given explicitly by binary rational coefficients, with a nonempty bounded feasible region, admits an exact rational optimal solution computable in time polynomial in its total encoding length. Exact polynomial-time LP algorithms are discussed in [Gleixner and Steffy, Section 1.3](https://arxiv.org/html/1912.12820v1#S1.SS3). All hypotheses have been checked above.

There is also no hidden exponential output requirement. An optimal vertex exists; its coordinates solve a nonsingular subsystem of the rational constraints. Clearing denominators, Cramer’s rule and Hadamard’s determinant bound give polynomial bit length for those coordinates.

Solving the displayed program exactly and outputting its \(p\)-coordinates therefore completes the task. Binary rational masses are handled directly as coefficients, without expanding them into an explicit voter population.

⟨structured verdict parsed — rendered above⟩

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

Overall assessment

The proof is correct and resolves the assigned problem. It establishes an exact polynomial-time algorithm using the support types and their binary rational masses directly. No major or minor mathematical issues were found.

Step-by-step verification

1. Utility-set decomposition

The claimed equality
\[ \mathcal U_t=\operatorname{conv}\{0,v_{t,1},\ldots,v_{t,m}\} \]
is justified in both directions.

Each listed vector is nonnegative, respects the ranking inequalities, and has total utility at most one. Convexity therefore gives the forward inclusion.

For the reverse inclusion, ranking consistency and nonnegativity imply
\[ x_1\geq\cdots\geq x_m\geq x_{m+1}=0. \]
Consequently, every coefficient \(\lambda_k=k(x_k-x_{k+1})\) is nonnegative. Both telescoping identities are correct: the coefficients sum to the total utility, and their weighted prefix vectors recover every coordinate. The remaining weight on zero is nonnegative. This also covers zero utilities and ties without any additional assumption.

Finding: Correct and complete.

2. Maximization for one candidate and type

The objective defining \(h_{a,t}(p)\) is linear in the utility vector. Its maximum over the established finite convex hull therefore equals its maximum over the listed vectors.

Evaluation at \(v_{t,k}\) gives exactly
\[ \frac{\mathbf1_{\{a\in P_{t,k}\}}-p(P_{t,k})}{k}. \]
The term for \(k=m\) is zero, so removing the separately listed zero alternative is valid. Every fraction is at most one, while the maximum is nonnegative because it includes that zero term.

Finding: Formula (1) and the bounds \(0\leq h_{a,t}(p)\leq1\) are correct.

3. Society-wide regret

Each utility set is closed and bounded in finite-dimensional space, and contains zero. Thus it is nonempty and compact, as asserted.

Exchanging the maximum over candidates with the maximum over utility profiles is valid: both describe maximization of the same expression over all candidate–profile pairs.

For a fixed candidate, the feasible profiles form a Cartesian product, and each summand depends on only one type’s utility. Maximizers can therefore be chosen independently. Positive masses preserve the direction of each maximization.

Finding: Formula (2) is justified. No assumption about an explicit voter population enters this step.

4. Linear-program equivalence

Constraint (3), divided by \(k>0\), imposes all the affine lower bounds defining \(h_{a,t}(p)\). Hence every feasible solution satisfies \(z_{a,t}\geq h_{a,t}(p)\). Constraint (4) and positive masses then imply \(r\geq R(p)\).

Conversely, choosing \(z_{a,t}=h_{a,t}(p)\) and \(r=R(p)\) satisfies every constraint. The upper bounds are valid because the masses sum to one.

These two directions establish equality of the optimal values. The final inequality chain correctly proves that every optimal LP solution yields a minimax lottery. Conversely, every minimax lottery has an optimal LP extension by the construction already given.

Finding: The LP represents the target optimization exactly.

5. Encoding and exact computation

The variable count is correct. There are \(m^2\tau\) prefix constraints; the remaining constraints preserve the stated asymptotic count. Encoding all matrix entries explicitly, including zeros and repeated masses, still takes polynomial space.

The proposed feasible point satisfies the constraints, and all variables are bounded. The stated exact rational LP theorem therefore applies. The cited [Section 1.3 of Gleixner and Steffy](https://arxiv.org/html/1912.12820v1#S1.SS3) explicitly discusses polynomial-time algorithms producing exact rational LP solutions, supporting this invocation.

The supplementary vertex argument is also valid: a nonempty bounded rational polyhedron has an optimal vertex, whose coordinates are determined by a nonsingular subsystem. The stated denominator-clearing and determinant bounds give polynomial coordinate bit length.

Finding: Exact output and polynomial bit complexity are established.

6. Edge cases and scope

The assumptions imply \(m\geq1\) and \(\tau\geq1\). For \(m=1\), the sole lottery has regret zero, and the displayed formulas and LP remain valid. Utility ties, unused utility capacity, and arbitrarily small positive rational masses are all covered.

Required repairs or clarifications: None.

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