3SAT 在多项式时间内解决？

Question

我在可满足和不可满足子句文件的 cnf 文件中看到了一些错误SATLIB 基准问题

更具体地说，我发现这里的 zip 文件夹的第一个文件： 20 个变量，91 个子句 - 1000 个实例，所有可满足的 包含一个标题为“uf20-01”的文件，其方程显然是不可满足的第 15 行的第 7 个子句和第 4 行的第 87 个子句彼此完全相反！((5 19 17) 和 (-5 -19 -17))

因此，在任何时间点对它们进行 AND 运算都会导致方程无法满足。

我得出的结论是，如果两个子句彼此完全相反，那么只有当方程不可满足时，否则方程是可满足的。我已经尝试了上述链接的另一个 UNSAT 文件，并进行了反复试验，尽管 MINISAT浏览器版本还说相同的文件不满意我已经找到了每个变量的 1 和 0 相同的解决方案。

上面的算法是我发布到期刊上的，但被拒绝了。

我的问题是：有人能给我一个不可满足的 3SAT 方程的例子吗？该方程仅包含 3 个变量（或者可能更多......），而没有任何子句与另一个子句完全相反？

如果我能得到这样的子句，那么算法就是错误的（但它仍然证明许多 SAT 基准问题是 UNSAT），并且不能证明第一个链接中的许多 UNSAT 问题确实是 SAT。

这是在逗我的心，希望大家能理解，如果上面的算法是对的，那么我就证明了P=NP！它也可以引发一场革命..

顺便说一句：我也已向 SATLIB 联系人发送了电子邮件，但 2 天后仍然没有回复有关第二个链接文件的信息。

Answer 1

在 CNF 的 3-Sat 中，所有子句都是 OR 子句，并且它们通过 AND 组合。所以你引用的两行定义了以下两个子句

x5 or x17 or x19
(not x5) or (not x17) or (not x19)

这两者都可以满足，例如，通过将 x5 设置为 true，x17 设置为 false，x19 设置为任意。