假设您有一个布尔可满足性的实例,其中 CNF 中给出的公式。此外,每个子句仅包含正面文字或负面文字。例如:
(a || b) && (!a || !c || !d) && (b || d)
这样的布尔公式有特殊的名称吗?与标准 CNF 公式相比,是否有更快的方法来测试此类公式的可满足性?
假设您有一个布尔可满足性的实例,其中 CNF 中给出的公式。此外,每个子句仅包含正面文字或负面文字。例如:
(a || b) && (!a || !c || !d) && (b || d)
这样的布尔公式有特殊的名称吗?与标准 CNF 公式相比,是否有更快的方法来测试此类公式的可满足性?
一类 CNF,使得每个子句要么是肯定的,要么是否定的,也就是说,没有同时包含肯定和否定文字的子句,被称为“单调 CNF”,例如 Hans Kleine Buening 在他的命题逻辑一书中. 最近一篇关于单调 CNF 的论文是 https://arxiv.org/abs/1603.07881 “Monotone 3-Sat-4 is NP-complete” 通过标准技术不难看出,单调 3-SAT(所有条款都是正或负,所有子句的长度(最多)3)是 NP 完全的,上面的论文通过展示每个变量最多出现四次的情况下的 NP 完全性来改进这一点。