子句消去法与子句计数法

姜咏江

在3SAT问题求解研究中，我先提出了子句消去计数法，然后又给出了子句分段消去法。后来感到前者就叫“子句计数法”，后者叫“子句消去法”更为合适。这两种3SAT解法之间有着怎样的关系？概括地说，子句计数法是以空间复杂度满足为基础，是获得k-SAT解算法时间复杂度最快速的方法，这也是设计硬件运算器的实用方法。子句消去法在空间复杂度一定的情况下，获得最佳时间复杂度的算法。

两种解决k-SAT问题的计算方法实际上都围绕着“反子句”这样一个概念展开的。将逻辑变量自身用“1”表示，它的非运算用“0”表示，叫做01表示法。k-SAT一个子句就是k个逻辑变量的一组0和1的表示值。将一个子句的01表示用其反码数表示称为原子句的反子句。k-SAT子句计数法和子句消去法的本质问题都是“只要k-SAT对一组n元选定值有反子句存在，那么这组选定值就不是满足解”。

我们都能清楚如下的内容。

子句就是一个逻辑多项式，使子句项为1的变量值我们之称为变量的解值。k-SAT就是合取范式k-CNF=1的问题。要使k-CNF=1成立，必须每个子句的值都要为1，因为子句有一项值是1，那么这个子句的值就是1。子句间是与运算的关系，因而消去值为1 的子句，不会改变剩余k-SAT的满足解求出。

在子句计数法中重要的概念是“一侧”^[1]。所谓的一侧是如下定义的：逻辑变量本身用1代表，其非运算用0表示， k个变量组成的子句就是一个k位二进制数。n个变量取值0或1排列的n位值向量，叫一侧。

我们给出反侧定义：将一侧的每位数码都换成反码，得到的一侧叫原一侧的反侧。

子句计数法中，每个子句都是某一侧的组成部分，那么每个一侧所包含的子句数应是n个元素取出k个取值的组合数C_n^k。根据定义，显然一侧不会包含互反子句。

如果某个n元k-CNF的一侧不包含任何子句，那么其计数将是0，这说明该一侧的反侧在本k-SAT都不存在反子句。于是只要我们设定这个反侧的变量表示为解值，就能使k-SAT有满足解。

子句计数法以预先设定硬件逻辑资源为代价，对于n个变量需要设定2ⁿ个标志位，每个标志位必须用一侧来命名。这种命名计算需要将变量有序排列，那么由数字表示的一侧就可以直接与变量取值一一对应。

子句计数法的优点是一次性可以求出k-SAT的全部满足解，而且通过设计好的硬件逻辑识别电路（用Verilog HDL语言设计十分方便），每输入一个k-CNF的子句，瞬间就可以得到输入部分的全部解。至于能否像加减法运算器那样通过软件方法实现硬件功能扩充，有待进一步研究。

子句消去法^[2]将文字用理解成变量值，将文字的表示转化成数码0和1来表示，把k-CNF中的0和1叫变量表示值，将求解中设定的变量值叫解值。这样就可用二进制限位数理论和方法进行分析操作。如果将一个变量的解值定为其表示值，那么将包含该变量及其表示值相同的子句都消去，不影响剩余的k-SAT求满足解。

由于反子句只出现在具有相同变量的子句类型当中，所以引进了子句块：相同变量组成的子句集称为子句块。在子句消去法实施过程中，那些具有相同未确定解值的变量称为动态子句块。子句块可用看作动态子句块的特例。动态子句块是在不断设定变量解值，消去相关子句之后的情况下得到的子句块，每设定一个变量的解值，显然都会得到降阶的动态子句块。

一个子句块包含所有可能的子句，我们称其为完全子句块^[3]。根据限位数理论，完全子句块中每个子句都有其反子句，所以无论选定怎样的变量解值都不能够将全部子句消去。因此，子句消去法求解的关键，就是避开选择变量解值后出现低一阶的完全子句块。如果不能避免出现完全子句块，那么k-SAT没有满足解。

子句消去法以动态子句块为单位，用逐步降阶的方法，在k-SAT有满足解的条件下，逐步将一些满足解求出，或者判断k-SAT没有满足解，是一种简单易行的计算方法。这种方法只需要对每个变量设定一次解值，就可以对任何的k-SAT施行求解。因而，毫无疑问子句消去法是一种O(n)时间复杂度的算法。

子句消去法求解，当k-SAT有唯一解时，效率最高。相对子句计数法来说，当k-SAT有多解时，常常不能够一次设定变量解值，就能求出k-SAT全部满足解，要求全部解，则需要将每个动态块的全部解都写出，最后组合成k-SAT的全部解。不过这与k-SAT是否能够在多项式时间求出满足解关系不大。

我已经认定子句计数法和子句消去法都是所谓多项式时间复杂度的算法。因为是2015年才研究出的方法，必有许多不够完善之处，望有兴趣的朋友们一块讨论。

【参考文件】

[1]  http://blog.sciencenet.cn/blog-340399-905817.html 

[2]  http://blog.sciencenet.cn/blog-340399-928224.html

[3]  http://blog.sciencenet.cn/blog-340399-946247.html

2016-01-02