这个特殊的 CNF 叫什么？答案

【问题标题】：What is this special CNF called?这个特殊的 CNF 叫什么？
【发布时间】：2017-05-10 03:15:57
【问题描述】：

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

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

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

【问题讨论】：

可能会误解某些东西，但不满足公式需要选择一个子句并将其中的所有变量分配为 false/true（取决于它是否不是类型子句）
我认为问题在于示例公式是析取范式，而不是合取范式。 - 参见例如en.wikipedia.org/wiki/Disjunctive_normal_form
你是对的 mcdowella。我修好了。
在计算机组织类中，这称为 sum 的乘积。

标签： algorithm complexity-theory boolean-logic

【解决方案1】：

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

【讨论】：

【解决方案2】：

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

【讨论】：