CMP设计分享 http://blog.sciencenet.cn/u/accsys 没有逆向思维就没有科技原创。 不自信是科技创新的大敌。

博文

3-SAT关联段子句消去法(详细解法)

已有 5467 次阅读 2015-10-4 06:54 |个人分类:科研论文|系统分类:论文交流| 3SAT, 分段子句消去法

3-SAT关联段子句消去法

姜咏江

摘要:本文给出了3-SAT分段消去子句的求解算法。证明了可以在多项式时间求出3-SAT的解。从而证实斯提芬.库克定义下的NP-complete问题就是一个P类问题。

关键词NP-completeP/NP问题,子句消去法

1.             引言

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

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

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

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

P问题,可以在多项式时间内求出解的问题,Polynomialproblem

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

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

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

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

2.             典型的NPC问题

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

本论文给出的是求3-CNF-SAT满足解的多项式时间复杂度的算法,还包括一些相关的概念和定理证明。这种算法只要将3换成k就可以得到k-CNF-SAT的解法。


1  典型NPC问题及相关

3.             子句消去的算法

子句消去法源自最简单的逻辑运算关系,即多个逻辑多项式之间的与运算结果为1,必须每一个多项式的值为1才行。3-SAT每个子句多项式有3个变量,只要其中一个变量表示是1,那么就可以将含有该变量表示的所有子句多项式消去,从而可以找到整个与运算表达式可能为1的那些解。一个个单独设置变量值,子句消去法不是一个多项式时间算法,但本文给出的分段子句消去法却有了惊人之处。

3.1        3-SAT的定义

所谓的3-SAT就是多个由3个逻辑变量或其非组成的多项式间形成与运算表达式。一般这种逻辑表达式被称为合取范式3-CNF

我们这里将逻辑或运算符用“+”表示,逻辑非运算符用“”表示,而将逻辑与运算符省略。将逻辑变量或其非表示组成的多项式叫“子句”。例如,

(x1’+x2’+x3’) (x1+x2’+x3’)(x1’+x2’+x4) (x3+x4’+x5)(x2’+x2+x3’)是一个3-CNF合取范式,我们要求出满足3-CNF=1的那些解,这个问题习惯上人们称之为3-SAT。表达式中每个括号之间是与运算的关系,每个括号内的多项式就是子句。

如果一个子句中包含一个变量和其非的项,那么显然该子句的值永远是1。我们称这样的子句是恒一子句

因为3元合取范式3-CNF=1中象(x2’+x2+x3’)这种恒一子句不影响求解,所以本文的3-CNF=1问题中不包括恒一子句,并用3-SAT 替代它。

3.2        子句消去法与规定

所谓的子句消去法,就是逐一设定变量的值,并将所有在变量值设定下值为1的子句消去,最终看是否剩余子句的算法。

例如,合取范式F=(x1’+x2’+x3’) (x1+x2’+x3’)(x1’+x2’+x4) (x3+x4’+x5)

我们令x1=0,x2=0,x3=1就可以将等式右面的全部子句消去(此处变量x4x5的值可以任意设置),那么就可以得到F=1的一组4个解:00100001100010100111

为了方便又不失一般性,我们给出子句变量的概念和去除未参与构成子句变量的规定。

定义1:不论是逻辑变量x还是其非x’在一个子句中,我们都称x是这个子句的变量,叫子句变量

规定,我们研究的3-SAT既不不含无关的变量,也不包括恒一子句。

4.             3-SAT格式表与反子句

采用子句消去法要建立3-SAT表格式(见图2),将子句以3位二进制数的形式写入表中。我们用0表示逻辑变量的非运算形式,用1表示逻辑变量本身,并称此种表示子句的二进制数为子句值例如,用000表示子句xi’+xj’+xk,而子句xi+xj’+xk则用100表示。子句左面的变量叫开始变量,右面的变量叫结束变量

4.1        合取范式的表格式

3-SAT的规范表格式如2所示。规定每个子句占用一行,并且要求变量相同的子句行相邻。


1  合取范式值格式

定义2:变量相同的子句放到一起叫子句块

23-SAT表中颜色相同的部分就是一个子句块。当然,单独的子句也自成一块。按照从编号1顺序划分有3个相邻变量的子句块叫标准块。其它3个变量组成的块叫非标准块。非标准块中不相邻变量组成的块叫分散块。变量取值与其它子句块变量无关的块,叫独立块

两子句块开始变量相同,叫同根;结束变量相同叫同尾;子句块的开始变量到结束变量之间有其它子句块,这叫跨越。

定义3:能够使子句块的子句全部消去的块中变量值叫块解

3-SAT一个子句块中子句值最多有8个,而块解最多只有7个。这一点下面会解释。

为了清晰起见,3-SAT表将选择确定的变量值放到表下面的对应位置。

4.2        反子句与关联段

两个数码之和为最大数码,一个就叫另一个的反码。二进制中数码01是互为反码。将一个数的数码都用其反码表示,叫原数的反码数,也简称反码。

定义4:子句块中子句值为反码的子句,一个叫另一个的反子句

3-SAT子句块的反子句最多有4对,用值表示分别是{000,111}{100,011}{010, 101}{110,001}。

子句消去法求3-SAT满足解的算法,要用到关联段的概念。

定义5:有相同变量的子句块称为关联块,通过关联块形成的子句块集合叫关联段。能使关联段中所有子句值为1的段中变量值,称为段解

3-SAT有一元关联、二元关联。

定义6:子句块间有一个共同变量的子句块叫一元关联。子句块间有2个共同变量的子句块叫二元关联3-SAT独立块间无变量关联。

定义6:在进行子句消去过程中由选择变量确定的子句形成的块叫动态块。能够使动态块子句消去的变量值叫动态块解

5.             相关定理与性质

为了说明子句消去法对k3合取范式k-CNF-SAT求解的有效性,我们以更一般的情况来论述本节内容。

子句消去法能够一次性求出k-CNF-SAT满足解基于如下的一些基本定理。

定理1:子句块中若有互反子句存在,则互反子句值都不是块解。

证明:依据子句消去法,以子句值消去的所有子句中不包括其反子句,因此总有一个子句值不能被消去。

推论1k-CNF-SAT子句块解不超过2k-1个。

推论2k-CNF-SAT子句块中已有子句的反子句值不是块解。

推论3:若 k-CNF-SAT中有2k个子句的子句块存在,则k-CNF-SAT无满足解。

定理2:从一个子句块出发确定的解,也可以从另一子句块出发确定这个解。

证明:假设由子句块A确定的解a不是由子句块B确定的解,那么因a中必含有B的一个子句值,于是可以从这个值出发,按照a的值扩充来求解,仍然是这个合取范式的一个解。于是可知,可以从A起始块或B做起始块得到相同的解。

由此定理可知,选择任何子句块做为起始块求解,效果一样。

推论4:从任意子句块出发都可能确定出合取范式的解。

定理3:关联段无解,则k-CNF-SAT无满足解。

证明:因为关联段解是k-CNF-SAT解的部分,其无解,k-CNF-SAT自然无解。

定理43-SAT有解的子句块确定了一个变量值,如剩下4个不同的值,则无段解。

证明:由表1可见,只要选值的两个变量值出现右侧的4个值,那么无论如何设值,都不能将其余子句消去。

1子句变量值表

块子句可能值

固定一个变量其它变量可取值

0

0

0

0

0

1

0

0

1

0

0

1

0

0

1

1

1

0

1

1

0

0

1

 

 

1

0

1

 

 

0

1

1

 

 

1

1

1

 

 

关联段性质:各关联段解相互独立。即一个关联段解改变,不影响其它段解。

因为关联段解不独立,则说明这是一个关联段。

 

推论5:动态块确定一个变量值后二剩余变量有3组值,则有惟一动态块解;两组或一组值,则有多个动态块解。

定理5:连续多值可选的关联段最终可确定段解。

证明:3-CNF求解中只有一个变量值确定的动态块可以产生多解。若设定关联变量值后的剩余动态块仍然有多值可设,则可连续查找关联动态块,直至无解、有惟一解或有关联段的结束动态块出现。如果最终出现动态块无解,则关联段无解。如果出现动态块有唯一解,可反方向设定关联变量值去确定前面每个多值动态块的解;如果多解情况最终关联的是未曾设定解的子句块,可以把子句块解设定,然后反方向去确定多解的动态子句块,最终会连成一个关联段,得到关联段的解或无解。

 6.             3-SAT分段求解方法

3-SAT的子句块有解,并且关联段有解,那么3-CNF=1才会有解。依据这一原理,我们先检查子句块是否都有解。如果子句块都有解,那么选择3-SAT的关联段,求出各关联段解,进而能够组合求出3-SAT的满足解。

6.1        关联段子句消去法

表格式3-CNF=1求解算法如下:

1)选择左侧子句块为起始块;判断有块解后选择一个块解,无块解3-CNF=1无解。

2)消去至少含有一个与这个块变量相同且值相同的所有子句。

3)向右寻找靠近的2个变量值已确定的动态块,设定最后一个变量值,将含有该变量且值相同的子句块消去;若设定01都不能够消去动态块全部子句,则知从起始块设定值开始得不到3-CNF=1的解,需要选择下一个起始块解进行从新操作;若起始块解都操作过并无解,则3-CNF=1无解。

4)若是只有1个变量值已确定的动态块,则需要同时确定2个变量的值。此时应依据定理4先判断有无解;无解,则需重复下一个起始块解。

5)通过(4)判定有解,并依靠推论4判断出有唯一解,则设定2个变量值,并消去所有相关子句。

6)如果通过(5)得出设定2个变量值多解的情况,依据定理5向后去确定关联段的解。

7)如果(6)的操作的关联段一端遇到无后续关联的子句块,并且关联段无跨越子句块,则该关联段结束,可以进入下一个关联段求解操作;如有跨越关联子句,需通过跨越子句向左右两个方向求段解。

8)依据子句消去法,若所有的关联段都有解,那么3-CNF=1就有解。其解为各关联段解的顺序组合。

由于3-CNF一个关联段最多有7个段解,所以3-CNF=1通过分段求解,如果每个关联段都有解,则可以配合出3-CNF=1的多组解。

6.2        子句消去法实例

我们以2的例子来说明子句消去法。

0)判断子句块中是否有子句数为8的,是, 3-SAT无解。

1)最左面的x1x2x3子句块为起始块,此块只有000100010三个块解。选择x1x2x3=010,消去有x1=0x2=1x3=0的所有子句(绿色部分是消去的子句)。



2  逐步消去子句块求解过程(1

2)向右,以子句块尾最靠左为原则,寻找剩余子句块。此例为块尾是x5的子句块。由于该块有x3=0,只有x4x5关联的动态块出现{001011},有唯一动态块解010,于是选x4x5=10消去相关子句。剩下以x6关联的动态块只需要设定x6=0就可以将该动态块消去,选择x6=0,并消去相关子句(见3)。



3  逐步消去子句块求解过程(2

3)剩余没有x7结尾的动态块,只二变量确定块尾为x8的动态块,设x8=0,消去x8=0相关子句后,遇到了需要设置x7x13=1001}多解的动态块解(见图4青色块)。


4  逐步消去子句块求解过程(3

4)在关联段中遇到动态块多值,为了避免选择关联段无解的分支,我们采用向下寻找唯一解的方法来保证关联块有解。此时暂不设置变量值,而是通过与其一元相关子句块连续寻找有唯一解的子句块。向上关联有x5x13x18子句块,向下有x6x13x21子句块和x13x14x16子句块。它们后续关联的都是需要三个变量设值的子句块。可以假定这些子句块是新的一个关联段,照顾到与前面关联关系,可设定子句块解,往回消去前面没有定解的动态块(见5青色所示)。



5  逐步消去子句块求解过程(4

5)由于x13x14x16子句块是无后续关联的,可以设定x13x14x16=001消去相关子句(见6)。



6  逐步消去子句块求解过程(5

6)动态子句块x7x8x13已有2个变量值被确定,必需设x7=1将其消去。然后将x11x12x14x9x10x11的子句块消去(见7



7  逐步消去子句块求解过程(6

7此时,x8x13x18动态块必需设x18=0。接续消去x18x19x20的子句块及关联子句块(图8)。


8  逐步消去子句块求解过程(7)

图8所示,至此就得到了这个3-CNF=1的一组解。

图8我们看到通过以上消去子句操作,已经没有了剩余子句。从表下面一行就得到了这个3-SAT的满足解。解的变量空白处,实际上是值为01两种情况,这表明实际上所求出的解是一组,解的数量应是2的空格数指数倍。本例求得的合取范式一组解包括23个解。

此例全部子句在一个关联段中,如果3-SAT含有多个独立的关联段,那么将段解组合在一起就是求得的3-SAT满足解。

如果想要求出3-SAT更多的解,必需将起始块解都考虑到,这样才能达到目的。

此例题其它两个起始块解都不能够形成段解,因而通过它们不可能有3-SAT的解。

6.3        关联段解处理讨论

3-SAT的满足解是由n个变量值组成的,其中任何一部分变量值不构成解的变量值,3-SAT就无解。这种局部特征是破解3-SAT难题的关键。依据定理4,只要3-SAT子句块都有解,那么一元关联段总可以判断出是否有解。二元关联段是否有解很容易判断。

判断一元确定的动态块有几个解,要看其余子句变量的状况。如果要确定的变量值为{000110}{110110110100110010之一,则有一个解;为{00011011}无解;而为{00}{11}{10}{01}{1001}{0011}之一,则有多个解。这种多解可以在一个变量值被确定的情况下,仍然可能选择另一个变量值将剩余子句块消去。

如果动态块有多个解,为了后续动态块不出现无解,可以依据动态块多解向后查找定解,然后反向确定动态块多解,不需要将所有的可能解都计算一遍,只要能够得到关联段解就达到了求3-SAT解的目的。

要求出更多解,需要将每个关联段的段解都求出来进行组合。下面例子是对一个关联段求解的过程。

8的起始段只有0001000103个块解,求解只要从这3个值出发就可以。81)出现二元判断无解的情况。82)出现一元判断无解的情况。83)才是有段解的情况。


9  有段解的判断

关联段结束在两个相互独立的子句块之间。

由于没有恒一子句的3-SAT子句数量不超过23Cn3个,并且相关子句越多,3-SAT的解越少。因而子句数量越接近23Cn3个,那么分段子句消去法的效率越高。每一个关联段就是一个3-SAT,因而3-SAT并不完全是一个全局性的问题。

 

7.             3-SAT分段子句消去法时间复杂度

3-CNF=1的解是由n个变量值组成的,如果其中任何一部分变量值不构成解的变量值,那么3-CNF=1就无解。

分段子句消去法,将3-CNF的子句分成了相互关联的段,并以段解来组成3-CNF=1的解。由于关联段是不重复的,所以3-CNF的关联段最多有[n/3]个,此时最多有一至两个子句块之间关联,其余子句块都是独立的。

由于3-CNF的每个关联段不会超过7次求段解操作得出段解,因而用分段子句消去法求出3-CNF=1的解或判定无解,最多需要进行7[n/3]次消去子句的过程。从这一点来说,用分段子句消去法求3-CNF=1的解是一个O(n)时间复杂度的算法。

其实,3-CNF=1是否有解,主要取决于子句数m和子句分配的结构,亦即子句之间关联的程度。3-CNF关联段子句越多,3-CNF=1的解就越少,反之解的数量会很多。当所有子句块只有一个子句并且都是独立块时,3-CNF=1会有最多的解。

8.             结论

3-SAT求满足解的分段子句消去法是一个多项式时间复杂度的算法。本算法证明了典型的NP-complete问题之一3-SAT是一个P类问题。依据学术界公认的观点,分段子句消去法可以说明P=NP

 

联系邮箱:accsys@126.com

              Accsysuibe@uibe.edu.cn

2015-09-19

 

备注:从Cn3个子句块中选块解,如同做除法试商。

 

修改于2015-10-04




https://blog.sciencenet.cn/blog-340399-925143.html

上一篇:一个简单的3-SAT求解例题
下一篇:中国人到国际期刊发表论文要比英语系国家的人困难
收藏 IP: 221.194.176.*| 热度|

0

该博文允许注册用户评论 请点击登录 评论 (2 个评论)

数据加载中...
扫一扫,分享此博文

Archiver|手机版|科学网 ( 京ICP备07017567号-12 )

GMT+8, 2024-4-23 17:35

Powered by ScienceNet.cn

Copyright © 2007- 中国科学报社

返回顶部