← back to the atlas

On the Edge of Core (Non-)Emptiness: An Automated Reasoning Approach to Approval-Based Multi-Winner Voting (d4-conf-aaai-2026-0988)

Answer: The decision problem is in \(\mathrm P\) under the stated explicit cost-table representation.

The anchor (named result in the paper)

Theorem 1 — class: other

The continuous mirror question, as graded

Given candidates \(C\), committee size \(k\), approval types \(T\subseteq 2^C\), rational population distribution \(\mu\in\Delta_{\mathbb Q}(T)\), margin \(\delta>0\), and conversion costs \(\gamma(A,B)\), choose \(W\in\binom{C}{k}\) and a transport plan \(y_{A,B}\ge 0\) with \(\sum_B y_{A,B}=\mu_A\), inducing \(\nu_B=\sum_A y_{A,B}\), to minimize \(\sum_{A,B}\gamma(A,B)y_{A,B}\) subject to \(\sum_{B:\,|B\cap W'|>|B\cap W|}\nu_B\le |W'|/k-\delta\) for every \(\varnothing\ne W'\subseteq C\) with \(|W'|\le k\).

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

Let \(C\) contain \(m\) candidates and let \(1\le k<m\). A society is given by its support: a list \(T\subseteq 2^C\) of \(\tau\) approval types with positive binary rational masses \(\mu_A\), summing to \(1\). Here \(\tau\) is the support size, not the number of possible approval sets; empty approval sets are allowed.
Conversions may send mass from any \(A\in T\) to any \(B\subseteq C\). The input explicitly lists all costs \(\gamma(A,B)\in\mathbb Q_{\ge0}\), with \(\gamma(A,A)=0\), and binary rational numbers \(\delta>0\) and \(b\ge0\). Let \(L\) be the total input bit length, including the cost table.
Choose a committee \(W\subseteq C\) with \(|W|=k\) and divisible transports \(y_{A,B}\in\mathbb R_{\ge0}\) satisfying \(\sum_{B\subseteq C}y_{A,B}=\mu_A\); write \(\nu_B=\sum_{A\in T}y_{A,B}\). Require
\(\sum_{B\subseteq C:\,|B\cap W'|>|B\cap W|}\nu_B\le |W'|/k-\delta\)
for every \(W'\subseteq C\) with \(1\le |W'|\le k\). Only strict approval-count improvements contribute; ties do not.
Decide whether such choices exist with \(\sum_{A\in T}\sum_{B\subseteq C}\gamma(A,B)y_{A,B}\le b\).

Is this decision problem in \(\mathrm P\), or is it \(\mathrm{NP}\)-hard? State running times in \(m,\tau,L,k\).

Known results: For finite approval profiles, the worst-profile maximum of the minimum, over committees, of the maximum deviation support excess has an exact MILP reformulation; this also holds over rational vote distributions ([source](https://arxiv.org/html/2512.16895v1)). This equivalence supplies no complexity classification for the transport problem above; no classification of that exact problem was located in the literature search.

Modeling choices made when packaging the task

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

Classification

The problem is in \(\mathrm P\) under the stated explicit cost-table representation. The decisive observation is that the input already contains \(\tau 2^m\) cost entries, so enumerating committees and deviations is polynomial in the total input length.

1. Fixing the committee gives an exact linear program

Define
\(\mathcal D_k=\{W'\subseteq C:1\le |W'|\le k\}\)
and
\(D_k=|\mathcal D_k|=\sum_{j=1}^k\binom mj\).

Fix a committee \(W\subseteq C\) with \(|W|=k\). For each destination \(B\subseteq C\) and deviation \(W'\in\mathcal D_k\), compute the constant

\(a^W_{B,W'}=\begin{cases}1,&|B\cap W'|>|B\cap W|,\\0,&|B\cap W'|\le |B\cap W|.\end{cases}\)

Thus ties have coefficient zero, exactly as required.

Consider the following rational linear feasibility problem with \(N=\tau 2^m\) nonnegative variables \(y_{A,B}\):

This formulation is equivalent to the original requirements for this fixed \(W\). Indeed, defining \(\nu_B=\sum_{A\in T}y_{A,B}\) gives

\(\sum_{A\in T}\sum_{B\subseteq C}a^W_{B,W'}y_{A,B}=\sum_{B:\,|B\cap W'|>|B\cap W|}\nu_B.\)

Consequently, each deviation constraint has exactly the intended left-hand side. The conservation and budget constraints also coincide with the original ones. Empty approval sets require no special treatment: they are included among the destinations.

We use the standard theorem that feasibility of a linear program with explicitly encoded rational coefficients and nonnegative real variables is decidable in time polynomial in its binary encoding length. Its hypotheses hold here: all coefficients and right-hand sides are rational, all constraints are linear and non-strict, and every variable and constraint is explicitly listed. Divisibility of transports means that no integrality constraint is needed.

2. Correctness of the algorithm

Enumerate all \(\binom mk\) committees of size \(k\), solve the corresponding linear programs, and accept precisely when at least one is feasible.

If the algorithm accepts, the feasible transport for the accepted committee satisfies every original constraint by the equivalence above. Conversely, any feasible solution of the original problem has a committee appearing in the enumeration, and its transport makes that committee’s linear program feasible. Hence the algorithm decides the problem exactly.

3. Encoding size and running time

Because the masses sum to one, \(T\) is nonempty. The explicitly listed cost table has \(N=\tau 2^m\) entries, each requiring at least one bit. Therefore

\(N\le L,\qquad 2^m\le L/\tau,\qquad \binom mk\le 2^m,\qquad D_k\le 2^m-1.\)

These inequalities use \(\tau\) as the actual support size.

For one fixed committee, the linear program has \(N\) variables and \(\tau+D_k+1\) constraints besides nonnegativity. A dense encoding has length at most

\(H=O\!\left(N(\tau+D_k+1)+(D_k+1)L\right).\)

To justify this bound, the conservation and deviation matrices contain only zero-one entries; the cost row and masses use at most their original input length; and each deviation right-hand side \(|W'|/k-\delta\) has bit length \(O(L)\). The latter follows by writing \(\delta=p/q\), giving right-hand side \((|W'|q-kp)/(kq)\).

Since \(N,\tau,D_k\le L\), we obtain \(H=O(L^2)\). Computing the comparison coefficients and assembling each program also takes polynomial time in these quantities.

Thus a running-time bound displaying all requested parameters is

\(O(L)+\binom mk\left(L+\tau 2^m+\sum_{j=1}^k\binom mj\right)^{O(1)}.\)

Using the explicit-table inequalities, this is \(L^{O(1)}\). The algorithm works for every permitted \(k\), arbitrary positive binary rational masses, and the stated arbitrary nonnegative rational costs.

The polynomial-time classification follows directly from this representation and the fixed-committee linear programs; it does not require the supplied worst-profile MILP equivalence.

⟨structured verdict parsed — rendered above⟩

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

Verification verdict

The prover’s output correctly resolves the task: the decision problem is in \(\mathrm P\) under the explicitly listed cost-table representation. The fixed-committee linear programs are exact, and both their sizes and the number of programs are polynomial in the total input length. No major or minor issues were found.

Step-by-step audit

1. Fixed-committee formulation

For a fixed committee \(W\), the variables \(y_{A,B}\) cover every permitted source and destination. Their nonnegativity and the conservation equations reproduce the transport requirements exactly.

The coefficients \(a^W_{B,W'}\) correctly distinguish strict improvement from a tie. In particular, approval-count comparisons are performed when constructing the coefficients; they do not introduce strict inequalities into the linear program.

The displayed identity
\[ \sum_{A\in T}\sum_{B\subseteq C}a^W_{B,W'}y_{A,B} = \sum_{B:\,|B\cap W'|>|B\cap W|}\nu_B \]
is valid by the definition of \(\nu_B\) and rearrangement of finite sums. Thus every deviation constraint has precisely the required left-hand side and threshold. The budget constraint is also unchanged.

Empty approval types are handled correctly, both as sources when present in \(T\) and as destinations. For an empty destination, every comparison coefficient is zero.

Finding: The fixed-committee equivalence is correct in both directions.

2. Applicability of polynomial-time linear programming

The invoked theorem is stated sufficiently precisely for this application: feasibility of an explicitly encoded rational linear program over nonnegative real variables is decidable in time polynomial in its binary encoding length.

Its hypotheses hold:

A possibly negative deviation threshold creates no exception to the theorem. Such constraints are retained and feasibility is decided normally. The argument therefore does not silently assume a smaller range for \(\delta\).

Finding: The theorem application is justified.

3. Committee enumeration and correctness

The algorithm enumerates every committee of the required size. Its acceptance criterion is exactly the existential choice of committee in the task.

Both directions of correctness follow from the established fixed-committee equivalence: acceptance supplies a valid committee and transport, while any valid original solution makes one enumerated program feasible.

Finding: The algorithm decides the stated problem exactly.

4. Input-length bounds

Positive masses summing to one imply \(\tau\ge1\). Since the input explicitly contains \(\tau2^m\) cost entries, each requiring at least one bit, the inequalities
\[ \tau2^m\le L,\qquad 2^m\le L/\tau \]
are valid. Consequently, both \(\binom mk\) and \(D_k\) are bounded by \(L\). This is the essential representation-dependent argument, and it uses the actual support size correctly.

The dense LP encoding bound is also valid. The conservation and deviation matrices have constant-size entries. The original cost row and masses contribute at most their input encoding length. For each deviation, the expression
\[ \frac{|W'|q-kp}{kq} \]
has bit length \(O(L)\), since the encodings of \(p,q\) and the relevant integers are bounded by the input length. Thus the claimed bound \(H=O(L^2)\) follows.

Finding: No hidden exponentially large encoding remains relative to \(L\).

5. Running time and scope

The stated bound
\[ O(L)+\binom mk \left(L+\tau2^m+\sum_{j=1}^{k}\binom mj\right)^{O(1)} \]
correctly displays the requested parameters. Constructing the comparisons introduces polynomial work in \(m\), which is absorbed by the displayed bound because the explicit-table inequality bounds \(m\) in terms of \(L\).

Substituting the established input-length bounds makes the entire running time \(L^{O(1)}\). No use of the supplied MILP equivalence is necessary.

Finding: The polynomial-time classification is established for the exact representation specified in the task. 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.