智能规划是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能够得到与精确值比较接近的近似模型个数。