SATLIB 的 SAT 基准被证明是错误的？

Question

我发现根据 SATLIB SAT 实例，许多可满足的问题实际上是不可满足的，因为它们都包含一个或多个子句，这些子句具有针对它们的精确反子句。例如，以下下载链接为20 个变量的 SATLIB cnf 子句，91 个子句 - 1000 个实例，全部可满足

第一个文件本身的第 7 条和第 86 条是彼此精确相反的，因此这个方程永远不会不成立。我已经在这里发布了一个与此相关的问题，但到目前为止还没有得到任何回复关于 P=NP 的老问题 任何评论都非常受欢迎，因为我真的很想知道基准问题是否仍然用于比赛，或者不像它们那样那么那些比赛确实是没有用的。所以，我的问题是：我确定这些错误并将其公开并征求意见是否正确？这些发现还有用吗？我已经发送了几封电子邮件要求基准问题网站管理员回复，但两个月后仍然没有回复，这让我感觉很糟糕。

Answer 1

我找不到反条款的正确定义，所以我不得不推测一下。

两个大小 > 1 的子句（每个字面量都被反转）本身并不矛盾。鉴于条款

 1  2  3 0
-1 -2 -3 0

我们可以找到满足这两个子句的多种解决方案，因为我们只需要满足每个子句的一个文字。一些部分解决方案是

 1 -2
-1  2
 2 -3
...

对于这些子句，只需选择一个正数和一个负数。