arXiv:2504.13842v1 宣布类型: 新 摘要: 现代社会充满了依赖概率推理、统计和组合学的计算挑战。有趣的是，许多这些问题可以被形式化为命题公式，并询问其模型的数量。随着对涉及模型计数的实际问题解决的兴趣不断增加，社区在2019年秋季组织了第一届模型计数（MC）竞赛。竞赛旨在推动应用的发展、识别具有挑战性的基准测试、促进新求解器的开发，并增强现有的模型计数问题及其变种的求解器。第一届竞赛将各种研究人员聚集在一起，确定了挑战，并激发了大量新的应用。在这篇文章中，我们全面介绍了2021年至2023年模型计数竞赛的流程和结果。竞赛包含了四条赛道，每条赛道专注于模型计数问题的不同变种。第一条赛道专注于模型计数问题（MC），旨在计算给定命题公式的模型数量。第二条赛道挑战开发者提交能够解决加权模型计数问题（WMC）的程序。第三条赛道专门研究投影模型计数（PMC）。最后，我们启动了结合投影和加权模型计数的轨道（PWMC）。竞赛继续获得高水平的参与度，共有七到九种不同的求解器提交，基于相当不同的技术。