← back to the atlas

d4-conf-aaai-2010-0094 (d4-conf-aaai-2010-0094)

Answer: Yes; a deterministic algorithm polynomial in \(m,\tau,k,L\) always returns a size-\(k\) committee with \(D_\mu(K)\leq 2\operatorname{OPT}_\mu\).

The anchor (named result in the paper)

Theorem 3 — class: algorithmic

PDF text-layer excerpt — equations and symbol order may be approximateThe LP-based algorithm has approximation ra- tio at most 2.

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

The continuous mirror question, as graded

Given \(m\) candidates, a committee size \(k\), and a finite support \(\mathcal S\) of approval sets with positive rational masses \(\mu_S\) summing to \(1\), return a committee \(K\) with \(|K|=k\) such that \(D_\mu(K) \le 2\operatorname{OPT}_\mu\), where \(D_\mu(K)=\max_{S\in\mathcal S} d_H(K,S)\) and \(\operatorname{OPT}_\mu=\min_{|K'|=k}D_\mu(K')\).

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

Let \(A\) be a set of \(m\geq1\) candidates and let \(k\in\{1,\ldots,m\}\). Approval types are arbitrary subsets of \(A\), including the empty set.
A society is given by its support: a nonempty list \(\mathcal S\) of \(\tau\) distinct approval types with positive binary rational masses \(\mu_S\) satisfying \(\sum_{S\in\mathcal S}\mu_S=1\). Here \(\tau\) is the support size, not the number of possible approval types; \(L\) is the total input bit length.
For an integral committee \(K\subseteq A\) with \(|K|=k\), define \(D_\mu(K)=\max_{S\in\mathcal S}d_H(K,S)\) and \(\operatorname{OPT}_\mu=\min_{K'\subseteq A:\,|K'|=k}D_\mu(K')\), using Hamming distance. Any committee satisfying the guarantee is acceptable.

Does a deterministic algorithm running in time polynomial in \(m,\tau,k,L\) always return a committee \(K\) with \(|K|=k\) and \(D_\mu(K)\leq2\operatorname{OPT}_\mu\)?

Caragiannis, Kalaitzis, and Markakis established a deterministic polynomial-time \(2\)-approximation for discrete minimax approval voting ([primary source](https://ojs.aaai.org/index.php/AAAI/article/download/7615/7476)).
The stated support objective is exactly that discrete objective on the listed types, so its \(2\)-approximation question is already settled affirmatively; this is not an open target.

Modeling choices made when packaging the task

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

Conclusion

Yes. The support formulation admits a deterministic polynomial-time \(2\)-approximation. The rational masses do not enter the objective, so no expansion according to their denominators is needed.

Known theorem and its hypotheses

Caragiannis, Kalaitzis, and Markakis prove that discrete minimax approval voting admits a deterministic polynomial-time algorithm returning a size-\(k\) committee whose maximum Hamming distance is at most twice optimum. Approval sets may be empty. Their algorithm solves a linear-programming relaxation and selects the \(k\) candidates with largest fractional coordinates. See [Theorem 3 of the primary source](https://ojs.aaai.org/index.php/AAAI/article/download/7615/7476).

The paper assumes that the number of voters exceeds \(k\). We ensure this without changing the objective by duplicating an existing approval type.

Reduction and proof of the guarantee

Write the nonempty support as \(\mathcal S=(S_1,\ldots,S_\tau)\). Construct a discrete profile \(P\) containing one voter with approval set \(S_i\) for each \(i\). If \(\tau\leq k\), append \(k+1-\tau\) additional voters, all approving \(S_1\). Thus the profile has
\[ n=\max\{\tau,k+1\}>k \]
voters. Every approval set is a subset of the same candidate set \(A\), and the committee size satisfies \(1\leq k\leq m\), as required.

For every size-\(k\) committee \(K\), duplication leaves the maximum unchanged:
\[ \max_{1\leq i\leq n}d_H(K,P_i) =\max_{S\in\mathcal S}d_H(K,S) =D_\mu(K). \]
Indeed, every support type appears in \(P\), and every appended approval set already appears among the support types. Taking minima over the identical family of feasible committees gives
\[ \operatorname{OPT}(P)=\operatorname{OPT}_\mu. \]

Apply the cited deterministic algorithm to \(P\). Its output \(K\) therefore satisfies
\[ |K|=k,\qquad D_\mu(K) =\max_i d_H(K,P_i) \leq 2\operatorname{OPT}(P) =2\operatorname{OPT}_\mu. \]
This is an absolute inequality, so it also covers \(\operatorname{OPT}_\mu=0\).

Running time

The constructed profile contains at most \(\tau+k+1\) ballots, each representable by \(m\) bits. Its encoding length is consequently polynomial in \(m,\tau,k\). Reading the original input takes time polynomial in \(L\); constructing the profile and applying the cited polynomial-time algorithm takes time polynomial in \(m,\tau,k,L\).

Thus the required algorithm exists for every valid input, independently of the sizes of the mass denominators.

⟨structured verdict parsed — rendered above⟩

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

The prover’s argument resolves the assigned question correctly. The cited theorem applies to the constructed profile, the reduction preserves the objective exactly, and the running time is polynomial in the required parameters. No major or minor mathematical issues were found.

Step-by-step verification

The definition of \(D_\mu(K)\) takes the maximum over the listed support types. It contains no mass values. Consequently, replacing each support type by one discrete ballot preserves this objective, regardless of the positive rational masses or their denominators.

This addresses the stated support formulation directly.

The relevant result guarantees that the LP-based algorithm returns a committee of cardinality \(k\) with maximum Hamming distance at most twice the optimum for discrete minimax approval voting. The source describes solving the LP relaxation and selecting the \(k\) largest fractional coordinates. It permits empty approval sets and assumes \(n>k\). These claims match the paper’s definitions, algorithm description, and Theorem 3. [Primary source](https://ojs.aaai.org/index.php/AAAI/article/download/7615/7476)

The theorem does not require voters to have distinct approval sets. Thus repeated ballots are permitted. Arbitrary rounding ties can be resolved deterministically; they do not weaken the cited guarantee.

Because the support is nonempty, \(S_1\) exists and can be duplicated.

If \(\tau>k\), the initial profile already has \(n=\tau>k\). If \(\tau\leq k\), the number of appended voters is the positive integer \(k+1-\tau\), giving
\[ n=\tau+(k+1-\tau)=k+1>k. \]
Hence the stated formula \(n=\max\{\tau,k+1\}\) is correct.

All ballots remain subsets of \(A\), and the original hypothesis \(1\leq k\leq m\) ensures that size-\(k\) committees exist.

Every support type appears in the constructed profile, and every extra ballot duplicates an existing type. Therefore, for every feasible committee \(K\),
\[ \max_{1\leq i\leq n}d_H(K,P_i) =\max_{S\in\mathcal S}d_H(K,S) =D_\mu(K). \]

Both optimization problems minimize over precisely the same family of size-\(k\) subsets of \(A\). Taking their minima therefore gives \(\operatorname{OPT}(P)=\operatorname{OPT}_\mu\). No implication is missing here.

Applying the theorem and substituting the established equalities yields exactly
\[ |K|=k,\qquad D_\mu(K)\leq2\operatorname{OPT}_\mu. \]

The argument uses an absolute inequality, without division by the optimum, so it includes \(\operatorname{OPT}_\mu=0\). Empty approval types, a singleton support, \(m=1\), and \(k=m\) satisfy the checked hypotheses and require no separate exception.

The constructed profile has \(n=\max\{\tau,k+1\}\leq\tau+k+1\) ballots, each encodable with \(m\) bits. Its explicit encoding therefore has polynomial size in \(m,\tau,k\). Applying the cited polynomial-time algorithm to that encoding, together with reading the original input, takes polynomial time in \(m,\tau,k,L\).

No denominator-dependent expansion occurs. The conclusion establishes polynomial-time computation of the requested approximation; it makes no claim of polynomial-time exact optimization.

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