k-LSAT (k≥3)是NP-完全的

合取范式(conjunctive normal form,简称CNF)公式F是线性公式,如果F中任意两个不同子句至多有一个公共变元.如果F中的任意两个不同子句恰好含有一个公共变元,则称F是严格线性的.所有的严格线性公式均是可满足的,而对于线性公式类LCNF,对应的判定问题LSAT仍然是NP-完全的.LCNF_≥k是子句长度大于或等于k的CNF公式子类,判定问题LSA(≥k)的NP-完全性与LCNF(≥k)中是否含有不可满足公式密切相关.即LSAT_≥k的NP-完全性取决于LCNF_≥k是否含有不可满足公式.S.Porschen等人用超图和拉丁方的方法构造了LCNF_≥3和LCNF_≥4中的不可满足公式,并提出公开问题:对于k≥5,LCNF_≥k是否含有不可满足公式?将极小不可满足公式应用于公式的归约,引入了一个简单的一般构造方法.证明了对于k≥3,k-LCNF含有不可满足公式,从而证明了一个更强的结果:对于k≥3,k-LSAT是NP-完全的.     

极小不可满足公式在多项式归约中的应用

合取范式(CNF)公式F是极小不可满足的,如果F不可满足,并且从F中删去任意一个子句后得到的公式可满足,(r,s)-CNF是限制CNF公式中每个子句恰有r个不同的文字,且每个变元出现的次数不超过s次的公式类,对应的满足性问题(r,s)-SAT指实例公式限制于(r,s)-CNF.对于正整数r≥3,有一个临界函数f(r),使得(r,f(r))-CNF中的公式都是可满足的,而(r,f(r)+1)-SAT却是NP-完全的.函数f是否可计算是一个开问题,除了知道f(3)=3,f(4)=4外,只能估计f(r)的界.描述了极小不可满足公式在CNF公式类之间转换中的作用.为使转换过程中引入较少的新变元,给出了CNF公式到3-CNF公式的一种新的转换方法,对于长度为l(＞3)的子句,仅需引入|l/2|个新变元.并且,给出了CNF到(r,s)-CNF公式转换以及(r,s)-CNF中不可满足公式构造的原理和方法.     

MAX(1)和MARG(1)中公式改名的复杂性

改名是一个将变元映射到变元本身或它的补的函数,变元改名是公式变元集合上的一个置换,文字改名是一个改名和一个变元改名的组合.研究CNF公式的改名有助于改进DPLL算法.考虑判定问题"对于给定的CNF公式H和F是否存在一个变元(或文字)改名ψ使得ψ(H)=F?"的计算复杂性.MAX(1)和MARG(1)是极小不可满足公式的两个子类,这两个子类中的公式可以用树表示.树同构的判定问题在线性时间内是可解的.证明了对于MAX(1)和MARG(1)中的公式,文字改名问题在线性时间内可解,变元改名问题在平方次时间内可解.     

一个正则NP-完全问题及其不可近似性

通过一个适当的归约变换,可以将一个CNF (conjunctive normal form)公式变换为另一个具有某种特殊结构或性质的公式,使两者具有相同的可满足性.带有正则结构的CNF公式的因子图在图论中具有某些良好的性质和结果,可以用于研究公式的可满足性和计算复杂性.极小不可满足公式具有一个临界特征,公式本身不可满足,从原始公式中删去任意一个子句后得到的公式可满足.借助此临界特性,给出了一个从3-CNF公式到正则(3,4)-CNF公式的多项式归约转换.这里,正则(3,4)-CNF公式是指公式中每个子句的长度恰为3,每个变元出现的次数恰为4.因此,正则(3,4)-SAT问题是一个NP-完全问题,并且MAX(3,4)-SAT是不可近似问题.     

MAX(1)和MARG(1)中公式改名的复杂性

改名是一个将变元映射到变元本身或它的补的函数,变元改名是公式变元集合上的一个置换,文字改名是一个改名和一个变元改名的组合.研究CNF公式的改名有助于改进DPLL算法.考虑判定问题"对于给定的CNF公式H和F是否存在一个变元(或文字)改名ψ使得ψ(H)=F?"的计算复杂性.MAX(1)和MARG(1)是极小不可满足公式的两个子类,这两个子类中的公式可以用树表示.树同构的判定问题在线性时间内是可解的.证明了对于MAX(1)和MARG(1)中的公式,文字改名问题在线性时间内可解,变元改名问题在平方次时间内可解.     

基于聚类和划分的SAT分治判定

提出了一种将布尔公式划分为子句组来进行布尔可满足性判定的方法.CNF(conjunctive normal form)公式是可满足的当且仅当划分产生的每个子句组都是可满足的,因此,通过判定子句组的可满足性来判定原公式的可满足性,相当于用分治法将复杂问题分解为多个子问题来求解.这种分治判定方法一方面降低了原公式的可满足性判定复杂度;另一方面,由于子句组的判定可以并行,因而判定速度能够得到进一步的提高.对于不能直接产生布尔子句组划分的情形,提出了一种利用聚类技术将CNF公式聚类成多个簇,然后消去簇间的公共变量来产生子句组划分的方法.     

MAX-k-SAT的PTAS归约等价性

通过构造适当的极小不可满足公式,利用子句拼接技术,引入了一个一般化的从k-CNF公式(k≥3)到3-CNF公式之间的归约转换。基于该转换,给出了一个真值指派的转换算法,并证明了MAX-k-SAT与MAX-3-SAT是PTAS归约等价的。因此,对于k,t≥3,MAX-k-SAT与MAX-t-SAT是PTAS归约等价的。     

不可满足公式的同态证明系统

合取范式(CNF)公式H到F的同态φ是一个从H的文字集合到F的文字集合的映射,并保持补运算和子句映到子句.同态映射保持一个公式的不可满足性.一个公式是极小不可满足的是指该公式本身不可满足,而且从中删去任意一个子句后得到的公式可满足.MU(1)是子句数与变元数的差等于1的极小不可满足公式类.一个三元组(H,φ,F)称为的一个来自H的同态证明,如果φ是一个从H到F的同态.利用基础矩阵的方法证明了:一个不可满足公式F的树消解证明,可以在多项式时间内转换成一个来自MU(1)中公式的同态证明.从而,由MU(1)中的公式构成的同态证明系统是完备的,并且由MU(1)中的公式构成的同态证明系统与树消解证明系统之间是多项式等价的.     

d-正则(k,s)-SAT问题的NP完全性

研究具有正则结构的SAT问题是否是NP完全问题,具有重要的理论价值.(k,s)-CNF公式类和正则(k,s)-CNF公式类已被证明存在一个临界函数f(k),使得当s≤f(k)时,所有实例都可满足;当s≥f(k)+1时,对应的SAT问题是NP完全问题.研究具有更强正则约束的d-正则(k,s)-SAT问题,其要求实例中每个变元的正负出现次数之差不超过给定的自然数d.通过设计一种多项式时间的归约方法,证明d-正则(k,s)-SAT问题存在一个临界函数f(k,d),使得当s≤f(k,d)时,所有实例都可满足;当s≥f(k,d)+1时,d-正则(k,s)-SAT问题是NP完全问题.这种多项式时间的归约变换方法通过添加新的变元和新的子句,可以更改公式的子句约束密度,并约束每个变元正负出现次数的差值.这进一步说明,只用子句约束密度不足以刻画CNF公式结构的特点,对临界函数f(k,d)的研究有助于在更强正则约束条件下构造难解实例.     

基于因子图求解(3,4=)-CNF公式类下可满足问题

合取范式(CNF)公式F是(3,4=)-CNF公式,如果F中每个子句的长度是3,每个变元出现的次数恰好为4次.与(3,4=)-CNF公式所关联的因子图是一类规则的二部图,即每个子句结点的度为3,每个变元结点的度为4,此类规则图被称为(3,4)-双向正则二部图.对于一个(3,4=)-CNF公式F,如果它关联的因子图GF有P7路径因子,则F可满足.     

多文字可满足SAT问题的相变点上界

可满足(SAT)问题是指：是否存在一组布尔变元赋值,使得随机合取范式(CNF)公式中每个子句至少有1个文字为真。多文字可满足SAT问题是指：是否存在一组布尔变元赋值,使得随机CNF公式中每个子句至少有2个文字为真。此问题仍然是一个NP难问题。定义约束密度α为CNF公式子句数与变元数之比,对该问题的相变点上界α^*进行了研究。如果α>α^*,则多文字可满足SAT问题高概率不可满足。通过一阶矩一个简单的推断,可以证明α^*=-ln 2/ln(1-(k+1)/2^k),当k=3时,α^*=1。利用Kirousis等人的局部最大值技术,提升了多文字可满足3-SAT问题的相变点上界α^*=0.7193。最后,选择了大量数据进行实验验证,结果表明,理论结果与实验结果相吻合。     

用于求解正则(3,4)-SAT实例集的修正警示传播算法

利用极小不可满足公式的临界特性,可以将任意的一个3-CNF公式多项式时间归约转换为一个正则(3,4)-CNF公式,从而得到一个保留NP完全性的正则(3,4)-SAT问题。警示传播算法(Warning Propagation,WP)在归约转换后的正则(3,4)-SAT实例集上高概率收敛,但在任意一个实例上都无法判断公式的可满足性,因此算法求解失效。对于一个归约转换后的正则(3,4)-CNF公式,每一变元出现的正负次数之差具有趋于稳定的结构特征,基于该特征,提出基于变元正负出现次数规则的WP算法来求解归约转换后的正则(3,4)-SAT实例。实验结果表明,修正的WP算法对正则公式的可满足性判定有效,从而可以利用公式的正则性特征进一步研究WP算法的收敛性特征条件。     

基于图分解的(3,4)-CNF公式的可满足性

对于规则的(3,4)-CNF公式F,公式F对应的因子图GF恰好是一个(3,4)-双向正则二部图.利用正则二部图的有关性质,证明了对于任意的(3,4)-CNF公式F,若其对应的因子图GF能够被划分为两个(3,2)-双向正则二部图,则F是可满足的.     

一阶子句搜索方法

子句集的可满足性判定是自动证明领域的热点之一.提出了子句搜索方法判定命题子句集Φ的可满足性,该方法查找Φ中子句的一个公共不可扩展子句C,当且仅当找到C时Φ可满足,此时C中各文字的补构成一个模型.结合部分实例化方法将子句搜索方法提升至一阶.一阶子句搜索方法可以判定子句集的M可满足性,具备终止性、正确性和完备性,是一种判定子句集可满足性的有效方法.     

求解多文字可满足SAT问题的置信传播算法

可满足(SAT)问题是指:是否存在一组布尔变元赋值,使得合取范式公式中每个子句至少有一个文字为真.多文字可满足SAT问题是指:是否存在一组布尔变元赋值,使得CNF公式中每个子句至少有两个文字为真.显然,此问题仍然是一个NP难问题.为了研究解决多文字可满足SAT问题的算法,引入随机实例产生模型,设计求解多文字可满足SAT问题的置信传播算法.最后,用实例模型产生了大量数据进行实验验证,结果表明:该算法求解多文字可满足SAT问题的性能优于其他启发式算法.     

SLS算法求解平衡正则(k,2r)-CNF公式

可满足性问题的求解算法和结构性质研究是计算机科学中重要问题之一，为寻求某些CNF公式子类问题有效算法或算法改进途径，对公式的结构加以某些限制，其中限定子句长度为恒定常数和变元出现次数是常见的处理方式。研究具有正则结构且每个变元正负出现均衡的结构化公式的可满足性问题求解，其随机生成模型的构建及随机实验测试有助于观察解分布状况。并且，随机局部搜索算法在求解具有一定规则结构CNF公式实例中具有良好效率。本文集中研究平衡正则(k, 2r)-CNF公式的求解问题，即限制每个子句的长度为k，每个变元出现的次数为偶数2r,并且每个变元正负出现的次数在相等情况下的可满足性问题求解。给出BR(n,  k, 2r)模型，以此模型来生成具有特殊结构的平衡正则(k, 2r)-CNF公式实例，利用随机局部搜索算法求解问题。通过限制初始指派的0文字和1文字各占一半且均匀生成，以WalkSAT算法和NSAT算法做实验对比，发现对于平衡正则(k, 2r)-CNF公式，实例具有明显效率。     

正则(3,4)-CNF公式的社区结构

通过构造适当的极小不可满足公式以实现在多项式时间内将3-CNF公式归约转换为一个正则(3,4)-CNF公式,转换后的公式与原公式具有相同的可满足性,同时公式的结构也发生相应的变化。图的社区结构反映了图的模块特性,文中将CNF公式转化为相应的图,研究公式图的模块特性与公式某些性质之间的关系。将归约前后的两类公式转换为相应的图并研究其模块特性,发现转换后得到的正则(3,4)-CNF公式具有较高的模块度。此外,在使用DPLL(Davis Putnam Logemann Loveland)算法求解CNF公式的过程中,发生冲突时利用冲突驱动子句学习策略,得到一个学习子句并将其添加到原公式中,使得原公式的模块度降低。研究发现:将DPLL算法与冲突驱动子句学习策略结合应用到正则(3,4)-CNF公式时,其学习子句所包含的绝大部分变元位于不同的社区中。     

图的树分解算法及其应用

一个图G=(V,E)的树分解是将结点集V的子集作为树T的节点,使得在T上任意一条路径上的两个端节点的交集包含于该路径上的任意一个节点中。将T上最小(节点)对应子集的元素个数减1定义为分解树T的宽度,用宽度最小的分解树T的树宽度定义图G的树宽度。一个合取范式(Conjunctive Normal Form,CNF)公式F可以用一个二分图G=(V∪C,E)表示(公式的因子图),其中变元结点集V对应公式F中的变元集,子句结点集C对应公式F中的子句集,变元在子句中的正(负)出现用实(虚)边表示。忽略公式因子图中边上的符号,得到一个二分图。文中研究了图的树分解算法,并将树分解算法应用到CNF公式的因子图树分解。通过实验观察公式因子图的树宽度与求解难度之间的联系。     

关于部分K值逻辑Sheffer函数(Ⅲ)

1.引言 在多值逻辑结构理论中,Sheffer函数的判定与构造是其中的一个重要的组成部分.它分别包括完全、部分多值逻辑Sheffer函数的结构与判定,其判定问题与函数系完备性之判定密切相关,并可归结为定出完全与部分多值逻辑中极大封闭集的最小覆盖.对于完全多值逻辑函数集中的Sheffer函数,其判定与构造问题已经完全解决.对于部分多值逻辑函数集中的Sheffer函数,文[2,3]对于k一3,4定出了P*k的极大封闭集的最小覆盖;在文[4～6]中,证明了极大封闭集(即准完备集)保E函数集TE、L型函数集TG4.2、拟线性函数集Lp在P*k的极大封闭集之最小覆盖中必须出现;文[7,8]证明了m一2时,满足一定条件的完满对称函数集在最小覆盖中必须出现;文[9,10]证明了m=2时,满足一定条件的完满对称函数集在最小覆盖中必须出现,并证明了另几类完满对称函数集和正则可离函数集不是最小覆盖的成员.     

一类可分离SAT问题的O(1.890n)精确算法

布尔可满足性问题（SAT）是指对于给定的布尔公式,是否存在一个可满足的真值指派.这是第1个被证明的NP完全问题,一般认为不存在多项式时间算法,除非P=NP.学者们大都研究了子句长度不超过k的SAT问题（k-SAT）,从全局搜索到局部搜索,给出了大量的相对有效算法,包括随机算法和确定算法.目前,最好算法的时间复杂度不超过O（（2-2/k）ⁿ）,当k=3时,最好算法时间复杂度为O（1.308ⁿ）.而对于更一般的与子句长度k无关的SAT问题,很少有文献涉及.引入了一类可分离SAT问题,即3-正则可分离可满足性问题（3-RSSAT）,证明了3-RSSAT是NP完全问题,给出了一般SAT问题3-正则可分离性的O（1.890ⁿ）判定算法.然后,利用矩阵相乘算法的研究成果,给出了3-RSSAT问题的O（1.890ⁿ）精确算法,该算法与子句长度无关.