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

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

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

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

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