← back to the atlas

Verifying Proportionality in Temporal Voting (aaai25-33509)

Answer: \(\mathrm{NP}\text{-complete}\)

The anchor (named result in the paper)

Theorem 3.1 — class: hardness

PDF text-layer excerpt — equations and symbol order may be approximateFor each of X 2 {w-JR, w-PJR, w-EJR}, veri- fying whether an outcome provides X is coNP-complete. The hardness result holds for w-JR and w-PJR even if |P| = 3, and for w-EJR even if |P| = 2.

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

The continuous mirror question, as graded

Given candidates P, horizon ℓ, rational masses over complete temporal approval types, and an integral outcome o∈P^ℓ, decide whether every submass whose support agrees in all ℓ rounds and has positive demand contains a type receiving positive satisfaction.

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

Given a finite candidate set \(P\), horizon \(\ell\), outcome \(o=(o_1,\ldots,o_\ell)\in P^\ell\), finite type set \(T\), and rational probability mass function \(\mu:T\to\mathbb{Q}_{\ge 0}\), each type \(\tau\in T\) has approval sets \(A_{\tau,r}\subseteq P\) for \(r\in[\ell]\). Define \(\operatorname{sat}_{\tau}(o)=|\{r\in[\ell]:o_r\in A_{\tau,r}\}|\).

A violating submass is a vector \(\lambda:T\to\mathbb{Q}_{\ge0}\) with \(\lambda_\tau\le\mu_\tau\), \(\lambda_\tau>0\Rightarrow\operatorname{sat}_{\tau}(o)=0\), \(\sum_{\tau\in T}\lambda_\tau\ge1/\ell\), and \(\bigcap_{\tau:\lambda_\tau>0}A_{\tau,r}\ne\varnothing\) for every \(r\in[\ell]\).

Target. Is deciding whether a violating submass exists solvable in polynomial time, or is it NP-hard?

For a finite voter list, deciding whether an outcome fails weak justified representation is NP-complete; equivalently, verifying weak justified representation is coNP-complete. No result for the distribution-over-types formulation above is assumed known.

Prover output (gpt-5.6-sol / xhigh, Bolzano prover prompt)

Complexity of Detecting a Violating Submass

Theorem

The decision problem is \( \mathrm{NP}\)-complete. In particular, it remains \( \mathrm{NP}\)-hard when \( |P|=3 \), the outcome is constant across all rounds, every type has positive rational mass, and every approval set has size at most two.

1. An Equivalent Optimization Formulation

Let

\[ Z=\{\tau\in T:\operatorname{sat}_{\tau}(o)=0\} \]

be the set of types eligible to receive positive violating submass.

For \(p=(p_1,\ldots,p_\ell)\in P^\ell\), define

\[ C(p)=\{\tau\in Z:p_r\in A_{\tau,r}\text{ for every }r\in[\ell]\} \]

and

\[ W(p)=\sum_{\tau\in C(p)}\mu_\tau. \]

Lemma 1

A violating submass exists if and only if there is some \(p\in P^\ell\) such that

\[ W(p)\geq \frac1\ell. \]

Proof

Suppose first that \(\lambda\) is a violating submass, and let

\[ S=\{\tau\in T:\lambda_\tau>0\}. \]

Every type in \(S\) belongs to \(Z\). For each round \(r\), the definition of a violating submass gives

\[ \bigcap_{\tau\in S}A_{\tau,r}\neq\varnothing. \]

Choose \(p_r\) from this intersection. Then every \(\tau\in S\) belongs to \(C(p)\), and therefore

\[ W(p)\geq\sum_{\tau\in S}\mu_\tau \geq\sum_{\tau\in S}\lambda_\tau \geq\frac1\ell. \]

Conversely, suppose \(W(p)\geq 1/\ell\). Define

\[ \lambda_\tau= \begin{cases} \mu_\tau,&\tau\in C(p),\\ 0,&\tau\notin C(p). \end{cases} \]

Then \(0\leq\lambda_\tau\leq\mu_\tau\), every type receiving positive mass has zero satisfaction, and

\[ \sum_{\tau\in T}\lambda_\tau=W(p)\geq\frac1\ell. \]

Moreover, for every \(r\), the candidate \(p_r\) belongs to \(A_{\tau,r}\) for every \(\tau\) in the support of \(\lambda\). Hence every required intersection is nonempty. Thus \(\lambda\) is a violating submass. \( \square \)

2. Membership in \( \mathrm{NP} \)

A certificate is a tuple \(p\in P^\ell\).

Given \(p\), one computes \(Z\), checks for each \(\tau\in Z\) whether \(p_r\in A_{\tau,r}\) for every \(r\), and sums the corresponding rational masses. By Lemma 1, the certificate is accepting exactly when this sum is at least \(1/\ell\).

The tuple has polynomial length because the outcome and the round-indexed approval sets already explicitly describe all \(\ell\) rounds. Addition and comparison of polynomially many binary-encoded rational numbers can be performed in polynomial time. Hence the problem belongs to \( \mathrm{NP} \).

3. Reduction from \( \mathrm{Independent\ Set} \)

We use the standard \( \mathrm{NP}\)-complete problem \( \mathrm{Independent\ Set} \): given a finite undirected graph \(G=(V,E)\) and an integer \(k\) with \(1\leq k\leq |V|\), decide whether \(G\) has an independent set of size at least \(k\).

Write \(n=|V|\) and \(m=|E|\). Set

\[ \ell=m+n+1. \]

There is one round \(r_e\) for each edge \(e\in E\), followed by \(n+1\) padding rounds.

Let

\[ P=\{a,b,d\}, \qquad o=(d,\ldots,d). \]

For every vertex \(v\in V\), create a type \(\tau_v\). Also create one dummy type \(\tau_\star\).

Arbitrarily orient each edge, writing it as \(e=(x_e,y_e)\). At its associated round \(r_e\), define

\[ A_{\tau_v,r_e}= \begin{cases} \{a\},&v=x_e,\\ \{b\},&v=y_e,\\ \{a,b\},&v\notin\{x_e,y_e\}. \end{cases} \]

At every padding round, put

\[ A_{\tau_v,r}=\{a,b\}. \]

For the dummy type, put

\[ A_{\tau_\star,r}=\{d\} \]

at every round.

Finally, define the probability masses by

\[ \mu_{\tau_v}=\frac{1}{k\ell} \quad\text{for every }v\in V, \qquad \mu_{\tau_\star}=1-\frac{n}{k\ell} =\frac{k\ell-n}{k\ell}. \]

Because \(\ell=m+n+1>n\) and \(k\geq1\), all these masses are positive. They sum to one, so \(\mu\) is a rational probability mass function. The construction has polynomial size.

Every vertex type has zero satisfaction because none of its approval sets contains \(d\). The dummy type has satisfaction \(\ell\), so it cannot receive positive violating submass.

4. Compatibility Encodes Independence

Lemma 2

For \(S\subseteq V\), the intersections

\[ \bigcap_{v\in S}A_{\tau_v,r} \]

are nonempty for every round \(r\) if and only if \(S\) is an independent set of \(G\).

Proof

Suppose \(S\) contains both endpoints \(x_e,y_e\) of some edge \(e\). At round \(r_e\), these two types approve respectively \(\{a\}\) and \(\{b\}\). Consequently,

\[ A_{\tau_{x_e},r_e}\cap A_{\tau_{y_e},r_e} =\{a\}\cap\{b\} =\varnothing. \]

Thus the required intersections cannot all be nonempty.

Conversely, suppose \(S\) is independent. Consider an edge \(e=(x_e,y_e)\). At most one of \(x_e,y_e\) lies in \(S\).

At every padding round all selected types approve \(\{a,b\}\). Hence every roundwise intersection is nonempty. \( \square \)

5. Correctness of the Reduction

Suppose \(G\) has an independent set \(S\) of size at least \(k\). Choose a \(k\)-vertex independent subset \(S'\subseteq S\) and define

\[ \lambda_{\tau_v}= \begin{cases} \frac{1}{k\ell},&v\in S',\\ 0,&v\notin S', \end{cases} \qquad \lambda_{\tau_\star}=0. \]

All types in its support have zero satisfaction. By Lemma 2, their approval sets have nonempty intersection in every round. Moreover,

\[ \sum_{\tau\in T}\lambda_\tau =\frac{k}{k\ell} =\frac1\ell. \]

Thus a violating submass exists.

Conversely, suppose a violating submass \(\lambda\) exists. The dummy type cannot belong to its support, so let

\[ S=\{v\in V:\lambda_{\tau_v}>0\}. \]

By the intersection condition and Lemma 2, \(S\) is independent. Since every vertex type has mass \(1/(k\ell)\),

\[ \frac1\ell \leq\sum_{\tau\in T}\lambda_\tau =\sum_{v\in S}\lambda_{\tau_v} \leq\frac{|S|}{k\ell}. \]

Multiplying by \(k\ell>0\) gives \( |S|\geq k \). Therefore \(G\) has an independent set of size at least \(k\).

The reduction is therefore correct.

Conclusion

The problem is both in \( \mathrm{NP} \) and \( \mathrm{NP}\)-hard, hence \( \mathrm{NP}\)-complete. Consequently, it is not polynomial-time solvable unless \( \mathrm{P}=\mathrm{NP} \). The hardness arises even with only three candidates; the unbounded horizon supplies the coordinates needed to encode pairwise incompatibilities.

⟨structured verdict parsed — rendered above⟩

Adversarial review (gpt-5.6-sol / high, Bolzano verifier prompt)

Verification Report

Overall assessment

The prover correctly establishes that deciding whether a violating submass exists is \( \mathrm{NP} \)-complete. The equivalence lemma, membership argument, and reduction from \( \mathrm{Independent\ Set} \) are logically sound and cover the claimed restrictions.

Step-by-step verification

1. Equivalent optimization formulation

The set

\[ Z=\{\tau\in T:\operatorname{sat}_{\tau}(o)=0\} \]

correctly identifies the only types permitted in the support of a violating submass.

Lemma 1 is correct in both directions:

There is no hidden fractional-selection issue: once a compatible collection has sufficient total available mass, taking all of it is permitted.

2. Membership in \( \mathrm{NP} \)

The certificate \(p\in P^\ell\) is sufficient by Lemma 1.

Under the explicit input representation used in the task, the certificate length is polynomial: the input already specifies approval sets for every type-round pair and therefore has size at least proportional to \(\ell\).

Eligibility, membership in \(C(p)\), rational summation, and comparison with \(1/\ell\) are all polynomial-time operations on binary-encoded rational inputs. Summing polynomially many rationals may increase numerator and denominator lengths, but only polynomially in the total input bit length.

Thus the membership argument is valid.

3. Construction of the reduction

The construction is polynomial in the size of \(G\):

The masses are valid:

\[ \sum_{v\in V}\frac{1}{k\ell}+\left(1-\frac{n}{k\ell}\right)=1. \]

Since \(\ell>n\) and \(k\geq1\), one has \(k\ell>n\), so the dummy mass is strictly positive. Every vertex mass is also strictly positive. Their binary encodings have polynomial length.

Every vertex type has zero satisfaction because \(d\) belongs to none of its approval sets. The dummy type has satisfaction \(\ell\), so the violating-submass definition excludes it from positive support.

4. Compatibility lemma

Lemma 2 correctly characterizes independent sets.

If \(S\) contains both endpoints of an edge, then at that edge's round the total intersection is contained in \(\{a\}\cap\{b\}=\varnothing\).

If \(S\) is independent, at most one endpoint of each edge belongs to \(S\). The corresponding intersection is therefore \(\{a\}\), \(\{b\}\), or \(\{a,b\}\), and padding rounds also have nonempty intersection.

For \(S=\varnothing\), the proof implicitly uses the conventional intersection of an empty family as the ambient set \(P\). This case is immaterial to the reduction's correctness because a violating submass has positive total mass and hence nonempty support.

5. Forward direction of the reduction

An independent set of size at least \(k\) contains a \(k\)-vertex independent subset. Assigning each selected vertex type its available mass \(1/(k\ell)\) yields total mass exactly \(1/\ell\).

All supported types have zero satisfaction, and Lemma 2 supplies the required roundwise intersections. This direction is correct.

6. Reverse direction of the reduction

The dummy type cannot be supported because its satisfaction is nonzero. The supported vertex set \(S\) is independent by Lemma 2.

The capacity bounds give

\[ \frac1\ell \leq \sum_{v\in S}\lambda_{\tau_v} \leq \frac{|S|}{k\ell}, \]

and hence \(|S|\geq k\). This correctly recovers a sufficiently large independent set.

Final adjudication

No major or minor correctness issue is present. The proof resolves the target and establishes \( \mathrm{NP} \)-completeness, including the stated restricted case.

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