基于扩展规则的＃SAT近似求解器的研究

摘要

智能规划是20世纪50年代后期迅速发展起来的一个前沿研究领域，近年来对该领域的研究取得了革命性的进展。其中，把规划问题编译为SAT问题，然后利用高效的SAT求解器进行求解的方法是目前规划求解的主流方法之一。研究表明，这种间接求解有时比直接求解更方便更快捷。＃SAT问题是由SAT问题引出的更具有挑战性的问题，许多概率推理问题如置信度分析、贝叶斯网络推理、概率规划问题等都可以转化成＃SAT问题进行求解。这是因为＃SAT问题是＃P完全问题的原型，几乎所有的＃P完全问题都能在多项式时间内归约为＃SAT问题。因此，研究＃SAT求解技术不仅对规划领域而且对其他许多领域有着重要的理论价值和现实意义。 许多＃SAT求解器都利用了归结方法，扩展规则方法是一种与归结方法对称的SAT求解方法，目前该方法已被进一步推广到＃SAT问题求解中，但是它的时间复杂度是指数级的，效率比较低。 本文在扩展规则的基础上提出了两种＃SAT问题的近似求解算法：上下界近似(Up-DownApprox)和采样近似(SampleApprox)。上下界近似是从计算不可满足赋值的近似个数出发，最终计算出近似模型个数。其基本思想是：对于容斥原理，将每个累加和视为一项，它的前奇数项之和是一个上界，前偶数项之和是一个下界，文中分析了在什么情况下能使某个上界或下界与精确不可满足赋值个数的近似偏量在某个范围内(如≤0.01或更小)，这样可以将该上界或下界视为不可满足赋值个数的近似值，从而得出近似模型个数。采样近似是将采样方法与改进的扩展规则方法MCIER相结合来得到近似模型个数。其基本思想是：首先选择若干个变量并赋值，这样可以限定一个子空间，然后利用采样方法计算出总的模型个数与被限定子空间的模型个数的近似倍率，并利用MCIER计算出被限定子空间的模型个数，将近似倍率乘以被限定子空间的模型个数就可以得到近似模型个数。 根据以上两种算法，本文设计了两个＃SAT近似求解器：UDApp和SamApp，为了与精确求解器进行比较，我们实现了精确模型计数算法MCER。实验结果表明两种近似求解器都比精确求解器MCER快，其中SamApp的运行速度有了成倍的提高；在精确性方面，如果近似偏量足够小，UDApp能得到与精确值非常接近的近似模型个数，SamApp能够得到与精确值比较接近的近似模型个数。

目录

文摘

英文文摘

声明

第一章引 言

1.1研究背景

1.2本文的主要工作

1.3论文的结构

第二章基于可满足性的规划

2.1规划主要求解方法

2.2基于可满足性的规划(Planning as Satisfiability)

2.2.1基于可满足性的规划方法

2.2.2基于可满足性的规划系统SATPLAN

2.2.3基于可满足性的规划系统Blackbox

2.2.4该类规划器在国际规划器竞赛中的表现

第三章命题可满足性问题的扩展—模型计数问题

3.1命题可满足性问题

3.2 SAT问题的求解方法

3.3模型计数问题

3.4#SAT问题的求解方法

3.4.1精确求解方法

3.4.2近似求解方法

第四章基于扩展规则的#SAT近似求解方法

4.1扩展规则及其相关定理

4.2基于扩展规则的#SAT求解方法

4.3基于扩展规则的#SAT近似求解方法

4.3.1上下界近似

4.3.2采样近似

4.3.3近似#SAT求解方法比较

第五章基于扩展规则的#SAT近似求解器的设计与实现

5.1求解器简介

5.2功能设计

5.2.1 UDApp的结构图

5.2.2 SamApp的结构图

5.3开发工具及测试环境

5.4实验结果分析

第六章总结与展望

6.1总结

6.2展望

参考文献

致 谢

在学期间公开发表论文及著作情况