姜咏江

最近我将SAT问题快速求解的算法寄给同行讨论。曾有人告诉我，国外SAT问题大赛，几十万个变量的问题都很快计算出来了。我查了一下所谓的竞赛，题目中子句块中子句都很少，因而参赛人蒙上正确的变量值可能性很大。所以比赛计算结果都要带回原式验证，才能知道对与错。这叫解决了SAT问题的算法？有些题目只要改变一两个变量值，就知道无解。这种竞赛有多大意义？

对那些随机给出的子句，能否保证没有重复？如果出现了重复，子句的数量不能说明什么。如果计算结果无需验证，就能够保证给出的SAT问题表达式是否根本无解，或得到的是满足解，这才是有意义的竞赛。这些都不能保证，所谓的竞赛就纯属扯淡！

我可以给出更多变量的SAT问题，并且保证事先就知道有解无解。

2016-12-6