| paper | Optimal Bounds for the No-Show Paradox via SAT Solving |
| authors | F. Brandt, Christian Geist, Dominik Peters |
| venue | ATAL 2016 |
| filed under | voting · theory |
| judged by | gpt-5.6-luna / xhigh (triple__luna__xhigh__c6r1) |
| judge confidence | high |
| authors would recognise it | yes |
The proposed population mirror is coherent: finite participation lifts naturally to positive-mass cohorts while preserving Condorcet margins. However, the sole proposed anchor is explicitly an axiomatic impossibility theorem, and the SAT encoding does not turn it into a named computational result. Therefore bit (a) fails despite the sensible continuous formulation.
fails bit a — no named computational result to mirror
The mirror covers the single-valued Condorcet-consistency and participation impossibility of Theorem 3. It leaves the positive lookup-table construction, maximin and Kemeny bounds, set-valued results, and probabilistic results without a qualifying anchored computational mirror.
The strongest honest case is a conditional one: the paper has a natural continuous-population mirror, but it does not contain a qualifying complexity-theoretic anchor. Its named results are impossibility and existence theorems, not NP-hardness, polynomial-time, FPT, or approximation results. The SAT encoding is a method, not a complexity classification.
If structural impossibility results are admissible, the lead anchor is Theorem 3 (the Section 6 main theorem, labelled thm:anonymous in the source). Proved in this paper, it states in full:
There is no Condorcet extension satisfying participation for \(m\ge 4\) alternatives and \(n\ge 12\) voters.
The natural mirror is Mass-No-Show Feasibility\(_\infty\). An instance consists of a candidate set \(A\), with \(|A|=m\ge4\), and the finite type space \(T\) of all strict rankings of \(A\). A society is a distribution \(\mu\in\Delta(T)\), where \(\mu_t\) is the population fraction having ranking \(t\). For candidates \(a,b\), define the normalized majority margin by \(g_\mu(a,b)=\sum_{t:a\succ_t b}\mu_t-\sum_{t:b\succ_t a}\mu_t\).
The decision question is whether there exists a resolute population voting rule \(F:\Delta(T)\to A\) satisfying:
Here \(e_t\) is the society consisting entirely of type \(t\). The solution is either an explicit rule \(F\) satisfying the two conditions on every society, or a finite contradiction proving that no such rule exists. The output remains an indivisible candidate; only the population is continuized.
This is recognisably the authors’ problem. In their finite model, adding one voter of type \(t\) to an \(n\)-voter profile changes the normalized society from \(\mu\) to \(\frac{n}{n+1}\mu+\frac{1}{n+1}e_t\). More generally, adding a block of \(k\) identical voters gives exactly the same convex-combination operation with \(\varepsilon=k/(n+k)\). Thus mass participation is not an arbitrary coalition axiom: it is the type-level closure of the paper’s individual participation condition. It is also the only non-vacuous analogue in an atomless population, where one individual has zero mass and cannot change the society.
The expected answer is an impossibility transferred from the finite witness. Given a continuous rule \(F\), define a finite rule by \(f(R)=F(\mu_R)\), where \(\mu_R\) is the normalized type distribution of profile \(R\). Condorcet margins are merely rescaled, so Condorcet consistency is preserved. Each finite participation comparison becomes one of the mass-participation comparisons above. Theorem 3 would then be contradicted. Hence the continuous problem has no solution for \(m\ge4\). This is a “hardness-transfers” shape of result, although strictly speaking it is transfer of an impossibility, not transfer of computational hardness.
The regime is plausible: a large national, professional, or institutional electorate may contain millions of agents but only \(m!\) distinct complete rankings for fixed \(m\). For \(m=4\), there are only \(24\) ranking types. A type represents agents indistinguishable for the paper’s purposes, and mass represents the fraction of the electorate turning out or joining. The mirror does not rely on individual-specific prices or identities, and it does not continuize the outcome space.
I would deliberately not claim that Theorem 4 supplies a second anchor. Its positive statement—existence of a Condorcet extension satisfying participation for \(m=4\) and \(n\le11\), additionally pairwise, Pareto-optimal, and top-cycle refining—is tied to a bounded finite electorate and has no comparably natural full-continuum counterpart. Likewise, the probabilistic theorem would introduce outcome-space lotteries as a second continuity mechanism, weakening the population-only focus.
The weakest point is decisive: the continuous condition changes individual participation into positive-mass cohort participation, and the resulting impossibility follows immediately by restricting to normalized finite profiles. The paper therefore supplies a convincing subject-matter mirror, but not a new ChoCo complexity result. Further work would need to study a genuinely computational boundary—for example, deciding feasibility on succinctly represented rational societies, approximate mass participation, infinitesimal or derivative participation, minimum joining mass, or probabilistic mass participation. Under the programme’s strict anchor rule, I would therefore record this as a natural but non-qualifying positive case rather than a full computational mirror.
The proponent has shown that a continuous-population formulation is natural. They have not shown a qualifying ChoCo mirror.
The decisive problem is that the paper contains no named computational result. The Section 6 theorem is an axiomatic existence theorem:
\[ \text{there is no function }f\text{ satisfying Condorcet consistency and participation.} \]
It does not define an input instance, an optimization objective, a complexity measure, or an algorithmic output. SAT solving is only the proof technology. The lookup table and MUS are certificates of an axiom-consistency result, not a complexity classification of a social-choice problem.
The proposed Mass-No-Show Feasibility\(_\infty\) remains the same kind of global synthesis question. Its alleged input is essentially just \(m\): the distribution \(\mu\) is quantified over, not supplied as an instance. Its output is either a rule \(F:\Delta(T)\to A\) satisfying universal axioms or a contradiction. Calling that “computation” does not make it a computational population problem in the programme’s sense. If one instead asks for \(F(\mu)\) for a supplied society, the question is under-specified: the theorem does not select a particular admissible rule, and the existence of a globally admissible rule is independent of the particular \(\mu\).
The better version of the mirror does not repair this. Requiring participation for every positive mass \(\varepsilon\), rather than only rational additions corresponding to finite voters, is mathematically coherent and is probably the right continuum definition. But it is still an axiom over a rule space, not an algorithmic question about a society. Restricting a hypothetical \(F\) to rational finite profiles gives the paper’s finite participation constraints directly; this explains why the continuous formulation is valid, but does not create a new computational object. Even if the continuum had produced a different answer, the paper would still lack a computational anchor.
Changing the type space cannot solve the basic problem. A richer anonymous type space preserves the global rule-synthesis character; an identity-, position-, or arrival-indexed space ceases to be the paper’s high-multiplicity voting model. Introducing lotteries would additionally continuize the outcome space, outside the programme’s target.
There are worthwhile new questions nearby—such as minimizing the mass needed to induce a no-show for a fixed rule, or synthesizing rules on a finite rational grid—but those are new computational problems, not mirrors of a computational result proved here. Thus the honest verdict is negative under ChoCo’s anchor rule, while conceding that the paper has a legitimate subject-matter continuous reformulation.
The adversarial triple: the proponent anchors on up to three named results; the opponent sees that case and must defeat every anchor; the judge decides which case convinced it. These are the pipeline’s own outputs, generated by tools/triple_run.py — no human edited them. The paper’s own text is not reproduced here beyond the quoted statement above.