3SAT 在多项式时间内求解？答案

【问题标题】：3SAT solved in polynomial time?3SAT 在多项式时间内求解？
【发布时间】：2015-05-26 08:36:17
【问题描述】：

我在可满足和不可满足子句文件SATLIB Benchmark Problems的cnf文件中看到了一些错误

更具体地说，我发现 zip 文件夹的第一个文件在这里： 20 variables, 91 clauses - 1000 instances, all satisfiable 包含一个标题为“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 天后仍然没有关于第二个链接文件的回复。

【问题讨论】：

标签： complexity-theory p-np

【解决方案1】：

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

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

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

【讨论】：

【解决方案2】：

有很多： (x1 or x2 or x3) and (not x1 or x2) and not x2 and not x3

一般来说，您需要引入更多变量来显示这一点。但直观地说，UNSAT 的发生不需要任何子句的所有变量的反转，这似乎并不正确。正如另一个答案指出的那样，即使在最基本的情况下，发生这种情况时仍然是 SAT。也许基准测试集往往有这个，但它没有概括。

【讨论】：