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

Question

假设您有一个布尔可满足性的实例，其中 CNF 中给出的公式。此外，每个子句仅包含正面文字或负面文字。例如：

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

这样的布尔公式有特殊的名称吗？与标准 CNF 公式相比，是否有更快的方法来测试此类公式的可满足性？

Answer 1

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

Answer 2

它被称为布尔可满足性问题或简称 SAT。尽管存在针对特殊情况的多项式解决方案（请参阅2SAT），但一般问题是 NP 完全的（这意味着它没有所谓的快速解决方案）。