Is Four Enough? Automated Reasoning Approaches and Dual Bounds for Condorcet Dimensions of Elections

A team of researchers from Carnegie Mellon University and the University of Washington has applied automated reasoning to a classic problem in social choice theory, narrowing a long-standing theoretical gap. The paper, 'Is Four Enough? Automated Reasoning Approaches and Dual Bounds for Condorcet Dimensions of Elections,' tackles the question of how large a committee must be to guarantee a Condorcet winning set—a group where, for any outsider, a majority prefers at least one member. While it was known that a single member (k=1) or a pair (k=2) isn't always enough, and that a quintet (k=5) always works, the gap between the proven lower bound (k≥3) and upper bound (k≤5) remained open.

The researchers' key innovation was designing a sophisticated Mixed-Integer Linear Program (MILP) to systematically search for counter-example elections that would require a committee larger than a conjectured size. They enhanced the model with techniques like symmetry breaking and constraint generation to efficiently explore what amounts to an infinite space of possible voter preferences. After running this automated search on moderate-sized elections, they failed to find any instance requiring a committee larger than size 3. This negative result is significant positive evidence.

Motivated by these computational findings, the team then analyzed the dual of their linear programming relaxation, simplifying it to formulate a new mathematical conjecture. If proven true, this conjecture would establish that a Condorcet winning set of size 4 is always sufficient, finally closing the gap to 3-4. The work, presented at the Games, Agents, and Incentives Workshop (GAIW-26), provides both a powerful general framework for computational social choice and a concrete analytical path toward a definitive proof.