作者:
王洪琳
关键词:
智能规划；#SAT；DPLL；时间复杂性上界
摘要:
智能规划是人工智能领域的一个前沿研究领域，近年来，对该领域的研究也取得了突破性的进展，研究人员提出了多种方法来求解该问题，其中一种非常高效的求解方法就是将智能规划问题转化成命题可满足性问题（简称SAT问题）。但是，在智能规划领域当中还有很多类经典规划问题，是不能通过转化成SAT问题来求解的，有的还需要计算命题公式的可满足赋值个数，因此衍生出了模型计数问题（简称#SAT问题）。在实际应用中，为了更加容易解决某些问题，研究者们通常会尽量将困难问题转化为逻辑结构尽量简单的命题公式。计算逻辑结构有所限制的命题公式的模型个数问题统称为#SAT子类问题，因此推动#SAT子类问题的研究，对智能规划乃至人工智能领域都有着极其深远的潜在应用价值。在目前求解SAT、#SAT及其子类问题的各种算法中，DPLL算法的性能是最为高效的，但是该算法的时间复杂度还是指数级别的，故，很多研究者在DPLL算法的基础上，通过提出新化简规则或者细化分支等多种手段进一步提高DPLL算法的性能，让该算法的性能获得指数级别的提高。同时，这种思想也催生了研究者们对SAT及其各种扩展问题的算法在最坏情况下，时间复杂性上界的关注。本文选择#SAT的一个子类问题—#2-SAT问题，作为研究课题，使用DPLL算法对目前时间复杂性上界最小的#2-SAT算法进行了改进，提出一种新算法—PMC算法。鉴于目前国内外大多以变量数目作为分析#SAT子类算法在最坏情况下的时间复杂性上界，本文还选择从子句数目角度出发，利用分支树方法计算分析PMC算法，将该算法在最坏情况下的时间复杂性上界从O(1.1892m)提高到O(1.1740m)。另外，根据PMC算法设计了#2-SAT求解器，并与原#2-SAT算法做了对比实验，实验结果表明，相同2-CNF公式进行求解，PMC算法的运行时间明显小于原#2-SAT算法。
在线下载