论文部分内容阅读
自动推理和规划是人工智能领域中两个重要的分支,同时也是难度非常大的课题。1971年Cook等证明了命题可满足问题（SAT问题）是NP完备的,1991年Chenoweth等严格证明了简单的积木世界规划问题至少是NP完备的。这就意味着如果P≠NP成立,从理论上我们无法找到这些问题的多项式时间算法。另一方面,目前的SAT问题求解器已经可以求解包含十万以上变量百万以上子句规模的SAT问题实例,规划问题求解器也能在十秒以内求解包含百万以上状态规模的规划问题实例。为什么理论与实际之间存在如此巨大的差异,为了回答这个问题就需要我们研究自动推理与规划问题中最小上界和相变规律。从理论上研究自动推理和规划问题的最小上界和相变规律不仅可以从本质上认识问题,揭示问题的求解规律,解释问题求解困难的原因,而且可以扩大算法对自动推理与规划问题的可解范围,仅以模型计数问题（#SAT问题）为例,对#SAT问题上界的一个微小的改进,例如,从O（ck）改进为O（（c-ε）k）)就会使得#SAT问题求解的算法在效率上获得指数级别的提高。另外,虽然研究这些问题的最小上界和相变规律不能让我们直接证明P、NP、PSPACE等问题之间是否相等,但是至少可以从一定程度上帮助我们了解什么样的问题易于求解,什么样的问题难于求解,从而帮助我们设计有针对性的自动推理和规划问题的求解算法,在实践中指导研究人员设计更为高效的自动推理和规划问题的求解系统。目前,有关最小上界的研究主要以变量的数目作为参数,如模型计数问题（#SAT问题）。到目前为止所有对#SAT问题执行时间上界的分析都是以变量的数目作为参数。事实上,我们知道,算法的时间复杂性是根据问题实例的大小计算所得。而对于涉及命题公式的一类问题,问题实例的大小不仅依赖于变量的数量,还依赖于子句的数量。因此,从子句数量的角度研究问题的时间复杂性具有重要的意义。另外,早期相变规律的研究主要是由实验物理学家完成的,2006年以后这方面的工作开始受到计算机研究人员的重视,但是目前主要集中于探讨复杂度为NP的问题。对于自动推理和规划问题,NP完全问题只是相对最为简单的一类问题。一致性规划问题等具有更高的计算复杂度。因此,本文深入地研究了自动推理和规划问题中最小上界和相变规律,主要考虑#SAT问题和一致性规划问题,主要工作如下:（1）从子句数目的角度给出了#2-SAT问题在最坏情况下的最小上界。提出了一种公式化简规则-五顶点规则,该规则可以移除公式F中度为3的变量,使得算法的效率得到了很大程度的提高。另外,通过分析变量之间的关系设计了基于DPLL求解#2-SAT的MC2算法,并证明该算法可以将求解#2-SAT问题在最坏情况下执行时间的上界改进为O（1.1892m）,其中m是公式中子句的数目。（2）从子句数目的角度给出了#3-SAT问题在最坏情况下的最小上界。通过结合多种分支选择方法,提出了一种基于DPLL的#3-SAT算法MCDP,证明了该算法可以将#3-SAT问题在最坏情况下的上界缩小为O（1.8393m）,其中m是公式中子句的数目。为了提高#3-SAT算法的求解效率,进一步提出了基于DPLL的MC3算法,该算法首先把3-子句公式化简为2-子句公式,然后通过调用求解#2-SAT问题的算法求解原始问题。证明了该算法可以将求解#3-SAT问题在最坏情况下执行时间的上界缩小为O（1.4142m）,其中m是公式中子句的数目。（3）从子句数目的角度给出了#SAT问题在最坏情况下的最小上界。提出了一种基于扩展规则的求解#SAT问题的推理分析算法,证明了基于扩展规则求解#SAT问题的推理分析算法在最坏情况下执行时间的上界是O（2m）,其中m是公式中子句的数量。另外,根据该算法设计了一种新的#SAT求解器—IAER系统。这种求解器在预处理阶段应用了单文字规则、等价化简规则和超二元归结规则;在组件分析阶段,系统采用组件分析技术把大问题分解为若干子问题,从而达到提高系统效率的目的。实验结果证明,单文字规则、等价化简规则、组件技术以及超二元归结技术可以有效提高问题的求解效率。（4）研究了EXPSPACE完全问题的相变,主要考虑具有EXPSPACE完全计算复杂度的一致性规划问题。通过设计一致性规划无解以及有解算法对有规划解和无规划解的界限做出了定量的估计,当动作的数量o不大于αub时,大部分一致性规划实例不存在规划解;当o不小于αlb时,大部分一致性规划实例存在规划解。随机一致性规划问题的实验也证明,随着Density（动作数/命题数）的增大,一致性规划问题出现了从无解到有解的现象。综上所述,本文深入研究了自动推理和规划问题中最小上界和相变规律的研究,主要考虑了#SAT问题在最坏情况下最小上界和一致性规划问题相变规律的研究。从理论上分析#SAT问题在最坏情况下的时间复杂性上界不仅可以认识到问题的本质,而且对#SAT问题上界的一个微小的改进都可以使得#SAT问题求解的算法在效率上获得指数级别的提高。从理论上计算一致性规划问题的相变点,不仅可以对一致性规划问题的相变区域做定量的估计,而且对于设计有针对性的高效的一致性规划算法具有重要的意义。因此,本文的研究成果对自动推理和规划问题具有重要的意义。