In an election where $n$ voters rank $m$ candidates, a Condorcet winning set is a committee of $k$ candidates such that for any outside candidate, a majority of voters prefer some committee member. Condorcet's paradox shows that some elections admit no Condorcet winning sets with a single candidate (i.e., $k=1$), and the same can be shown for $k=2$. On the other hand, recent work proves that a set of size $k=5$ exists for every election. This leaves an important theoretical gap between the best known lower bound $(k\geq 3)$ and upper bound $(k \leq 5)$ for the number of candidates needed to guarantee existence. We aim to close the gap between the existence guarantees and impossibility results for Condorcet winning sets. We explore an automated reasoning approach to tighten these bounds. We design a mixed-integer linear program (MILP) to search for elections that would serve as counter-examples to conjectured bounds. We employ a number of optimizations, such as symmetry breaking, subsampling, and constraint generation, to enhance the search and model effectively infinite electorates. Furthermore, we analyze the dual of the linear programming relaxation as a path towards obtaining a new upper bound. Despite extensive search on moderate-sized elections, we fail to find any election requiring a committee larger than size 3. Motivated by our experimental results in this direction, we simplify the dual linear program and formulate a conjecture which, if true, implies that a winning set of size 4 always exists. Our automated reasoning results provide strong empirical evidence that the Condorcet dimension of any election may be smaller than currently known upper bounds, at least for small instances. We offer a general-purpose framework for searching elections in ranked voting and a new, concrete analytical path via duality toward proving that smaller committees suffice.

翻译：在$n$个选民对$m$个候选人进行排序的选举中，孔多塞获胜集是一个由$k$个候选人组成的委员会，使得对于任何外部候选人，多数选民更偏好委员会中的某位成员。孔多塞悖论表明，某些选举不存在单人（即$k=1$）的孔多塞获胜集，同理可证$k=2$的情况也不存在。另一方面，近期研究证明，对于任何选举，存在大小为$k=5$的获胜集。这导致保证存在性所需候选人数量方面，已知下界（$k\geq 3$）与上界（$k\leq 5$）之间存在重要的理论空白。我们旨在缩小孔多塞获胜集存在性保证与不可能性结果之间的差距。我们探索了一种自动化推理方法来收紧这些界。我们设计了一个混合整数线性规划（MILP）来搜索可能作为猜想界的反例的选举。我们采用多种优化技术，如对称性破缺、子采样和约束生成，以增强搜索能力并有效模拟无限选民群体。此外，我们分析了线性规划松弛的对偶形式，作为获取新上界的途径。尽管对中等规模选举进行了广泛搜索，我们未能发现任何要求委员会规模大于3的选举。基于该方向的实验结果，我们简化了对偶线性规划并提出了一个猜想：若该猜想成立，则意味着大小为4的获胜集总是存在。我们的自动化推理结果提供了强有力的实证证据，表明任何选举的孔多塞维度可能小于当前已知的上界，至少对于小规模实例如此。我们提供了一个用于搜索排序选举问题的通用框架，以及一条通过对偶性证明更小委员会已经足够的新具体分析路径。