通过阻塞子句分解改进SAT求解器

最具竞争力的CDCL（冲突驱动子句学习）SAT求解器所使用的决策变量选择策略要么是VSIDS（变量状态独立衰减和），要么是它的变体如指数版本EVSIDS。VSIDS及其变体的共同特点是在求解过程中利用统计信息，但忽略问题的结构信息。为此，本文改进了决策变量选择策略，提出了一种基于BCD（阻塞子句分解）的SAT求解技术。其基本思想是：一部分决策变量由VSIDS启发式选择，而另一部分决策变量由通过BCD获得的阻塞集选择。与现有的基于BCD的技术相比，我们的技术简单，且不需要对CNF公式重新编码。针对认证UNSAT轨道的SAT求解器也可应用我们的基于BCD的技术。我们在应用基准上的实验表明，基于BCD的新变量选择策略能够提升诸如abcdSAT等SAT求解器的性能。带有BCD的求解器解决了SAT Race 2015中的一个实例，该实例迄今为止未被任何求解器解决。这表明在某些情况下，基于结构信息的启发式比基于统计信息的启发式更高效。