The fair division literature in economics considers how to divide resources between multiple agents such that the allocation is envy-free: each agent receives their favorite piece. Researchers have developed a variety of fair division protocols for the most standard setting, where the agents want to split a single item, however, the protocols are highly intricate and the proofs of envy-freeness involve tedious case analysis. We propose Slice, a domain specific language for fair-division. Programs in our language can be converted to logical formulas encoding envy-freeness and other target properties. Then, the constraints can be dispatched to automated solvers. We prove that our constraint generation procedure is sound and complete. We also report on a prototype implementation of Slice, which we have used to automatically check envy-freeness for several protocols from the fair division literature.
翻译:经济领域的公平分配文献考虑了如何在多个机构之间分配资源,使其分配是不嫉妒的:每个机构都可获得其喜欢的份额。研究人员开发了各种公平分配方案,适用于最常见的情况,即机构要分割单个项目。但是,这些方案非常复杂,而嫉妒性的证明涉及繁琐的案例分析。我们提出了公平分配语言Slice。我们的语言中的程序可以转换为编码嫉妒性和其他目标属性的逻辑公式。然后,可以将约束条件分配给自动求解器。我们证明了我们的约束生成程序是正确和完备的。我们还报告了Slice的原型实现,我们已经使用该实现自动检查了公平分配文献中几个协议的嫉妒性。