基于擴(kuò)展規(guī)則的＃QBF求解系統(tǒng)的研究及實(shí)現(xiàn).pdf

1、智能規(guī)劃是設(shè)計(jì)某個(gè)(組)實(shí)體從初始狀態(tài)出發(fā)，到達(dá)目標(biāo)狀態(tài)的動(dòng)作序列，其結(jié)果被稱為規(guī)劃解。目前的規(guī)劃求解器只能求解問(wèn)題的一個(gè)解，不能求解問(wèn)題的所有解的個(gè)數(shù)，如對(duì)手規(guī)劃，二人游戲贏的所有策略數(shù)等問(wèn)題。雖然這些智能規(guī)劃問(wèn)題可以通過(guò)相應(yīng)的處理器(BlaekBox)轉(zhuǎn)化成＃QBF問(wèn)題進(jìn)行求解，但是目前還沒(méi)有開(kāi)發(fā)出＃QBF求解器。 針對(duì)這一問(wèn)題，本文提出了一類新的求解＃QBF問(wèn)題的方法--基于擴(kuò)展規(guī)則的＃QBF計(jì)數(shù)方法，用來(lái)求解相應(yīng)的智能規(guī)

2、劃問(wèn)題。這類方法的基本思想是利用擴(kuò)展規(guī)則把原公式擴(kuò)展成和它等價(jià)的極大項(xiàng)組成的集合，然后利用極大項(xiàng)的個(gè)數(shù)來(lái)進(jìn)行撐QBF計(jì)數(shù)，并利用容斥原理來(lái)解決空間復(fù)雜性問(wèn)題。這類方法與基于歸結(jié)的方法相比，當(dāng)包含互補(bǔ)文字的子句越多時(shí)效率越高，因此它們可以看作是和歸結(jié)互補(bǔ)的方法?；诖怂枷?，本文首先提出了一種基本的基于擴(kuò)展規(guī)則的＃QBF計(jì)數(shù)方法；然后，為了提高效率，本文還提出了一種改進(jìn)的＃QBF計(jì)數(shù)方法，即基于知識(shí)編譯的方法，其思想是把要求解的問(wèn)題應(yīng)用擴(kuò)展

3、規(guī)則編譯成EPCCL語(yǔ)言，然后進(jìn)行＃QBF計(jì)數(shù)；最后，受組件分析思想的啟發(fā)，本文提出了基于組件分析的拌QBF計(jì)數(shù)方法，這種方法的思想是把要求解的問(wèn)題先分解成組件，然后對(duì)每個(gè)組件利用擴(kuò)展規(guī)則進(jìn)行求解。由于該方法中還加入了單文字處理的功能，所以與前兩種方法相比，它不僅可以處理比較一般的＃QBF計(jì)數(shù)問(wèn)題，還可以處理規(guī)模較大的＃QBF計(jì)數(shù)問(wèn)題。 在給出算法的基礎(chǔ)上，本文采用C++語(yǔ)言對(duì)算法進(jìn)行了實(shí)現(xiàn)，設(shè)計(jì)了基于擴(kuò)展規(guī)則的三個(gè)＃OBF計(jì)數(shù)

4、系統(tǒng)：＃ER、＃KCER和＃CSER，并用實(shí)例對(duì)其性能加以測(cè)試。實(shí)驗(yàn)結(jié)果表明，在處理一般問(wèn)題時(shí)，＃ER的時(shí)間復(fù)雜性是指數(shù)級(jí)的，效率比較低；＃KCER算法理論上要優(yōu)于＃ER算法，但是經(jīng)過(guò)編譯后的子句集擴(kuò)大的規(guī)模在最壞情況下是指數(shù)級(jí)的，所以它的效果也不盡如人意；＃CSER算法由于加入了單文字處理和組件分析的功能，使得它處理問(wèn)題的能力比前兩種方法要好。由于目前國(guó)內(nèi)尚沒(méi)有一個(gè)公開(kāi)成型的基于擴(kuò)展規(guī)則的＃QBF計(jì)數(shù)器，所以本文的三個(gè)系統(tǒng)特別是＃CS