我发现根据 SATLIB SAT 实例，许多可满足的问题实际上是不可满足的，因为它们都包含一个或多个子句，这些子句具有针对它们的精确反子句。例如，以下下载链接为20 个变量的 SATLIB cnf 子句，91 个子句 - 1000 个实例，全部可满足
第一个文件本身的第 7 条和第 86 条是彼此精确相反的，因此这个方程永远不会不成立。我已经在这里发布了一个与此相关的问题，但到目前为止还没有得到任何回复关于 P=NP 的老问题 任何评论都非常受欢迎，因为我真的很想知道基准问题是否仍然用于比赛，或者不像它们那样那么那些比赛确实是没有用的。所以，我的问题是：我确定这些错误并将其公开并征求意见是否正确？这些发现还有用吗？我已经发送了几封电子邮件要求基准问题网站管理员回复，但两个月后仍然没有回复，这让我感觉很糟糕。
我在可满足和不可满足子句文件的 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 天后仍然没有回复有关第二个链接文件的信息。