| paper | d4-conf-ecai-2020-0194 |
| authors | — |
| venue | ? |
| filed under | unclassified |
| judged by | gpt-6-luna / xhigh (triple__luna__xhigh__c6r1) |
| judge confidence | high |
| authors would recognise it | yes |
Theorem 1 is an impossibility about whether a rule satisfying three axioms exists, not a result about computing a solution or computational hardness. The SAT encoding and solver runs support that axiomatic analysis, but the paper gives no named computational result to continuize, so bit (a) fails.
fails bit a — no named computational result to mirror
The proposed mirror restates Theorem 1's proportionality, Pareto-efficiency, and cautious-strategyproofness requirements over approval-type masses; it does not turn the paper's SAT methodology or its other results into computational-complexity results.
Under your stated anchor rule, I find no named computational result in this paper. The closest is Theorem 1, proved here: for \(k\ge3\), \(m>k\), and \(n\) divisible by \(k\), no rule for electing \(k\)-member committees from \(m\) candidates is simultaneously minimally proportional, Pareto efficient, and immune to manipulation by cautious voters. Its proof uses a SAT-assisted base case and then an induction. This is a named impossibility theorem, but it classifies no computational problem as tractable or hard. The other numbered propositions likewise establish existence or properties of rules, not computational complexity.
If an axiomatic impossibility is allowed as a near-miss anchor, the strongest population mirror is concrete. Let the types be approval sets \(T=2^C\), and let a society be a rational distribution \(\mu\) over \(T\). Seek a rule \(F\) mapping each such \(\mu\) to a nonempty set of \(k\)-member committees. Require mass-based minimal proportionality: on party-list societies, if \(\mu_{\{c\}}\ge1/k\), every committee in \(F(\mu)\) includes \(c\). Require Pareto efficiency using the paper’s cardinality-based preferences for each positive-mass type. To retain its incentive condition, require that for every \(n\) divisible by \(k\), moving one voter’s mass \(1/n\) from a truthful approval type to a misreported type cannot strictly improve the outcome under that type’s cautious Kelly preference.
The scenario is a large electorate choosing a parliament or committee, with many voters but relatively few distinct approval sets. This mirror has a direct impossibility: restricting \(F\) to societies whose masses are multiples of \(1/n\) induces a finite voting rule. It would inherit all three axioms, contradicting Theorem 1. So the continuous rule-design question has a definite negative answer.
The weak point is also decisive for ChoCo’s scope: this is still an axiomatic existence question, not a computational-complexity question. And if the population is genuinely atomless, a single voter’s report change has zero mass, making strategyproofness vacuous; preserving the theorem’s incentive condition requires retaining finite \(1/n\) changes. That makes this a plausible population-based restatement of the paper’s impossibility, but not a qualifying continuous computational mirror.
The FOR case identifies the central obstacle itself: this paper proves no computational-complexity result. Theorem 1 is a named impossibility theorem, but it concerns whether a voting rule with three axioms exists. The SAT solver is a tool in that proof, not a result about the complexity of a computational problem.
The proposed population model is sensible: take approval sets as types, require a candidate to win a seat when singleton-approval mass reaches \(1/k\), and define Pareto efficiency over types with positive mass. The difficulty is the incentive axiom. If one voter has zero mass, changing that voter’s report leaves \(\mu\) unchanged, so strategyproofness becomes vacuous. Preserving the paper’s individual deviations requires an atom of mass \(1/n\). Requiring those deviations on every \(n\)-voter grid imports the finite theorem directly; treating a positive-mass group as the deviator changes the axiom to coalitional or block manipulation. Either way, the resulting impossibility is an axiomatic rule-existence result, outside ChoCo’s computational-complexity scope.
The paper’s SAT methodology does not supply a computational mirror either. Its encoding has finitely many variables because \(n,m,k\) are fixed and the rule is a table over finitely many profiles. A continuous rule over rational mass distributions has infinitely many inputs. To ask a computational question about synthesizing or checking such a rule, one would first need to choose a representation for rules and a finite way to verify their axioms. Different choices would define new problems, not continuizations of a complexity result in this paper.
One could, for example, study winner determination for PAV given weighted approval types. That is a plausible high-multiplicity problem, but the paper reports no complexity result about PAV winner determination, so it is not a mirror of one of its results. I cannot rule out a worthwhile new project built from this model. The negative case is strong on the narrower point the programme needs: none of this paper’s named results anchors a continuous computational mirror.
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.