| paper | Automated Search for Impossibility Theorems in Social Choice Theory: Ranking Sets of Objects |
| authors | Christian Geist, Ulrich Endriss |
| venue | JAIR 2011 |
| filed under | voting · theory |
| judged by | gpt-5.6-luna / xhigh (triple__luna__xhigh__c6r1) |
| judge confidence | high |
| authors would recognise it | no |
The paper has no numbered result with the required computational character: its named results are axiomatic impossibilities and model-theoretic reductions. The proposed mass-weighted tie-rule repair is a potentially interesting new computational-social-choice problem, but it introduces an electorate, aggregation rule, common institutional relation, and repair objective that the paper does not study. Therefore no anchored result supplies a valid continuous mirror.
fails bit a — no named computational result to mirror
The proposal covers only a newly constructed population-level repair interpretation of the paper's finite axiom-consistency results; the 84 SAT-discovered impossibilities and the finite-domain SAT methodology remain outside any continuous-population mirror.
There is a defensible positive case, but it is narrow: this paper supports a continuous high-multiplicity mirror of axiom-consistency and axiom-repair for tie outcomes. It does not support a claim about NP-hardness dissolving, because it contains no named theorem of the form “NP-hard”, “in P”, “FPT”, or similar.
My lead anchor is Theorem 3, “Impossibility No. 16”. It is proved in this paper: the automated search discovers it, and the paper gives a manual proof. It states that, for every linearly ordered set \(X\) with \(|X|\ge4\), there is no transitive binary relation \(\succeq\) on \(2^X\setminus\{\varnothing\}\) satisfying all four of:
Importantly, this is impossibility even for an arbitrary transitive relation: reflexivity and completeness are not needed.
The continuous mirror I would hand to a prover is Continuous Tie-Set Axiom Repair.
An instance contains a finite candidate set \(C\), a finite set of voter or constituency types \(T\), and a rational distribution \(\mu\) over \(T\). A type is a complete pair consisting of a ballot ranking of \(C\) and a portfolio \(\Delta_t\) of tie-set principles it requires. The mass \(\mu_t\) is the fraction of the electorate belonging to that type. This is a credible high-multiplicity regime: millions of voters or recurring constituencies may fall into a small number of ballot-and-policy types.
A fixed scoring rule converts \(\mu\) into an aggregate strict order \(\dot\ge_\mu\) on candidates; instances with tied aggregate scores can either be excluded or resolved by a specified deterministic convention. The decision variable is one common transitive relation \(R\) on the finite set \(2^C\setminus\{\varnothing\}\) of possible tied-winner sets. The objective is
\[ \max_R \sum_{t\in T}\mu_t\, \mathbf 1\!\left[R\models_{\dot\ge_\mu}\Delta_t\right]. \]
Thus the problem asks for a single institutional ranking of tied winner sets that satisfies the principles of as much population mass as possible. The all-mass feasibility question is the special case in which the optimum must equal \(1\).
This is recognisably the paper’s problem rather than a tractable substitute. The paper already studies which combinations of preference-extension principles can coexist, and its SAT program searches exactly for satisfying relations over set outcomes. The continuous version merely gives repeated identical normative requirements their honest mass representation. The outcomes remain finite sets; the object being continuized is the population.
Theorem 3 gives an immediate boundary result. If \(|C|\ge4\) and a positive-mass type requires all four principles in the theorem, no common transitive \(R\) can represent that type at all. The obstruction survives every voter distribution \(\mu\): its combinatorics live in the number of alternatives, not in the number of voters. In ChoCo’s terminology, this is a Class-B-style obstruction rather than a continuum-specific one. For variable \(|C|\), I would expect the weighted repair problem to inherit the finite SAT or weighted-Max-SAT difficulty of the underlying axiom-consistency problem; for fixed \(|C|\) and a fixed axiom universe, the continuous masses only become rational objective weights.
The paper’s Theorem 2 and Corollary 1 strengthen the plausibility of this mirror. Theorem 2, proved here, says that existentially set-guarded sentences are preserved in subset-consistent substructures. Corollary 1, also proved here, says that if an ESG axiom set \(\Gamma\) is impossible on every linearly ordered \(n\)-element domain, then it is impossible on every larger domain. In the mirror, this suggests finite certificates for many continuous infeasibility results: increasing the population mass or adding more repeated voter types cannot repair an obstruction witnessed by a bounded alternative configuration.
Further questions follow naturally: whether the mass-weighted repair problem has an FPT algorithm parameterised by \(|C|\) or the number of axiom portfolios; whether the ESG preservation result extends to genuinely atomless type spaces; and whether allowing different extension relations for different voter types destroys the collective problem by making it separable.
The weakest point is that the continuous population is an added social-choice layer. The paper’s core theorem concerns one relation over one finite object domain, and its impossibility does not itself depend on population multiplicity. A sceptical referee could therefore call the mirror an application of the paper rather than its direct continuation. That objection is real. Also, no named standard complexity result appears in the paper, so this is not a strong anchor for ChoCo’s usual hardness-versus-tractability programme. Still, the tie-set application, the SAT-computed consistency problem, and the explicit high-multiplicity repair objective make this a respectable—and honestly bounded—continuous mirror.
The paper offers no named computational result in the ChoCo sense. Theorem 3 is an impossibility theorem about whether one decision maker’s order over \(2^X\setminus\{\varnothing\}\) can satisfy four axioms. Theorem 2 and Corollary 1 are model-theoretic preservation results. The SAT solver is a proof and discovery tool, not the subject of a complexity theorem. Thus the proposed mirror must add a population-level problem rather than continuize one studied computationally in the paper.
Theorem 3 is the proponent’s strongest anchor, but the proposed construction adds too much. In the paper, \(X\) is the set of objects and \(\dot{\ge}\) is one agent’s order over those objects. It is not an electorate’s aggregate preference. Replacing it with a scoring order \(\dot{\ge}_\mu\) introduces an electoral model absent from the theorem, while the relation \(R\) remains one institutional relation over tied-winner sets.
The population then does not actually enter the axiom constraints. If all types require the same portfolio \(\Delta\), the objective
\[ \max_R \sum_{t\in T}\mu_t\mathbf{1}[R\models_{\dot\ge_\mu}\Delta] \]
is simply \(0\) or \(1\); the distribution is irrelevant except through the aggregate order. If types have different portfolios, the masses merely weight heterogeneous logical constraints. That is a newly invented weighted Max-SAT or institutional-repair problem, not a high-multiplicity version of the paper’s preference-extension problem.
The more charitable repairs do not solve this problem. Give every type its own relation \(R_t\), and the optimization separates into independent feasibility tests, so the society contributes only a weighted sum of pointwise answers. Require one common \(R\), and the problem becomes social aggregation of normative requirements. That could be a legitimate new computational-social-choice problem, but it requires a new institutional rationale, aggregation objective, or disagreement metric that the paper neither studies nor motivates. The paper supplies axioms as constraints, not a theory of why a population should share one set-preference relation.
Theorem 2 and Corollary 1 do not provide an independent continuous anchor. Their substructure \(Y\subseteq X\) is a restriction of the object domain, with \(n=|Y|\) counting objects, not voters, types, or population mass. The existential witnesses preserved by the ESG condition are elements of sets of objects. Nothing in the theorem refers to a measure \(\mu\), repeated agents, type support, or weighted satisfaction.
Reinterpreting \(Y\) as a subset of voter types would not work: restricting types can change the aggregate order \(\dot{\ge}_\mu\), and the ESG argument has no measure-theoretic analogue. Making the object domain itself continuous would be a different, out-of-scope continuization of alternatives or outcomes rather than of the population.
The 84 SAT-discovered impossibilities do not repair the gap. Their computational content is a finite enumeration over axiom subsets and small object domains. The paper gives no complexity classification whose high-multiplicity relaxation can be studied. Calling the added weighted-repair problem “the SAT difficulty of the paper” therefore overstates the connection.
The honest limitation is that the negative case cannot prove that no researcher could make the proposed aggregation problem worthwhile. Repeated voters with common ballots are a plausible high-multiplicity regime, and a carefully specified weighted tie-rule design problem could be interesting. But that would be a new population-level problem inspired by the paper, not a continuous mirror of one of its computational results. The strongest defensible verdict is therefore that this paper has no strong ChoCo mirror: Theorem 3 is a contrived wrapper, while Theorem 2 and Corollary 1 concern alternatives rather than populations.
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.