模型计数竞赛 2021-2023

现代社会充满了依赖概率推理、统计学和组合数学的计算挑战。令人趣见的是，这些问题许多都可以通过将其编码为命题公式，然后询问其模型数量来形式化。随着对实际问题解决任务（尤其是涉及模型计数）日益关注的增长，社区于 2019 年秋季设立了模型计数（Model Counting, MC）竞赛，并于 2020 年举办首届。该竞赛旨在推动应用发展、识别具有挑战性的基准、培育新求解器的开发，并提升现有求解器以解决模型计数问题及其变体。首届竞赛汇聚了 various researchers，识别了挑战，并激发了大量新的应用。本文综述了 2021-2023 年三届模型计数竞赛，详细阐述了其执行方式与结果。竞赛包含四个轨道，每个轨道聚焦于模型计数问题的不同变体。第一个轨道聚焦于模型计数问题（MC），旨在计算给定命题公式的模型数量。第二个轨道挑战开发者提交程序，以解决加权模型计数问题（WMC）。第三个轨道专注于投影模型计数问题（PMC）。最后，我们启动了一个将投影模型计数与加权模型计数结合的轨道（PWMC）。该竞赛在高水平的参与下持续进行，各轨道提交的求解器数量在 7 至 9 个之间，技术手段差异巨大。