algorithm - 这个特殊的 CNF 叫什么？

Question

假设您有一个 bool 可满足性实例，其中公式在 CNF 中给出。此外，每个子句仅包含肯定文字或否定文字。例如:

(a || b) && (!a || !c || !d) && (b || d)

这样的 bool 公式有专门的名字吗？与标准 CNF 公式相比，是否有更快的方法来测试此类公式的可满足性？

Answer 1

CNF 类使得每个子句要么是肯定的要么是否定的，也就是说，没有子句同时包含肯定和否定文字，例如 Hans Kleine Buening 在他的书中被称为“单调 CNF”关于命题逻辑。最近一篇关于单调 CNF 的论文是 https://arxiv.org/abs/1603.07881“单调 3-Sat-4 是 NP 完全”通过标准技术不难看出，单调 3-SAT(所有子句要么是正的要么是负的，所有子句的长度(最多)为 3)是 NP 完全的，上面的论文通过显示 NP-每个变量最多出现四次的情况的完整性。