基于局部搜索隱蔽集算法的QBF求解器研究.pdf

1、智能規(guī)劃是人工智能中比較熱門的研究領(lǐng)域之一,目前智能規(guī)劃求解的主要方法之一是將智能規(guī)劃問題轉(zhuǎn)化為命題可滿足問題(Propositional Satisfiability Problem,簡稱SAT),然后利用高效的SAT求解器進(jìn)行求解。
　　 命題可滿足性問題(簡稱SAT)是當(dāng)今人工智能研究的核心問題。SAT問題可以描述為給定一個命題邏輯公式,其變元是否存在一個真值賦值使命題公式成立(可滿足),如果成立則返回這些變元的真值賦值。

2、SAT問題是比較難求解的問題,其計(jì)算復(fù)雜性是NP完備的,而實(shí)例的隱藏結(jié)構(gòu)能夠找到有效的SAT求解方法,Backdoors就是這種隱藏結(jié)構(gòu)之一。
　　 隱蔽集(backdoor sets)是SAT問題的一個重要韻隱藏結(jié)構(gòu),與問題難度有很大的關(guān)系。它的選擇能使剩下的問題在多項(xiàng)式時間內(nèi)求解。隱蔽集可以描述為一個較小的變量子集B,對B中的變量進(jìn)行真值指派后,簡化后的公式可以在多項(xiàng)式時間內(nèi)求解。由于其在復(fù)雜問題求解中的重要性,近年來隱蔽集

3、的研究已逐步成為研究的熱點(diǎn)。目前隱蔽集的求解方法已經(jīng)擴(kuò)展到QBF問題中。
　　 量化布爾公式(Quantifled Boolean Formulae,簡稱QBF)是一種帶有存在量詞和全稱量詞前綴的命題邏輯公式。當(dāng)QBF公式中的量詞中只含存在量詞時,QBF問題就轉(zhuǎn)化為SAT問題。因此QBF問題可以看作是SAT問題的泛化。QBF問題是比SAT問題更加難解的問題,其計(jì)算復(fù)雜性是PSPACE完備的。隱蔽集的引入能提高QBF問題的求解效率

4、。
　　 本文首先對現(xiàn)有的隱蔽集問題的求解算法進(jìn)行一個總體的概述,其次針對QBF問題設(shè)計(jì)了一種新的基于重命名的隱蔽集求解算法,并將隱蔽集首次應(yīng)用到的QBF求解器中從而設(shè)計(jì)出一種新的BDQBF求解器。在BDQBF中,我們用隱蔽集中的變量作啟發(fā)式,引導(dǎo)算法進(jìn)行分支搜索,從而減小了算法的搜索空間和回退次數(shù),并提高了QBF問題的求解效率。最后本文針對這一算法進(jìn)行了兩類實(shí)驗(yàn):第一類實(shí)驗(yàn)是在Windows環(huán)境下用標(biāo)準(zhǔn)的C++實(shí)現(xiàn)這一算法,并