基于超擴展規則的動態在線推理算法

劉磊, 牛當當, 李壯, 呂帥

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

基于超擴展規則的動態在線推理算法

劉磊, 牛當當, 李壯, 呂帥

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

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

關鍵詞：自動推理；知識編譯；擴展規則；超擴展規則；動態在線推理

網絡出版地址：http://www.cnki.net/kcms/detail/23.1390.U.20151104.1633.004.html

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

許多約束問題僅判定是否可滿足是遠遠不夠的，如將概率推理問題[1]、一致性概率規劃問題[2]轉換為命題公式集后，除了判斷可滿足性，還需求解#SAT問題，即計算該公式集中的模型數。求解#SAT問題的方法通常可分為離線推理和知識編譯后在線推理。

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

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

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

1超擴展規則

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

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

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

定理1超擴展規則中，子句C及擴展結果D是等價的。

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

與經典擴展規則不同，超擴展規則用子句A對子句C進行擴展，但這種擴展方法產生的C∨A為非子句形式(C∨A為標準子句形式)，因此需要對C∨A以適當形式展開。假設A= {b1,b2，…,bn}，則運用德摩根律，E= {C∨A} = {C∨(b1∨…∨bn)} = {C∨b1,C∨b2…,C∨bn}。上述展開過程是語義等價的，但由于每個bi(i= 1,…,n)兩兩不同且均不在C中出現，所以E的互補因子較低，難以利用擴展規則的推理特性。為了保證擴展結果子句間的互補性，采用如下方法展開[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)的互補展開保證了超擴展規則的等價性，并且展開結果子句之間存在互補文字對。

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

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

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

2基于超擴展規則的定理證明方法

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

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

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

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

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

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

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

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

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

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

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

3超擴展規則與擴展負超歸結的關聯關系

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

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

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

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

擴展負超歸結也可以通過弱化規則和超擴展規則直接證明。

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

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

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

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

4基于超擴展規則的動態在線推理算法IKCCER

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

4.1　IKCCER算法

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

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

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

研究過程中發現：如果在知識編譯過程中進行動態在線推理，則能夠減少大量存儲空間使用，同時不影響推理過程的時間復雜性。基于此，本文提出了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的子句數

6.While j<Σ2的子句數

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//超擴展規則

11.j= j+1

12.i= i+1

13.j= 0

14.While k<Σ2的子句數

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

16.k=k+1

17.Σ2=?

18.Return 2m-Num

IKCCER算法對KCCER算法的改進之處在于：在一次循環結束后，直接計算出子句集Σ2所能擴展出的極大項數，并刪除Σ2。原因在于：若任何一個子句與其他子句存在互補文字對，則它所擴展的任何極大項都不會被其他子句擴展。因此，該算法的動態在線推理過程是正確的。

4.2　IKCCER算法的時間復雜性分析

IKCCER算法與KCCER算法的時間復雜性相同。

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

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

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

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

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

4.3　IKCCER算法的空間復雜性分析

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

為了說明存儲空間的壓縮效果，對變量數m為15、20和25，子句數n為50、75和100的隨機3-SAT問題予以測試，實驗結果分別如圖2~4所示。

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

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

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

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

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

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

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

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

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

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

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

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

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

5結束語

本文提出了超擴展規則，并證明了超擴展規則和擴展負超歸結的關聯關系；重寫了KCER算法，在KCCER算法的基礎上提出了IKCCER算法，解決了KCCER算法應用在大規模子句集中容易產生內存溢出的問題。實驗結果表明，采用動態在線推理策略的IKCCER算法，在存儲空間利用方面存在著巨大的優勢，能夠適應于大規模子句集模型計數問題的求解。

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

參考文獻：

[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]殷明浩, 林海, 孫吉貴. 一種基于擴展規則的#SAT求解系統[J]. 軟件學報, 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]賴永, 歐陽丹彤, 蔡敦波, 等. 基于擴展規則的模型計數與智能規劃方法[J]. 計算機研究與發展, 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]. 計算機學報, 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-)，男，教授，博士生導師;

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

收稿日期：2014-04-16.網絡出版日期：2015-11-04.

中圖分類號：TP301，TP181

文獻標志碼：A

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

doi:10.11990/jheu.201404055