论在核心 (非) 空缺上的问题：基于 Approval-Based 多胜选投票的自动推理方法

核心稳定性是多胜选投票中一种自然且被广泛研究的群体公平性概念，涉及从候选人池中选择委员会成员的任务。我们研究的设置是选民对每位候选人要么批准，要么不批准；在这种情况下，是否存在始终存在核心稳定委员会仍为一个主要的开放问题。本文我们发展了一种基于混合整数线性规划的方法，用于决定核心稳定委员会是否必然存在。与计算社会选择中流行的 SAT 方法不同，我们的方法可以为特定候选人数量的证明，而不受选民数量的制约。除了这些计算上的优势，我们的程序也为核心稳定问题提供了一种新颖的对偶性改写，由此获得了在特殊情况下的新存在性结果。进一步，我们利用我们的框架揭示了核心稳定性与其他可取性质（如价格可实现性等价性）之间的先前未知关系。