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

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

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

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

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