K-CNF-SAT多项式时间求解算法和软件

姜咏江

                                                Email:accsys@126.com                

摘要：给出子句消去计数法分组定解算法，该算法可以在多项式时间求出k-CNF-SAT的全部解。证明了斯提芬.库克定义下的NPC问题就是一个P类问题。

关键词：NPC，P/NP问题，子句消去计数法分组定解

1.              背景简介

P/NP问题曾于2000年被美国克雷数学所定为最难的难题，有甚者说其挑战了人类智慧。所谓P/NP问题的定义是这样给出的：

复杂度类P包含所有那些可以由一个确定型图灵机在多项式表达的时间内解决的问题；类NP由所有其肯定解可以在给定正确信息的多项式时间内验证的决定问题组成，或者等效的说，那些解可以在非确定图灵机上在多项式时间内找出的问题的集合。

实际上这个定义有很多歧义，涉及到人们对确定型图灵机、非确定型图灵机、多项式时间、问题、决定问题、肯定解、给定正确信息、验证等一系列概念的认识的不统一，很难形成统一的见解。人们能够统一的是P类问题属于NP类问题，但NP类问题是否就是P类问题，一直没有确定的结论。

1971年斯提芬.库克 (Stephen A. Cook) 发表了〈The Complexity of Theorem Proving Procedures〉才把P之外的问题归结为三大类，即 NP、NP-complete 及 NP-hard。库克的分类得到了学术界的认可。在库克的定义下，P、NP、NPC、NPH问题的定义如下：

P问题，可以在多项式时间内求出解的问题，Polynomial problem。

NP问题，可以在多项式的时间里验证一个解的问题，Non-deterministic polynomial

NPC问题，如果所有的NP问题都存在多项式时间算法使其能够归约为某一NP问题，则称该NP问题为NPC问题，Np complete。

NPH问题，如果所有的NP问题都存在多项式时间算法使其归约到某问题，则称该问题为NPH问题，Np hard。

由以上NPC问题的定义，我们不难想到，只要我们能够找到一个NPC问题，并能够找到其多项式时间的求解算法，那么就可以肯定这个NPC问题就是一个P问题。因为所有的NP问题都可以通过多项式时间算法归约成NPC问题，并且所有的NPC之间都有多项式时间算法实现转化，因而只要找到一个NPC问题的多项式时间算法，也就等于找到了所有NP问题的多项式时间算法，于是也就证明了NP=P。

长时间以来，人们将寻找NPC类问题的多项式时间算法作为了解决P=NP问题的关键途径。一些典型的NPC问题（见图1所示）已经被数学家明是NPC问题。例如合取范式满足问题3-CNF-SAT、子集和问题SUBSET-SUM、旅行商问题TSP、哈密顿回路问题HAM-CYCLE等都是NPC问题寻找多项式时间解法的研究热门问题。但时至今日，除去本人新近研究出来的k-CNF-SAT多项式时间算法之外，未见到任何NPC问题的多项式时间复杂度的算法出现。

2.              子句消去计数法分组定解算法的形成

本人发明的子句消去计数法分组定解的算法，源自本人设计的子句消去计数法。子句消去计数法适合于制作确定n个变量与k阶子句的合取范式求解的运算器。由于运算器的逻辑电路是并行执行方式，因而求解的速度可达几十纳秒之间完成。

子句消去计数法求解需要设立可能解名称计数器。一般n个变量则需要有2ⁿ个以逻辑变量x和x’排序形成的字为名称的计数器。在消去子句的过程中，要看子句所含变量表示包含在哪个计数器名称中，则该计数器加1。计数器的初值都为0，消去全部子句后，若某计数器的值仍然为0，则说明计数器的名称取反得到n元变量值是k-CNF-SAT的解。

我进一步研究发现，事实上求解的过程并不需要具体的计数，而是只要知道那些值为0的计数器名称，可以对其表示可能解的名称取反，就可以得到全部解。因而在运算器设计上，完全取消了计数器，而专用以可能解命名的标志寄存器就达到了求解的要求。

图1  典型的NPC问题

尽管子句消去计数法能够实现硬件并行瞬间求解，但在软件编程来看，n个逻辑变量的合取范式可能解有2ⁿ个。在子句消去的过程中，需要通过子句的变量确定那些不为0的可能解标志。如果采用逐一访问可能解标志的方式，必然是一个指数时间复杂度的算法。如何有效地减少对2ⁿ个可能解标志的访问，就是突破k-CNF-SAT问题多项式时间算法的关键。

3.              子句消去计数法求解的算法

要能够理解子句消去计数法分组定解的算法，必须先弄清楚什么是子句消去计数法。

3.1         一些规定

一个逻辑多项式如果存在一项的值是1，那么这个逻辑多项式的值一定就是1。同样，一个逻辑项的存在为0的因子，那么这个逻辑项的值一定是0。逻辑变量非的值，一定是逻辑变量值的反码。逻辑运算的这些基本规律是子句消去法计数法成立的基础。

为了用计算机表示方便，我们这里用“+”表示或运算，用“’”表示非运算，将子句用括号括起，并将与运算符号省略。逻辑变量x和x’我们经常会用1和0分别表示，这叫值化。为了方便，在不引起混淆的情况下，我们会不区别x与1，x’与0。

由于k阶合取范式满足k-CNF-SAT的子句中包含变量x与x’同在的情况，这样的子句的逻辑值永远是1。我们将这样的子句称为恒一子句。显然，恒一子句的存在与不存在并不影响合取范式满足k-CNF-SAT的满足解，因而下面的讨论中，都会将恒一子句去除。

3.2         子句消去计数法

用子句消去计数法求解k-CNF-SAT问题算法如下：

（0）设立n元单侧计数器：x1’x2’x3’…xn-1’xn’[],x1’x2’x3’…xn-1’xn[],…, x1x2x3…xn-1xn []，共计2ⁿ个。计数器后面的方括号内放k个变量都在其中的子句数。计数器初值为0。

（1）去掉值为1的恒一子句，则n元k-CNF的子句最多剩有个。从前到后消去每个子句，并将k个变量都在某计数器名称中的计数器加1。

（2）全部子句消去后，寻找计数器为0的计数器名称，以其每个变量表示的反码取值，得到的每一个n位二进制数就是这个k-CNF-SAT的全部解。

若没有计数器值为0，则表示此k-CNF-SAT无解。

例1，f(x₁,..., x₆)= (x₁+x₁'+x₂')(x₂+x₃+x₄)(x₁'+x₃'+x₄')(x₁'+x₂+x₅')(x₂+x₃+x₆)(x₁+x₅+x₆')，求满足

f(x₁,..., x₆)=1的解。

（0）设计数器x₁’x₂’x₃’…x₅’x₆’[],x₁’x₂’x₃’…x₅’x₆ [],…, x₁x₂x₃…x₅x₆ []，共计64个。

（1）去掉恒一子句(x₁+x₁'+x₂')，剩(x₂+x₃+x₄)(x₁'+x₃'+x₄')(x₁'+x₂+x₅')(x₂+x₃+x₆)(x₁+x₅+x₆')

（2）消去剩下合取范式的第一子句，使含x₂x₃x₄标识的计数器都加1；

（3）消去第二子句，使含x₁'x₃'x₄'标识的计数器都加1；

（4）往下继续操作5次，则所有的子句都被消去，计数器计数完成。

（5）令为0计数器的变量取反码值即得解。例如，计数器x₁’x₂’x₃ x₄’x₅’x₆ [0]，于是得f(x₁,..., x₆)值为1的解有：（110110）。

（6）一次性可以写出所有解。如果互为反码标识的计数器都为0，则对应逻辑变量组合双方都是解。

验证：

对于所得解可以带入原式验证。例如将x₁=1、x₂=1、x₃=0、x₄=1、x₅=1、x₆=0带入原式得：f(1,1,0,1,1, 0)=1。

4.              子句消去计数法的概念与性质

为什么子句消去计数法就能够求出k-CNF=1的解？它的证明就在下面的概念和方法中。

定义1：如果子句中同时有逻辑变量和其反表示，则称子句为恒一子句。

显然，恒一子句的值总是1，与逻辑变量的取值无关。

定义2：所有包含变量x的非恒一子句叫x相关子句。

定义3：我们将n对互反变量表示只取变量或变量非，得到的k个变量子句组合，叫一侧。

例如，3个变量只取x₁’、x₂、x₃’，形成的2阶子句一侧为x₁’+x₂、 x₁’+x₃’、 x₂+x₃’。而x₁’+x₂’、 x₁’+x₃’、 x₂’+x₃’是x₁’、x₂’、x₃’形成的一侧。如此不难知道，n个逻辑变量构成的一侧共有2ⁿ个。

子句消去计数法的计数器就是为了记录一侧含有的子句数量而设计的。

定理1：n个变量合取范式k-CNF中一侧相关子句数最多为组合数。

证明：因为一侧只有n个变量的惟一表示，从中取出k个形成子句，即为从n个元素中取出k个的组合数。

此定理可以用来检查给定的合取范式是否不正确。如果给出的合取范式的一侧相关子句超过这个数，则可判定合取范式有错误。

定义4：将合取范式子句中一个变量的表示（x或x’）值定为1的子句全部消去求解的方法，称为子句消去法。

显然，子句消去法经过n次消去，若没有剩余子句，则k-CNF是可满足的，反之不满足。

定理2：非恒一子句全体，消去x相关子句中，一定不含有其反变量x’一侧子句。

证明：因为非恒一子句x与x’是不同时出现在一个子句，所以消去x相关子句，x’相关子句依然存在。

定义5：包含所有可能子句的合取范式k-CNF，叫完全合取范式。

完全定理：n个逻辑变量所成的k阶合取范式k-CNF，最多有个子句。非恒一子句最多有个。

证明：因为每个子句的元素可以是逻辑变量或它的非，这相当从2n个元素中取出k个的组合数，即为。而恒一子句最多有个，所以非恒一子句最多有个。

推论：完全合取范式的值恒为0。

因为完全合取范式包含x与x’的所有相关子句。所以用子句消去法无论经过怎样的n次消去子句，都不能使之没有剩余子句，而剩余子句的值是0，则合取范式的值是0。

可满足定理：若非恒一子句中互反变量有一侧相关子句不存在，则k-CNF-SAT可满足。

证明：因为x的相关子句全体包含一侧所有的n个变量或其非，如果其中一侧不存在，则可确定将这一侧相反一侧变量逐一消去，依据定理2可知最终将没有剩余子句。

可满足定理是我们进行k-CNF-SAT求解子句消去计数算法正确性的依据。实际上，n个变量的每个一侧子句的全体变量表示，刚好是一个n位二进制数，将这个n位二进制数用变量名表示，就是一侧相关子句数量计数器的名称。当消去一个子句的时候，就要看该子句属于哪一侧，从而使对应的计数器加1。

子句消去计数法关键就是记录一侧相关子句的数量，如果一侧子句数量为0，说明这一侧的相关子句在合取范式中都不存在，而将计数器名称相反一侧变量的子句一一消去，则不会再有剩余子句了。这种子句消去计数法可能会最终有若干个计数器值为0，那么k-CNF-SAT就会有若干组解。如果没有计数器的值为0，说明k-CNF-SAT无解。

由于子句消去计数法求k-CNF-SAT的解问题，转化成了一侧计数器是否为0 的问题，因此在设备设计上将计数器换成了与计数器名称一样的可能解标志寄存器，通过可能解标志为0来确定k-CNF-SAT的满足解。

5.              子句消去计数法分组定解算法

设n个逻辑变量的k阶合取范式子句的数量为m，则去掉恒一子句之后，m的变化范围应有1≤m≤。从这一点来看，决定子句消去计数法算法动作的次数是m的可能变化范围，因而消去子句的过程是一个与n有关的多项式时间。但因为每消去一个子句，都要到2ⁿ个可能解标志中去查找子句所在的一侧，故而这一过程是与n有关的指数型时间算法。可见要使k-CNF-SAT在多项式时间内求出解，则需要设法使查询可能解标志的过程变为多项式时间的算法。

5.1         可能解标志分组设想

合取范式k-CNF-SAT的全部可能解就在2ⁿ个与n位二进制数一一对应的集合之中。这n位二进制数的每一位，不是0，就是1，只要将每个位置都放上0和1各一遍，那么这2ⁿ个与n位二进制数就表达出来了。另一方面，当我们把子句的变量与可能解标志核对时，只要看变量对应的位置的0或1，而无需观查其他位置的数码是0还是1。这样我们就可以用*号来代表0和1，使查询的可能解标志一下子从2ⁿ个转化到只查询几个（最多是2^k个）就能够将那些可能解标志应该为1的全部找到。正是这一创新的可能解标志用*分组的方法，解决了对以往2ⁿ个可能解标志访问的指数时间，使该过程变成了多项式时间算法。

创新的要点是n个逻辑变量所有可能解标志可以用n个“*”表示（*本身表示0或1）。这样一来，最初的可能解标识我们就用*_n*_n-1*_n-2…*₂*₁这一个字来表示（这里的下标只是说明位置，计算中不写）。我们在消去子句的过程中，会将这个可能解标志进行分裂分组，并去掉那些为1的标志组，从而在多项式时间内求出合取范式k-CNF-SAT满足的所有解。

5.2         基本设计思想

根据子句消去计数法，消去一个非恒一子句，合取范式可能解标志集中，消去子句的变量位置至少会有一个是其反码表示的可能解标识留下。例如，消去子句x3+x5+x7’，那么最初全是*表示10个变量的3-CNF的可能解标志组就分裂成了7个分组，其中*表示是0或1。这个剩余的可能解标志分组用集合B记录。

B=｛***0*0*0**，***0*0*1**，***0*1*0**， ***1*0*0**，***1*0*1**，***1*1*0**，***1*1*1**｝。而从**********中分裂出来的***1*1*0**分组，其可能解标志都变成了1，因而就全部消去了。

若再有子句x3’+x5’+x7，则恰有***1*0*0**被消去。则

B=｛***0*0*0**，***0*0*1**，***0*1*0**， ***1*0*1**，***1*1*0**，***1*1*1**｝

若有变量落在*的位置，则因*即可是0，亦可是1，所以可将本组分解。

例如，若再消去x3’+x5’+x10知从上次剩余标标志组B中知，该子句的标识落在***0*0*0**组中，被消去的为1**0*0*0**，将其消去，应剩0**0*0*0**。于是可能解变为：B=｛0**0*0*0**，***0*0*1**，***0*1*0**， ***1*0*1**，***1*1*0**，***1*1*1**｝；

若再有子句x3’+x7+x10’，但因该子句在标志组***1*1*0**中，则剩余

B=｛0**0*0*0**，***0*0*1**，***0*1*0**， ***1*0*1**，1**1*1*0**，***1*1*1**｝；

如此继续，直至全部子句消去。当全部的子句消去之后，从剩下的用0、1和*表示的可能解标志取反（*位既取0，又取1），这样就可以得到合取范式全部解！

5.3         子句消去计数法分组定解算法

子句消去计数法分组定解算法如下：

（0）输入k阶合取范式，并将同变量的子句尽可能放到一起；

（1）设立一个n位字，每位都是“*”的可能解标志集B；

（2）从头开始，逐一消去子句，恒一子句直接消去，若是非恒一子句，则依子句变量表达形式的采用拆分标志组，去掉相应标志组包含该子句的部分（若子句变量值正好与B的对应位相同，那么消去该组，不然从存在标志组中分裂组中将其消去），获得剩余可能解标志组集合B；

（3）重复（2），直至无子句或全部可能解标志组都被消去；

（4）若B标志完全被消去，说明此合取范式无满足解，不然各可能解标识的0、1位分别取反码，*位分别选择0或1，得到的n位二进制数都是原合取范式的解。

为了能够具体了解子句消去计数法分组定解算法，我们用例子加以解释。

5.4         子句消去计数法分组定解算法例题

例题：5个逻辑变量的3阶合取范式

F=(x1’+x1+x3’)(x1’+x2’+x3’)(x2’+x3+x4)(x3+x4’+x5)(x1+x2+x3)(x2’+x4’+x5’) (x3’+x4’+x5’),

求满足F=1的解。

解：令B=｛*****｝，因(x1’+x1+x3’)是恒一子句，直接消去。

消去(x1’+x2’+x3’)，则分裂后剩余

B=｛**001，**010，**011，**100，**101，**110，**111｝；

再消去(x2’+x3+x4)，则因其标志在**100、**101中，消去*110*，剩，*0100，*0101，于是

B=｛**001，**010，**011，*0100，*0101，**110，**111｝；

再消去(x3+x4’+x5)，则因其标志在*0100、*0101、**110和**111中，则从消去101**，剩00100、00101、00110、01110、11110、00111、01111、11111，于是

B=｛**001，**010，**011，00100，00101，00110，01110，11110，00111，01111，11111｝；

再消去(x1+x2+x3)，则因其标志在00111，01111，11111中，消去无剩余，得

B=｛**001，**010，**011，00100，00101，00110，01110，11110｝；

再消去(x2’+x4’+x5’)，则消去00100和00101，得

B=｛**001，**010，**011，00110，01110，11110｝；

然后在标志**001的分裂组中，消去标志00001，剩余01001、10001、11001，则得

B=｛01001、10001、11001，**010，**011，00110，01110，11110｝；

再消去(x3’+x4’+x5’)，则在**010和**011分裂组中消去00010和00011，得

      B=｛01001、10001、11001，01010，10010，11010，01011，10011，11011，00110，01110，11110｝；  

根据标志取反得解方法，得此合取范式共有12个向量解，分别是B’＝｛10110，01110，00110，10101， 01101，00101，10100，01100，00100，11001，10001，00001｝。

5.5         K-CNF-SAT多项式时间复杂度的证明

子句消去计数法分组定解的算法的简捷之处，在于依据子句的构成，简化成一次性直接去访问那些有关的可能解标志，而不用对那些无关的可能解标志逐一进行访问。这样做的结果，将对可能解标志的查找就会从2ⁿ个转化为对m组子句数据的多项式时间查找。

5.5.1   子句分块

从我编写的3SAT求解程序执行的过程中，使我感到将相同变量的子句组成块进行计算，速度会格外地快。因而我们下面就以同名变量子句分块，来加一讨论子句消去计数法分组定解的算法的多项式时间复杂度。

由于k个变量表示子句组成的块，子句数不会超过2^k个，而且如果出现2^k个k-CNF的子句块，则该合取范式一定无解。例如3SAT的一个块中如果有子句x_i’x_j’x_s’、x_ix_j’x_s’、x_i’x_jx_s’、x_ix_jx_s’、x_i’x_j’x_s、 x_ix_j’x_s、x_i’x_jx_s、x_ix_jx_s，则会出现所有的可能解标志都被消去，这就说明合取范式无解。

一个块中子句越多，剩下的子句可能解标志就越少，这样就可以减少后面消去子句时查找要消去标志的数量。根据这个原则，我们在输入时尽量将子句数多的块放到合取范式的前面，以便消去这个块的子句之后，产生更少的标志组。

对于k-CNF-SAT来说，究竟子句可以分成多少块，这要看它所含有的子句数量和变量的分布来决定。一般来说，非恒一子句数m要受到1≤m≤的限制，因而块的数量会是一个确定的自然数。

5.5.2   可能解标志组分段

在子句消去计数法分组定解的算法中，为了方便子句所在标志的查找，我们将n个变量组成的可能解原始标志组进行分段。如果是k阶合取范式，那么就将k个连续变量标号的标志组分为一段，最后不足k个标志的也单独成为一段。那么总能分出[n/k]个标志段。

我们把这种连续k个变量组成的可能解标志组段，叫标准段。

每个标准段可以表达2^k个可能解标志。一般用n个*刚好能代表2ⁿ个可能解标志，因为其每段代表2^k个标志，假如刚好有n/k个标准段，那么依据乘法原理，应共有 (2^k) ^n/k= 2ⁿ个可能解标志。

标志段内每一k位二进制数，我们都称为一个段值。各段段值的数量可以不同，那么所表达的可能解标志数量就是各段值数量的乘积。例如，有 3个标准段的段值数量分别是5、16、8，那么，所表示的可能解标志数为这些数之积，即640个可能解标志组。

依据标准段段值数量的这种关系，我们很容易写出每个可能解标志。假如n=10，k=3，且最后得到的各段值如下：

那么这4个段可能解标志有：

011 010 010 0

011 101 010 0

011 011 010 0

111 010 010 0

111 101 010 0

111 011 010 0

一般地说，t个标准段段值分别为u₁、u₂、u₃、...、u_t，那么可能解标志就共有

u1×u2×u3×...×ut个。

有了可能解标志组分段及段值，则可能解标志组就可以通过段值的形式表达，而无需一个个地将可能解标志单独写出来。

5.5.3   消去子句时段值的变化

可能解标志组按序分成标准段之后，最简单的情况是一个子句局限在一个标准段中，这样消去子句关联的段值，就在一个k元的标准段中查找就是了，实际查找的段值不会超过2^k-1个，连续消去子句会使段值数量不断减少。为了能够使后面的访问段值的数量尽可能地少，我们要将属于标准段的子句块都放到子句队列的最前面，这样既能够减少访问次数，又能够方便后续非标准段的访问。

实际上，除了属于标准段之外，一些子句的变量可能同时属于多到k个标准段的情况。如果子句变量属于一个标准段，除了子句块的第一个子句消去时要产生从*表示转到0、1表示的分裂之外，每消去一个k阶子句，只要从那2^k-1个段值中找到它的值表示，然后消去即可。但分散的变量子句最多可能要访问k个标准段，这时如果直接消去相应的数码0或1，那就不对了。这种情况也会产生从数值段到数值段的分裂。当然，如果有的段仍然是*表示的，那么按照*表示进行分裂就可以。但若是相对位都是数码表示的，那么产生分裂，计算起来会相对麻烦一些。

（1）对应*的标准段分裂

用*表示的标准段分裂最为简单。其实k个*就对应着k位二进制限位数。此时只要将第一个子句变量的数表示从中去掉，剩下的2^k-1个k位二进制数就是分裂的结果。

标志分段之后，如果继续消去属于这个标准段内的子句，那么就从该段值中将它们消去即可。

（2）多个标准段的处理

消去一个非标准段的子句时，可能子句包含的变量散落在多个标准段之中，这时也要产生分裂。这种分裂要比标准段的分裂复杂。

如果一个子句的变量需要查询多个标准段，除了全为*的标准段，都要转化成多个段共同位长的单一的数码表示的基本可能解标志，然后消去相应的那些包含子句变量表示的标志组。

这种一个子句最多也就能够占居k个标准段，因而形成最多的是一个k×k位的大段，但只因为要访问的是k个位置，根据子句的变量名称，经过k次判断就可以确定消去。这种占有多个标准段的子句我们要尽可能地放到后面消去，因为此时每个标准段的段值数都会很少，因而访问量也较少。为了最大限度地降低访问次数，我们将合取范式的变量紧凑子句放到前面去，越松散的子句越要放到后面后面，会减少许多访问的时间。

由于k-CNF的非恒一子句最多有，且因k个变量的子句数不能超过2^k-1个，否则无解，所以最大的段段值也不会超过(2^k-1)^k个。即使每个子句消去时都是访问这种最大的段，那么消去m个子句，访问的次数也不会超过m(2^k-1)^k个段值。

5.5.4   算法的多项式时间复杂度

子句消去计数法分组定解的算法是不是一个多项式时间复杂度的算法，事关NP-complete是不是P问题的大事。如果能够证明k-CNF-SAT可以有多项式时间算法，那么也就确定了NPC=P，进而能够得出P=NP的结论。

从前面介绍的子句消去计数法分组定解的算法，我们已经得出了确定k-CNF-SAT的满足解最多需要m(2^k-1)^k个段值访问。由于在k-CNF中阶数k是一个常数，而子句数m是个变量，所以可以认为m(2^k-1)^k分组定解的过程就是一个O(m)的多项式时间复杂度算法。如果非要牵扯到变量个数n对m的约束，那么也会得出与n有关的最多子句消去计数法分组定解的多项式时间计算公式(2^k-1)^k()。这个计算公式(2^k-1)^k是个常数，是个k次方多项式，因而可以说明子句消去计数法分组定解算法的时间复杂度是O(n^k)。

6.              结论与感受

    我研究P/NP问题前后只有一年的时间。在这一年的时间里，我探讨了程序执行时间的算法。为了能够按照所谓传统的“算法多项式时间复杂度”去寻找多项式时间解决NPC一类问题，我先后重点研究了子集和问题和k-CNF-SAT可解问题。

子集和问题采用的是先建所有子集，后查找和的方法，虽然可以求解，但在程序执行的总体时间上尚未摆脱2ⁿ次操作。按照传统的对多项式时间的认识，应该承认还未找到多项式时间算法。

之后我又重点研究了k-CNF-SAT可解问题。在这个问题中我逐渐有了突破。

第一、先提出了看似极为简单的子句消去法，实际上这是一种变相的验证解的方法。

第二、进一步探求研究，找到了k-CNF-SAT的子句消去计数法，该方法运用可能解标志记数，得到了“只要某可能解标志为0，那么其n位序名称取反，即可以一次性得到k-CNF-SAT的全部解。该方法的可能解标志仍然具有2ⁿ个，如果不采取特殊的查询标志方法，仍然摆脱不了所谓的与n有关的指数时间约束。

第三、经过再深入细致地研究，发现了子句消去计数法分组定解算法，可以依据对可能解标志分组实现多项式时间求出k-CNF-SAT全部解的算法，从而真正解决了NPC一族的关键性的k-CNF-SAT问题的多项式时间复杂度算法。其中证明这是一个多项式时间的算法，花费了巨大的心思。

由于NPC一类难题都可以规约到k-CNF-SAT问题求解。因此，本人发明的子句消去计数法分组定解的算法理论和实际意义不言而喻。

给一个求解3SAT的程序，供下载体会子句消去计数法分组定解的解法。本软件尚未做多项式时间更高效处理。提供给朋友目的是让有兴趣的朋友先试试求解的可能性。还会修改成更高效的多项式时间算法。

3SAT.rar

特别声明：本算法是我个人独创，如有引用请注明出处。

（证明多项式时间复杂度的部分较前进行了修改）。

2015-08-13

此方法过于复杂，请看简单的：http://blog.sciencenet.cn/blog-340399-928224.html