构建精确的伪布尔模型计数器

模型计数是计算机科学中的一项基础任务，旨在确定布尔公式的可满足赋值数量，这些公式通常表示为合取范式（CNF）。尽管针对 CNF 公式的模型计数已受到广泛关注并具有广泛的应用，但对伪布尔（PB）公式模型计数的研究却相对被忽视。伪布尔公式比命题布尔公式更为简洁，在表示现实世界问题时提供了更大的灵活性。因此，研究针对 PB 公式的高效模型计数技术至关重要。在本工作中，我们提出了首个基于通过代数决策图进行知识编译方法的精确伪布尔模型计数器 PBCount。我们广泛的实证评估表明，PBCount 能够计算 1513 个实例的计数，而当前最先进的方法只能处理 1013 个实例。我们的工作为 PB 公式模型计数领域的未来研究开辟了多条途径，例如预处理技术的开发以及对知识编译以外方法的探索。