真实场景下的模型计数
Model Counting in the Wild
AI总结：
本研究针对模型计数的可扩展性问题，调研11个应用领域收集2262个基准测试用例，评估6款顶尖模型计数器，发现性能跨域差异显著且与社区提出的两个参数弱相关，为投资组合式方法的发展指明挑战与机遇。
摘要：
模型计数是自动推理领域的一个基础问题，应用于概率推理、网络可靠性分析、神经网络验证等多个领域。尽管理论上由于#P完全性，模型计数在计算上难以处理，但过去十年间，顶尖模型计数器的开发取得了显著进展，以应对可扩展性挑战。\n在本研究中，我们对真实场景中模型计数器的可扩展性进行了严格评估。为此，我们调研了11个应用领域，并从这些领域收集了总计2262个基准测试用例。随后，我们在这些实例上评估了6款顶尖模型计数器，以衡量其可扩展性和运行时性能。\n我们的实证评估表明，模型计数器的性能在不同应用领域间差异显著，凸显了终端用户需谨慎选择的必要性。此外，我们针对模型计数社区提出的两个参数，研究了不同计数器的表现，发现二者仅存在弱相关性。我们的分析凸显了模型计数中基于投资组合的方法所面临的挑战与机遇。
英文摘要：
Model counting is a fundamental problem in automated reasoning with applications in probabilistic inference, network reliability, neural network verification, and more. Although model counting is computationally intractable from a theoretical perspective due to its #P-completeness, the past decade has seen significant progress in developing state-of-the-art model counters to address scalability challenges. In this work, we conduct a rigorous assessment of the scalability of model counters in the wild. To this end, we surveyed 11 application domains and collected an aggregate of 2262 benchmarks from these domains. We then evaluated six state-of-the-art model counters on these instances to assess scalability and runtime performance. Our empirical evaluation demonstrates that the performance of model counters varies significantly across different application domains, underscoring the need for careful selection by the end user. Additionally, we investigated the behavior of different counters with respect to two parameters suggested by the model counting community, finding only a weak correlation. Our analysis highlights the challenges and opportunities for portfolio-based approaches in model counting.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
