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

博文

子句消去法如何破解P与NP难题

已有 4126 次阅读 2016-3-9 10:47 |个人分类:P/NP问题|系统分类:科研笔记| 子句消去法

子句消去法如何破解PNP难题

姜咏江

子句消去法是能够在多项式时间求出SAT问题满足解的一种算法。也就是说斯提芬.库克理论认定的NP-complete问题之3-SAT问题,实际是可以在多项式时间求出解的P类问题。依据NP-complete问题的定义,就可以得出P=NP。我以前写出的子句消去法博文,分成了若干篇,比较松散。本文将系统详细一些介绍子用句消去法快速求3-SAT满足解的原理和方法。

1.             引言

在百度查找P/NP问题,在头条你就会见到下面的话:

P/NP问题是在理论信息学中计算复杂度理论领域里至今没有解决的问题,它被克雷数学研究所Clay Mathematics Institute, 简称CMI)在千禧年大奖难题中收录。 P/NP问题中包含了复杂度类PNP的关系。1971年史提芬·古克(Stephen A.Cook) Leonid Levin 相对独立的提出了下面的问题,即是否两个复杂度类PNP是恒等的(P=NP?)。

所谓P/NP问题的定义是这样给出的:

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

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

1971年斯提芬.库克 (Stephen A. Cook) 发表了论文〈The Complexity of Theorem Proving Procedures[2]〉,他把P之外的问题归结为三大类,即 NPNP-complete NP-hard。所谓归约,就是用一种快速的多项式时间算法,能将A问题变成B问题,且B问题的解就包含A问题的解,则称A归约到B。库克的分类得到了学术界的认可。库克的PNPNPCNPH等类问题的定义如下:

P问题——可以在多项式时间内求出解的问题(Polynomialproblem)。

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

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

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

由以上NPC问题的定义,我们不难想到,只要我们能够找到一个NPC问题的多项式时间求解算法,就可以肯定所有的NP问题都有多项式时间算法,于是也就证明了NP=P

据维基百科介绍,只要能够证明NP类问题包含在P类问题当中,那么象密码学、集成电路设计、运筹学、生命科学和生物技术、数学、计算机科学等都会产生巨大的变革。由此可见PNP问题解决的重大意义。

 

2.             典型的NPC问题

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

 

 

1  典型NPC问题及相关

Fig. 1   NPC Problems

本文先给出3-CNF-SAT满足解的多项式时间复杂度的算法,其中包括一些相关的概念和定理。然后只要将3换成k,就可以得到3-CNF-SAT的解法。进而推广到具有任意子句的SAT满足解的多项式时间复杂度的算法。

3.             3-SAT定义

在诸多的NPC问题中,一般认为最简单直观的是只含有3个逻辑变量逻辑表达式的合取范式3-CNF。多个由3个逻辑变量及其非组成多项式,这些多项式之间又在进行与运算,这样形成的表达式,就是所谓的3-CNF。其中或运算的多项式称为子句,子句的逻辑项(一个变量或者它的非运算形式)又被国外称为文字。

例如,(x1’+ x1+ x3’)(x1’+x2’+ x3’)(x3’+x4+ x5’)(x2’+x4’+ x5)就是一个3-CNF,每一个括号内的多项式就是一个子句,带“”的变量是这个变量的非运算形式组成的项。子句的项是由变量本身,或者变量的非运算形式构成。3-CNF可以用数学语言描述。

将逻辑变量x的非运算用x’表示,集合A=x1,x2,...,xn, A’=x1’,x2,...,xn},3-CNF定义如下:

3-CNF=


其中m是子句的数量,xijAA’.

3-CNF=1解的问题一般就叫3-SAT问题。

如果一个变量和它的非运算形式都在同一个子句当中,根据逻辑运算的知识,这个子句的值一定是1,不影响3-CNF=1的求解。

定义1:子句中包含同一变量及其非表达形式,称该子句为恒一子句。

很明显,研究3-SAT问题可以排除恒一子句,因为不论如何,恒一子句的值总是1,使3-CNF=1的解完全由其它变量的值来确定。本文中一般情况下不考虑恒一子句的存在。

4.             二进制限位数

3-SAT问题中的变量本身用1来表示,将变量自身的非运算用0表示,这样就可以用二进制限位数知识进行分析求解。这里简单介绍一下相关内容。

确定位数的用数码表示的数叫限位数。

限位数的无效0不能够省略。例如,十进制限3位数为000,001,...,999共有103=1000个。限位数的个数总数很有用。3-SAT的子句可以用二进制数码01来表示,因而使用的是二进制限位数。3位二进制限位数共有23=8个(k位有2k个)。它们是000,001,010,011,100,101,110,111。限位数全体我们称其为完全数集,将完全数集的数竖起来排列,可以发现一些有用的性质。

000

001

010

011

100

101

110

111

性质1:二进制完全数集相同位置的01各占一半。

性质2:二进制完全数集对应位数码不同的数成对。

01在此是互为反码。将一个限位数的数码都用其反码替换,得到的数叫原数的反码。

性质3:在二进制完全数集中的一个数,除其反码之外的那些数,至少有一对应位置与该数的数码相同。

性质4:完全数集一位数码相同的限位数,其余位置的数码组成降位的完全数集。

上面的性质可以从完全数集直接得到。例如性质4,最高位是01时,3位二进制数都有低两位得到是2位数的完全数集。

研究SAT问题可以将限位数的数码反方向排列,这不影响上面提到的限位数性质。例如排列成下面的形式,并不影响我们在SAT问题中的分析。

x1  x2  x3

0  0   0

1  0   0

0  1   0

1  1   0

0  0   1

1   0   1

0  1   1

1  1   1

性质5:二进制非完全数集总能够找到一个限位数,使数集中的数都有一位,与该数对应位的数码相同。

容易看到,性质5是性质3的另一种说法。

5.             子句消去法

所谓求3-SAT的满足解,就是求3-CNF=1的解。3-SAT的每个逻辑与运算因子都是一个逻辑3项式。由逻辑代数知识可知,逻辑多项式的任何一项值为1,则多项式的值就为1。这样,当某个子句的值为1的时候,就可以由3-SAT的其它子句的变量值来确定整个3-SAT的解。由此,我们得到了一种简单求出3-SAT满足解的方法。

定义2:按照一定规则设定子句中逻辑项值为1,并消去该项值为1的所有子句的方法,称为子句消去法。

一个n元逻辑变量的3-SAT,如果我们能够逐一设定每个变量的值,并能够将3-SAT的子句全部消去,这说明每个子句的值都是1,从而就可以知道,所设定的n元变量的一组值就是3-SAT的满足解。

例1,求3-CNF=(x1’+ x1+ x3’)(x1’+x2’+ x3’)(x3’+x4+ x5’)(x2’+x4’+ x5)=1的解。

:由于(x1’+ x1+ x3’)是恒一子句,所以求解中可以不予考虑,仅考虑(x1’+ x2’+ x3’)(x3’+x4+ x5’)(x2’+x4’+ x5)=1的解就可以。我们可以设定x1 =0,这样子句(x1’+ x2’+ x3’)的值就是1。同样设定x2 =0x3 =0,就可以使子句(x3’+ x4+ x5’)(x2’+ x4’+ x5)的值都为1。我们再设定x4 =1x5 =1,那么就得到x1x2 x3 x4 x5=00011,这就是本例3-SAT的一组满足解。

3-CNF=1常常具有多解。例如上式只令x2 =0x3=0就可以使3-CNF=1成立,此时x1, x4, x5的取值可以任意为01。也就是说,当x2 =0x3=0时会有8个满足解。

上面这个例子的解是用子句消去法求出来的吗?是。由于第一个子句是恒一子句,因而求解中可以将其直接消去。从后面的3个子句来看,设定x2=0x3=0,那么每个子句的值都是1,因而子句都能够消去,这样就得到了3-CNF=1的满足解。容易理解,在某些变量的值没有设定的情况下,子句就被消除干净,说明没有设定值的那些变量值可以任意,它们每组任意的值都会与已取值的那些变量值组成不同的解。这是3-SAT有多解的原因。

3-SAT中并不是所有的子句设定变量值后都可以消去,也就是说并不是3-SAT都有满足解。例如包含变量x1x2 x3的全部形如(x1’+ x2+ x3’)(x1+ x2’+ x3) 子句对构成的3-CNF=1,就无论如何找不到满足解。

3-SAT有没有满足解的根本原因涉及到反子句的概念。

定义3:将子句中的项用非运算表示得到的子句叫原子句的反子句。

依据定义,(x1’+ x2+ x3’)(x1+ x2’+ x3) 就是一对反子句。

   由于互为反子句具有逻辑值相反的特点,对3个变量的互反子句总体来说,不论如何设置变量的值,总有互反子句一个子句的值是1,另一个子句的值是0。这样的互为反子句做与运算的结果一定是0。因而,由全部互为反子句组成的3-SAT一定没有满足解。

定理1:对n元变量的3-SAT施行子句消去法,若无剩余子句,则有满足解,不然无解。

此定理由子句消去法,立即得证。

6.             3-CNF的表形式

3-CNF中的变量用逻辑运算符连接起来,形成的是逻辑表达式。用逻辑表达式直接求解3-SAT的满足解不容易。子句消去法将3-CNF组织成表格形式,然后依据二进制限位数理论可以获得求解3-SAT满足解的一些独特规则,使没有规律的设定变量的值,变成有规律的求解方法。

6.1        3-CNF的表格式

将逻辑变量x1表示,x’0表示,建立的3-CNF表格式如表1所示。子句以3位二进制数的形式占表中一行,为了方便观查变量值对子句的影响,规定变量相同的子句行都要相邻放置。

表中对应每个逻辑变量的01,我们称之为变量的之间表示值,而把求解中要设定的逻辑变量值叫做变量的解值。用01表示子句非常方便子句消去法设定变量的解值,即只要将变量的表示值设定为解值,那么所有含有相同项的子句都可以消去。

我们可以在表头的上方设置一个空行,在求解的时侯将变量的解值写在此行中,这样方便观查求解。

1  3-CNF表格式

x1

x2

x3

x4

x5

x6

x7

x8

x9

x10

x11

x12

x13

x14

x15

x16

1

 

 

 

 

 

 

 

 

 

 

 

 

 

0

1

0

 

 

 

 

 

 

 

 

 

 

 

 

 

1

1

0

0

0

 

 

 

 

 

 

 

 

 

 

 

 

 

1

0

0

 

 

 

 

 

 

 

 

 

 

 

 

 

0

1

0

 

 

 

 

 

 

 

 

 

 

 

 

 

1

1

0

 

 

 

 

 

 

 

 

 

 

 

 

 

0

1

1

 

 

 

 

 

 

 

 

 

 

 

 

 

 

 

1

 

 

 

0

 

 

 

0

 

 

 

 

 

 

 

0

 

 

 

1

 

 

 

0

 

 

 

 

 

 

 

 

0

0

0

 

 

 

 

 

 

 

 

 

 

 

 

 

1

0

0

 

 

 

 

 

 

 

 

 

 

 

 

 

0

1

0

 

 

 

 

 

 

 

 

 

 

 

 

 

1

1

0

 

 

 

 

 

 

 

 

 

 

 

 

 

0

0

1

 

 

 

 

 

 

 

 

 

 

 

 

 

1

0

1

 

 

 

 

 

 

 

 

 

 

 

 

 

0

1

1

 

 

 

 

 

 

 

 

 

 

 

 

 

 

 

 

0

1

 

0

 

 

 

 

 

 

 

 

 

 

 

 

1

0

 

1

 

 

 

 

 

 

 

 

 

 

 

 

 

1

0

0

 

 

 

 

 

 

 

 

 

 

 

 

 

1

1

1

 

 

 

 

 

 

 

 

 

 

 

 

 

 

 

 

 

1

1

1

 

 

3-CNF的子句是由3个变量的表示构成的,不难看出,将具有相同变量的子句放到一起研究,能够显示出SAT的限位数特性,方便找出解题的特有规律。

6.2        子句块

逻辑变量x还是它的非运算形式x,在合取范式中是不同的项,但它们都直接涉及同一变量的取值,为此,称xx是同一个变量。在这种概念之下,我们给出子句块和关联段的概念。

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

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

例如,表1x4x5 x67组值形成的7个子句组成了一个子句块。x4x5 x6000是这个子句块的块解。另外x1x2 x3形成的有5个子句的子句块,块解有x1x2 x3=000x1x2 x3=010x1x2 x3=110

定义6:如果一个子句块所有可能出现的子句都存在,则称之为完全子句块。

01表示的完全子句块就是一个二进制完全数集。因此,k-CNF完全子句块的子句数量为2k个。

6.3        关联段

子句块之间可能有部分共同的变量,也可能没有共同的变量。有共同变量的子句块之间求解会相互影响。

定义7:由相同变量联接的子句块组称为关联段,否则称为独立段。

一个子句块和全体的子句块之间没有共同的变量,它就是独立段。独立段是关联段的特例。表1中有底色的5个子句块是相互关联的,形成了关联段。而另外有2个子句块不与其它子句块相互关联,成为了独立段。

为了区分子句块间的关联程度,我们引进关联度的概念。

定义8:如果子句块间有m个共同变量,则称子句块间的关联度为m

研究中发现3-SAT的满足解和关联段有直接关系,为此我们引进段解的概念。

定义9:能使关联段中所有子句值为1的段中那些变量值,称为段解。

由于关联段将具有相同变量的子句块都集中在了一起,所以关联段不会重合。因此,n元变量的3-CNF关联段不会超过[n/3]个。很明显,关联段间是相互独立的,因而求3-CNF=1的解可以分开来求每个关联段的解,然后将段解进行组合,就可以得到最终的结果。

7.             子句消去法相关定理

为了能够运用子句消去法对合取范式快速地求解,我们以整数k1时的k-CNF=1这种更一般的情况来论述那些有用的性质。

7.1        k-CNF子句块性质

依据二进制限位数理论,可以归纳出k-CNF子句块的一些性质。

定理2:子句块中若有互反子句存在,则表达它们的二值都不是块解。

证明:依据子句消去法,当以有反子句存在的子句表示值来设定子句块的解,那么该子句的反子句不可能消去,则知互反子句表示值都不是块解。

推论1k-CNF中子句的反子句表示值不是块解。

定理3k-CNF子句块解不超过2k-1个。

证明:根据定理2及推论1,容易理解子句块包含的子句越多,这个子句块的解就越少。k个变量组成的子句最多有2k个,若子句块只有一个子句时,除了其反子句之外,每个可能在这个子句块中的子句都会至少有一位数码与这个子句的对应位数码相同。根据子句消去法,这2k-1个子句表示值都是这个只有一个子句的子句块解。

例如,表1的子句块x12x13 x14只有一个子句111,该子句块有解:100010110001101011111。即有23-1个解。

推论2:有m个无反子句组成的子句块有2k-m个块解(m2k-1)。

例如,表1的子句块x1x15 x162个子句,其反子句都未出现,则有6个解:000110001101011111

推论3:有m1个无反子句和m2对有反子句的子句块m1+2m22k-1),有2k-(m1+2m2)个解。

例如,表1的子句块x1x2 x35个子句,其中有一对互反子句,则块解数为23-3-2=3,即有解:000010110

推论4:若 k-CNF子句块中有2k个子句存在,则该子句块无解。

证明:因为此时块中每个子句都存在反子句。依据子句消去法知无块解。

定理4k-CNF子句块中若有一个变量有2k-1个相同的值,那么这个值一定组成块解。

证明:因为若一个变量有2k-1个相同的值,依据二进制限位数性质4,那么其余k-1位数必组成2k-1k-1阶完全子句块,依据推论4,该k-1阶子句块一定无解。于是只有选定那个变量2k-1个相同的值的值,这些子句才可以消去,即该值一定是块解的组成部分。

例如,表1的子句块x4x5 x67个子句,x640值,若选x6=1,则必然不会得到这个子句块的解。选择x6=0,在剩余的子句块中,不考虑x6的表示值,再运用此定理,选x5=0x4=0,则得到子句块x4x5 x6的解。

定理5:从一个子句块出发确定的k-CNF=1解,也可以从另一子句块出发确定这个解。

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

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

定理6n个变量的k-CNF子句块最多有Cnk

证明:显然k阶子句的变量是从n个变量中取出k个构成的集合,每个变量取值01就构成了子句块。依据排列组合知识,知定理6成立。

由完全子句块定义可知,不包括恒一子句的合取范式k-CNF最多有2kCnk个子句。

定理7:子句块或关联段无解,则k-CNF=1无解。

证明:因为子句块解与关联段解都是k-CNF=1解的组成部分,其无解,3-CNF=1自然无解。

定理8k-CNF=1的求解可以分别对各关联段求解。

证明:由3-CNF的表格式可知关联段是不重合的,并且将各关联段的解按照变量顺序组合就是3-CNF=1的解,所以可以分开求解。

定义10:子句消去过程中关联段剩余子句块间由相同变量构成,则称这些子句块为动态块,消去此动态块的变量值叫动态块解。

例如,2x1x2 x3子句块和x2 x3 x4子句块已经选择了x1=0和x4=1,各自剩下了3个子句没有消去,子句块x2 x3就是动态子句块。

动态块本质上是降阶的子句块,因而只要不出现完全子句块,就可以找到块解。

2  3-CNF动态子句块

x1=0

x2

x3

x4=1

1

0

0

0

1

1

0

0

1

0

1

0

 

定理9:动态块无解,则关联段无解。

证明:因为动态块变量是关联段解的组成部分,所以动态块无解,其所在关联段就无解。

定理10:确定了一些变量值后得到的动态块无解,则此次段选值不是段解。

证明:依据推论4,如果动态子句块的变量所有可能值形成的子句都存在,那么动态块则无解,因而前面选择的那些变量值不会成为关联段的解。

k-SAT的满足解,将子句块看成特殊的动态块,那么最重要的是避开动态块无解。K-CNF=1无解来自于出现了1阶、2阶、...k-1阶、k阶完全子句块。因而,求解中避开出现降阶的完全子句块是用子句消去法求解的最根本方法。

7.2        3-SAT求解

本节以3-SAT实例来介绍子句消去法求解。

例1,      (x1’+ x2’ + x3’)(x1+ x2’+ x3’) (x1’+ x2 + x3’) (x1+ x2+ x3’)(x1’+ x2’ + x3)

(x1’+ x4’+ x6’) (x1+ x4’+ x6’) (x1’+ x4 + x6’) (x1’+ x2 + x4) (x2+ x4’+ x6) (x2+ x4+ x6)(x3’+ x4’ + x5’)(x3+ x4’+ x5’) (x3’+ x4 + x5’) (x3+ x4+ x5’) (x3’+ x4’+ x5) (x3’+ x5 + x6) (x4’+ x5’+ x6’) (x4+ x5’+ x6’) (x4’+ x5 + x6’) (x4+ x5+ x6’) (x5’+ x6’+ x8’) (x5+ x6 + x8’)(x5+ x6’+ x8) (x6+ x8’+ x11) (x6’+ x8’+ x11) (x7’+ x8 + x9) (x8+ x9+ x10’)=1的解。

3是例1的表格形式,用子句消去法求解如下:

3  1的二进制数码表示

 

 

 

 

 

 

 

 

 

 

 

x1

x2

x3

x4

x5

x6

x7

x8

x9

x10

x11

0

0

0

 

 

 

 

 

 

 

 

1

0

0

 

 

 

 

 

 

 

 

0

1

0

 

 

 

 

 

 

 

 

1

1

0

 

 

 

 

 

 

 

 

0

0

1

 

 

 

 

 

 

 

 

0

 

 

0

 

0

 

 

 

 

 

1

 

 

0

 

0

 

 

 

 

 

0

 

 

0

 

1

 

 

 

 

 

0

1

 

1

 

 

 

 

 

 

 

 

1

 

0

 

1

 

 

 

 

 

 

1

 

1

 

1

 

 

 

 

 

 

 

0

0

0

 

 

 

 

 

 

 

 

1

0

0

 

 

 

 

 

 

 

 

0

1

0

 

 

 

 

 

 

 

 

1

1

0

 

 

 

 

 

 

 

 

0

0

1

 

 

 

 

 

 

 

 

0

 

1

1

 

 

 

 

 

 

 

 

0

0

0

 

 

 

 

 

 

 

 

1

0

0

 

 

 

 

 

 

 

 

0

1

0

 

 

 

 

 

 

 

 

1

1

0

 

 

 

 

 

 

 

 

 

0

0

 

0

 

 

 

 

 

 

 

1

1

 

0

 

 

 

 

 

 

 

1

0

 

1

 

 

 

 

 

 

 

 

1

 

0

 

 

1

 

 

 

 

 

0

 

1

 

 

1

 

 

 

 

 

 

0

1

1

 

 

 

 

 

 

 

 

 

1

1

0

 

1)依据定理5,令x3=0, x5=0, x6=0,并消去相关子句,得到4

2)子句块x5x6x8已确定2个变量的值,因而该子句块已经降到了一阶,所以必设x8=0。消去相关子句,得到5

35的所有子句块都有多解,可选x1=0, x2=1, x9=1消去全部子句。最终得到这个3-SAT的满足解(见6)。

需要说明,用子句消去法可以一次性求出3-SAT的多个满足解,6那些没有定值的变量可以任意选择01,这就是一次可以求出多个满足解的原因。本次共求出了8个有11个分量的向量满足解,不知读者是否认可?

4  设定变量必选值

 

 

0

 

0

0

 

 

 

 

 

x1

x2

x3

x4

x5

x6

x7

x8

x9

x10

x11

0

0

1

 

 

 

 

 

 

 

 

0

 

 

0

 

1

 

 

 

 

 

0

1

 

1

 

 

 

 

 

 

 

 

1

 

0

 

1

 

 

 

 

 

 

1

 

1

 

1

 

 

 

 

 

 

 

 

 

1

1

 

0

 

 

 

 

 

 

 

 

1

 

0

 

 

1

 

 

 

 

 

 

0

1

1

 

 

 

 

 

 

 

 

 

1

1

0

 

 

5  得到多解关联段

 

 

0

 

0

0

 

0

 

 

 

x1

x2

x3

x4

x5

x6

x7

x8

x9

x10

x11

0

0

1

 

 

 

 

 

 

 

 

0

 

 

0

 

1

 

 

 

 

 

0

1

 

1

 

 

 

 

 

 

 

 

1

 

0

 

1

 

 

 

 

 

 

1

 

1

 

1

 

 

 

 

 

 

 

 

 

 

 

0

1

1

 

 

 

 

 

 

 

 

 

1

1

0

 

 

6  最终解

0

1

0

 

0

0

 

0

1

 

 

x1

x2

x3

x4

x5

x6

x7

x8

x9

x10

x11

由此例我们容易理解,求3-SAT满足解不必使用猜测验证的方法就可以完成,这是因为3-CNF自身有特殊的结构。用表的方式可以明显地展示出3-CNF的结构规律,从而使我们能够依据这些规律快速地求出3-SAT的一些解。

7.3        k-SAT的降阶求解

从前节解题的例子我们能够看到,求没有k阶完全子句块的SAT满足解,可以用子句消去法逐步降阶,最终获得k-SAT的满足解。

在一个逻辑变量的值被设定之后,消去相应子句,原子句块中这个变量表示值不是解值的那些子句会剩余下来。再继续求解时,这个变量已经成了常量。因而k-CNF经过子句消去法设定了一个变量值之后,就变成了(k-1)-CNF。如果这个k-1阶合取范式不存在完全子句块,那么就可以继续求解。

在相互关联的子句块存在的情况下,除去已经设定了值的变量,会出现其余部分表示重复的情况。我们可以去掉重复部分来观查是否有降阶的完全子句块。如果没有,就可以继续用子句消去法求解。

23-SAT7所示,求满足解。

7  2

 

 

 

 

 

x1

x2

x3

x4

x5

0

0

0

 

 

0

0

1

 

 

1

1

0

 

 

1

1

1

 

 

 

1

0

1

 

 

1

0

0

 

 

1

1

0

 

 

1

1

1

 

 

0

0

 

0

 

1

0

 

0

:不难看出,如果x1取值1,不论x4取值0还是1,降阶的x2 x3都会出现2阶动态完全子句块,这样就得不到这个3-SAT的满足解。为此,我们选择x1取值0,避免了出现动态完全子句块,最终可以得到满足解。

8.             总结

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

2)由于子句消去法是回避无解的完全子句块出现的方法,因而只要关联段有解,就可以一次性求出。求出3-CNF=1的解的过程只需要n次设定变量的解值,子句消去法求3-CNF=1的解是一个O(n)时间复杂度的算法。

33-CNF=1求解的降阶计算方法,完全可以推广到k-CNF=1。不仅如此,子句消去法完全适合对任意的SAT求满足解。因为无论有几阶的子句存在,只要子句的值为1,就可以消去。只要避开完全子句块,最终就可以求出SAT的满足解。

 

2016-03-08

 

 


 

 



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

上一篇:150个顶点的图求哈密顿回路要若干年吗?
下一篇:科学网的博客为什么老是丢图?
收藏 IP: 120.52.24.*| 热度|

1 邱嘉文

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

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

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

GMT+8, 2024-11-23 06:16

Powered by ScienceNet.cn

Copyright © 2007- 中国科学报社

返回顶部