基于擴展規(guī)則的＃SAT近似求解器的研究.pdf

1、智能規(guī)劃是20世紀50年代后期迅速發(fā)展起來的一個前沿研究領域，近年來對該領域的研究取得了革命性的進展。其中，把規(guī)劃問題編譯為SAT問題，然后利用高效的SAT求解器進行求解的方法是目前規(guī)劃求解的主流方法之一。研究表明，這種間接求解有時比直接求解更方便更快捷。＃SAT問題是由SAT問題引出的更具有挑戰(zhàn)性的問題，許多概率推理問題如置信度分析、貝葉斯網(wǎng)絡推理、概率規(guī)劃問題等都可以轉化成＃SAT問題進行求解。這是因為＃SAT問題是＃P完全問題的原

2、型，幾乎所有的＃P完全問題都能在多項式時間內歸約為＃SAT問題。因此，研究＃SAT求解技術不僅對規(guī)劃領域而且對其他許多領域有著重要的理論價值和現(xiàn)實意義。 許多＃SAT求解器都利用了歸結方法，擴展規(guī)則方法是一種與歸結方法對稱的SAT求解方法，目前該方法已被進一步推廣到＃SAT問題求解中，但是它的時間復雜度是指數(shù)級的，效率比較低。 本文在擴展規(guī)則的基礎上提出了兩種＃SAT問題的近似求解算法：上下界近似(Up-DownAppr

3、ox)和采樣近似(SampleApprox)。上下界近似是從計算不可滿足賦值的近似個數(shù)出發(fā)，最終計算出近似模型個數(shù)。其基本思想是：對于容斥原理，將每個累加和視為一項，它的前奇數(shù)項之和是一個上界，前偶數(shù)項之和是一個下界，文中分析了在什么情況下能使某個上界或下界與精確不可滿足賦值個數(shù)的近似偏量在某個范圍內(如≤0.01或更小)，這樣可以將該上界或下界視為不可滿足賦值個數(shù)的近似值，從而得出近似模型個數(shù)。采樣近似是將采樣方法與改進的擴展規(guī)則方法

4、MCIER相結合來得到近似模型個數(shù)。其基本思想是：首先選擇若干個變量并賦值，這樣可以限定一個子空間，然后利用采樣方法計算出總的模型個數(shù)與被限定子空間的模型個數(shù)的近似倍率，并利用MCIER計算出被限定子空間的模型個數(shù)，將近似倍率乘以被限定子空間的模型個數(shù)就可以得到近似模型個數(shù)。 根據(jù)以上兩種算法，本文設計了兩個＃SAT近似求解器：UDApp和SamApp，為了與精確求解器進行比較，我們實現(xiàn)了精確模型計數(shù)算法MCER。實驗結果表明兩