投影模型计数中的动态阻塞子句消去

在本文中，我们探索阻塞子句消去在投影模型计数中的应用。投影模型计数问题是确定在消去给定变量集 X 后命题公式 Σ 的模型数量 ||∃X.Σ||。尽管阻塞子句消去是 SAT 求解的著名技术，但其直接应用于模型计数具有挑战性，因为它通常会改变模型数量。然而，我们通过将阻塞子句搜索聚焦于投影变量，证明阻塞子句消去可以在保持正确模型计数的情况下加以利用。为了在模型计数中高效利用阻塞子句消去，我们引入了一种新颖的数据结构和相关算法。我们的方法在模型计数器 d4 中实现。实验表明了我们新方法在投影模型计数中计算方面的优势。