首页 | 本学科首页   官方微博 | 高级检索  
检索     
共有20条相似文献,以下是第1-20项 搜索用时 359 毫秒

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

2.  MAX^+公式的结构特征  
   姚雷博  董红政  郭超  张伟民  段晓明《计算机与数字工程》,2010年第38卷第9期
   改名是一个将变元映射到变元本身或它的补的函数,变元改名是公式变元集合上的一个置换,文字改名是一个改名和一个变元改名的组合。改名技术在简化一些难例公式的消解证明和构造高效的可满足算法方面有重要意义。MAX^+公式是MU公式中的一个重要子类,该类公式可以通过递归的方式产生。通过分析MAX^+公式的结构,得到了一些关于此类公式的结构特点,对进一步研究这类公式的改名问题有较大意义。    

3.  极小不可满足公式在多项式归约中的应用  被引次数:8
   许道云《软件学报》,2006年第17卷第5期
   合取范式(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中不可满足公式构造的原理和方法.    

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

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

6.  k-LSAT(k≥3)是NP-完全的(英文)  被引次数:1
   许道云  邓天炎  张庆顺《软件学报》,2008年第19卷第3期
   合取范式(conjunctive normal form,简称CNF)公式F是线性公式,如果F中任意两个不同子句至多有一个公共变元.如果F中的任意两个不同子句恰好含有一个公共变元,则称F是严格线性的.所有的严格线性公式均是可满足的,而对于线性公式类LCNF,对应的判定问题LSAT仍然是NP-完全的.LCNF≥k是子句长度大于或等于k的CNF公式子类,判定问题LSAT≥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-完全的.    

7.  MAX^+(1)和MAX^+(2)公式的分裂特征  
   姚雷博  布挺  董红政  段晓明《计算机与数字工程》,2010年第38卷第11期
   改名技术在简化一些难例公式的消解证明和构造高效的可满足算法方面有重要意义。MAX^+公式是MU公式中的一个重要子类,该类公式可以通过递归的方式产生。为研究MAX^+公式改名问题的复杂性,对MAX^+(1)和MAX^+(2)公式的分裂问题进行了分析,得到了一些关于这两类公式的若干分裂特征,对进一步研究MAX+公式的改名问题有较大的现实意义。    

8.  求解SAT问题的线性半定规划算法  
   李厚银  许道云  万武族《计算机与数字工程》,2009年第37卷第11期
   将线性半定规划应用到SAT问题的求解过程中。首先将SAT实例转化为整数规划问题,然后松弛为线性规划模型,最后再转化为一般的线性半定规划模型去求解。用SDPA-M软件求解线性半定规划问题后,规定了如何根据目标函数值去判定SAT实例和当CNF公式可满足时如何根据最优指派的概率X^*i(i=1,…,n)去进行变元赋值,以期求得该公式的可满足指派。上述算法不仅可以判定SAT问题,而且对于符合算法规定可满足的CNF公式皆可给出一个可满足指派。求解SAT问题的线性半定规划算法在文章中被描述并被给予相应算例。    

9.  基于因子图求解(3,4=)-CNF公式类下可满足问题  
   聂国霞  秦永彬  许道云《计算机与数字工程》,2013年第41卷第5期
   合取范式(CNF)公式F是(3,4=)-CNF公式,如果F中每个子句的长度是3,每个变元出现的次数恰好为4次.与(3,4=)-CNF公式所关联的因子图是一类规则的二部图,即每个子句结点的度为3,每个变元结点的度为4,此类规则图被称为(3,4)-双向正则二部图.对于一个(3,4=)-CNF公式F,如果它关联的因子图GF有P7路径因子,则F可满足.    

10.  k-LSAT (k≥3)是NP-完全的  被引次数:1
   许道云  邓天炎  张庆顺《软件学报》,2008年第19卷第3期
   合取范式(conjunctive normal form,简称CNF)公式F是线性公式,如果F中任意两个不同子句至多有一个公共变元.如果F中的任意两个不同子句恰好含有一个公共变元,则称F是严格线性的.所有的严格线性公式均是可满足的,而对于线性公式类LCNF,对应的判定问题LSAT仍然是NP-完全的.LCNFk是子句长度大于或等于k的CNF公式子类,判定问题LSA(≥k)的NP-完全性与LCNF(≥k)中是否含有不可满足公式密切相关.即LSATk的NP-完全性取决于LCNFk是否含有不可满足公式.S.Porschen等人用超图和拉丁方的方法构造了LCNF3和LCNF4中的不可满足公式,并提出公开问题:对于k≥5,LCNFk是否含有不可满足公式?将极小不可满足公式应用于公式的归约,引入了一个简单的一般构造方法.证明了对于k≥3,k-LCNF含有不可满足公式,从而证明了一个更强的结果:对于k≥3,k-LSAT是NP-完全的.    

11.  多区间上非线性程序的终止性判定  
   牟琳  李轶  李玲娜  刘栋《四川大学学报(工程科学版)》,2011年第43卷第3期
   主要解决了如下形式的程序的终止性判定的问题:while(x∈Ω)do{x:=(f)(x)}end,其中,x为程序变元,Ω(Ω=(a1,b1‖∪‖a2,b2‖∪…∪‖an,bn),其中,‖∈{(,),[,]},n ∈ N*)是间段并集(f)是一个多项式函数.证明了:当ψ(b1)ψ(a2)>0,…,ψ(bn-1)ψ(an)>0(其中,ψ(x)=(f)(x)-x)时,这类区间上的非线性程序不终止的必要条件是:在Ω内部或者边界上存在不动点.如果不动点仅仅在Ω内部,则上述结果是充要条件.通过添加一定的约束条件,对于仅区间边界有不动点的情况,也给出了判定的方法.对一类多项式函数的终止性给出了完备性的算法(TNPSI).    

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

13.  关于线性微分多项式的值分布  
   杨力《西安工业学院学报》,2000年第20卷第1期
   下述定理得到证明 :设 f是一超越亚纯函数 ,ψ[f]是 f的一个k阶线性微分多项式 .如果微分方程 (ψ[ω])′ =0的亚纯解ω均为 (ψ[f])′的小函数 ,则对任意正数ε及任意 q(q≥ 2 )个判别有穷复数bj(j =1,2 ,… ,q) ,恒有(q - 1) (1- 1kq q- 1)T(r ,ψ[f]) < qj =1N(r ,1ψ[f]-bj) εT(r ,ψ[f]) S(r ,ψ[f])且对一切有穷复数b ,有∑b≠∞δ(b ,ψ[f]) ≤ 12k 1 1上述结果是杨乐的两个定理的推广 .定理中的条件“(ψ[ω])′ =0的亚纯解ω均为 (ψ[f])′的小函数”是必要的 .    

14.  一种寻找极小不可满足子公式的方法  
   李立峰《西安邮电学院学报》,2009年第14卷第5期
   用F表示经典命题逻辑的合取范式(CNF)公式,Ci为F中的子句。公式F是极小不可满足的,如果F不可满足,并且从F中删去任意一个子句后得到的公式可满足。本文在经典命题逻辑中引入由F所诱导的形式背景,并基于此建立了概念格;给出了F不可满足公式的判定方法,当F为不可满足公式时,运用概念格的方法从F及其子句集的关系出发给出了F极小不相容子公式的判定定理。    

15.  MAX-k-SAT的PTAS归约等价性  
   许道云  秦永彬《计算机科学与探索》,2009年第3卷第6期
   通过构造适当的极小不可满足公式,利用子句拼接技术,引入了一个一般化的从k-CNF公式(k≥3)到3-CNF公式之间的归约转换。基于该转换,给出了一个真值指派的转换算法,并证明了MAX-k-SAT与MAX-3-SAT是PTAS归约等价的。因此,对于k,t≥3,MAX-k-SAT与MAX-t-SAT是PTAS归约等价的。    

16.  求解公式关键文字集的信息传播算法  
   王晓峰  许道云  秦永彬《山东大学学报(工学版)》,2011年第41卷第3期
   关键文字集影响判定布尔公式可满足性的判定难度。如果能找到公式的关键文字集或关键文字集的子集,就可使公式的可满足性判定变得容易。通过对警示传播算法的原理分析,发现高概率决定的部分变元对公式的求解难度有一定的影响。当某个子句与变元之间的警示信息具有一致性时,表明该子句的可满足性完全由该变元的取值决定,其它变元的取值都不能使得该子句可满足。进一步研究发现,当该算法收敛时,具有一致性的警示信息对应的变元集合是关键文字集的子集,这就佐证了警示传播算法可用于求解公式的关键文字集。基于该算法的特征,给出了一个寻找公式关键文字集的信息传播算法。    

17.  求解MAX-CNF问题的一种随机近似算法  
   李伟  曾文华《计算机工程与应用》,2006年第42卷第34期
   已有的Johnson算法是求解组合问题的一种随机近似算法,可以用于求解MAX-CNF问题。基于该算法,提出新的随机近似算法RCNF求解MAX-CNF问题。概率推导和实验数值均表明,RCNF具有良好的近似比和稳定的性能。在构成难可满足问题的CNF实例上,将新算法与演化算法结合,进一步提出扩展算法E-RCNF。扩展算法利用演化算法的并行性,可以在较短时间内,简单有效地求出最多可满足子句数的近似值。    

18.  正则3-SAT问题的相变现象  
   张明明  许道云《计算机科学》,2016年第43卷第4期
   通过对3-CNF公式加以限制,要求其中每个变元出现的次数相同,引出正则3-SAT问题。进一步,通过对两种子句产生机制形成的(3,s)-CNF公式进行可满足性观察,发现在规模较小的情况下,正则3-CNF公式比非正则3-CNF公式更容易满足。从而推测与非正则3-SAT问题相比,正则3-SAT问题的相变点有偏移现象。最后,从变元自由度的角度对这一现象给出了定性解释。    

19.  基于布尔可满足性的逻辑电路等价性验证方法  
   刘歆  熊有伦《微电子学与计算机》,2007年第24卷第11期
   提出了基于布尔可满足性(Boolean Satisfiability,SAT)的逻辑电路等价性验证方法。这一验证方法把每个电路抽象成一个有穷自动机(FSM),为两个待验证的电路构造积机,把等价性验证问题转换成了积机的断言判定问题。改进了Tseitin变换方法,并将其用于把电路约束问题变换成(Conjunctive Normal Form,CNF)公式。之后则用先进的CNF SAT求解器zChaff判定积机所生成的布尔公式的可满足性。事例电路验证说明了该方法的有效性。    

20.  消除子句冗余的算法及复杂性  
   任国珍 马绍汉《计算机研究与发展》,1996年第33卷第11期
   本文讨论了知识子句表示的冗余消除,着重讨论了子句中冗余文字的消除的民政部压缩是消除子句文字冗余的一种重要类型除对这种类型的问题的可判定性以及复杂性结果进行讨论外,本文还给出了压缩问题的一个子问题的多项式算法。    

设为首页 | 免责声明 | 关于勤云 | 加入收藏

Copyright©北京勤云科技发展有限公司  京ICP备09084417号