劉磊, 牛當(dāng)當(dāng), 李壯, 呂帥

(吉林大學(xué) 計(jì)算機(jī)科學(xué)與技術(shù)學(xué)院,吉林 長(zhǎng)春130012)

基于超擴(kuò)展規(guī)則的動(dòng)態(tài)在線推理算法

劉磊, 牛當(dāng)當(dāng), 李壯, 呂帥

(吉林大學(xué) 計(jì)算機(jī)科學(xué)與技術(shù)學(xué)院,吉林 長(zhǎng)春130012)

摘要：為了提高擴(kuò)展規(guī)則的擴(kuò)展性能，提出了超擴(kuò)展規(guī)則，并證明了其與擴(kuò)展負(fù)超歸結(jié)之間的關(guān)聯(lián)關(guān)系。KCER算法中使用擴(kuò)展規(guī)則擴(kuò)展子句，利用超擴(kuò)展規(guī)則替換擴(kuò)展規(guī)則能夠更清晰地展示擴(kuò)展過程，因此提出了基于超擴(kuò)展規(guī)則的動(dòng)態(tài)在線推理算法IKCCER。IKCCER采用離線編譯和在線推理過程交互執(zhí)行的方式，在保持推理效率不變的同時(shí)，其空間復(fù)雜性為KCCER算法空間復(fù)雜性的2/(n+1)，其中n為輸入子句集的子句數(shù)。

關(guān)鍵詞：自動(dòng)推理；知識(shí)編譯；擴(kuò)展規(guī)則；超擴(kuò)展規(guī)則；動(dòng)態(tài)在線推理

網(wǎng)絡(luò)出版地址：http://www.cnki.net/kcms/detail/23.1390.U.20151104.1633.004.html

呂帥(1981-)，男，講師.

許多約束問題僅判定是否可滿足是遠(yuǎn)遠(yuǎn)不夠的，如將概率推理問題[1]、一致性概率規(guī)劃問題[2]轉(zhuǎn)換為命題公式集后，除了判斷可滿足性，還需求解#SAT問題，即計(jì)算該公式集中的模型數(shù)。求解#SAT問題的方法通?？煞譃殡x線推理和知識(shí)編譯后在線推理。

在離線推理的研究中，在擴(kuò)展規(guī)則提出之前，絕大多數(shù)#SAT問題的求解算法都是基于#DPLL算法設(shè)計(jì)的[3]。林海等[4]提出了擴(kuò)展規(guī)則推理方法(extension rule，ER)，被著名人工智能專家Davis稱為與歸結(jié)方法“互補(bǔ)”的方法。擴(kuò)展規(guī)則推理方法通過計(jì)算輸入子句集所能擴(kuò)展出的極大項(xiàng)數(shù)來判斷其可滿足性及模型數(shù)。殷明浩等[5]基于容斥原理提出了解決ER算法空間復(fù)雜性問題的CER算法；賴永等[6]提出了#ER算法，并結(jié)合#DPLL算法和#ER算法提出了求解效率較高的#CDE算法。

知識(shí)編譯是知識(shí)表示與推理領(lǐng)域的一個(gè)重要論題，它試圖將問題轉(zhuǎn)化為多項(xiàng)式時(shí)間內(nèi)能夠得到解決的表示形式。Selman[7]設(shè)計(jì)了將原子句集轉(zhuǎn)化為等價(jià)Horn子句集的編譯方法，但并非所有子句集都存在與其等價(jià)的Horn子句集，因此該方法不完備。Val[8]提出了一種精確的知識(shí)編譯方法，并通過運(yùn)行一個(gè)完備的求本原蘊(yùn)含式的算法過程保證編譯后子句集上的單元?dú)w結(jié)完備。Marquis[9]提出了一種基于本原蘊(yùn)含式的知識(shí)編譯方法。Schrag[10]提出了一種對(duì)偶的基于本原蘊(yùn)含的方法。Darwiche[11]將子句形式轉(zhuǎn)換為可分解否定范式DNNF，并給出知識(shí)編譯的發(fā)展圖譜。在擴(kuò)展規(guī)則的基礎(chǔ)上中，Lin等[12]提出了一種基于擴(kuò)展規(guī)則的知識(shí)編譯方法KCER，可以將子句集編譯為EPCCL理論。殷明浩等[5]提出了用于求解模型計(jì)數(shù)問題的KCCER算法。劉大有等[13]基于擴(kuò)展規(guī)則提出了一種新的知識(shí)編譯算法C2E，該算法具有較高的編譯效率。

傳統(tǒng)的擴(kuò)展規(guī)則難以直接利用一個(gè)文字集對(duì)一個(gè)子句進(jìn)行擴(kuò)展，因此本文提出超擴(kuò)展規(guī)則(hyper extension rule，HER)，描述了利用超擴(kuò)展規(guī)則的推理過程，并證明了超擴(kuò)展規(guī)則與擴(kuò)展負(fù)超歸結(jié)的等價(jià)性?；跀U(kuò)展規(guī)則能夠?qū)⒁粋€(gè)公式集編譯為EPCCL理論，然而現(xiàn)有編譯方法由于擴(kuò)展規(guī)則的限制，在編譯過程中容易出現(xiàn)內(nèi)存溢出的現(xiàn)象。本文針對(duì)基于擴(kuò)展規(guī)則的知識(shí)編譯過程，提出了基于超擴(kuò)展規(guī)則的動(dòng)態(tài)在線推理算法IKCCER，解決了采用離線編譯和在線推理過程交互執(zhí)行的方式，在保持推理效率不改變的同時(shí)，降低空間復(fù)雜性，有效解決內(nèi)存溢出問題。

1超擴(kuò)展規(guī)則

定義1(擴(kuò)展規(guī)則)[4]給定一個(gè)子句C和一個(gè)變量集M，D= {C∨a,C∨a}，其中a∈M并且a和a都不在C中出現(xiàn)，將C到D的推導(dǎo)過程稱為擴(kuò)展規(guī)則，D中的子句稱為C擴(kuò)展得到的結(jié)果，并且C≡D。

擴(kuò)展規(guī)則要求一個(gè)子句結(jié)合一個(gè)變量進(jìn)行擴(kuò)展，本文提出超擴(kuò)展規(guī)則，允許一個(gè)子句結(jié)合另一個(gè)子句進(jìn)行擴(kuò)展。為了表示方便，定義子句C的(原子)變量集合為V(C)，子句集F的(原子)變量集合為V(F)。

定義2(超擴(kuò)展規(guī)則)給定2個(gè)子句C和A，D= {C∨A,C∨A}，其中V(C)∩V(A) = ?，將C到D的推導(dǎo)過程稱為超擴(kuò)展規(guī)則，D中的元素為C應(yīng)用超擴(kuò)展規(guī)則的結(jié)果。

定理1超擴(kuò)展規(guī)則中，子句C及擴(kuò)展結(jié)果D是等價(jià)的。

證明：可以通過真值表證明子句C及其擴(kuò)展結(jié)果語義上是等價(jià)的。證畢。

與經(jīng)典擴(kuò)展規(guī)則不同，超擴(kuò)展規(guī)則用子句A對(duì)子句C進(jìn)行擴(kuò)展，但這種擴(kuò)展方法產(chǎn)生的C∨A為非子句形式(C∨A為標(biāo)準(zhǔn)子句形式)，因此需要對(duì)C∨A以適當(dāng)形式展開。假設(shè)A= {b1,b2，…,bn}，則運(yùn)用德摩根律，E= {C∨A} = {C∨(b1∨…∨bn)} = {C∨b1,C∨b2…,C∨bn}。上述展開過程是語義等價(jià)的，但由于每個(gè)bi(i= 1,…,n)兩兩不同且均不在C中出現(xiàn)，所以E的互補(bǔ)因子較低，難以利用擴(kuò)展規(guī)則的推理特性。為了保證擴(kuò)展結(jié)果子句間的互補(bǔ)性，采用如下方法展開[14]：

(1)

稱式(1)的展開過程為互補(bǔ)展開，則E= {C∨A} = {C∨b1,C∨b1∨b2,…,C∨b1∨…∨bn-1∨bn}，進(jìn)而D= {C∨b1∨…∨bn,C∨b1,C∨b1∨b2,…,C∨b1∨…∨bn-1∨bn}。

定理2依賴式(1)的互補(bǔ)展開保證了超擴(kuò)展規(guī)則的等價(jià)性，并且展開結(jié)果子句之間存在互補(bǔ)文字對(duì)。

證明：假設(shè)A= {b1, b2…,bn}，由于C本身對(duì)擴(kuò)展結(jié)果性質(zhì)沒有影響，只需要證明：1)A=(b1∨…∨bn)與Z= {{b1},{b1∨b2},…,{b1∨…∨bn-1∨bn}}等價(jià)；2){b1,b1∨b2,…,b1∨…∨bn-1∨bn}子句之間存在互補(bǔ)文字對(duì)。其中2)顯然成立。下面證明1)。

綜上，結(jié)論1)得證，進(jìn)而定理2成立。證畢。

超擴(kuò)展規(guī)則能夠利用一個(gè)子句擴(kuò)展另一個(gè)子句，并且利用互補(bǔ)展開在保證可滿足性的前提下保證了擴(kuò)展之后的子句間存在互補(bǔ)文字對(duì)，這使得擴(kuò)展過程能夠高效進(jìn)行并得到能夠發(fā)揮擴(kuò)展規(guī)則推理方法特性的理論。超擴(kuò)展規(guī)則同時(shí)也是一種等價(jià)性規(guī)則，可以利用超擴(kuò)展規(guī)則和推導(dǎo)規(guī)則作為核心推理規(guī)則構(gòu)建新的推理框架。

2基于超擴(kuò)展規(guī)則的定理證明方法

定義3一個(gè)非重言式子句是集合M上的極大項(xiàng)當(dāng)且僅當(dāng)包含集合M上的所有原子或其否定。

基于超擴(kuò)展規(guī)則將一個(gè)子句集擴(kuò)展為極大項(xiàng)集的過程為：

首先對(duì)子句集中每一個(gè)子句做擴(kuò)展，假設(shè)變量集為M，則D= {C∨{M-V(C)},C∨{M-V(C)}}，將新擴(kuò)展的子句集D與原子句集合并，并去掉重復(fù)子句或可被蘊(yùn)含的子句，如此不斷擴(kuò)展，最終會(huì)得到一個(gè)極大項(xiàng)集。

定理3利用超擴(kuò)展規(guī)則擴(kuò)展出的極大項(xiàng)集與原子句集等價(jià)。

證明：擴(kuò)展過程中僅使用超擴(kuò)展規(guī)則和推導(dǎo)規(guī)則。根據(jù)定理2，超擴(kuò)展規(guī)則保證了擴(kuò)展結(jié)果與原子句集等價(jià)，因此，整個(gè)擴(kuò)展過程中是等價(jià)變換，利用超擴(kuò)展規(guī)則擴(kuò)展出的極大項(xiàng)集合與原子句集等價(jià)。證畢。

定理4在命題邏輯中，基于超擴(kuò)展規(guī)則的極大項(xiàng)擴(kuò)展方法是有效完備的。

證明：類似文獻(xiàn)[4]中定理3.2的證明過程，上述定理顯然成立。證畢。

定理5給定一個(gè)子句集F由V(F)上的極大項(xiàng)組成，|V(F)| =m，則F不可滿足當(dāng)且僅當(dāng)F中包含2m個(gè)互不相同的極大項(xiàng)。

定理6[5]給定一個(gè)子句集F由V(F)上的極大項(xiàng)組成，|V(F)| =m，則F的模型數(shù)為2m-S，當(dāng)且僅當(dāng)F中包含S個(gè)互不相同的極大項(xiàng)。

定理6給出了模型數(shù)與極大項(xiàng)的關(guān)系，如果要計(jì)算一個(gè)子句集的模型數(shù)，首先需要將子句集擴(kuò)展為與其等價(jià)的極大項(xiàng)集，再根據(jù)定理6計(jì)算出原子句集的模型數(shù)。

超擴(kuò)展規(guī)則能夠?qū)⒁粋€(gè)子句集擴(kuò)展為極大項(xiàng)集，然而擴(kuò)展結(jié)果的子句集規(guī)模往往較大，最壞情況下的空間復(fù)雜性是指數(shù)級(jí)的。實(shí)際上并不需要將所有的極大項(xiàng)都擴(kuò)展處理，只需要計(jì)算它的個(gè)數(shù)即可。若一個(gè)子句集能夠擴(kuò)展出的極大項(xiàng)集中元素個(gè)數(shù)為S，則子句集包含2m-S個(gè)模型。容斥原理可以高效實(shí)現(xiàn)模型個(gè)數(shù)的計(jì)算，并在基于擴(kuò)展規(guī)則的模型計(jì)數(shù)方法中采用，具體細(xì)節(jié)請(qǐng)參閱文獻(xiàn)[5]。

3超擴(kuò)展規(guī)則與擴(kuò)展負(fù)超歸結(jié)的關(guān)聯(lián)關(guān)系

Peter等給出了負(fù)超歸結(jié)的基本定義[15]，該定義可以進(jìn)一步擴(kuò)展。

定義4 (擴(kuò)展負(fù)超歸結(jié)，extension negative hyper resolution)假設(shè)存在子句集{Ci∨x1∨…∨xi-1∨xi} (i= 1,2，…,r)和子句C0∨x1∨…∨xr，其中xi是文字，C0和Ci是負(fù)文字的析取形式，且有可能為空，則可以直接歸結(jié)出C0∨C1∨…∨Cr，這種歸結(jié)方式稱為擴(kuò)展負(fù)超歸結(jié)。

上述歸結(jié)方式可以通過有序弱化并使用擴(kuò)展規(guī)則予以證明，如圖1所示。

圖1　擴(kuò)展負(fù)超歸結(jié)的歸結(jié)樹Fig.1　The resolution tree of extension negative hyper resolution

擴(kuò)展負(fù)超歸結(jié)也可以通過弱化規(guī)則和超擴(kuò)展規(guī)則直接證明。

假設(shè)C=C0∨C1∨…∨Cr，則定義5中所有子句中的Ci(i= 0,1,…,r)，可以通過弱化規(guī)則得到子句C，即定義5中所有子句的弱化結(jié)果可以表示為{C∨x1∨…∨xr,C∨x1,C∨x1∨x2,…,C∨x1∨…∨xn-1∨xn}，即超擴(kuò)展規(guī)則的擴(kuò)展結(jié)果D的形式。根據(jù)定理1可知：該擴(kuò)展結(jié)果D與C等價(jià)，即可以通過定義5中的所有子句歸結(jié)出C0∨C1∨…∨Cr。

推論1若所有Ci(i= 0,1,…,r)均相同，則超擴(kuò)展規(guī)則與擴(kuò)展負(fù)超歸結(jié)等價(jià)。

定義5(混合負(fù)超歸結(jié)，hybrid negative hyper resolution)假設(shè)存在子句集{Ck∨xk,Ck+1∨xk∨xk+1,…,Ci∨xk∨…∨xi-1∨xi| 1≤k≤i≤r}和子句C0∨x1∨…∨xr，其中xi是文字，C0和Ci是負(fù)文字的析取形式，且有可能為空，則可以直接歸結(jié)為C0∨C1∨…∨Cr，這種歸結(jié)方式稱為混合負(fù)超歸結(jié)。

負(fù)超歸結(jié)與擴(kuò)展負(fù)超歸結(jié)為混合負(fù)超歸結(jié)的特殊形式。當(dāng)k=i時(shí)，混合負(fù)超歸結(jié)等價(jià)于負(fù)超歸結(jié)；當(dāng)k= 1時(shí)，混合負(fù)超歸結(jié)等價(jià)于擴(kuò)展負(fù)超歸結(jié)；當(dāng)任一k滿足1

4基于超擴(kuò)展規(guī)則的動(dòng)態(tài)在線推理算法IKCCER

本文在EPCCL理論編譯過程中利用超擴(kuò)展規(guī)則替換了擴(kuò)展規(guī)則，設(shè)計(jì)并實(shí)現(xiàn)了動(dòng)態(tài)在線推理算法IKCCER，該算法不需要保存臨時(shí)變量，從而大幅度降低了知識(shí)編譯求解#SAT問題的空間復(fù)雜性。實(shí)驗(yàn)結(jié)果表明該算法具有較好的存儲(chǔ)開銷。

4.1　IKCCER算法

利用擴(kuò)展規(guī)則可以將一個(gè)子句集編譯成EPCCL理論。在EPCCL理論中，解決推理問題只需要多項(xiàng)式時(shí)間，KCER算法為將一個(gè)子句集編譯成EPCCL理論的最具代表性的高效算法，其具體流程參見文獻(xiàn)[12]。

用超擴(kuò)展規(guī)則代替了經(jīng)典擴(kuò)展規(guī)則，能更清晰地描述整個(gè)擴(kuò)展過程(體現(xiàn)在算法1第10行)。當(dāng)子句Ci和Cj不存在互補(bǔ)文字對(duì)且彼此不蘊(yùn)含時(shí)，只需要求解差集Ci-Cj，就能找到Cj需要擴(kuò)展的所有文字，然后利用超擴(kuò)展規(guī)則，利用這些文字組成的子句對(duì)Cj進(jìn)行擴(kuò)展。

殷明浩等基于KCER算法提出了KCCER算法，是一種高效的#SAT問題計(jì)算方法，對(duì)于互補(bǔ)因子較高的公式集求解，能夠取得非常好的求解效率[5]。由于離線編譯過程通?？梢酝ㄟ^前期的理論分析得以有效預(yù)處理，所以人們通常只關(guān)注在線推理時(shí)間，離線時(shí)間通常不作為評(píng)價(jià)標(biāo)準(zhǔn)予以考慮。KCCER算法首先利用知識(shí)編譯將子句集離線編譯為一個(gè)EPCCL理論，之后在該理論上在線推理，計(jì)算編譯后的#SAT問題只需要多項(xiàng)式時(shí)間，高效的在線推理性能使得該算法能夠用于#SAT問題的高效求解。

研究過程中發(fā)現(xiàn)：如果在知識(shí)編譯過程中進(jìn)行動(dòng)態(tài)在線推理，則能夠減少大量存儲(chǔ)空間使用，同時(shí)不影響推理過程的時(shí)間復(fù)雜性?；诖?，本文提出了IKCCER算法。

算法1 IKCCER

1.令子句集Σ1= {C1,…,Cn}, Σ2= Σ3= ?

2.sum = 0, i = 0, j = 0

3.While Σ1≠?

4.從Σ1中選擇一個(gè)子句C，將其加入到Σ2中

5.While i<Σ1的子句數(shù)

6.While j<Σ2的子句數(shù)

7.If Ci和Cj含互補(bǔ)文字對(duì) Then skip

8.Else if Ci蘊(yùn)含CjThen 從Σ2中刪除Cj9.Else if Cj蘊(yùn)含CiThen 從Σ1中刪除Ci

10.Else將Cj替換為Cj∨{Ci-Cj}∪Cj∨Ci-Cj//超擴(kuò)展規(guī)則

11.j= j+1

12.i= i+1

13.j= 0

14.While k<Σ2的子句數(shù)

15.Num=Num+2m-|V(Ck)|

16.k=k+1

17.Σ2=?

18.Return 2m-Num

IKCCER算法對(duì)KCCER算法的改進(jìn)之處在于：在一次循環(huán)結(jié)束后，直接計(jì)算出子句集Σ2所能擴(kuò)展出的極大項(xiàng)數(shù)，并刪除Σ2。原因在于：若任何一個(gè)子句與其他子句存在互補(bǔ)文字對(duì)，則它所擴(kuò)展的任何極大項(xiàng)都不會(huì)被其他子句擴(kuò)展。因此，該算法的動(dòng)態(tài)在線推理過程是正確的。

4.2　IKCCER算法的時(shí)間復(fù)雜性分析

IKCCER算法與KCCER算法的時(shí)間復(fù)雜性相同。

1)在線推理時(shí)間：首先將EPCCL理論中所有子句能擴(kuò)展的極大項(xiàng)數(shù)，放在知識(shí)編譯過程中計(jì)算，該過程中并沒有增加或減少計(jì)算量，因此與KCCER算法的在線推理效率相同。

2)離線知識(shí)編譯時(shí)間：由于IKCCER算法同樣需要將一個(gè)子句集編譯為一個(gè)EPCCL理論，不可能提前結(jié)束，因此離線編譯時(shí)間與KCCER算法相同。

因此，IKCCER算法與KCCER算法時(shí)間復(fù)雜性等價(jià)。由于IKCCER算法和KCCER算法所需執(zhí)行時(shí)間相同，因此本文不列出實(shí)驗(yàn)結(jié)果對(duì)比分析。僅通過定理7證明IKCCER算法為何不能提前結(jié)束。

定理7假設(shè)子句集Σ= {C1,…,Cn}，|V(Σ)| = m，在IKCCER算法的知識(shí)編譯過程中，若已編譯的子句集能夠擴(kuò)展的極大項(xiàng)數(shù)為2m，則Σ1必為?。

證明：知識(shí)編譯的一次循環(huán)，需要找到一個(gè)所有子句間存在互補(bǔ)文字對(duì)，且與當(dāng)前Σ1中所有子句存在互補(bǔ)文字對(duì)的子句集。假設(shè)Σ1不為?，則必然存在一個(gè)子句與當(dāng)前編譯得到的子句集中所有子句存在互補(bǔ)文字對(duì)，則當(dāng)前編譯得到的子句集能夠擴(kuò)展的極大項(xiàng)不會(huì)包含該子句所能擴(kuò)展的極大項(xiàng)，因此與當(dāng)前擴(kuò)展的極大項(xiàng)數(shù)為2m條件沖突，結(jié)論成立。證畢。

4.3　IKCCER算法的空間復(fù)雜性分析

IKCCER算法比KCCER算法的空間復(fù)雜性低。由于KCCER算法需要不斷保存中間過程，因此始終需要一個(gè)數(shù)組保存中間結(jié)果，增加了存儲(chǔ)空間使用量。IKCCER算法采用動(dòng)態(tài)在線推理，不保存中間結(jié)果。假設(shè)平均每次能夠擴(kuò)展出k個(gè)子句，則KCCER算法每次需要增加k個(gè)子句的存儲(chǔ)空間，在執(zhí)行過程中累計(jì)需要保存k+2k+3k+…+nk= (n2+n)k/2個(gè)子句的存儲(chǔ)空間，而IKCCER算法只需要nk個(gè)子句的存儲(chǔ)空間，為KCCER算法的2/(n+1)，這對(duì)于大規(guī)模子句集來說效果更加明顯。

為了說明存儲(chǔ)空間的壓縮效果，對(duì)變量數(shù)m為15、20和25，子句數(shù)n為50、75和100的隨機(jī)3-SAT問題予以測(cè)試，實(shí)驗(yàn)結(jié)果分別如圖2~4所示。

(a)內(nèi)存消耗3-SAT(15，50)

(b)內(nèi)存消耗3-SAT(20，50)

(c)內(nèi)存消耗3-SAT(25，50)圖2　IKCCER和KCCER空間開銷對(duì)比(n = 50)Fig.2　The comparison of spending space between IKCCER and KCCER (n = 50)

(a)內(nèi)存消耗3-SAT(15，75)

(b)內(nèi)存消耗3-SAT(20，75)

(c)內(nèi)存消耗3-SAT(25，75)圖3　IKCCER和KCCER空間開銷對(duì)比(n = 75)Fig.3　The comparison of spending space between IKCCER and KCCER (n = 75)

(a)內(nèi)存消耗3-SAT(15，100)

(b)內(nèi)存消耗3-SAT(20，100)

(c)內(nèi)存消耗3-SAT(25，100)圖4　IKCCER和KCCER空間開銷對(duì)比(n = 100)Fig.4　The comparison of spending space between IKCCER and KCCER (n = 100)

需要注意的是：由于子句規(guī)模變大后，所對(duì)比的KCCER算法存儲(chǔ)空間需求遠(yuǎn)遠(yuǎn)高于本文提出的IKCCER算法，便于對(duì)比分析，圖2和圖3的縱坐標(biāo)為線性坐標(biāo)，而圖4選用了指數(shù)縱坐標(biāo)。圖2~4中的橫坐標(biāo)代表正在進(jìn)行的循環(huán)層，縱坐標(biāo)代表了需要的額外存儲(chǔ)空間，用子句數(shù)刻畫。

實(shí)驗(yàn)結(jié)果表明：1)圖2和圖3的對(duì)比結(jié)果容易看出：IKCCER算法的存儲(chǔ)開銷基本上無明顯變化，保持較低的存儲(chǔ)空間開銷，直到算法執(zhí)行完畢；而KCCER算法的存儲(chǔ)空間開銷隨著循環(huán)執(zhí)行持續(xù)增加；2)循環(huán)剛開始，IKCCER算法與KCCER算法所需的額外存儲(chǔ)空間相近；3)隨著循環(huán)的逐步執(zhí)行，IKCCER算法所需存儲(chǔ)空間明顯少于KCCER算法，甚至相差4~5個(gè)數(shù)量級(jí)；4)圖3中IKCCER曲線出現(xiàn)若干孤立點(diǎn)的情況，是由于測(cè)試結(jié)果為0而無法在指數(shù)級(jí)坐標(biāo)很好的表示，并不影響整體結(jié)論；5)圖4中IKCCER曲線波動(dòng)較大，但在線性坐標(biāo)下(類似圖2和圖3)存儲(chǔ)開銷基本趨于穩(wěn)定。

在小規(guī)模子句集上的測(cè)試結(jié)果顯示了IKCCER算法的存儲(chǔ)開銷優(yōu)勢(shì)，更大規(guī)模的測(cè)試樣例對(duì)于KCCER算法在系統(tǒng)運(yùn)行空間上是難以承受的，上述測(cè)試結(jié)果(IKCCER算法存儲(chǔ)開銷基本上無明顯變化)使得有理由相信IKCCER算法將繼續(xù)保持該優(yōu)勢(shì)，而原算法將難以使用。

因此，本文提出的IKCCER算法具有很好的存儲(chǔ)空間開銷。由于經(jīng)典擴(kuò)展規(guī)則需要保存中間結(jié)果較多，并且在擴(kuò)展之后子句集規(guī)模較大，利用動(dòng)態(tài)在線推理的IKCCER算法能夠明顯降低空間復(fù)雜性，從而解決了KCCER算法容易內(nèi)存溢出的問題。

5結(jié)束語

本文提出了超擴(kuò)展規(guī)則，并證明了超擴(kuò)展規(guī)則和擴(kuò)展負(fù)超歸結(jié)的關(guān)聯(lián)關(guān)系；重寫了KCER算法，在KCCER算法的基礎(chǔ)上提出了IKCCER算法，解決了KCCER算法應(yīng)用在大規(guī)模子句集中容易產(chǎn)生內(nèi)存溢出的問題。實(shí)驗(yàn)結(jié)果表明，采用動(dòng)態(tài)在線推理策略的IKCCER算法，在存儲(chǔ)空間利用方面存在著巨大的優(yōu)勢(shì)，能夠適應(yīng)于大規(guī)模子句集模型計(jì)數(shù)問題的求解。

該算法可以作為擴(kuò)展規(guī)則方法的典型，在不適合歸結(jié)方法求解的大規(guī)模子句集可滿足性問題和模型計(jì)數(shù)問題等領(lǐng)域發(fā)揮子句集互補(bǔ)特性，為高效推理提供了可能。

參考文獻(xiàn)：

[1]MAJERCIK S M, LITTMAN M L. Contingent planning under uncertainty via stochastic satisfiability[J]. Artificial Intelligence, 2003, 147(1/2): 119-162.

[2]PALACIOS H, GEFFNER H. Compiling uncertainty away in conformant planning problems with bounded width[J]. Journal of Artificial Intelligence Research, 2009, 35: 623-675.

[3]BIRNBAUM E, LOZINSKII E L. The good old Davis-Putnam procedure helps counting models[J]. Journal of Artificial Intelligence Research, 1999, 10: 457-477.

[4]LIN Hai, SUN Jigui, ZHANG Yimin. Theorem proving based on the extension rule[J]. Journal of Automated Reasoning, 2003, 31(1): 11-21.

[5]殷明浩, 林海, 孫吉貴. 一種基于擴(kuò)展規(guī)則的#SAT求解系統(tǒng)[J]. 軟件學(xué)報(bào), 2009, 20(7): 1714-1725.YIN Minghao, LIN Hai, SUN Jigui. Solving #SAT using extension rules[J]. Journal of Software, 2009, 20(7): 1714-1725.

[6]賴永, 歐陽丹彤, 蔡敦波, 等. 基于擴(kuò)展規(guī)則的模型計(jì)數(shù)與智能規(guī)劃方法[J]. 計(jì)算機(jī)研究與發(fā)展, 2009, 46(3): 459-469.LAI Yong, OUYANG Dantong, CAI Dunbo, et al. Model counting and planning using extension rule[J]. Journal of Computer Research and Development, 2009, 46(3): 459-469.

[7]SELMAN B, KAUTZ H. Knowledge compilation using horn approximations[C]//Proceedings of the 9th National Conference on Artificial Intelligence. Anaheim, USA, 1991: 904-909.

[8]DEL VAL A. Tractable databases: How to make propositional unit resolution complete through compilation[C]//Proceedings of the 4th International Conference on Principles of Knowledge Representation and Reasoning (KR’94). Bonn, Germany, 1994: 551-561.

[9]MARQUIS P. Knowledge compilation using theory prime implicates[C]//Proceedings of the 14th International Joint Conference on Artificial Intelligence (IJCAI’95). Montréal, Québec, Canada, 1995: 837-843.

[10]SCHRAG R, MIRANKER D P. Compilation for critically constrained knowledge bases[C]//Proceedings of the 13th National Conference on Artificial Intelligence (AAAI’96). Portland, USA, 1996: 510-515.

[11]DARWICHE A, MARQUIS P. A knowledge compilation map[J]. Journal of Artificial Intelligence Research, 2002, 17(1): 229-264.

[12]LIN Hai, SUN Jigui. Knowledge compilation using the extension rule[J]. Journal of Automated Reasoning, 2004, 32(2): 93-102.

[13]劉大有, 賴永, 林海. C2E: 一個(gè)高性能的EPCCL編譯器[J]. 計(jì)算機(jī)學(xué)報(bào), 2013, 36(6): 1254-1260.LIU Dayou, LAI Yong, LIN Hai. C2E: An EPCCL compiler with good performance[J]. Chinese Journal of Computer, 2013, 36(6): 1254-1260.

[14]LARROSA J, HERAS F, DE GIVRY S. A logical approach to efficient Max-SAT solving[J]. Artificial Intelligence, 2008, 172(2/3): 204-233.

[15]PETER J, JUSTYNA P. Local consistency and SAT-solvers[J]. Journal of Artificial Intelligence Research, 2012, 43: 329-351.

Dynamic online reasoning algorithm based on the hyper extension rule

LIU Lei, NIU Dangdang, LI Zhuang, LYU Shuai

(College of Computer Science and Technology, Jilin University, Changchun 130012, China)

Abstract：In order to improve the extension ability of extension rules, hyper extension rule(HER) is proposed in this paper, and the relevant relationship between the hyper extension rule and extension negative hyper resolution is proven. HER replaces extension rule(ER) in knowledge compilation using extension rule(KCER), so the extension process can be shown more clearly. Then the dynamic online reasoning algorithm interactive knowledge compilation for counting models using extension rule(IKCCER) is proposed based on HER. It adopts an interactive execution mode between offline compilation and online reasoning process. IKCCER does not change the efficiency of knowledge compilation for counting models using extension rule(KCCER), and its space complexity is 2/(n+1) of KCCER's space complexity (n is the number of clauses of the input CNF formula).

Keywords：automated reasoning; knowledge compilation; extension rule; hyper extension rule; dynamic online reasoning

通信作者：呂帥，E-mail：lus@jlu.edu.cn.

作者簡(jiǎn)介：劉磊(1960-)，男，教授，博士生導(dǎo)師;

基金項(xiàng)目：國(guó)家自然科學(xué)基金資助項(xiàng)目(61300049，61402195)；教育部高等學(xué)校博士學(xué)科點(diǎn)專項(xiàng)科研基金資助項(xiàng)目(20120061120059);吉林省科技發(fā)展計(jì)劃資助項(xiàng)目(20130206052GX，20140520069JH).

收稿日期：2014-04-16.網(wǎng)絡(luò)出版日期：2015-11-04.

中圖分類號(hào)：TP301，TP181

文獻(xiàn)標(biāo)志碼：A

文章編號(hào)：1006-7043(2015)12-1614-06

doi:10.11990/jheu.201404055