Source-linked AI summary
Multi-Winner Voting with Argumentative Ballots
Ryuta Arisaka, Hirotaka Ono
TL;DR
The paper asks how multi-winner voting can represent defeasible candidate preferences and preserve justified representation when approvals depend on arguments. It introduces MVArg with attack and defence relations, generalises cohesion and JR/PJR/EJR, and proves that expressiveness increases while existence and verification properties change. The results are formalised and mechanically checked in Lean 4.
Problem
Approval ballots do not let voters express preferences in as much detail as argumentative formats, while full rankings are often unrealistic in computational and operational settings.
Method
MVArg replaces primitive approval markings with argumentative ballots whose attack and defence relations induce candidate approvals, alongside generalised cohesion and justified-representation axioms.
Results
MVArg is strictly more expressive than approval-based multi-winner voting; ArgJR always has a satisfying winner set, while stronger counterparts may not, and ArgJR verification is coNP-hard despite polynomial-time construction.
Takeaways & Limitations
Argumentative ballots preserve relational information absent from ordinary approval ballots while retaining conservative generalisations of classical cohesion and justified representation.
Takeaways & Limitations
The paper leaves the more precise boundary for restoring existence of all stronger representation axioms open and identifies practical elicitation as future work.
Abstract
from arXiv · showhide
We introduce multi-winner voting with argumentative ballots (MVArg) and investigate theoretical properties. As our conceptual contribution, we generalise approval ballots to argumentative ballots, thereby allowing voters to express defeasible preferences over candidates. We accordingly generalise voter cohesion and justified representation axioms JR, PJR and EJR. As our theoretical contribution, we establish several key results. First, MVArg is strictly more expressive than multi-winner voting with approval ballots (MV). Second, our notions of cohesion and justified representation are conservative generalisations of their counterparts in MV. Third, the MVArg counterpart of JR can always be satisfied, whereas the counterparts of PJR and EJR cannot always be. Fourth, although verifying whether a winner set satisfies the MVArg counterpart of JR is already coNP-hard, such a winner set can be constructed in polynomial time. All definitions, propositions, auxiliary lemmas and theorems have been formalised and mechanically checked in Lean 4.
1 Introduction
The paper extends approval-based multi-winner voting with argumentative ballots that encode attack and defence relations, motivated by the need for richer but practical preference expression. It develops corresponding cohesion and representation concepts and characterizes their expressive, existence, and computational properties.
- Motivation: Approval-based multi-winner voting selects a fixed-size winner set from voters’ candidate approval sets in collective decision-making.The paper situates this model in parliamentary elections, participatory budgeting, and recommendation formation.
- Motivation: Proportional representation requires sufficiently large, cohesive voter groups to receive representation proportional to their shared candidate support.JR, PJR, and EJR provide qualitative fairness criteria for evaluating winner-selection methods.
- MVArg: Argumentative ballots let voters draw directed attack claims between candidates, with approvals determined from the combined graph of those claims.The framework uses abstract argumentation: attack and defence relations determine candidate acceptability.
- MVArg: MVArg can produce different collective approvals from the same individual approval sets because attack and defence relations retain information that ordinary approval ballots discard.In the example, Alice and Bob collectively approve c3 and c1 under argumentative ballots but only c3 under ordinary approval ballots.
- Contributions: MVArg conservatively generalises approval-based multi-winner voting while being strictly more expressive, and its cohesion and representation notions conservatively generalise the classical ones.The paper formulates argumentative counterparts of JR, PJR, and EJR and studies their theoretical properties.
- Contributions: ArgJR is always satisfiable, whereas ArgPJR and ArgEJR may fail to be satisfiable; ArgJR verification is coNP-hard despite polynomial-time construction of a satisfying winner set.The paper also formalises its definitions and results in Lean 4 and supplies a Java implementation of GreedyGrounded for Theorem 8.
2 Technical Preliminaries
The preliminaries define classical multi-winner voting, justified representation, and grounded acceptance, then motivate argumentative cohesion through sufficiently agreeing voter subsets. They also note that grounded semantics offers unique, polynomial-time computable acceptance, unlike more disputable alternatives.
- Multi-winner voting: A classical multi-winner voting profile consists of voters, candidates, an approval profile assigning each voter a candidate subset, and a winner-set size k.The approval profile is A = (A_v1, ..., A_vn), with A_vi ⊆ C.
- Multi-winner voting: In classical approval voting, a voter subset collectively approves exactly the candidates approved by every voter in that subset.This intersection-based collective approval underlies cohesion and justified-representation definitions.
- Cohesion: A voter subset is l-cohesive when it meets both a size threshold based on l times the Hare quota and a shared-approval threshold.The supplied definition introduces cohesion through group size and common candidate approvals.
- Argumentative ballots: Argumentative ballots represent candidate attacks directly, so collective approvals can differ across voter subsets even when the individual ballots are fixed.Figure 1 contrasts individual ballots with collective approvals for pairs and the full voter set; blank ballots approve all candidates by default.
- Justified representation: JR, PJR, and EJR require increasingly strong representation for sufficiently cohesive voter groups, with EJR contained in PJR and PJR contained in JR.Classically, some qualifying winner set is polynomial-time computable, while verifying PJR or EJR is coNP-complete and JR verification is polynomial-time decidable.
- Grounded acceptance: Grounded acceptance is the least fixed point of the defence operator and is unique and polynomial-time computable for every abstract argumentation framework.The grounded extension contains arguments defended by the current set, iterated to the least fixpoint.
- Grounded acceptance: Other argumentation semantics may encode more disputable acceptance, lack uniqueness, and require more computation than grounded semantics.This motivates using grounded acceptance as the paper’s baseline semantics.
3 Multi-Winner Voting with Argumentative Ballots
This section defines argumentative ballots by pooling voters’ attack claims and approving candidates in the grounded extension of the combined framework. It shows that this model conservatively generalises approval voting while permitting richer collective-approval patterns and develops corresponding cohesion notions.
- Conceptualisation: Argumentative ballots let voters report attack claims, which are pooled to determine collective approvals from the grounded extension of the combined framework.An attack ci →cj means that acceptance of ci undermines the case for cj.
- Conceptualisation: Adding a voter can make a previously non-approved candidate approved because newly pooled attacks can neutralise an existing attack.This non-monotonicity cannot occur with standard approval ballots, whose approvals are primitive.
- Relationship between MM and MA: An approval profile can be transformed into an argumentative profile that preserves every group’s collective approvals.One simple construction represents each individual non-approval with a self-loop on that candidate.
- Relationship between MM and MA: Argumentative voting is strictly more expressive: identical individual approvals can produce different collective approvals because attacks interact through defence after combination.Ordinary approval voting fixes each group’s collective approval as the intersection of its members’ approval sets.
- Argumentative cohesion and (l, m, n)-cohesion: Argumentative cohesion is defined through an l-eligible agreeing subset with at least 2^l·|V|/k − 1 eligible subsets.The framework also establishes conservation with (l, 0, 0)-cohesion, monotonicity under supersets and parameter relaxation, and a lifting result.
- Argumentative cohesion and (l, m, n)-cohesion: The relaxation making argumentative cohesion monotonic is harmless for winner selection.This is stated as following from Theorem 1 in Section 4.
4 Justified Representation
The paper defines argumentative justified-representation axioms by evaluating winner sets against approvals of eligible voter subsets, then establishes their correspondence, hierarchy, existence, and computational properties.
- Axiom design: Argumentative representation axioms compare winners with approvals induced by eligible voter subsets, rather than only individual approvals.This distinction addresses the possibility that collective approval differs from every individual voter’s approval.
- Correspondence: Under the approval-preserving embedding, MVArg’s ArgJR, ArgPJR, and ArgEJR correspond respectively to JR, PJR, and EJR.EJR also coincides with ArgEJR-Spot on embedded ordinary approval profiles.
- Axiom relationships: ArgEJR-Spot is stronger than ArgEJR, while ArgEJR, ArgPJR, and ArgJR form the expected inclusion hierarchy.The hierarchy is ArgEJR-Spot ⊆ ArgEJR ⊆ ArgPJR ⊆ ArgJR, and each inclusion is separable.
- Existence: ArgJR is always satisfiable, whereas ArgPJR, ArgEJR, and ArgEJR-Spot can be impossible for some profiles and h.Under robust h, however, each of the three stronger axioms has a satisfying winner set.
- Computational complexity: Verification of every argumentative representation axiom is coNP-hard, but GreedyGrounded constructs an ArgJR winner set in polynomial time.The stated adjacency-matrix bound is O(k^2 · |V| · |C|^2).
- Computational complexity: GreedyGrounded maintains voter allocations, stored voter-subset selections, and a priority set while iteratively selecting candidates.The algorithm outputs a size-k subset and updates candidate–voter-subset priorities during construction.
5 Conclusions
MVArg extends approval voting by deriving approvals from grounded acceptance, preserving ordinary approval structure while retaining attack and defence relations. Its representation axioms generalise JR, PJR and EJR, but existence and verification become uneven.
- 5 Conclusions: MVArg induces approvals through grounded acceptance while retaining relational information absent from ordinary approval ballots.Individual approvals can remain fixed while attack and defence relations alter collective approvals.
- 5 Conclusions: ArgJR, ArgPJR, ArgEJR and ArgEJR-Spot conservatively generalise JR, PJR and EJR and preserve their inclusion hierarchy.These axioms reformulate justified representation for non-monotonic argumentative approvals.
- 5 Conclusions: A winner set satisfying ArgJR always exists, whereas winner sets satisfying the stronger axioms need not exist.The precise boundary between existence and non-existence remains open.
- 5 Conclusions: ArgJR verification is coNP-hard, yet an ArgJR-satisfying winner set is polynomial-time constructible.The construction result contrasts with the hardness of checking a given winner set.
- 5 Conclusions: Further work includes additional representation axioms, candidate costs, strategic behaviour, and practical elicitation of argumentative ballots.These directions mark the framework’s current scope boundary.
Appendix: Proofs
The appendix provides proofs for the paper’s main claims, linking propositions and theorems through auxiliary lemmas. Its existence proofs use direct inductive covering rather than optimisation of a specific voting rule.
- Appendix: Proofs: The appendix contains all proofs of the claims presented in the main text.It identifies the lemmas used to prove Propositions 2 and Theorem 1 and Theorem 5.
- Appendix: Proofs: The existence proofs for Theorems 4 and 6 use a direct inductive covering argument rather than optimisation of a specific voting rule.The paper characterises this proof strategy as novel, to the authors’ knowledge, in justified representation.
A1 Proofs of Propositions
The proposition proofs establish the approval-preserving transformation, the limits of representing argumentative profiles by ordinary profiles, and structural properties of cohesion and eligibility.
- A1 Proofs of Propositions: An approval-preserving transformation maps ordinary approval profiles to argumentative profiles while preserving collective approvals.The construction uses argumentative ballots whose relations encode the approval sets.
- A1 Proofs of Propositions: No bijection from argumentative profiles to ordinary approval profiles can preserve the relevant collective behaviour for every profile.The proof invokes collective approval gadgets to show that ordinary profiles cannot represent all argumentative outcomes.
- A1 Proofs of Propositions: An l-eligible voter set must satisfy the implicit size requirement |V′| ≥ l · |V|/k.This follows because the number of eligible subsets cannot exceed the number of subsets of V′.
- A1 Proofs of Propositions: The proofs relate argumentative cohesion to approval cohesion by showing that shared approval and subset-wide approval conditions transfer to corresponding thresholds.They also establish that eligible voter sets contain an unattacked candidate under the stated assumptions.
A2 Proofs of Theorems
The theorem proofs establish the hierarchy and existence properties of argumentative representation axioms, then analyze construction, verification, and runtime. They show a polynomial-time construction despite coNP-hard verification.
- A2 Proofs of Theorems: ArgEJR-Spot and ArgEJR are linked through their eligibility conditions, while the representation axioms retain the inclusion chain ArgEJR ⊆ ArgPJR ⊆ ArgJR.The proof establishes the corresponding implications between the argumentative axioms.
- A2 Proofs of Theorems: ArgPJR cannot always be satisfied because the constructed instance would require |W| = 16 despite k = 12.By contrapositive, the impossibility extends to ArgEJR and ArgEJR-Spot.
- A2 Proofs of Theorems: Verification is coNP-hard, while Algorithm 1 constructs an ArgJR winner set in polynomial time.The complement of verification is NP-hard; the construction repeatedly updates waiting until |out| = k.
- A2 Proofs of Theorems: With adjacency-matrix ballots, Algorithm 1 runs in O(k^2|V||C|^2) time, or O(k|V||C|^2) with incremental waiting updates.Both bounds remain polynomial, and the latter follows from updating only candidate pairs associated with affected voter sets.
- A2 Proofs of Theorems: A size-k winner set satisfying ArgJR exists for every argumentative voting profile.The correctness proof relies on the existence theorem and the selection process covering all voters after at most k additions.
A3 Claims and Proofs of Auxiliary Lemmas
The auxiliary lemmas establish gadget conditions and a correspondence between ordinary cohesion in approval profiles and argumentative cohesion after transformation. They show how cohesive subsets and their non-empty subgroups transfer between the two representations.
- Auxiliary gadgets: Lemma 1 introduces collective approval gadgets for argumentative voting profiles under specified structural conditions.
- Auxiliary gadgets: A constructed profile uses candidates c0, cv1, …, cvj, and cV′ with prescribed self-attacks and attacks from c_vx to cV′.
- Auxiliary gadgets: Lemma 2 specifies non-approval gadgets using two candidates, voter partitions, self-attacks, and a restricted attack relation.
- Cohesion correspondence: If V′ is l-cohesive in an approval profile, then it is (l, l, l)-cohesive in the transformed argumentative profile.
- Cohesion correspondence: If V′ is argumentative l-cohesive, some non-empty subset is both argumentative l-cohesive and l-cohesive in the original profile.
- Cohesion correspondence: When V′ is both argumentative l-cohesive and l-cohesive, every argumentative l-cohesive non-empty subset V′′ is l-cohesive in the original profile.