关于CNF转换用于SAT枚举的论文
摘要：使用归结或Plaisted和Greenbaum变换的CNF编码可定位到解决的SAT问题，而不需要CNF问题预编码。 然而，在解决到列举的转变过程中，产生尽可能小的部分满足的分配是关键的，这引发了这种CNF编码是否也适用于列举的问题。 在这篇论文中，我们从理论和实证的角度研究了CNF转换对SAT列举的有效性。 并从消极的一面展示出：(i) Tseitin变换阻止求解器产生短的部分分配，严重影响列举的有效性；(ii) Plaisted和Greenbaum变换只在某种程度上解决了这个问题。 从积极的一面来看，我们展示了将Plaisted和Greenbaum变换与非标准化的预处理结合起来的结果 - 这通常不用于解决 - 可以完全克服问题，并可以大大减少部分赋值的数量和执行时间。
作者：Gabriele Masina, Giuseppe Spallitta and Roberto Sebastiani
论文ID：2303.14971
分类：Logic in Computer Science
分类简称：cs.LO
提交时间：2023-06-06