我在cnf文件中看到一些可满足和不可满足的子句文件的错误
更具体地说，我发现这里的zip文件夹的第一个文件:20个变量，91个子句- 1000个实例，都是可满足的包含一个标题为"uf20-01"的文件，其方程显然是不令人满意的，因为第15行第7条款和第4行第87条款是完全相反的!((5 19 17)和(-5 -19 -17))
因此，在任何时间点有它们的与运算将导致方程不满足。
我得到一个结论，当且仅当两个子句互为完全反比时，方程是不满足的，否则方程是可满足的。我已经尝试了上述链接的另一个UNSAT文件，虽然miniat浏览器版本也说相同的文件不满意，但我已经找到了每个变量1和0的解决方案。
上面的算法被我发表在一个期刊上，但是被拒绝了。
我的问题是:谁能给我举个例子，一个不能满足的3SAT方程，它只包含3个变量(或者更多一点)，没有任何一个子句是另一个的完全逆?
如果我能得到这样一个子句，那么算法是错误的(但它仍然证明许多SAT基准问题是UNSAT)，并且它不会证明第一链接中的许多UNSAT问题确实是SAT。
这是逗我玩的，希望大家都能理解，好像上面的算法是对的，那么我就证明了p =NP!它也可以引发一场革命……
顺便说一下:我也给SATLIB联系人发了邮件，但关于第二个链接文件，2天后仍然没有回复。
在CNF的3-Sat中，所有子句都是or子句，它们由and组合。因此，您引用的这两行定义了以下两个子句
x5 or x17 or x19
(not x5) or (not x17) or (not x19)
可以同时满足，例如，将x5设为true, x17设为false, x19设为任意
有很多:(x1或x2或x3)和(不是x1或x2)而不是x2和x3
一般来说，您需要引入更多的变量来显示这一点。但是，从直觉上看，UNSAT的发生甚至不需要任何条款的所有变量的反转，这似乎是不正确的。另一个答案指出，即使在最基本的情况下，当这种情况发生时，它仍然是SAT。也许基准测试集倾向于这样做，但它没有泛化。