MILP the Gap: An Automated Reasoning Approach to Condorcet's Paradox

Computational social choice studies how conflicting individual preferences are aggregated into a collective decision, with applications to elections, AI evaluation/alignment, and recommendation systems. We focus on settings where n voters (e.g., human evaluators or algorithmic benchmarks) each rank m alternatives (e.g., human candidates or AI models/outputs), and the goal is to select a committee of k alternatives. One measure of the (in)stability of the outcome is the number of voters who prefer an unchosen alternative to all alternatives in the committee. If this number is less than half the electorate, the committee is a Condorcet winning set, which may not exist if k ≤ 2. More generally, there exist instances where any committee of size k has at least a frac2(k+1)-ε fraction of the electorate preferring another alternative, for arbitrarily small ε. While recent work has made remarkable progress narrowing the gap, it is currently unknown whether this lower bound is tight. We develop a mixed-integer linear programming framework that computes exact bounds for fixed parameter values. Our approach depends only on m and k; by modeling electorates as distributions over rankings, we eliminate any dependence on n. Our programs allow us to rule out counterexamples over arbitrary electorate sizes and obtain tight bounds for fixed m and k. Further, our framework provides a pathway for proving general upper bounds. In particular, we show a linear regime, k ≥ frac8m9, in which the conjectured frac2(k+1) upper bound indeed holds, providing the first results that match known lower bounds. Beyond stability, our framework can characterize the relationships among other social choice axioms, which we demonstrate by producing minimal incomparability results.