Stable Voting and the Splitting of Cycles

TL;DR

The paper investigates how Stable Voting (SV) and Simple Stable Voting (SSV) compare to Split Cycle (SC) for resolving majority cycles. It introduces a rigorous SAT-based framework to test whether the SSV winner must lie among SC winners in all cases without ties, proving the conjecture for up to six alternatives and providing a 7-alternative counterexample. The authors detail a full encoding (4.1–4.4) and present computational results showing unsatisfiability up to six alternatives and counterexamples thereafter, illustrating the power of SAT in social choice. They discuss practical implications for small-election settings and outline future directions for applying the SAT approach to broader axioms and tie-handling variants.

Abstract

Algorithms for resolving majority cycles in preference aggregation have been studied extensively in computational social choice. Several sophisticated cycle-resolving methods, including Tideman's Ranked Pairs, Schulze's Beat Path, and Heitzig's River, are refinements of the Split Cycle (SC) method that resolves majority cycles by discarding the weakest majority victories in each cycle. Recently, Holliday and Pacuit proposed a new refinement of Split Cycle, dubbed Stable Voting, and a simplification thereof, called Simple Stable Voting (SSV). They conjectured that SSV is a refinement of SC whenever no two majority victories are of the same size. In this paper, we prove the conjecture up to 6 alternatives and refute it for more than 6 alternatives. While our proof of the conjecture for up to 5 alternatives uses traditional mathematical reasoning, our 6-alternative proof and 7-alternative counterexample were obtained with the use of SAT solving. The SAT encoding underlying this proof and counterexample is applicable far beyond SC and SSV: it can be used to test properties of any voting method whose choice of winners depends only on the ordering of margins of victory by size.

Figures (6)

• Figure 1: Upper row and bottom left: three majority cycles, with their weakest links shown as dashed arrows. Bottom right: the head-to-head victories that count as defeats according to Split Cycle. The only undefeated candidate is $d$.
• Figure 2: Left: margins between alternatives. Right: the defeats according to Split Cycle, yielding multiple undefeated candidates.
• Figure 3: Three-alternative elections considered in the computation of the SSV winners for the four-alternative election in Figure \ref{['TwoWinners']}. SSV winners are shown in green.
• Figure 4: The 7-alternative counterexample to Conjecture \ref{['ConjInformal']}.
• Figure 5: The 8-alternative counterexample with one Split Cycle winner ($g$) that defeats the SSV winner ($a$).

Theorems & Definitions (36)

• Conjecture 1: HP2023
• Definition 1
• Lemma 2
• Definition 3
• Lemma 4
• proof
• Definition 5
• Definition 6
• Lemma 7
• proof