← back to the atlas

d4-conf-ecai-2020-0022 (d4-conf-ecai-2020-0022)

Answer: Computing an exact maximizing committee is NP-hard; deciding whether \(\operatorname{OPT}=1\) is NP-complete. Both problems admit \(2^m\operatorname{poly}(m,\tau,L)\) and \(2^{O(8^\tau)}\operatorname{poly}(m,\tau,L)\) algorithms.

The anchor (named result in the paper)

Theorem 3 — class: hardness

PDF text-layer excerpt — equations and symbol order may be approximateDeciding if there is a nonempty committee that satisfies all the voters under the tmaj-threshold rule is NP-hard.

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 support \(\mathcal A\subseteq 2^C\) of approval types, and positive binary-rational masses \(\mu_A\) summing to \(1\), find a nonempty committee \(S\subseteq C\) maximizing \(\sum_{A\in\mathcal A}\mu_A\mathbf 1[|A\cap S|\ge\lceil |S|/2\rceil]\). Classify the exact problem in terms of \(|C|\), \(|\mathcal A|\), and the mass encoding length; in particular, determine the complexity of deciding whether the optimum is \(1\).

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

Let \(C\) be a finite candidate set with \(m=|C|\ge 1\). A society is given by its support: an explicit list \(\mathcal A\subseteq 2^C\) of \(\tau=|\mathcal A|\) approval types with positive binary-rational masses \(\mu_A\), where \(\sum_{A\in\mathcal A}\mu_A=1\). Here \(\tau\) is the support size, not the number of possible approval types; let \(L\) be the total mass encoding length. Empty approval types are allowed.
A committee is any nonempty subset \(S\subseteq C\); its size is unrestricted. Type \(A\) is satisfied exactly when \(|A\cap S|\ge\lceil |S|/2\rceil\), so equality counts as satisfaction.
Define \(F(S)=\sum_{A\in\mathcal A}\mu_A\mathbf 1[|A\cap S|\ge\lceil |S|/2\rceil]\) and \(\operatorname{OPT}=\max_{\varnothing\ne S\subseteq C}F(S)\). Any maximizing committee is an acceptable optimizer.

Is computing an exact maximizing committee polynomial-time solvable or NP-hard, and is deciding whether \(\operatorname{OPT}=1\) in \(\mathrm P\) or NP-hard? State running times in \(m,\tau,L\).

For explicitly listed, equally weighted voters, deciding whether some nonempty committee satisfies every voter is NP-hard; computing majority-threshold winners is reported FPT in either the number of candidates or the number of voters ([source](https://arxiv.org/pdf/1711.06641)).
No result explicitly treating the binary-rational support-mass formulation was located in the search.

Modeling choices made when packaging the task

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

1. Result

Computing an exact maximizing committee is NP-hard. Deciding whether \(\operatorname{OPT}=1\) is NP-complete. Thus neither problem has a polynomial-time algorithm unless \(\mathrm P=\mathrm{NP}\).

Both problems are fixed-parameter tractable in either \(\m\) or \(\tau\), with polynomial dependence on \(\L\). The arguments below establish this directly for the support-mass representation.

2. Satisfaction and unanimity

Write the distinct support types as \(\mathcal A=\{A_1,\ldots,A_\tau\}\). For every committee \(\S\), integer-valuedness gives
\[ \]
A type \(\A_i\) is satisfied exactly when \(\2|A_i\cap S|-|S|\ge 0\): this is equivalent to \(\|A_i\cap S|\ge\lceil |S|/2\rceil\), including equality.

Since every mass is strictly positive and the masses sum to \(\1\),

\(\displaystyle F(S)=1\quad\Longleftrightarrow\quad S\text{ satisfies every }A_i.\)

Consequently, deciding whether \(\operatorname{OPT}=1\) depends only on the support, not on the particular positive masses. An empty approval type makes this decision immediately negative, because committees must be nonempty.

3. Hardness for the support-mass formulation

We use the established theorem that, given explicitly listed voters, deciding whether a nonempty committee satisfies every voter under the threshold \(\|S|/2\) is NP-hard. This is precisely Theorem 8 of [Faliszewski, Slinko, and Talmon](https://arxiv.org/pdf/1711.06641). Its threshold agrees with the present ceiling threshold because intersection sizes are integers, and its committees are explicitly required to be nonempty.

Take an instance of that problem with \(\n\ge 1\) explicitly listed voters and \(\m\) candidates. Remove duplicate approval ballots, obtaining distinct types \(\A_1,\ldots,A_\tau\), where \(\1\le\tau\le n\). Removing duplicates preserves the existence of a committee satisfying everyone.

To ensure short encodings even if “binary-rational” is interpreted as requiring dyadic rationals, set

\(\displaystyle D=2^{\lceil\log_2\tau\rceil},\qquad \mu_{A_i}=\frac1D\ (1\le i<\tau),\qquad \mu_{A_\tau}=\frac{D-\tau+1}{D}.\)

All these masses are positive: \(\D\ge\tau\). Their sum is

\(\displaystyle \frac{\tau-1+D-\tau+1}{D}=1.\)

Each mass has encoding length \(\O(\log(\tau+1))\), so the total length is \(\L=O(\tau\log(\tau+1))\). Deduplication and constructing these masses take polynomial time in the original explicit input length.

By Section 2,

\(\displaystyle \text{the original voters admit a unanimously satisfactory nonempty committee} \quad\Longleftrightarrow\quad \operatorname{OPT}=1 \text{ in the constructed society}.\)

This is a polynomial-time many-one reduction, proving NP-hardness of the unanimity decision problem.

The problem also belongs to \(\mathrm{NP}\). A certificate is the \(\m\)-bit incidence vector of a nonempty committee. For each support type, count its approved committee members and check the threshold. This takes \(\operatorname{poly}(m,\tau,L)\) time and does not require summing masses. Hence the problem is NP-complete.

Finally, an exact optimizer would solve this decision problem: compute its maximizing committee and check whether it satisfies every support type. Therefore computing any exact maximizing committee is NP-hard, regardless of how ties are broken.

4. Exact algorithm parameterized by candidates

Enumerate the \(\2^m-1\) nonempty committees, compute each score exactly, and retain a maximizer.

Here is an explicit bit-complexity bound under the usual binary numerator/denominator encoding. Write \(\mu_{A_i}=a_i/b_i\), and define

\(\displaystyle Q=\prod_{i=1}^{\tau}b_i,\qquad w_i=a_i(Q/b_i).\)

Then \(\w_i\) are positive integers, \(\sum_i w_i=Q\), and

\(\displaystyle F(S)=\frac1Q\sum_{i:\,A_i\text{ is satisfied by }S}w_i.\)

The binary lengths of \(\Q\) and every \(\w_i\) are \(\O(L)\). Using elementary integer arithmetic, preprocessing takes \(\O(L^3)\) bit operations. For each committee, straightforward counting and score summation take \(\O(m\tau\log(m+1)+\tau L)\) bit operations.

Thus a conservative exact running time is

\(\displaystyle O\!\left(L^3+2^m\bigl(m\tau\log(m+1)+\tau L\bigr)\right).\)

In particular, both optimization and unanimity decision have running time \(\2^m\operatorname{poly}(m,\tau,L)\).

5. Exact algorithm parameterized by support size

Candidate signatures and integer feasibility

For each candidate \(\c\), define its signature

\(\displaystyle T(c)=\{i\in\{1,\ldots,\tau\}:c\in A_i\}.\)

Let \(\mathcal T\) be the set of signatures occurring among candidates, let \(\d=|\mathcal T|\), and let \(\n_T\) count candidates with signature \(\T\). Then

\(\displaystyle d\le\min\{m,2^\tau\}.\)

Introduce one integer variable \(\x_T\) per occurring signature, representing how many candidates of that signature the committee contains. Exactly the realizable nonempty committees, up to interchange of candidates with the same signature, are described by

\(\displaystyle 0\le x_T\le n_T\quad(T\in\mathcal T),\qquad \sum_{T\in\mathcal T}x_T\ge1,\qquad x_T\in\mathbb Z.\)

For such a committee,

\(\displaystyle |S|=\sum_Tx_T,\qquad |A_i\cap S|=\sum_{T:\,i\in T}x_T.\)

Therefore satisfaction of type \(\A_i\) is exactly the linear inequality

\(\displaystyle \sum_{T\in\mathcal T}\bigl(2\mathbf1[i\in T]-1\bigr)x_T\ge0.\)

For any \(\B\subseteq\{1,\ldots,\tau\}\), impose these inequalities for every \(\i\in B\), together with the bounds and nonemptiness constraint. This integer program is feasible exactly when some nonempty committee satisfies all types indexed by \(\B\).

All coefficients are integers. The satisfaction coefficients are \(\{-1,1\}\), the bounds are at most \(\m\), and the program has \(\d\) integer variables and \(\O(d+\tau)\) inequalities. Its encoding length is polynomial in \(\m,\tau\).

Fixed-dimensional integer programming decides feasibility in time \(\2^{O(d^3)}\operatorname{poly}(H)\), where \(\H\) is the program’s binary encoding length. This conservative bound follows from Lenstra’s algorithm; it is stated explicitly in [Kannan’s primary paper](https://doi.org/10.1145/800061.808749). All its hypotheses hold here. A feasible vector can also be recovered; alternatively, bounded-coordinate binary search uses \(\O(d\log(m+1))\) feasibility calls.

Optimization by enumerating satisfied-type requirements

Enumerate all \(\2^\tau\) subsets \(\B\). For each feasible subset, compute

\(\displaystyle W(B)=\sum_{i\in B}\mu_{A_i},\)

and choose a feasible subset \(\B_{\max}\) of largest weight. Recover a committee satisfying its requirements.

To prove optimality, let \(\S^\star\) be an optimal committee and let \(\B^\star\) be its actual set of satisfied types. Then \(\B^\star\) is feasible and \(\W(B^\star)=\operatorname{OPT}\).

Conversely, for every feasible \(\B\), a witnessing committee \(\S_B\) satisfies at least those types. Since masses are positive,

\(\displaystyle W(B)\le F(S_B)\le\operatorname{OPT}.\)

Thus the largest feasible requirement weight is exactly \(\operatorname{OPT}\). Any committee witnessing feasibility of \(\B_{\max}\) has score at least that weight, and hence is an exact optimizer.

The resulting running time is

\(\displaystyle 2^\tau\,2^{O(d^3)}\operatorname{poly}(m,\tau,L) \;\le\; 2^{O(8^\tau)}\operatorname{poly}(m,\tau,L).\)

For unanimity decision, solve just the integer program with \(\B=\{1,\ldots,\tau\}\). Its running time is

\(\displaystyle 2^{O(d^3)}\operatorname{poly}(m,\tau,L) \;\le\; 2^{O(8^\tau)}\operatorname{poly}(m,\tau,L).\)

These bounds establish fixed-parameter tractability in the support size \(\tau\), with polynomial dependence on the binary mass encoding length \(\L\). No expansion into individual voters is needed.

⟨structured verdict parsed — rendered above⟩

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

Verdict

The output resolves both questions in substance, with only minor notation defects. Computing an exact maximizing committee is NP-hard, and deciding whether \(\operatorname{OPT}=1\) is NP-complete. Both stated parameterized algorithms are justified for the support-mass representation.

No major mathematical gap, false central step, or unverified theorem application was found.

Step-by-step verification

1. Satisfaction and unanimity

The intended equivalence
\[ |A_i\cap S|\ge\lceil |S|/2\rceil \quad\Longleftrightarrow\quad 2|A_i\cap S|-|S|\ge0 \]
is correct because the intersection size is an integer. It handles both committee parities and counts equality as satisfaction.

Strict positivity of every mass and normalization to total mass \(1\) justify the asserted equivalence between score \(1\) and satisfaction of every support type. Since the candidate set is finite and nonempty, the maximum exists, so this also characterizes \(\operatorname{OPT}=1\).

The empty-approval-type observation is correct: no nonempty committee satisfies such a type.

Issue: The displayed notation contains stray backslashes and an empty display. These are minor transcription defects; the surrounding statements determine the intended expressions.

2. Cited hardness theorem

The cited theorem matches the required source problem. Theorem 8 explicitly concerns a nonempty committee satisfying every voter, and the paper defines its majority threshold as half the committee size, with a weak inequality. Thus its threshold agrees with the task’s ceiling threshold for integer intersection sizes. [Faliszewski, Slinko, and Talmon, Section 6 and Theorem 8](https://arxiv.org/pdf/1711.06641).

The prover states the relevant theorem and checks the two potentially consequential hypotheses: nonemptiness and equality at the threshold. This application is verified.

3. Reduction to support masses

Removing duplicate ballots preserves unanimity: repeating an identical satisfaction requirement does not change feasibility. Distinct ballots therefore provide a valid support.

The mass construction is correct:

Deduplication and mass construction are polynomial in the explicitly listed source input. The resulting equivalence of yes-instances follows from the already verified unanimity characterization. The many-one reduction is valid.

4. NP membership and optimization hardness

An incidence vector certifies a nonempty committee using \(m\) bits. Checking each support type’s threshold is polynomial in \(m,\tau,L\). On the valid inputs specified by the task, mass summation is unnecessary for this certificate check.

Consequently, the unanimity decision problem is NP-complete.

The optimization reduction is also valid: any exact maximizing committee has score \(1\) precisely when unanimity is feasible. Checking its satisfaction of every support type decides the NP-complete problem. Allowing arbitrary tie-breaking does not weaken this argument.

5. Enumeration by candidates and exact arithmetic

Enumerating all nonempty committees includes every admissible optimizer.

The common-denominator construction is valid under the explicitly stated numerator/denominator encoding. Its properties follow from the input normalization:

Thus the claimed running time
\[ O\!\left(L^3+2^m\bigl(m\tau\log(m+1)+\tau L\bigr)\right) \]
is justified. It establishes fixed-parameter tractability in \(m\), with polynomial dependence on \(L\).

6. Candidate signatures and integer feasibility

Candidates sharing a signature have identical membership in every support type. Their identities therefore do not affect satisfaction; selecting their multiplicities suffices.

The integer bounds describe exactly the realizable multiplicities. The nonemptiness constraint excludes the otherwise automatically feasible empty committee.

The formulas for committee size and approved committee members are correct. Substituting them into the satisfaction condition gives exactly the stated linear inequality with coefficients in \(\{-1,1\}\).

For each requirement set \(B\), feasibility consequently means that a nonempty committee satisfies every indexed type. It need not mean that these are its only satisfied types, and the subsequent optimization argument correctly accounts for that distinction.

The variable bound \(d\le\min\{m,2^\tau\}\), constraint count, and polynomial encoding-length claim are all valid.

7. Fixed-dimensional integer programming

The invoked theorem concerns feasibility of integer linear inequalities with binary-encoded integer data and gives dependence \(2^{O(d^3)}\operatorname{poly}(H)\). The cited Kannan abstract explicitly records this bound for Lenstra’s algorithm. [Kannan, *Improved algorithms for integer programming and related lattice problems*](https://doi.org/10.1145/800061.808749).

The constructed programs meet these hypotheses. Bounded-coordinate recovery using the stated number of feasibility calls is a routine search-to-decision procedure; no additional mathematical result is missing here.

8. Optimization over requirement sets

The two inequalities used to prove optimality are sound:

These establish that the largest feasible requirement weight equals the optimum. Any witness for a maximizing requirement set is therefore an exact optimizer.

Exact requirement-weight comparisons can use the previously described integer weights, so binary masses introduce only polynomial arithmetic overhead.

Finally, \(d^3\le8^\tau\), and the enumeration and recovery factors fit the stated bounds:
\[ 2^\tau 2^{O(d^3)}\operatorname{poly}(m,\tau,L) \le 2^{O(8^\tau)}\operatorname{poly}(m,\tau,L). \]
For unanimity, a single requirement set containing all support types suffices.

Actionable feedback

Minor — mathematical transcription throughout. Remove stray backslashes from identifiers and numeric expressions, correct the malformed absolute-value notation, and delete the empty display in Section 2. No new lemma, reduction, or algorithmic argument 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.