基于知识编译的QBF求解器的研究

基于知识编译的QBF求解器的研究

论文摘要

智能规划是人工智能研究领域的一个重要分支,已在许多领域得以广泛应用。求解智能规划问题的一个重要方法即把智能规划问题转化为命题逻辑公式求解。动作和世界状态确定的规划问题可以转化成经典命题逻辑问题(SAT)求解;动作确定,初始状态不确定的一致性规划可以在有效时间内转化成量化布尔公式(Quantified Boolean Formulae,简称QBF)问题求解。QBF是SAT的泛化,它可以对状态空间较大的一致性规划问题求解。QBF问题作为标准的PSPACE完备问题在人工智能领域的重要性日益增长。非单调性推理,并行一致性推理等许多人工智能领域问题也可以在多项式时间内转换成QBF问题,并且实验数据表明基于转换的方法比基于域依赖的方法有效。知识编译是近年来出现的一个新的研究方向,它用于处理一般命题逻辑推理的计算复杂性。根据这种方法,推理过程被分为两个阶段:离线编译阶段和在线查询阶段。离线阶段,命题理论被编译成某种易处理的目标语言;在线阶段编译目标被用于有效应答指数级数量的查询。知识编译的主要动机是将主要花销放在离线阶段,用无数次的有效在线查询抵消,并生成一个快捷的在线推理系统。知识编译是应用于命题逻辑SAT上的,并在SAT上取得了很好的效果,QBF是SAT的泛化,知识编译同样可以应用于QBF。本文讨论了EPCCL、D-FNNF、FNNF、D-OFNNF、OFNNF这五种命题语言的基本性质,完备性,易处理性,以及它们的简洁性。根据OFNNF的性质,我们提出一种新的模型计数方法—表推演模型计数。根据对五种目标语言的讨论结果,我们选出两种目标语言OFNNF和D-OFNNF,并为之设计了编译器,这两种目标语言在加上兼容性约束后作为QBF的主式可使QBF在多项式时间内求解,并给出相应的算法,根据算法我们设计出一款基于知识编译的QBF求解器。

论文目录

  • 摘要
  • Abstract
  • 引言
  • 第一章 智能规划
  • 1.1 智能规划概念
  • 1.2 智能规划的发展
  • 1.3 智能规划的求解方法
  • 1.4 一致性规划问题编码为QBF
  • 第二章 知识编译
  • 2.1 相关概念
  • 2.2 完备性
  • 2.3 易处理性
  • 2.4 简洁性
  • 2.5 表推演模型计数
  • 第三章 QBF
  • 3.1 QBF 相关概念
  • 3.2 求解QBF
  • 第四章 基于知识编译的QBF
  • 4.1 相关概念
  • 4.2 VAL(QPROPPS)易处理性
  • 第五章 基于知识编译的QBF 求解器的设计与实现
  • 5.1 求解器概述
  • 5.2 编译器功能结构图
  • 5.3 求解器流程图
  • 5.4 开发工具及测试环境
  • 5.5 实验结果分析
  • 第六章 总结与展望
  • 参考文献
  • 致谢
  • 在学期间公开发表论文及著作情况
  • 相关论文文献

    • [1].基于QBF的循环不变式构造技术[J]. 计算机工程与科学 2010(09)
    • [2].QBR、QBF高效生化处理技术在碱渣处理装置中的应用及改进[J]. 化学工程与装备 2010(12)
    • [3].QBF法在污水处理场的应用研究[J]. 油气田环境保护 2011(01)
    • [4].QBF求解算法研究综述[J]. 计算机研究与发展 2011(05)
    • [5].求解QBF问题的启发式调查传播算法[J]. 软件学报 2011(07)
    • [6].QBF化工有机废气高效生物处理技术[J]. 中国环保产业 2012(09)

    标签:;  ;  ;  ;  ;  

    基于知识编译的QBF求解器的研究
    下载Doc文档

    猜你喜欢