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

1. Problem Statement

The paper addresses a fundamental gap in Voting Theory regarding Condorcet Winning Sets (CWS).

• Context: In ranked voting, Condorcet's paradox demonstrates that a single candidate ($k=1$) or a pair ($k=2$) may not exist who is preferred by a majority over all other candidates.
• Definition: A Condorcet Winning Set of size $k$ is a committee $W$ such that for any candidate $c \notin W$, a majority of voters prefer at least one member of $W$ over $c$.
• The Gap:
  • Lower Bound: It is known that $k=2$ is insufficient (counter-examples exist), and specific elections require $k=3$.
  • Upper Bound: Recent theoretical work proved that $k=5$ is always sufficient.
  • Open Question: Does a winning set of size $k=3$ or $k=4$ always exist? The paper aims to close the gap between the known lower bound ($k \ge 3$) and the upper bound ($k \le 5$).

2. Methodology

The authors employ Automated Reasoning using Mixed-Integer Linear Programming (MILP) to search for counter-examples (elections where no CWS of size $k$ exists) and to derive analytical bounds via duality.

A. Optimization Formulation

The problem is modeled as a max-min game:

• Maximizer: Selects a voter profile (probability distribution over rankings) to maximize the defeat margin $\alpha$ (the fraction of voters preferring an outsider over the committee).
• Minimizer: Selects a committee $W$ of size $k$ to minimize this margin.
• Goal: Find the smallest $k$ such that the worst-case margin $\alpha^* < 0.5$ (for strict majority). If $\alpha^* > 0.5$, a counter-example exists.

B. Key Technical Innovations

To handle the exponential complexity of the search space ($m!$ rankings), the authors developed several optimizations:

1. Continuous Voter Modeling: Instead of discrete voters, the electorate is modeled as a probability distribution over rankings. This allows the search to cover "effectively infinite" electorates.
2. Symmetry Breaking:
   • Fixed Committee: For standard MILP, a specific committee is fixed as the "worst-case" candidate to reduce isomorphic solutions.
   • Lexicographic Ordering: Enforces an ordering on challenger selection to reduce symmetry.
3. Permutation Reduction: Groups rankings based on their top $m-k$ prefixes, reducing variables from $m!$ to $m!/k!$.
4. Constraint Generation: Uses a "Restricted Master Problem" (RMP) and a separation subproblem. It iteratively solves a relaxed problem and only adds constraints for committees that violate the current solution, avoiding the need to build the full model.
5. Enhanced MILP (infMILP): Introduces a conceptual trick where candidates are treated as infinite cycles of clones. This forces the solver to find committees robust against "self-challenges" (where a clone of a committee member defeats the committee). This formulation allows searching over effectively infinite candidate spaces.
6. Subsampling: Randomly samples a fixed number of rankings ($z$) to scale the search to larger numbers of candidates ($m$), trading completeness for the ability to find counter-examples in large spaces.

C. Dual Analysis

Motivated by experimental results, the authors analyze the Dual of the Linear Programming (LP) relaxation of their MILP. They simplify the dual formulation to derive a theoretical conjecture regarding the upper bound of $\alpha$.

3. Key Contributions

1. Scalable MILP Framework: Developed a highly optimized MILP framework that outperforms previous SAT-based approaches (e.g., Geist [10]) by handling continuous voter distributions and effectively infinite candidates via the infMILP abstraction.
2. Empirical Evidence for $k=4$: Despite exhaustive searches on moderate-sized elections ($m \le 9$) and heuristic searches on larger ones, the solver failed to find any election requiring a committee size $k > 3$.
3. The Dual Bound Conjecture:
   • The authors observed that the solver's upper bounds consistently satisfied $\alpha \le 2/k$.
   • They derived a simplified dual LP and formulated Conjecture 1.1: The optimal objective value of the simplified dual is bounded by $2/k$.
   • Implication: If true, this proves that $\alpha \le 2/4 = 0.5$, meaning a Condorcet Winning Set of size 4 always exists.

4. Results

• Recovery of Known Bounds: The solver successfully recovered the known lower bound construction where $k=3$ is required (finding $\alpha > 0.5$ for $k=2$).
• Failure to Find Counter-Examples for $k=4$:
  • For $m \in [7, 9]$ and $k=4$, extensive searches (using subsampling and infMILP) yielded no counter-examples.
  • In all runs where an upper bound was computed, the value was $\le 2/k$.
• Comparison of Models:
  • infMILP produced tighter (larger) $\alpha$ values than standard MILP, confirming the necessity of the infinite clone abstraction for finding worst-case scenarios.
  • However, even infMILP could not push $\alpha$ above $2/k$ for $k=4$.
• LP Relaxation Behavior: The root LP relaxation values approached 1 as $m$ increased, but the branch-and-bound process consistently tightened the bound to $\le 2/k$, suggesting a structural property of the problem.

5. Significance and Conclusion

• Theoretical Impact: The paper provides strong empirical evidence that the theoretical upper bound for Condorcet dimensions can be tightened from $k=5$ to $k=4$.
• New Analytical Path: By shifting focus from searching for counter-examples to analyzing the dual of the LP relaxation, the authors offer a concrete mathematical path to proving the $k=4$ bound.
• Methodological Advance: The work demonstrates the power of combining automated reasoning (MILP) with structural abstractions (infinite clones) and duality theory to tackle open problems in social choice theory that were previously intractable for discrete solvers.
• Future Work: The primary challenge remains the formal proof of the Dual Bound Conjecture. Proving that the simplified dual is bounded by $2/k$ would definitively close the gap, establishing that 4 candidates are always sufficient to guarantee a Condorcet winning set.