← back to the atlas

d4-conf-aaai-2026-0317 (d4-conf-aaai-2026-0317)

Answer: \(\mathrm{PSPACE}\text{-complete}\), hence \(\mathrm{NP}\text{-hard}\)

The anchor (named result in the paper)

Theorem 3.4 — class: hardness

PDF text-layer excerpt — equations and symbol order may be approximateGiven an instance (A, k) and two JR commit- tees, deciding whether the two committees are connected in JR(A, k) is PSPACE-complete.

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

The continuous mirror question, as graded

Given a candidate set \(C\), committee size \(k\), a finite support of approval types \(A\subseteq C\) with positive binary-rational masses \(\mu_A\) summing to \(1\), and two size-\(k\) committees \(W_s,W_t\), decide whether there is a finite path \(W_s=W_0,\ldots,W_r=W_t\) in which consecutive committees differ by one swap and every \(W_i\) satisfies \(\sum_{A:\,c\in A,\ A\cap W_i=\emptyset}\mu_A<1/k\) for every \(c\in C\).

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

Let \(C\) be a candidate set with \(m=|C|\), and let \(1\le k\le m\) be an integer. A society is given by its support: a list \(\mathcal S\) of \(\tau\) distinct approval types \(A\subseteq C\), each with positive binary-rational mass \(\mu_A\), with \(\sum_{A\in\mathcal S}\mu_A=1\). Empty approval types are allowed. Here \(\tau\) is the support size, not the number of possible approval types; let \(L\) be the total input bit length.
A committee is a subset \(W\subseteq C\) with \(|W|=k\). Call it admissible if \(\sum_{A\in\mathcal S:\ c\in A,\ A\cap W=\emptyset}\mu_A<1/k\) for every \(c\in C\); equality violates admissibility.
The input includes two admissible committees \(W_s,W_t\). Decide whether there is a finite sequence \(W_s=W_0,\ldots,W_r=W_t\), with \(r\ge0\), of admissible committees such that \(|W_i\setminus W_{i+1}|=|W_{i+1}\setminus W_i|=1\) at every step. Intermediate committees may use any candidates in \(C\).

Is this rational-mass committee reachability problem solvable in polynomial time in \(m,\tau,k,L\), or is it NP-hard?

For an explicitly listed finite electorate, reachability between two committees satisfying justified representation under these single-swap moves is PSPACE-complete ([Dong et al., 2026](https://ojs.aaai.org/index.php/AAAI/article/download/38727/42689)). No separate result for exactly the rational-mass formulation was located 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 \(\mathrm{PSPACE}\)-complete, and therefore \(\mathrm{NP}\)-hard. A polynomial-time algorithm would imply \(\mathrm{P}=\mathrm{PSPACE}\).

Here, “binary-rational” is interpreted as a rational number whose numerator and denominator are encoded in binary. The reduction below uses exact fractions.

1. Justified representation as an unrepresented-support condition

Consider an explicitly listed electorate with \(n\ge 1\) voters and approval ballots \(A_1,\ldots,A_n\). For a committee \(W\) and candidate \(c\), define

\(U_c(W)=\{i:c\in A_i,\ A_i\cap W=\emptyset\}.\)

We claim that

\(W\text{ satisfies justified representation}\quad\Longleftrightarrow\quad |U_c(W)|<n/k\text{ for every }c\in C.\)

Indeed, if \(|U_c(W)|\ge n/k\), these voters form a group of size at least \(n/k\) with common approved candidate \(c\), and none approves any member of \(W\). This violates justified representation.

Conversely, a violation of justified representation consists of a group \(G\) of at least \(n/k\) voters who share an approved candidate \(c\) and are all unrepresented by \(W\). Thus \(G\subseteq U_c(W)\), implying \(|U_c(W)|\ge n/k\).

This equivalence includes the boundary case: equality violates justified representation.

2. Polynomial reduction to rational masses

We use the following established result: reachability between two JR committees in an explicitly listed electorate, using swaps of one candidate and allowing all candidates in intermediate committees, is \(\mathrm{PSPACE}\)-complete. This is Theorem 3.4 of [Dong et al., *Reconfiguring Proportional Committees*](https://ojs.aaai.org/index.php/AAAI/article/download/38727/42689).

Take an instance of that problem. Keep \(C\), \(k\), \(W_s\), and \(W_t\) unchanged. Group identical approval ballots. For each distinct ballot \(A\), let

\(n_A=|\{i:A_i=A\}|,\qquad \mu_A=n_A/n.\)

Let \(\mathcal S\) contain exactly the distinct ballots that occur. These types are distinct, their masses are positive, and

\(\displaystyle\sum_{A\in\mathcal S}\mu_A=\frac{\sum_{A\in\mathcal S}n_A}{n}=1.\)

An empty ballot, if present, is treated identically.

For every committee \(W\subseteq C\) of size \(k\) and every candidate \(c\),

\(\displaystyle\sum_{\substack{A\in\mathcal S\\c\in A,\ A\cap W=\emptyset}}\mu_A=\frac{|U_c(W)|}{n}.\)

Consequently,

\(\displaystyle\sum_{\substack{A\in\mathcal S\\c\in A,\ A\cap W=\emptyset}}\mu_A<\frac1k \quad\Longleftrightarrow\quad |U_c(W)|<\frac nk.\)

By Section 1, the admissible committees of the constructed instance are exactly the JR committees of the original instance.

Since the candidate set and committee size are unchanged, adjacency under a single swap is also unchanged. Thus the entire reconfiguration graph is preserved, including committees using candidates outside \(W_s\cup W_t\). In particular, the endpoint promise is preserved, and the two instances have the same reachability answer.

The construction is polynomial. Grouping explicitly listed ballots takes polynomial time; \(\tau\le n\); and each fraction \(n_A/n\) needs \(O(\log(n+1))\) bits. Using candidate incidence vectors, the resulting input has length

\(O\!\left(\tau m+\tau\log(n+1)+m+\log(k+1)\right),\)

which is polynomial in the explicit source input size. This proves \(\mathrm{PSPACE}\)-hardness.

3. Polynomial-space upper bound

First, admissibility can be checked exactly in polynomial time.

Write each input mass as \(\mu_A=p_A/q_A\), with positive integer denominator \(q_A\), and set

\(Q=\prod_{A\in\mathcal S}q_A.\)

The bit length of \(Q\) is at most the sum of the denominator bit lengths, hence \(O(L)\). For each candidate \(c\), admissibility is equivalent to the integer comparison

\(\displaystyle k\sum_{\substack{A\in\mathcal S\\c\in A,\ A\cap W=\emptyset}}p_A(Q/q_A)<Q.\)

All integers involved have polynomial bit length. Thus exact arithmetic handles equality without approximation.

Now let \(G\) be the graph whose vertices are admissible committees and whose edges are single swaps. It has at most

\(\binom{m}{k}\le 2^m\)

vertices. If two vertices are connected, deleting repeated-vertex segments from a connecting walk gives a path of length less than \(2^m\).

Here is a deterministic polynomial-space reachability procedure. For admissible \(U,V\), define \(R_j(U,V)\) to mean that there is a path of length at most \(2^j\).

At \(j=0\), check whether \(U=V\) or whether they are adjacent. For \(j\ge1\), use

\(R_j(U,V)\Longleftrightarrow \exists Z\text{ admissible}:R_{j-1}(U,Z)\ \text{and}\ R_{j-1}(Z,V).\)

For the forward implication, split a path after at most \(2^{j-1}\) edges. For the reverse implication, concatenate the two paths.

Enumerate possible \(Z\) as \(m\)-bit incidence vectors, checking cardinality and admissibility. Evaluate the recursive calls sequentially. The recursion depth for \(R_m(W_s,W_t)\) is \(m\), and each level stores only a constant number of committees and enumeration counters. Together with the exact-arithmetic workspace, this uses polynomial space.

Therefore the problem belongs to \(\mathrm{PSPACE}\), completing the proof.

⟨structured verdict parsed — rendered above⟩

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

The prover’s claim is correct and rigorous under its explicitly stated encoding of rational numbers. The reduction establishes \(\mathrm{PSPACE}\)-hardness, and the reachability procedure establishes membership in \(\mathrm{PSPACE}\). No major or minor mathematical issues were found.

1. Scope and encoding

The prover interprets “binary-rational” as a rational number represented by a numerator and denominator encoded in binary. This is a natural interpretation of the task’s rational-mass formulation, and the interpretation is stated explicitly.

The fractions used in the reduction are valid under that interpretation. The argument does not establish a result for a separately imposed restriction to dyadic masses, but the task does not explicitly impose that restriction.

2. Equivalence between JR and the support inequality

The claimed equivalence is correct.

These implications correctly handle nonintegral \(n/k\): an integer group size meets the threshold precisely when it is at least \(n/k\). Equality is correctly treated as a violation.

Empty ballots cause no difficulty because they cannot belong to a group sharing an approved candidate.

3. Verification of the cited hardness theorem

The citation is accurate. Theorem 3.4 states \(\mathrm{PSPACE}\)-completeness of deciding connectedness between two given JR committees. The paper’s definitions use fixed-size committees, single-candidate swaps, and intermediate committees drawn from the full candidate set. Thus the cited source problem matches the problem invoked by the prover. See [Dong et al., Theorem 3.4 and Section 2](https://ojs.aaai.org/index.php/AAAI/article/download/38727/42689).

The endpoint condition also matches: both source committees satisfy JR. No hypothesis needed for this application is missing.

4. Validity of the reduction

Every part of the construction is justified.

\[ \sum_{\substack{A\in\mathcal S\\c\in A,\ A\cap W=\emptyset}}\mu_A =\frac{\lvert U_c(W)\rvert}{n}. \]

Consequently, the construction preserves the entire vertex set of the reconfiguration graph. Keeping the candidate set and committee size unchanged also preserves every edge. This establishes both directions of reachability preservation, including paths using candidates outside the endpoint union.

The size analysis is correct for the stated incidence-vector representation. There are at most \(n\) occurring types, and each numerator and denominator needs \(O(\log(n+1))\) bits. Grouping and producing the output take polynomial time in the explicitly listed source input.

Thus the reduction establishes \(\mathrm{PSPACE}\)-hardness.

5. Exact admissibility checking

The common-denominator calculation is valid. Every \(q_A\) divides \(Q\), and multiplication by the positive integer \(kQ\) converts the original inequality into precisely the integer comparison written by the prover.

The bit length of \(Q\) is bounded by the sum of the denominator bit lengths. Products, partial sums, and the final multiplication by \(k\) all have polynomial bit length. There are polynomially many arithmetic operations.

Therefore admissibility is decidable exactly in polynomial time. Equality is rejected correctly.

6. Polynomial-space reachability

The graph has at most \(\binom{m}{k}\le 2^m\) vertices. Removing repeated-vertex segments gives a connecting path with fewer than \(2^m\) edges, so testing \(R_m\) suffices.

The recurrence is correct. A path of length at most \(2^j\) can be split so that both portions have length at most \(2^{j-1}\); concatenating two such portions proves the reverse implication. Zero-length portions are permitted by the definition.

The base case correctly accepts equality or adjacency between admissible committees. Enumeration filters out invalid cardinalities and inadmissible intermediate committees.

Sequential recursive evaluation requires only polynomial storage: the recursion depth is \(m\), each frame stores polynomially many bits, and the exact-arithmetic workspace is polynomial. Exponential running time does not invalidate the polynomial-space bound.

The argument also covers equal endpoints, \(k=1\), and \(k=m\).

7. Adjudication and feedback

The output fully resolves the assigned problem. Its \(\mathrm{PSPACE}\)-completeness conclusion follows, as do \(\mathrm{NP}\)-hardness and the consequence that a polynomial-time algorithm would imply \(\mathrm{P}=\mathrm{PSPACE}\).

No repair or additional clarification is required under the stated rational encoding.

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