玩科学还是研究科学？

姜咏江

网友柳渝在评论中告诉我：注意目前有SAT的solver，可解几十万个变元（n）、几百万个字句（k）的例子，见每年举行的国际SAT竞赛网站：http://www.satcompetition.org。

我先是很震惊“可解几十万个变元（n）、几百万个字句（k）的例子”，后来一想，这不过是一种游戏而已。科学上的东西有很多是可以玩的。

K-CNF-SAT问题如何确定满足还是不满足，在没有找到有效方法之前，玩也许是寻找规律的一种方法。其实科学问题分为成功之前的玩和成功之后的玩。成功之前的玩，是一种“瞎玩”，而成功地找到规律之后，玩起来更有目的性。柳渝说的几十万个变量，几百万的子句的玩，就是一种瞎玩的表现。

K-CNF-SAT问题有两个限制数，一个是变量的个数n，另一个是子句中变元的数量k。实际上，这两个数量确定之后，子句的最大数量也就确定了，超出最大数量的子句，一定是前面的重复，而且K-CNF一定值为0。为什么？

第一、子句中各项只允许出现变量和变量的非，且数量为k，所以可能出现的子句总数不会超过C_zn^k=zn(2n-1)…(2n-k+1)/k!个。此时的K-CNF我称为完全合取范式。

第二、子句形如（x1+x2+…+xk）与（x1’+x2’+…+xk’）的值必为反码。一般地，一个子句的变量形式是另一个子句对应变量的非形式，则这样的子句叫互反子句。显然，互反子句A、B的与AB=0。

第三、合取范式K-CNF中只要有一个值为0 的子句，那么K-CNF的值就是0，即K-CNF-SAT问题不成立。

从以上三条来看，完全合取范式的值必为0。还有，只要K-CNF中有互反子句，那么合取范式的值必为0。

再者，给出的合取范式f(x1,x2,…,xn)是要通过随机发出的程序执行给出吧？不然成千上万的子句哪里来？编程很有意思，但目的是证明K-CNF是NPC问题，还是证明它是P问题？意义何在？

我在前文给出的“子句消去法”不用搞那么多子句，就可以指出K-CNF-SAT问题成立与否，而且可以在n次子句消去之后，就能够得出K-CNF-SAT问题成立与否的结论。

用子句消去法计算，如果K-CNF-SAT问题成立，那么同时就求出了成立的解。并且能够对任意的n位二进制数直接验证是否是解。

在对K-CNF-SAT问题的研究中，“子句消去法”的作用可想而知。

有了简单的处理K-CNF-SAT问题方法，那种成千上万，费时的玩科研还有必要吗？当然，属于游戏的东西还是要以玩为主。

2015-7-5