SAT中的局部冗余：阻塞子句的泛化
摘要：局限性消除程序在简化合取范式公式中起着重要作用，对现代SAT求解具有重要意义。在实际求解过程之前或期间，这些程序能够识别和移除与求解结果无关的子句。这些简化通常依赖于所谓的冗余性质，这些性质描述了移除一个子句不会影响公式可满足性的情况。其中一个特别成功的冗余性质是封锁子句，因为它概括了其他几个冗余性质。要确定一个子句是否封锁（从而是冗余的），只需要考虑它的解析环境，即它可以与之解析的子句。因此，我们说封锁子句的冗余性质是局部的。在本文中，我们展示了存在比封锁子句更一般的局部冗余性质。我们提出了封锁的语义概念，并证明它构成了最一般的局部冗余性质。我们还引入了基于语法的集合封锁和超级封锁概念，并证明后者与我们的语义封锁概念一致。此外，我们还展示了如何通过Davis和Putnam的消除原子公式规则来替代特征化语义封锁。最后，我们进行了详细的复杂性分析，并将我们的新颖冗余性质与文献中著名的冗余性质相关联。
作者：Benjamin Kiesl, Martina Seidl, Hans Tompits, Armin Biere
论文ID：1702.05527
分类：Logic in Computer Science
分类简称：cs.LO
提交时间：2023-06-22