模型计数竞赛 2020
The Model Counting Competition 2020
AI总结：
本文报告了 2020 年模型计数竞赛（MC 2020）的执行情况与结果，该竞赛包含 MC、WMC 和 PMC 三个赛道，共收到来自 8 个小组的 9 个求解器的 34 个版本。
摘要：
现代社会中的许多计算问题归结为概率推理、统计学和组合数学。这些现实世界问题中有许多可以通过将问题表示为（布尔）公式，并将公式的模型数量直接与问题的答案相关联来解决。由于近年来人们对模型计数在实际问题求解方面的兴趣日益浓厚，模型计数（MC）竞赛于 2019 年秋季被构想出来。该竞赛旨在促进应用，识别新的具有挑战性的基准，并推广新的求解器以及改进模型计数问题及其相关版本的现有求解器。我们希望这些结果能够作为模型计数当前可行性的良好指标，并激发许多新的应用。在本文中，我们报告了 2020 年模型计数竞赛的详细信息、竞赛的执行情况以及结果。该竞赛包含模型计数问题的三个版本，我们在单独的赛道中对其进行了评估。第一个赛道以模型计数问题（MC）为特色，该问题要求计算给定布尔公式的模型数量。在第二个赛道上，我们挑战开发者提交解决加权模型计数问题（WMC）的程序。最后一个赛道专门用于投影模型计数（PMC）。总共有来自 8 个小组的 9 个求解器的 34 个版本参赛，这一数量令人惊讶。
英文摘要：
Many computational problems in modern society account to probabilistic reasoning, statistics, and combinatorics. A variety of these real-world questions can be solved by representing the question in (Boolean) formulas and associating the number of models of the formula directly with the answer to the question. Since there has been an increasing interest in practical problem solving for model counting over the last years, the Model Counting (MC) Competition was conceived in fall 2019. The competition aims to foster applications, identify new challenging benchmarks, and to promote new solvers and improve established solvers for the model counting problem and versions thereof. We hope that the results can be a good indicator of the current feasibility of model counting and spark many new applications. In this paper, we report on details of the Model Counting Competition 2020, about carrying out the competition, and the results. The competition encompassed three versions of the model counting problem, which we evaluated in separate tracks. The first track featured the model counting problem (MC), which asks for the number of models of a given Boolean formula. On the second track, we challenged developers to submit programs that solve the weighted model counting problem (WMC). The last track was dedicated to projected model counting (PMC). In total, we received a surprising number of 9 solvers in 34 versions from 8 groups.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
