-1

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

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

因此，在任何时间点都有它们的 AND 运算将导致方程不可满足。

我得出的结论是，如果两个子句彼此完全相反，那么只有这个方程是不可满足的，否则这个方程是可满足的。浏览器版本还说相同的文件不满意我已经为每个变量找到了相同的 1 和 0 的解决方案。

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

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

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

这是在逗我，希望大家能看懂，好像上面的算法是对的，那我证明了P=NP！它也可以引发一场革命。

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

4

2 回答 2

5

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

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

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

于 2015-07-15T06:52:55.523 回答
0

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

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

于 2021-04-05T18:13:55.123 回答