| paper | Finding strategyproof social choice functions via SAT solving |
| authors | F. Brandt, Christian Geist |
| venue | ATAL 2014 |
| filed under | voting · manipulation |
| judged by | gpt-5.6-luna / xhigh (triple__luna__xhigh__c6r1) |
| judge confidence | medium |
| authors would recognise it | yes |
other→P discrete result → its continuous mirror
Answer: \(\mathrm P\) · discrete side: other · adjudication: proved
full proof & adversarial review →
Theorem 2
statement extracted from the paper’s text layer
For \(m=5\), \(A\) fixed, and a generic society \(\mu\in\Delta(\mathcal L(A))\), decide whether there exists a neutral rule \(F_\infty:\Delta(\mathcal L(A))\to2^A\setminus\{\varnothing\}\) depending only on the strict pairwise-majority tournament \(T_\mu\), selecting the unique Condorcet winner when one exists, satisfying \(F_\infty(\mu)\subseteq BP(T_\mu)\), and obeying \(\neg(F_\infty(\mu')P_t^K F_\infty(\mu))\) for every true type \(t\) and mass transfer \(\mu'=\mu-\delta e_t+\delta e_{t'}\) with \(0<\delta\leq\mu_t\).
Types are complete rankings \(t\in\mathcal L(A)\), masses are \(\mu_t\), and \(T_\mu\) is computed from pairwise margin signs. The decision variable is a neutral tournament table \(f\), with \(F_\infty(\mu)=f(T_\mu)\); the objective is SAT-style feasibility, followed by rule evaluation.
Arbitrary \(\delta\)-moves are coordinated type-bloc deviations rather than the paper's unilateral voter deviations, so the authors might reject the nonatomic strategic convention even though Theorem 1 makes the induced tournament condition identical.
fatal: False
The mirror directly covers Theorem 2's SAT-found \(P^K\)-strategyproof refinement of \(BP\); Theorem 1 supplies the tournament bridge, while Theorem 3 is only a descriptive distributional boundary. It leaves aside SAT-engineering details, MUS extraction, composition-consistency, and variable-domain complexity.
The strongest honest case is a modest but real one: this paper supports a continuous-population mirror of its majoritarian social-choice-function design problem. It does not contain a named NP-hardness, polynomial-time, FPT, or similar complexity theorem. Its computational results are SAT-established existence and impossibility theorems, so I will not mislabel them as complexity results.
My lead anchor is Theorem 2, proved in this paper:
There exists a majoritarian Condorcet extension that refines the bipartisan set \(BP\) and is still \(P^K\)-strategyproof. Consequently, \(BP\) is not a finest majoritarian Condorcet extension satisfying \(P^K\)-strategyproofness.
The construction is found computationally for five alternatives; the paper also discusses extensions to larger domains. The theorem is not merely about the SAT encoding: its underlying object is an irresolute social choice function \(f\) mapping majority tournaments to nonempty choice sets.
A natural continuous mirror is the following. Fix \(m=5\), \(A=\{a_1,\ldots,a_m\}\), and let \(T=\mathcal L(A)\) be the \(m!\) complete rankings. A society is a distribution \(\mu\in\Delta(T)\), where \(\mu_t\) is the population fraction with ranking \(t\). For generic societies, define
\[ M_\mu(a,b)=\sum_{t\in T}\mu_t \bigl(\mathbf 1[a\succ_t b]-\mathbf 1[b\succ_t a]\bigr), \]
and let \(T_\mu\) be the tournament containing \(a\to b\) exactly when \(M_\mu(a,b)>0\). The social choice rule is \(F_\infty(\mu)\), a nonempty subset of \(A\), and it must depend only on \(T_\mu\). Thus \(F_\infty(\mu)=f(T_\mu)\).
The continuous problem is:
Mass-Kelly-BP Extension. Given \(m=5\), find a rule \(F_\infty\) such that:
The last condition is the continuous strategic condition. If a mass \(\delta\) of voters of true type \(t\) changes its reported ranking to \(t'\), the new society is
\[ \mu'=\mu-\delta e_t+\delta e_{t'}, \qquad 0<\delta\leq \mu_t. \]
The rule must never satisfy
\[ F_\infty(\mu')P_t^K F_\infty(\mu), \]
where \(P_t^K\) is the strict part of the Kelly extension induced by ranking \(t\). A solution is therefore a single rule \(F_\infty\), not a fractional outcome or a lottery.
This is a credible high-multiplicity regime. Think of a large election or representative assembly with millions of voters but only \(m!=120\) possible complete rankings. The relevant data are type masses, not named voters. A type is a complete ranking, and voters of the same type are interchangeable for everything this paper uses. The continuous model preserves the paper’s outcome space: choice sets of alternatives remain discrete; only the population becomes a distribution.
The bridge is particularly clean because of Theorem 1, proved in the paper. It states that a majoritarian SCF is \(P^E\)-strategyproof exactly when it is \(P^E\)-tournament-strategyproof. If a mass \(\delta\) of true type \(t\) changes its report, every majority edge that disappears must have been oriented according to \(t\)’s true ranking:
\[ T_\mu\setminus T_{\mu'}\subseteq \{(a,b):a\succ_t b\}. \]
Thus the paper’s tournament formulation already controls precisely the mass-transfer moves in the continuous model. Theorem 2 therefore supplies a positive continuous rule: take the SAT-found \(f\) and define \(F_\infty(\mu)=f(T_\mu)\).
For a fixed \(m\) and an explicit table for \(f\), evaluating the rule on a society is straightforward: compute all pairwise margins and look up the corresponding tournament. The synthesis problem remains finite and potentially exponential in \(m\), just as in the paper, but the continuous population itself does not create a new obstacle. I would describe this as a tractable fixed-domain mirror after rule synthesis, not as a claimed polynomial-time theorem.
My second, boundary anchor is Theorem 3, also proved in this paper:
For every \(m\geq5\), there is no majoritarian SCF satisfying both \(P^F\)-strategyproofness and Pareto-optimality.
Here \(P^F\) is the strict part of Fishburn’s extension. For completeness, \(X R_t^F Y\) requires that every element of \(X\setminus Y\) be at least as good as every element of \(X\cap Y\), every element of \(X\cap Y\) be at least as good as every element of \(Y\setminus X\), and every element of \(X\setminus Y\) be at least as good as every element of \(Y\setminus X\).
The corresponding continuous question is:
Mass-Fishburn-Pareto Feasibility. Given \(m\geq5\), does there exist a neutral, majoritarian rule \(F_\infty\) on generic distributions over rankings such that:
A solution would again be a rule \(F_\infty\), with the population represented only by \(\mu\). The expected answer is no. Any finite odd-voter profile \(R\) embeds as its empirical distribution \(\mu_R\). A unilateral report change by one voter becomes a transfer of mass \(1/n\). Therefore, a rule solving the continuous problem would induce a majoritarian finite SCF satisfying Fishburn-strategyproofness and Pareto-optimality, contradicting Theorem 3.
The paper’s Lemma 4 supplies the SAT-verified base case at \(m=5\), while Lemma 3 supplies the induction from \(m+1\) alternatives to \(m\). Lemma 2 identifies Pareto-optimality with refinement of the uncovered set, which makes the continuous Pareto condition exact rather than an invented relaxation. This is the positive value of the negative anchor: the continuum does not automatically dissolve the impossibility. It gives a genuine boundary for the mirror.
The authors should recognise these as continuous analogues because their own objects are already anonymous distributions in disguise: the SCF depends only on aggregate pairwise comparisons, and Theorem 1 explicitly removes the identity of individual voters. What the mirror adds is the population interpretation, type masses, and mass-valued strategic perturbations. It is not outcome-space continuity, probability over winners, or a smoothed-noise model.
The main weakness is also clear. In a genuinely nonatomic population, one individual has zero mass and cannot change a majority relation, making ordinary individual strategyproofness vacuous. My mirror therefore uses a same-type mass transfer, or, if one insists on strictly unilateral manipulation, a one-voter transfer of size \(1/n\) inside a high-multiplicity rational society. That is a co-modification of the strategic model and could be criticised as closer to coalitional strategyproofness. The defence is that the paper’s tournament-strategyproofness formulation handles exactly these aggregate changes, and that high multiplicity makes type-level mass action a sensible object.
The mirror consequently generates useful follow-up questions: compute the minimum mass needed for a Fishburn or Kelly manipulation; handle societies with pairwise ties; determine whether the five-alternative refinement can also satisfy composition-consistency; and study the complexity of representing or evaluating the synthesized rule when \(m\) is variable. The paper itself does not answer those computational questions, but it gives a credible, technically faithful starting point for asking them.
The decisive objection is that this paper has no named computational result to continuize. Theorem 2 and Theorem 3 are existence and impossibility theorems about axioms of tournament solutions; Theorem 1 is an equivalence lemma. SAT is the proof technology, not the computational problem being solved. There is no given society, mass-transfer objective, complexity classification, or algorithm for bribery, control, campaigning, or robustness.
The proposed Theorem 2 mirror is mathematically coherent, but it does not make the population computationally operative. For \(m=5\), let
\[ q(\mu)=\left(\operatorname{sgn}\sum_t\mu_t \bigl(\mathbf 1[a\succ_t b]-\mathbf 1[b\succ_t a]\bigr)\right)_{a<b}. \]
Then the proposed rule is simply
\[ F_\infty(\mu)=f(q(\mu)). \]
The simplex of ranking distributions is partitioned into finitely many regions—at most \(2^{\binom{5}{2}}=1024\) tournament regions—and \(F_\infty\) is constant on each. Evaluating it means computing ten margins and performing a finite lookup. Synthesizing it means exactly the paper’s original SAT search over tournament tables. The mass vector is merely a redundant representation of the tournament; no population-level optimization remains.
Theorem 1 does not repair this. It shows that the paper’s individual-manipulation condition can be expressed at the tournament level. That is evidence that the voter population has already been quotiented away, not evidence of a continuous computational bridge. In a genuinely nonatomic society, an individual has zero mass and cannot change a majority edge. A positive transfer \(\delta\) from type \(t\) to \(t'\) is instead a coordinated bloc deviation. Using \(1/n\) restores the paper’s setting by returning to a finite electorate; allowing arbitrary \(\delta\) replaces individual strategyproofness with a new coalitional notion. Both are defensible research questions, but neither is the paper’s result continuized.
A stronger proposal could retain the full distribution, or ask for the minimum mass needed to change the outcome. That would be more genuinely continuous, but it would no longer mirror Theorem 2: majoritarianity would have been abandoned, or a new robustness objective would have been added. The paper supplies neither such objective nor an associated computational theorem. A weighted version of its average choice-set size would likewise require inventing a measure over societies; it would be a new mechanism-design project, not a mirror of the stated result.
The same problem defeats the Theorem 3 anchor. The continuous nonexistence claim follows immediately because every rational finite profile embeds as a distribution and the rule still factors through its tournament. Lemmas 2 and 3 use only uncovered sets, Condorcet losers, and tournament restrictions; they contain no population variable. Thus the proposed continuum merely restates the finite impossibility on a larger, redundant domain. If one permits a distribution-dependent rule, the finite impossibility need not apply—but then one is studying a new rule class, not Theorem 3.
The large-election interpretation is perfectly sensible as a high-multiplicity story. What it does not provide is a ChoCo-style computational problem. This paper’s substantive object is automated axiomatic rule synthesis over alternatives, not computation over a continuous society. If ChoCo expands to include SAT complexity for synthesizing anonymous social choice functions, or explicitly studies bloc manipulation, a worthwhile project can be built. Under the programme’s stated population-continuization standard, however, neither proposed anchor survives: one collapses to a finite tournament lookup, and the other is a finite impossibility theorem written in distributional notation.
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.