我发现根据 SATLIB SAT 实例，许多可满足的问题实际上是不可满足的，因为它们都包含一个或多个对它们有确切反条款的子句。例如下面的SATLIB cnf 子句的下载链接，包含 20 个变量、91 个子句 - 1000 个实例，都可以满足
有第一个文件本身，其中第 7 和第 86 条彼此完全相反，因此这个等式永远不会不满足。我已经在这里发布了一个关于此的问题，但到目前为止没有得到任何答复P = NP 上的旧问题 非常欢迎任何评论，因为我真的很想知道基准问题是否仍然用于比赛，就好像它们一样那么那些比赛真的没用。所以，我的问题是：我在确定这些错误并将它们暴露给公众并征求意见方面是否正确？这些发现还有用吗？我已经发送了几封电子邮件，要求基准问题网站的管理员回复，但 2 个月后仍然没有回复让我感觉很糟糕。