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

(吉林大學(xué) 計算機科學(xué)與技術(shù)學(xué)院,吉林 長春130012)

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

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

(吉林大學(xué) 計算機科學(xué)與技術(shù)學(xué)院,吉林 長春130012)

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

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

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

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

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

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

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

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

1超擴展規(guī)則

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

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

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

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

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

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

(1)

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

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

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

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

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

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

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

基于超擴展規(guī)則將一個子句集擴展為極大項集的過程為：

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

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

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

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

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

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

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

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

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

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

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

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

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

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

擴展負超歸結(jié)也可以通過弱化規(guī)則和超擴展規(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}，即超擴展規(guī)則的擴展結(jié)果D的形式。根據(jù)定理1可知：該擴展結(jié)果D與C等價，即可以通過定義5中的所有子句歸結(jié)出C0∨C1∨…∨Cr。

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

定義5(混合負超歸結(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是負文字的析取形式，且有可能為空，則可以直接歸結(jié)為C0∨C1∨…∨Cr，這種歸結(jié)方式稱為混合負超歸結(jié)。

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

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

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

4.1　IKCCER算法

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

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

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

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

算法1 IKCCER

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

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

3.While Σ1≠?

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

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

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

7.If Ci和Cj含互補文字對 Then skip

8.Else if Ci蘊含CjThen 從Σ2中刪除Cj9.Else if Cj蘊含CiThen 從Σ1中刪除Ci

10.Else將Cj替換為Cj∨{Ci-Cj}∪Cj∨Ci-Cj//超擴展規(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算法對KCCER算法的改進之處在于：在一次循環(huán)結(jié)束后，直接計算出子句集Σ2所能擴展出的極大項數(shù)，并刪除Σ2。原因在于：若任何一個子句與其他子句存在互補文字對，則它所擴展的任何極大項都不會被其他子句擴展。因此，該算法的動態(tài)在線推理過程是正確的。

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

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

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

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

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

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

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

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

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

為了說明存儲空間的壓縮效果，對變量數(shù)m為15、20和25，子句數(shù)n為50、75和100的隨機3-SAT問題予以測試，實驗結(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空間開銷對比(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空間開銷對比(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空間開銷對比(n = 100)Fig.4　The comparison of spending space between IKCCER and KCCER (n = 100)

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

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

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

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

5結(jié)束語

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

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

參考文獻：

[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]殷明浩, 林海, 孫吉貴. 一種基于擴展規(guī)則的#SAT求解系統(tǒng)[J]. 軟件學(xué)報, 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]賴永, 歐陽丹彤, 蔡敦波, 等. 基于擴展規(guī)則的模型計數(shù)與智能規(guī)劃方法[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: 一個高性能的EPCCL編譯器[J]. 計算機學(xué)報, 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.

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

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

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

中圖分類號：TP301，TP181

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

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

doi:10.11990/jheu.201404055