MAX<'+>(k)中公式改名的复杂性

来源 :贵州大学 | 被引量 : 0次 | 上传用户:wanxueguan55
下载到本地 , 更方便阅读
声明 : 本文档内容版权归属内容提供方 , 如果您对本文有版权争议 , 可与客服联系进行内容授权或下架
论文部分内容阅读
对于极小不可满足公式和它的子类的研究是近年来兴起的一个热门方向。我们对极小不可满足公式集感兴趣主要基于两方面的原因:一是大多数的消解难例公式都是极小不可满足的;二是对于极小不可满足公式的深入理解,有助于我们构造新的难例公式以及新的满足性算法。 一个CNF公式F称为极小不可满足的(MU),如果F是不可满足,并且在F中删去任意一个子句后所得到的公式是可满足的。一个MU中的公式F称为最大的,如果对于任意一个子句f∈F且对于任意一个文字L,(_)L,L(¢)f,将L添加到f中,公式F变为可满足的。最大的极小不可满足公式类记作MAX,MAX(k)=MU(k)∩MAX。公式F的一个改名是一个定义在var(F)上的函数(ψ),使得对每个变元x,(ψ)(x)∈{x,(_)x};公式F的一个变元改名是var(F)上的一个置换;公式F的一个文字改名是一个变元改名和一个改名的组合。可以看出以上这三种改名不改变公式的可满足性。 改名规则在创建有效的满足性算法和简化某些消解难例的证明中起到了重要作用。许道云教授已经证明:MU(k)中的变元和文字改名都等价于图同构的判定问题。众所周知,图同构的判定问题是NP问题。近年来,人们一直寻找某些极小不可满足公式的子类,使其变元和文字改名的判定问题可以在多项式时间内完成。 在本文中,我们找到了一个能递归构造的极小不可满足公式的子类MAX+,MAX+={F∈MAX|(E)x∈var(F)(A)splittings(Fx,F(_)x):Fx,F(_)x∈MAX+∪{(□)}},其中□代表空子句。MAX+(k)=MAX+∩MAX(k)。显然,MAX+是MAX中分裂公式的闭包,即公式的分裂在MAX+中是封闭的。而且证明了这种递归构造方法具有可靠性和完备性。 另一方面,我们将研究关于MAX+(k)中公式改名的判定问题的复杂性。基于分裂技术并通过证明MAX(1)中公式改名问题在多项式时间内可以判定。我们证明了:MAX+(k)中公式的改名问题在多项式时间内可以判定,并给出相应的算法。最后,我们给出了一个文字改名的应用,以此来说明改名问题在证明系统中起到的重要作用。
其他文献
自从Internet诞生以来,互联网上的信息正以指数形式飞速增长。如何在WWW这个全球最大的数据集合中发现用户的有用信息已成为数据挖掘研究的热点,Web数据挖掘也由此应运而生。
3GPP在R5中提出的IP多媒体子系统(IMS)汇集了移动通信领域最先进的概念和技术,它在以下三个方面进行了改善:QoS保证、计费控制和对不同业务的融合,为进一步在PS域上开展新业务提
信任管理基于实体的属性而不是身份进行访问控制,克服了传统的基于身份的访问控制方法在分布式环境中的不足,能够满足基于属性访问控制的需求。信任管理系统的中心思想是一致
随着电子商务规模的进一步扩大,为顾客提供越来越多选择的同时,其结构也变得更加复杂。一方面,顾客面对大量的商品信息束手无策,经常会迷失在大量的商品信息空间中,无法顺利找到自
本文对基于MVC设计模式的Struts框架的研究与应用进行了研究。文章首先介绍适合于构建复杂商务应用的J2EE框架及其相关技术,对J2EE框架的特点进行分析。阐述MVC设计模式的思想
工作流技术是实现企业业务过程建模、过程管理与过程自动化的核心技术。随着信息技术的发展和计算机应用的普及,工作流技术正在受到越来越多的关注。在与工作流相关的各类技术
在企业中,动态监测是生产管理的重要工作内容,也是保证企业正常、安全、经济运行的重要手段。在西方发达国家,自动化数据采集与控制系统已经成为生产的配套设施。将现场信息和管
Internet的飞速发展已经深刻地影响着传统商业模式的运作,电子商务已经被越来越多的人所接受,目前基于Agent的电子商务研究成为业界研究热点。如何快速、高效地进行Agent协商,已
进化算法是一种基于生物自然选择与遗传机理的随机搜索与全局优化方法,该算法的核心思想源于生物进化历程。而生物从简单到复杂,从低级到高级的进化过程是一个自然的、并行发生
随着计算机技术的发展,用户对系统的应用要求越来越高,最近出现的联机商业模式需要系统提供365×7×24小时连续服务,因此停机时间成为系统的一个非常重要的指标,为减少系统停机时