SAT中的局部冗余：阻塞子句的推广
计算机科学中的逻辑
2023-06-22 v3
摘要
简化合取范式公式的子句消除过程在现代SAT求解中起着重要作用。在实际求解过程之前或期间，此类过程识别并移除与求解结果无关的子句。这些简化通常依赖于所谓的冗余性质，其刻画了移除某子句不影响公式可满足性状态的情况。一种特别成功的冗余性质是阻塞子句（blocked clauses），因为它推广了其他几种冗余性质。要确定一个子句是否阻塞——从而冗余——只需考虑它的归结环境，即它可以与之归结的子句。因此，我们说阻塞子句的冗余性质是局部的。在本文中，我们展示了存在比阻塞子句更一般的局部冗余性质。我们提出了阻塞的语义概念，并证明它构成了最一般的局部冗余性质。此外，我们引入了基于语法的集合阻塞（set-blocking）和超阻塞（super-blocking）概念，并表明后者与我们的语义阻塞概念一致。另外，我们展示了如何经由Davis和Putnam消除原子公式的规则来另地刻画语义阻塞。最后，我们进行了详细的复杂性分析，并将我们的新冗余性质与文献中著名的冗余性质联系起来。
引用
@article{arxiv.1702.05527,
title = {Local Redundancy in SAT: Generalizations of Blocked Clauses},
author = {Benjamin Kiesl and Martina Seidl and Hans Tompits and Armin Biere},
journal= {arXiv preprint arXiv:1702.05527},
year = {2023}
}