面向投影和增量伪布尔模型计数的探索

模型计数是指确定逻辑公式（通常为合取范式，CNF）的满足赋值数量的基本任务。虽然CNF模型计数在最近数十年中受到广泛关注，但关于伪布尔（PB）模型计数的兴趣仅刚刚萌芽，部分原因是PB公式的更大灵活性。因此，我们注意到现有PB计数器存在功能缺口，如对投影和增量setting的支持不足，这可能阻碍其采纳。本文我们的主要贡献是引入PB模型计数器PBCount2，这是第一个支持投影和增量模型计数的精确PB计数器。我们的计数器使用我们的最小出现加权级联度（LOW-MD）计算排序启发式方法来支持投影模型计数，并通过缓存机制实现增量模型计数。在我们的评估中，PBCount2在投影模型计数方面的基准数量至少是竞争方法的1.40倍，在增量模型计数方面至少是竞争方法的1.18倍。