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.

翻译：在计算社会选择领域，解决偏好聚合中多数循环的算法已被广泛研究。包括泰德曼排序配对法、舒尔茨击败路径法以及海茨格河流法在内的多种复杂循环解决方法，均是对分裂循环法的改进——该方法通过舍弃每个循环中最弱的多数获胜边来化解多数循环。最近，霍利迪与帕奎特提出了一种新的分裂循环法改进方案，称为稳定投票法，及其简化版本简单稳定投票法。他们猜想：当不存在两条多数获胜边规模相同时，SSV是SC的一种改进。本文中，我们证明了该猜想在候选方案不超过6个时成立，并在候选方案超过6个时推翻了该猜想。虽然我们对不超过5个候选方案的证明采用了传统数学推理，但6候选方案的证明与7候选方案的反例均通过SAT求解获得。支撑该证明与反例的SAT编码方法具有远超SC与SSV的适用性：它可用于检验任何仅依据获胜边规模排序决定胜者的投票方法的性质。