On the Edge of Core (Non-)Emptiness: An Automated Reasoning Approach to Approval-Based Multi-Winner Voting

TL;DR

This paper introduces an automated reasoning approach using mixed-integer linear programming to determine the existence of core-stable committees in approval-based multi-winner voting, providing new theoretical insights and computational advantages.

Contribution

It develops a novel MILP-based method for analyzing core stability, enabling proofs independent of voter count and revealing new relationships with other fairness properties.

Findings

MILP approach can decide core stability existence efficiently.

New existence results for specific voting scenarios.

Revealed links between core stability and priceability.

Abstract

Core stability is a natural and well-studied notion for group fairness in multi-winner voting, where the task is to select a committee from a pool of candidates. We study the setting where voters either approve or disapprove of each candidate; here, it remains a major open problem whether a core-stable committee always exists. In this work, we develop an approach based on mixed-integer linear programming for deciding whether and when core-stable committees are guaranteed to exist. In contrast to SAT-based approaches popular in computational social choice, our method can produce proofs for a specific number of candidates independent of the number of voters. In addition to these computational gains, our program lends itself to a novel duality-based reformulation of the core stability problem, from which we obtain new existence results in special cases. Further, we use our framework to reveal previously unknown relationships between core stability and other desirable properties, such as notions of priceability.