姜咏江 用 n 个逻辑变量和其变量非形式中的不超过 k （ k 是一个常数）个，写出若干个或运算多项式（子句），问能不能设定这 n 个变量的一组值（是一个 n 位二进制数），使每一个多项式的逻辑值都是 1 （真）？这个问题就是被国外认定的世界难题 SAT 。 举个例子，有逻辑变量 x 1 , x 2 , … , x 5 ，它们的非形式是 x 1 ’, x 2 ’ , x 3 ’, x 4 ’, x 5 ’ ，随便写出的多项式有： x 1 ’+ x 2 ’+ x 3 ’+ x 4 ’+ x 5 ’ ， x 1 ’+ x 2 ’+ x 3 + x 4 + x 5 ’ ， x 1 + x 2 ’+ x 3 + x 4 ’+ x 5 ’ ， x 1 + x 2 + x 3 ’+ x 4 ’+ x 5 ’ ， 问是否能够将这几个多项式值都为 1 的那些二进制数找出来？ 这些多项式中都有变量的非项，可以马上找出 00000 可以满足要求。 如果上面的由 5 个变量及其非形式组成的多项式可能“残缺不全”，并且有很多个，你还能够一下子找出满足条件的二进制数吗？这个问题用穷举法可以办到，这需要将二进制数从 00000 一直到 11111 这 32 个数一一带入每个多项式验证。 n 个变量的这种验证次数总是 2 n 。 显然，当 n 较小的时侯，验证的工作量不大，但若 n 变大，而 k 不变的时侯，工作量就会以惊人的速度增大，以至于有上百个变量，而多项式并不太多的时侯，用计算机来验证也难以短时间内完成。 有 n 个变量的 SAT 如果有解，一定是在二进制数 0 ～ 2 n -1 之中。能不能根据多项式将这 2 n 个数中不是解或是解的单独找出来？这样在 n 位二进制数已知的情况下，速度会加快。 为了简单，我们用 1 表示多项式中的变量 x ，用 0 表示 x ’。那么每个多项式就可以写成二进制数的形式。如此我们就引进了子句块的概念，并且能够证明互反子句（二进制数表示的子句互为反码）都不在子句块中，都是 SAT 解的组成部分，有一个在子句块中，它的反子句就不是 SAT 解的组成部分。所谓子句块是相同变量组成的子句全体。子句是不是 SAT 解的组成部分，是由数码的位置来确定的。例如， 1 1 0 是 11100 、 10100 、 ... 、 11110 的组成部分，但不是 01100 的组成部分，虽然 110 在 01100 当中，这是因为 1 1 0 在 01100 对应位置数码不同。 我们能不能用带位置二进制数码表示的子句，找出 SAT 的全部解？这就是本文要谈的中心内容。 计算机中的数都是二进制数码表示的，同一数码在不同位置是它们的根本区别。 如果一组数码和一个子句块变量位置相对应，且能够使子句块中每一个子句的值为1，那么这组数码一定是 n 个变量SAT解的组成部分；如果这组数码虽然与子句块的变量的位置对应，但不能使这个子句块的所有子句值为1，那么这组数码对应所在的 n 位二进制数，一定不是 n 个变量SAT的解。 我们把二进制表示的子句所在n位二进制数叫子句的标志。根据子句消去法，SAT的解一定在子句标志当中。如果我们将SAT子句的所有标志，通过子句将其它们从 n 位二进制数中消去，那么剩下的 n 位二进制数就一定是由SAT中子句的反子句或不在SAT中的互反子句构成的。 在子句消去法中有一个很重要的定理： 反子句不在和互反子句都不在子句块中的子句是该子句块的解 。 根据这一定理，将剩下的 n 位二进制数取反，得到的数一定都是SAT的解。 如果你对 SAT 有所了解，或者看过我的子句消去法，我想理解上面的叙述不会有问题。问题会在这一过程中的算法，是不是多项式时间复杂度？ 假如 SAT 中最高阶子句有 k 个变量，那么 SAT 最多有2 k C n k +2 k-1 C n k-1 +...+2C n 1 这 k 次多项式计算结果个子句。我们可以先从低阶子句开始消去子句标志，那么最多也就是要进行 2 k C n k +2 k-1 C n k-1 +...+2C n 1 次（实际上，由于高阶子句包含低阶子句，这种操作要少得多）就可以完成子句标志消去的工作，剩下的 n 位数的反码就都是 SAT 的解！可见整个 子句标志消去法 的算法时间复杂度为 O( n k ) 。 需要说明，在计算机中 0 ～ 2 n -1 个二进制数是放在文件中，或地址编码本身，计算机中只有二进制数，因而寻找子句的标志可以用一个指令实现。由此可见，由子句消去其标志就是一个 O(1) 时间复杂度。 以上我谈的问题是计算机理论和方法中的问题，搞计算机理论的人都可以鉴定对与错，没有必要非要请“洋专家”评判。 请参阅： http://blog.sciencenet.cn/blog-340399-1009188.html http://blog.sciencenet.cn/blog-340399-1009397.html http://blog.sciencenet.cn/blog-340399-987007.html 2016-10-31
标签: 子句标志消去法
