智能规划是人工智能研究领域的一个重要分支,已在许多领域得以广泛应用。求解智能规划问题的一个重要方法即把智能规划问题转化为命题逻辑公式求解。动作和世界状态确定的规划问题可以转化成经典命题逻辑问题(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求解器。