基于扩展规则的#QBF求解系统的研究及实现

来源 :东北师范大学 | 被引量 : 0次 | 上传用户:kccsong
下载到本地 , 更方便阅读
声明 : 本文档内容版权归属内容提供方 , 如果您对本文有版权争议 , 可与客服联系进行内容授权或下架
论文部分内容阅读
智能规划是设计某个(组)实体从初始状态出发,到达目标状态的动作序列,其结果被称为规划解。目前的规划求解器只能求解问题的一个解,不能求解问题的所有解的个数,如对手规划,二人游戏赢的所有策略数等问题。虽然这些智能规划问题可以通过相应的处理器(BlackBox)转化成#QBF问题进行求解,但是目前还没有开发出#QBF求解器。针对这一问题,本文提出了一类新的求解#QBF问题的方法——基于扩展规则的#QBF计数方法,用来求解相应的智能规划问题。这类方法的基本思想是利用扩展规则把原公式扩展成和它等价的极大项组成的集合,然后利用极大项的个数来进行#QBF计数,并利用容斥原理来解决空间复杂性问题。这类方法与基于归结的方法相比,当包含互补文字的子句越多时效率越高,因此它们可以看作是和归结互补的方法。基于此思想,本文首先提出了一种基本的基于扩展规则的#QBF计数方法;然后,为了提高效率,本文还提出了一种改进的#QBF计数方法,即基于知识编译的方法,其思想是把要求解的问题应用扩展规则编译成EPCCL语言,然后进行#QBF计数;最后,受组件分析思想的启发,本文提出了基于组件分析的#QBF计数方法,这种方法的思想是把要求解的问题先分解成组件,然后对每个组件利用扩展规则进行求解。由于该方法中还加入了单文字处理的功能,所以与前两种方法相比,它不仅可以处理比较一般的#QBF计数问题,还可以处理规模较大的#QBF计数问题。在给出算法的基础上,本文采用C++语言对算法进行了实现,设计了基于扩展规则的三个#QBF计数系统:#ER、#KCER和#CSER,并用实例对其性能加以测试。实验结果表明,在处理一般问题时,#ER的时间复杂性是指数级的,效率比较低;#KCER算法理论上要优于#ER算法,但是经过编译后的子句集扩大的规模在最坏情况下是指数级的,所以它的效果也不尽如人意;#CSER算法由于加入了单文字处理和组件分析的功能,使得它处理问题的能力比前两种方法要好。由于目前国内尚没有一个公开成型的基于扩展规则的#QBF计数器,所以本文的三个系统特别是#CSER系统将具有一定的研究价值与应用前景。
其他文献
近年来,通过计算机对人脸进行自动处理成为当前计算机视觉、模式识别、计算机图形学等领域的一个热点研究课题,在影视制作、视频会议、智能人机交互等方面有着广泛的应用前景
近年来,为适应社会发展需要,各高校发展迅猛,校园建设、设备购置、教师引进、教学改革、分配方式改革、扩大招生等工作的步伐加快,给高校的信息管理工作带来很大困难,如数据量增大
客户是企业生存和发展的基础,但现有的客户关系管理过分强调企业如何为客户提供价值,实际上并非所有的客户对企业来说都是有价值的,对企业来说选择有价值的客户,对客户的价值作有
时间表问题是一类特殊的资源调度问题,广泛应用于学校课程和考试的时间安排、各类大型会议、体育比赛、航班(火车、飞机、轮船等)时刻表的制定等。由于考试时间表问题属于NP完
近年来,随着无线通信技术的发展和大量智能移动终端的出现,机会网络研究在学术界受到了广泛的关注。本文就机会网络链路预测和路由策略展开研究。报文的投递成功率是衡量网络
我国是天然气资源丰富的国家之一,天然气远景储量约达38万亿m3,其中陆上占79%,海上占21%。天然气的生产、利用过程是一个流程复杂、规模大、速度快且连续运行的系统。在这个系统中
随着移动智能产品的极速发展,移动终端在人们的生活中占据着越来越重要的地位。根据CNNIC报告,截至2014年12月,中国手机网民规模达5.57亿,较2013年底增加5672万人,手机网民人群占
传送带缺陷检测是传送带修补的基础,也是传送带安全使用的保障。随着计算机技术和机器视觉的发展,以往的人工检测逐渐被自动化检测所取代。缺陷检测技术融合了图像去噪、增强
软件体系结构从系统全局刻画系统的结构,是软件动态演化的重要依据。现有的基于体系结构的软件动态演化模型中,通常使用体系结构描述语言(ADL)来刻画系统的状态和结构,但以此为
智能规划是20世纪50年代后期迅速发展起来的一个前沿研究领域,近年来对该领域的研究取得了革命性的进展。其中,把规划问题编译为SAT问题,然后利用高效的SAT求解器进行求解的