命題模態(tài)邏輯S5系統(tǒng)中并行推理方法*

楊 洋，李廣力，張桐搏，劉 磊，呂 帥,2,3+

1.吉林大學 計算機科學與技術(shù)學院，長春 130012

2.吉林大學 數(shù)學學院，長春 130012

3.符號計算與知識工程教育部重點實驗室（吉林大學），長春 130012

命題模態(tài)邏輯S5系統(tǒng)中并行推理方法*

楊 洋1，李廣力1，張桐搏1，劉 磊1，呂 帥1,2,3+

1.吉林大學 計算機科學與技術(shù)學院，長春 130012

2.吉林大學 數(shù)學學院，長春 130012

3.符號計算與知識工程教育部重點實驗室（吉林大學），長春 130012

YANG Yang,LI Guangli,ZHANG Tongbo,et al.Parallel reasoning methods in propositional modal logic S5. Journal of Frontiers of Computer Science and Technology,2016,10(12)：1783-1792.

S5系統(tǒng)是一類知識表示能力和處理能力都較強的模態(tài)公理系統(tǒng)，它是認知邏輯、信念邏輯等非經(jīng)典邏輯理論的基礎(chǔ)。根據(jù)Kripke語義模型以及S5系統(tǒng)中部分公理，對命題模態(tài)邏輯S5公理系統(tǒng)的性質(zhì)進行了較為深入的研究，并對S5系統(tǒng)中一類具有代表性的標準模態(tài)子句集的特性進行了分析，提出了一種基于擴展規(guī)則方法的命題模態(tài)邏輯推理算法（propositional modal clausal reasoning based on novel extension rule，PMCRNER）。針對樸素算法時間復雜度較高的問題，利用任務(wù)間潛在的關(guān)聯(lián)性對算法同時進行了粗粒度與細粒度并行化，提出了并行算法PPMCRNER（parallel PMCRNER）理論框架，并且與基本算法進行了對比。實驗結(jié)果表明，PPMCRNER算法在不可滿足的子句集上的推理具有良好的加速比，為高時間復雜性的模態(tài)推理方法的進一步研究提供了一種可行方案。

命題模態(tài)邏輯；S5公理系統(tǒng)；并行推理；擴展規(guī)則

1 引言

近年來，多種以模態(tài)邏輯為基礎(chǔ)的復雜公理系統(tǒng)與框架被相繼提出[1-3]，關(guān)于模態(tài)邏輯甚至是更高階的邏輯知識表示形式的理論研究逐漸成為人們關(guān)注的熱點[4]。模態(tài)邏輯推理方法的研究是高階公理系統(tǒng)和框架的原型實現(xiàn)的基礎(chǔ)。自動推理領(lǐng)域主流的推理方法為歸結(jié)方法、表推演方法和擴展規(guī)則推理方法。推理的公式集一般為非CNF（conjunctive normal form）和CNF公式。結(jié)合基礎(chǔ)推理方法，命題模態(tài)邏輯的推理方法有直接推理和轉(zhuǎn)換推理兩種。鑒于不同模態(tài)系統(tǒng)中的公理存在著較大差異，因此現(xiàn)階段主流模態(tài)推理方法和證明系統(tǒng)大部分都是基于具體的模態(tài)公理系統(tǒng)或者模態(tài)語言。

2006年，Wu等人提出了一種在命題模態(tài)邏輯K系統(tǒng)中的破壞性擴展規(guī)則推理方法[5]，并且將擴展規(guī)則推理過程和化簡過程交替進行，加速算法的求解過程。該方法保留了擴展規(guī)則求解問題的優(yōu)勢，對于互補因子率較高的模態(tài)公式能夠快速地進行可滿足性判定。同年，Schmidt探討了命題動態(tài)模態(tài)邏輯不同推理方法的發(fā)展，闡明了表推演系統(tǒng)、歸結(jié)系統(tǒng)、雙重表推演系統(tǒng)中如何通過一些規(guī)則使其能夠擴展到一階命題邏輯[6]。2007年，Nalon等人提出了一種正規(guī)模態(tài)邏輯中基于歸結(jié)的推理方法，通過一組公理來對模態(tài)邏輯公式進行直接推理，同時為許多正規(guī)多模態(tài)邏輯的推理方法給出了正確性和完備性的結(jié)果[7]。2008年，吳瑕等人提出了一種命題模態(tài)邏輯中關(guān)系擴展規(guī)則推理方法[8]。其主要思想是使用關(guān)系轉(zhuǎn)換函數(shù)對Kripke語義模型進行轉(zhuǎn)換，使用一階擴展規(guī)則方法對轉(zhuǎn)換后的結(jié)果進行推理。2013年，Benzmüller等人提出了一種使用高階邏輯定理證明器來求解一階模態(tài)邏輯可滿足性問題的方法，并且給出了一階模態(tài)邏輯（first-order modal logic，F(xiàn)ML）到高階邏輯（high-order logic，HOL）的轉(zhuǎn)換工具[9]。近年來，由于SAT（satisfiability）比賽的推廣以及命題邏輯SAT求解器求解效率的大幅提升，更多的學者開始尋求轉(zhuǎn)換方法來將多種不同的模態(tài)公理系統(tǒng)轉(zhuǎn)化為命題SAT求解。2013年，Kaminski等人通過一組公理轉(zhuǎn)換規(guī)則將模態(tài)可滿足性問題轉(zhuǎn)化成普通的布爾可滿足性問題，調(diào)用命題SAT求解器進行求解，得到了較好的效果[10]。2014年，Rajeev等人提出了一種使用二元決策圖（binary decision diagrams，BDDs）替換DPLL的算法求解模式來求解模態(tài)可滿足性問題，通過與多個求解器進行對比展現(xiàn)了其優(yōu)越的求解能力[11]。

2 基礎(chǔ)知識

2.1 擴展規(guī)則

擴展規(guī)則方法的原理為給定命題變量集上的所有極大項之間的合取是不可滿足的。擴展規(guī)則[12]的定義為：給定一個子句C和不在C中出現(xiàn)的原子a，D={C∨a，C∨?a}，稱由C到D的推導過程為擴展規(guī)則，D為子句C關(guān)于原子a應(yīng)用擴展規(guī)則的結(jié)果。顯然，公式集D在真值指派上和公式集C邏輯等價。因此，可以對子句集中的任意子句應(yīng)用類似上述的推導過程，逐步擴展成只包含形式為極大項的子句集。樸素擴展規(guī)則算法（extension rule，ER）的基本思想是：搜索所有的極大項空間，若待判定的子句集能夠擴展出所有的極大項空間，則該子句集不可滿足；否則該子句集可滿足。

在2009年李瑩等人提出的基于擴展規(guī)則的NER（novel extension rule）推理方法中[13]，其進行逆向推理，不斷取給定命題變量集上的極大項依次判斷能否被指定子句集擴展出來，以此來獲得公式是否可滿足的結(jié)論。在該方法中，其避免了樸素擴展規(guī)則ER繁重的容斥原理求解過程和內(nèi)存溢出問題，以時間效率換取空間開銷，是一種較優(yōu)的推理方法。本文將借助NER推理方法來進行模態(tài)公式推理。

目前，擴展規(guī)則的應(yīng)用研究還僅限于起步階段，其研究成果主要包括命題邏輯知識編譯、搜索方法的啟發(fā)式策略、可能性推理與知識編譯、模型計數(shù)以及#SAT問題求解等[14-19]。而對于高階邏輯的推理方法的應(yīng)用研究還處于空白階段。

2.2 命題模態(tài)系統(tǒng)

命題模態(tài)邏輯公理系統(tǒng)在命題邏輯系統(tǒng)的基礎(chǔ)上進行了擴展，在保持系統(tǒng)推理結(jié)構(gòu)封閉的情況下加入了部分公理和規(guī)則。公理系統(tǒng)分為正規(guī)系統(tǒng)和非正規(guī)系統(tǒng)，通常對模態(tài)邏輯的正規(guī)系統(tǒng)進行推理。常用的模態(tài)邏輯正規(guī)系統(tǒng)主要有K、T、D、S4、S5、B等系統(tǒng)。K系統(tǒng)為命題模態(tài)邏輯中最小的正規(guī)系統(tǒng)，它相比于經(jīng)典命題邏輯系統(tǒng)增加了K公理(□(P→Q)→(□P→□Q))和必然化規(guī)則（如果?KP，則?K□P）。而其他系統(tǒng)分別在K系統(tǒng)的基礎(chǔ)上添加了相應(yīng)的公理，使得相應(yīng)的公理系統(tǒng)增加了不同的約束和性質(zhì)。需要強調(diào)的是：S5系統(tǒng)是在T系統(tǒng)的基礎(chǔ)上添加了E公理而形成的[20]。命題模態(tài)邏輯推理是在特定的公理系統(tǒng)中對一組任意的命題模態(tài)公式進行可滿足性判斷的過程。命題模態(tài)邏輯推理的過程比命題邏輯推理更復雜，因為在對模態(tài)公式進行推理時不僅要考慮命題變量集的真值指派，還要考慮必然和可能算子導致的命題公式在Kripke可能世界模型中的世界轉(zhuǎn)移，所以如何對模態(tài)算子的處理是命題模態(tài)邏輯推理過程的核心，對于命題的部分，只需要考慮使用常規(guī)命題邏輯的推理方法即可。命題模態(tài)邏輯S5公理系統(tǒng)是一種有代表性的公理系統(tǒng)，它也是認知邏輯和信念邏輯的基礎(chǔ)。在S5系統(tǒng)中，可以只保留一個模態(tài)算子，即必然算子□。在不同的邏輯中，該算子代表的含義也不盡相同。如在認知邏輯中，該算子代表某智能體知道某個事件；而在信念邏輯中，該算子代表某個智能體相信某個事件。因此，研究該系統(tǒng)的推理方法對于更高級的認知邏輯、信念邏輯和道義邏輯等推理方法的研究有著重要意義。

需要指出的是，目前命題模態(tài)邏輯的推理方法研究還處于理論階段，并且大多數(shù)對于該邏輯的研究主要集中在K、T公理系統(tǒng)中，對于多約束的公理系統(tǒng)的通用形式化推理算法還較少，本文將對S5系統(tǒng)的推理方法進行研究，并進行一系列相關(guān)實驗。

3 命題模態(tài)邏輯S5系統(tǒng)中標準模態(tài)子句集推理方法

3.1 定義與引理

模態(tài)邏輯S5公理系統(tǒng)在T系統(tǒng)的基礎(chǔ)上增加了E公理（◇P→□◇P），利用該公理，對于系統(tǒng)中的模態(tài)公式可以進行模態(tài)度歸約，使得任意公式能夠歸約為模態(tài)度小于等于1的模態(tài)公式，并且通過化簡等手段將模態(tài)公式轉(zhuǎn)化為標準模態(tài)子句集或者標準模態(tài)子句塊。

下面給出標準模態(tài)子句的定義：

標準模態(tài)子句：令ФP為模態(tài)文字，其中Ф是有限個必然與可能算子的序列，并且該序列可以為空串，P為命題文字。若干個模態(tài)文字的析取式為標準模態(tài)子句。

S5系統(tǒng)具有對稱性，不能使用破壞性方法對其進行推理，因此可以通過間接轉(zhuǎn)化的方法對其進行推理，其中最重要的轉(zhuǎn)化規(guī)則為分裂規(guī)則和歸約規(guī)則。

分裂規(guī)則[5]：如果一個子句集包含一個至少包含兩個模態(tài)文字的子句C，那么該子句集可以由兩個子句集來替代，其中一個子句集是原子句集中非C子句集與子句C中的一個模態(tài)文字的合取，另一個子句集是原子句集中非C子句集與子句C中的其余子句的合取。

歸約規(guī)則：因為S5系統(tǒng)是S4系統(tǒng)的擴張，那么借助S4系統(tǒng)中與S5系統(tǒng)中□P?□□P，◇P?◇◇P，◇P?□◇P，□P?◇□P這4條定理，可以對任意長度的模態(tài)算子序列，刪去前面的任意長度而只保留最里層的模態(tài)算子。

因為K系統(tǒng)是最小的正規(guī)模態(tài)系統(tǒng)，所以K系統(tǒng)中的任意定理在S5系統(tǒng)中都適用，K系統(tǒng)中的定理(◇P∨◇Q?◇(P∨Q))可以應(yīng)用于S5系統(tǒng)中，對在一個標準模態(tài)子句中具有相同可能算子前綴的模態(tài)文字進行合并，便于后續(xù)處理。

單模態(tài)單元子句：令ФQ為單模態(tài)單元子句，其中Ф是單個必然算子或者單個可能算子或者為空，Q為命題邏輯中的標準子句。由單模態(tài)單元子句組成的子句集叫作單模態(tài)單元子句集。

3.2 基于NER的命題模態(tài)子句推理算法

基于上述的規(guī)則和定義，命題模態(tài)邏輯S5系統(tǒng)中子句形式的推理算法的核心思想如下：

（1）預(yù)處理

對于初始輸入的標準模態(tài)子句集，使用歸約規(guī)則對含有超過一個模態(tài)算子序列的模態(tài)文字進行歸約，使得算法真正處理的輸入為所有模態(tài)文字均不含有超過一個模態(tài)算子的標準模態(tài)子句集，該操作能夠在線性時間復雜度內(nèi)完成。

（2）合并

掃描經(jīng)過預(yù)處理的標準模態(tài)子句集，對子句中出現(xiàn)的形如◇P∨◇Q析取式進行合并。注意，形如□P∨□Q的公式無法進行合并，因為合并后的形式與原形式不保持Kripke語義等價，只合并可能算子。該操作同樣能夠在線性時間復雜度內(nèi)完成。

（3）拆分

任意選取經(jīng)過合并操作后的子句集中的非單模態(tài)單元子句，使用分裂規(guī)則對子句集進行拆分，形成兩個子句列表，子句列表之間的可滿足性為析取關(guān)系。

（4）可滿足性判定

在拆分過程中，可以邊拆分邊判斷，判斷的形式是拆分的子句列表出現(xiàn)單模態(tài)單元子句集。調(diào)用可滿足性判定算法（在后文詳述）。如果一個子句列表判定為可滿足，則結(jié)束全部的拆分和求解過程，返回可滿足；否則只有當所有子句列表都返回不可滿足時，算法結(jié)束。

單模態(tài)單元子句集的可滿足性判定：

輸入?yún)?shù)為單模態(tài)單元子句集時，考慮到多模態(tài)算子公式已經(jīng)被歸約為單模態(tài)算子，則在處理單模態(tài)算子時只需要考慮一層的世界轉(zhuǎn)移即可，即判斷當前世界以及當前世界的后繼世界即可，不需要再考慮后繼的后繼或者更多，因此在處理過程中只需要將子句集轉(zhuǎn)化成命題形式即可。

對于命題子句集，不僅需要考慮當前世界的可滿足性，還得考慮其對后繼世界的可滿足性影響。因為S5系統(tǒng)是在T公理系統(tǒng)之上的模態(tài)邏輯公理系統(tǒng)，則T公理系統(tǒng)中的約束對于S5系統(tǒng)同樣成立。在T公理系統(tǒng)中，有公理P→◇P，則在處理單模態(tài)單元子句集時，需要將每一個出現(xiàn)的命題子句進行復制，并且對復制后的每一個子句最外層附加一個可能算子，將這樣的公式加入原單模態(tài)單元子句集中進行求解。對于帶模態(tài)算子的子句，優(yōu)先考慮帶必然算子的單模態(tài)單元子句，當前世界的后繼世界的個數(shù)為命題變量個數(shù)的2的冪次方。在可滿足性判定時，首先使用該子句列表中的所有帶必然算子的單模態(tài)單元子句依次對這些不可滿足的后繼可能世界進行“殺死”操作，進行完一輪后，剩余的可能世界集為滿足所有帶必然算子中的命題公式。然后將帶可能算子的單模態(tài)單元子句的命題部分傳遞到剩余世界判定，如果存在一個世界能夠使得該子句的命題部分為真，則判斷結(jié)束，依次判斷所有帶可能算子的單模態(tài)單元子句。

開始使用帶必然算子的單模態(tài)單元子句集“殺死”任意一個使其命題部分為假的世界實際上是對于該部分子句集的命題部分，尋找是否有解，能夠使得帶必然算子的單模態(tài)單元子句的命題部分全部為真。接下來使用帶可能算子的單模態(tài)單元子句的命題部分在剩下的世界里尋找是否存在能夠使其為真的世界，是將每一個帶可能算子的單模態(tài)單元子句的命題部分加入帶必然算子的單模態(tài)單元子句集的命題部分尋找該整體命題子句集是否有解。最后對命題部分的求解，同樣是受限于T公理的約束，在T公理系統(tǒng)中，有公理（□P→P）。因此，必須將該子句列表中的所有帶必然算子的單模態(tài)單元子句的命題部分進行剝落，然后將其添加到該子句列表的命題公式部分，統(tǒng)一進行可滿足性判定。

因此本文在處理過程中將帶必然算子的單模態(tài)單元子句集的命題部分單獨判定其可滿足性，然后依次把帶可能算子的單模態(tài)單元子句的命題部分加入到帶必然算子的單模態(tài)單元子句集的命題子句集中，判定其可滿足性，只要存在一個使其不可滿足，則整體不可滿足，只有每一個帶可能算子的單模態(tài)單元子句判定均可滿足，則整體才可滿足。

例 F={□◇□A∨◇◇B,□?A∨◇?B∨C}，對該公式的推理步驟如下：

返回SAT。

綜上所述，給出命題模態(tài)邏輯S5中的子句形式的推理算法。

算法1 PMCRNER（propositional modal clausal reasoning based on novel extension rule）

算法2 SMRNER（single modal reasoning based on novel extension rule）

算法1中的IsSingle函數(shù)是判斷當前合取公式是否為單模態(tài)單元子句集，如果是，則調(diào)用基于NER的單模態(tài)單元子句集求解算法SMRNER進行求解，否則繼續(xù)進行拆分，直到所有單模態(tài)單元子句集全部被處理。choose函數(shù)是在公式F1中任意選擇一個標準模態(tài)子句進行拆分。

算法2中的GetP函數(shù)的功能為得到當前子句列表中的命題部分；AddPO函數(shù)的功能為為當前子句列表中的每一個命題子句的最外層添加一個可能算子，將其變成命題模態(tài)子句；GetNO函數(shù)的功能為得到當前子句列表中所有帶必然算子的子句的命題部分；GetPO函數(shù)的功能為得到當前子句列表中所有帶可能算子的子句的命題部分。

顯然，該算法對于命題模態(tài)邏輯S5公理系統(tǒng)中的子句形式推理是正確并且完備的。

3.3 PPMCRNER算法

上節(jié)給出了PMCRNER算法，但樸素版本的算法時間復雜度較高，需要尋找新的方法使得算法的執(zhí)行效率得到提高，在進行可滿足性判定時能夠提前結(jié)束。本節(jié)將該形式的推理算法進行了并行化，在特定的子句集上得到了較好的加速效果。

3.3.1 粗粒度并行

上節(jié)中，將標準模態(tài)子句拆分成不同的子句列表進行求解，該部分在串行算法中是順序執(zhí)行的?？梢詫⒃摬糠謭?zhí)行過程并行化，得到粗粒度并行的目的。

3.3.2 細粒度并行

也可以考慮將子句列表的可滿足性判定過程并行化。在對子句列表運用T系統(tǒng)中的兩條公理后，將后繼世界之間的可滿足性判定和命題邏輯的可滿足性判定并行化。由于多個帶可能算子的子句均需要同所有帶必然算子的子句進行后繼世界可滿足性判定，可以將它們的執(zhí)行過程并行化，同時將命題部分的執(zhí)行過程同樣并行化，達到細粒度并行的目的。

3.3.3PMCRNER算法的并行化

綜上所述，當將算法粗粒度和細粒度并行化之后，就得到了全并行的PMCRNER推理算法——PPMCRNER算法。下面給出PPMCRNER算法的理論框架。

在算法執(zhí)行之前，需要對公式集進行預(yù)處理，處理的大致流程如下。

算法3 PPMCRNER(parallel propositional modal clausal reasoning based on novel extension rule)

否則返回第1步.

算法4 PSMRNER（parallel single modal reasoning based on novel extension rule）

在Predeal中，flag變量和Flag[]數(shù)組分別為標記變量和標記數(shù)組，用于主方法對子方法進行調(diào)度控制。在PPMCRNER算法中，Allocate函數(shù)的功能為將當前生成的單模態(tài)單元子句集（子句列表）按照一定的策略分給某個分方法，用于并行執(zhí)行。算法中其余符號與PMCRNER算法中的符號含義相同。

4 實驗結(jié)果與分析

該部分擬采用隨機生成的標準模態(tài)子句集來對串行、全并行算法的性能進行測試。在進行實驗的過程中，發(fā)現(xiàn)同樣規(guī)模的標準模態(tài)子句集和命題邏輯子句集，在推理時其時間復雜度已經(jīng)差了好幾個數(shù)量級。因此，為了實驗?zāi)軌虍a(chǎn)生令人接受的有效結(jié)果，在隨機生成標準模態(tài)子句集時將標準模態(tài)子句中的必然算子的個數(shù)限制在3個以內(nèi)，而可能算子的個數(shù)與命題原子的個數(shù)不作限制。本文分別在可滿足的標準模態(tài)子句集和不可滿足的標準模態(tài)子句集上進行了大量的測試，隨機樣例有兩個參數(shù)＜N, K＞，其中N代表子句集中變量的個數(shù)，K代表子句的個數(shù)。實驗環(huán)境：Windows 8操作系統(tǒng)，i7-3770 CPU，8 GB RAM。

4.1 不可滿足子句集

本組對比實驗中，選取命題變量數(shù)為10，模態(tài)算子數(shù)任意的不可滿足標準模態(tài)子句集進行測試，結(jié)果如圖1所示。其中，圖（a）為串行算法和全并行算法的時間對比圖，橫軸為子句數(shù)，縱軸為CPU時間。圖（b）為全并行算法相對于串行算法的加速比。很明顯，隨著子句數(shù)的不斷增加，加速比呈不斷上升趨勢并且接近于3。

本組對比實驗中將命題變量數(shù)改為15，其余條件和設(shè)定同上組實驗一樣，結(jié)果如圖2所示。可以看出，該組對比實驗呈現(xiàn)出了與上組實驗相同的效果和趨勢?？梢哉J為，該算法對于不同規(guī)模的測試樣例是具有穩(wěn)定性的。

Fig.1 Experimental results of random problem＜10,K＞instances on unsatisfiable clause sets圖1 不可滿足子句集上隨機問題＜10,K＞用例測試結(jié)果

4.2 可滿足子句集

本組對比實驗里選取命題變量數(shù)為10，模態(tài)算子數(shù)任意的可滿足標準模態(tài)子句集進行測試，結(jié)果如圖3所示。其中，圖（a）為串行算法和全并行算法的時間對比圖，橫軸為子句數(shù)，縱軸為CPU時間。圖（b）為全并行算法相對于串行算法的加速比。可以看出，在測試數(shù)據(jù)為可滿足子句集的情況下，串行算法和全并行算法的效率差距不大，且略高于全并行算法。

同樣的，對于可滿足的標準模態(tài)子句集，增加測試數(shù)據(jù)的規(guī)模，將命題變量數(shù)增加到15，結(jié)果如圖4所示。可以看出，即使測試數(shù)據(jù)的規(guī)模增加，算法的對比結(jié)果仍然保持同樣的趨勢。算法對于可滿足的不同規(guī)模的測試數(shù)據(jù)是具有穩(wěn)定性的。

Fig.2 Experimental results of random problem＜15,K＞instances on unsatisfiable clause sets圖2 不可滿足子句集上隨機問題＜15,K＞用例測試結(jié)果

4.3 分析

本文對大量數(shù)據(jù)集進行了測試，分析結(jié)果如下：

（1）此類測試數(shù)據(jù)集具有代表性的通用benchmark較少，故采用隨機生成的策略來產(chǎn)生數(shù)據(jù)集。大量測試表明，隨機生成可滿足的標準模態(tài)子句集更容易。

（2）模態(tài)公式的推理時間復雜度遠遠超過了同規(guī)模的命題公式，子句個數(shù)一旦過大，推理的時間復雜度將以指數(shù)級別的增長趨勢達到讓人難以接受的程度。

（3）從大量測試數(shù)據(jù)來看，并行算法具有一定的適用性。事實上，并行算法并不是在所有的標準模態(tài)子句集上都比串行快，相反的，在某些特定的子句集上其性能略低于串行算法。在可滿足的標準模態(tài)子句集上，并行算法的執(zhí)行效率反而比串行算法慢。原因在于對可滿足的標準模態(tài)子句集進行推理的時候，大部分子句集在拆分子句列表的時候其中前一部分子句列表集合中就已經(jīng)出現(xiàn)可滿足的子句列表，那么并行算法的粗粒度并行并沒有得到真正執(zhí)行。相反的，并行算法真正實現(xiàn)的時候其復雜的線程之間的調(diào)度與通信往往是一筆不小的開銷，執(zhí)行效率反而有所降低。

（4）并行算法對于不可滿足的標準模態(tài)子句集具有穩(wěn)定的加速比，但無論分多少個任務(wù)并行，真正的加速比還是受限于CPU物理內(nèi)核的個數(shù)，其加速比能夠接近CPU物理內(nèi)核的個數(shù)。

（5）實驗表明，細粒度并行策略的加速比并不顯著。在實驗中，嘗試分別將粗粒度并行與細粒度并行進行分開實驗。事實上，全并行算法的加速比和只有粗粒度并行的版本相比，其加速程度并沒有明顯提高。細粒度并行的加速程度主要受限于單模態(tài)單元子句集中可能算子的個數(shù)，同時在粗粒度與細粒度同時并行的時候，其融合后的加速比受限于物理硬件。

Fig.3 Experimental results of random problem＜10,K＞instances on satisfiable clause sets圖3 可滿足子句集上隨機問題＜10,K＞用例測試結(jié)果

Fig.4 Experimental results of random problem＜15,K＞instances on satisfiable clause sets圖4 可滿足子句集上隨機問題＜15,K＞用例測試結(jié)果

5 結(jié)論與展望

本文提出了命題模態(tài)邏輯S5系統(tǒng)中一種新的基于擴展規(guī)則的標準模態(tài)子句集的串行推理算法和并行推理算法，并對其進行了大量的對比測試。實驗表明，PPMCRNER算法具有一定的適用性，在不可滿足的子句集中具有穩(wěn)定的加速比，在可滿足的子句集中加速效果并不明顯。

完備算法的時間復雜度較高，原因在于一旦標準模態(tài)子句中必然算子的個數(shù)增加，則整個子句集的推理時間復雜度的增加程度是難以接受的。此外完備算法中應(yīng)用規(guī)則時，標準模態(tài)子句中只有可能算子間的文字能夠進行合并，而必然算子間卻不允許，原因在于◇P∨◇Q?◇(P∨Q)成立，而□P∨□Q?□(P∨Q)卻不成立。因此可以在實際推理時先運行一個不完備的算法，思想是加強完備算法中的歸約規(guī)則，加入一條定理□P∨□Q→□(P∨Q)。運用此定理合并標準模態(tài)子句中的所有必然算子，將所有的標準模態(tài)子句全部變成最多只有一個必然算子和一個可能算子的子句，這樣推理的時間復雜度會大大降低。如果不完備算法返回不可滿足，則原公式也不可滿足；若不完備算法返回可滿足，則需要重新調(diào)用完備的算法來進行推理。

可以進一步研究并行算法的粗粒度并行策略，使得其對于可滿足的標準模態(tài)子句集也同樣具有穩(wěn)定的加速比。該問題的關(guān)鍵在于采用何種子句列表拆分策略使得各分線程在能夠“均勻”地處理子句列表的同時，線程之間的同步與通信的開銷不至于過大，這樣可以使得算法的加速性能得到進一步提升。

[1]Meghdad G.Distributed knowledge justification logics[J]. Theory of Computing Systems,2014,55(1):1-40.

[2]Zadeh L A.A note on modal logic and possibility theory[J]. Information Sciences,2014,279:908-913.

[3]Larsen K G,Mardare R.Complete proof systems for weighted modal logic[J].Theoretical Computer Science,2014,546: 164-175.

[4]French T,van der Hoek W,Iliev P,et al.On the succinctness of some modal logics[J].Artificial Intelligence,2013, 197:56-85.

[5]Wu Xia,Sun Jigui.Destructive extension rule in proposition modal logic K[C]//Proceedings of the 1st International Conference on Computational Methods,Singapore,Dec 15-17,2004:1087-1091.

[6]Schmidt R A.Developing modal tableaux and resolution methods via first-order resolution[C]//Proceedings of the 6th Conference on Advances in Modal Logic,Noosa,Australia,Sep 25-28,2006,6:1-26.

[7]Nalon C,Dixon C.Clausal resolution for normal modal logics[J].Journal ofAlgorithms,2007,62(3):117-134.

[8]Wu Xia,Yu Haihong,Li Zehai,et al.Relational extension rule[J].Journal of Jilin University:Science Edition,2008, 46(3):504-508.

[9]Benzmüller C,Raths T.HOL based first-order modal logic provers[C]//LNCS 8312:Proceedings of the 19th International Conference on Logic for Programming,Artificial Intelligence,and Reasoning,Stellenbosch,South Africa, Dec 14-19,2013.Berlin,Heidelberg:Springer,2013:127-136.

[10]Kaminski M,Tebbi T.InKreSAT:modal reasoning via incremental reduction to SAT[C]//LNCS 7898:Proceedings of the 24th International Conference on Automated Deduction,Lake Placid,USA,Jun 9-14,2013.Berlin,Heidelberg: Springer,2013:436-442.

[11]Rajeev G,Kerry O,Jimmy T.Implementing tableau calculi using BDDs:BDDTab system description[C]//LNCS 8562: Proceedings of the 7th International Joint Conference on Automated Reasoning,Vienna,Austria,Jul 19-22,2014.Berlin,Heidelberg:Springer,2014:337-343.

[12]Lin Hai,Sun Jigui,Zhang Yimin.Theorem proving based on the extension rule[J].Journal of Automated Reasoning, 2003,31(1):11-21.

[13]Sun Jigui,Li Ying,Zhu Xingjun,et al.A novel theorem proving algorithm based on extension rule[J].Journal of Computer Research and Development,2009,46(1):9-14.

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

[15]Li Ying,Sun Jigui,Wu Xia,et al.Extension rule algorithms based on IMOM and IBOHM heuristics strategies[J].Journal of Software,2009,20(6):1521-1527.

[16]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.

[17]Yin Minghao,Lin Hai,Sun Jigui.Solving#SAT using extension rules[J].Journal of Software,2009,20(7):1714-1725.

[18]Yin Minghao,Sun Jigui,Lin Hai,et al.Possibilistic extension rules for reasoning and knowledge compilation[J]. Journal of Software,2010,20(11):2826-2837.

[19]Liu Lei,Niu Dangdang,Lv Shuai.Knowledge compilation methods based on the hyper extension rule[J].Chinese Journal of Computers,2016,39(8):1681-1696.

[20]Zhou Beihai.Introduction to modal logic[M].Beijing:Peking University Press,1997.

附中文參考文獻：

[8]吳瑕,于海鴻,李澤海,等.關(guān)系擴展規(guī)則[J].吉林大學學報:理學版,2008,46(3):504-508.

[13]孫吉貴,李瑩,朱興軍,等.一種新的基于擴展規(guī)則的定理證明算法[J].計算機研究與發(fā)展,2009,46(1):9-14.

[15]李瑩,孫吉貴,吳瑕,等.基于IMOM和IBOHM啟發(fā)式策略的擴展規(guī)則算法[J].軟件學報,2009,20(6):1521-1527.

[16]賴永,歐陽丹彤,蔡敦波,等.基于擴展規(guī)則的模型計數(shù)與智能規(guī)劃方法[J].計算機研究與發(fā)展,2009,46(3):459-469.

[17]殷明浩，林海，孫吉貴.一種基于擴展規(guī)則的#SAT求解系統(tǒng)[J].軟件學報,2009,20(7):1714-1725.

[18]殷明浩，孫吉貴，林海,等.可能性擴展規(guī)則的推理和知識編譯[J].軟件學報,2010,21(11):2826-2837.

[19]劉磊,牛當當,呂帥.基于超擴展規(guī)則的知識編譯方法[J].計算機學報,2016,39(8):1681-1696.

[20]周北海.模態(tài)邏輯導論[M].北京:北京大學出版社,1997.

YANG Yang was born in 1992.He is an M.S.candidate at Jilin University.His research interests include intelligent planning,automated reasoning and cloud computing,etc.

楊洋（1992—），男，吉林大學碩士研究生，主要研究領(lǐng)域為智能規(guī)劃，自動推理，云計算等。

LI Guangli was born in 1992.He is an M.S.candidate at Jilin University.His research interests include automated reasoning,cloud computing and parallel programming,etc.

李廣力（1992—），男，吉林大學碩士研究生，主要研究領(lǐng)域為自動推理，云計算，并行編程等。

ZHANG Tongbo was born in 1995.He is a student at Jilin University.His research interests include automated reasoning,cloud computing and parallel programming,etc.

張桐搏（1995—），男，吉林大學學生，主要研究領(lǐng)域為自動推理，云計算，并行編程等。

LIU Lei was born in 1960.He received the M.S.degree in computer software from Jilin University in 1985.Now he is a professor and Ph.D.supervisor at Jilin University.His research interest is software theory and technology.

劉磊（1960—），男，吉林長春人，吉林大學教授、博士生導師，主要研究領(lǐng)域為軟件理論與技術(shù)。累計發(fā)表學術(shù)論文180余篇，主持國家自然科學基金等科研項目30余項。

LV Shuai was born in 1981.He received the Ph.D.degree in computer software and theory from Jilin University in 2010.Now he is an associate professor at Jilin University.His research interests include intelligent planning and automated reasoning,etc.

呂帥（1981—），男，吉林公主嶺人，2010年于吉林大學獲得博士學位，現(xiàn)為吉林大學副教授，主要研究領(lǐng)域為智能規(guī)劃，自動推理等。累計發(fā)表學術(shù)論文61篇，主持國家自然科學基金等科研項目7項，獲得全國商業(yè)科技進步一等獎2項、吉林省科學技術(shù)進步三等獎2項。

Parallel Reasoning Methods in Propositional Modal Logic S5*

YANG Yang1,LI Guangli1,ZHANG Tongbo1,LIU Lei1,LV Shuai1,2,3+
1.College of Computer Science and Technology,Jilin University,Changchun 130012,China
2.College of Mathematics,Jilin University,Changchun 130012,China
3.Key Laboratory of Symbolic Computation and Knowledge Engineering(Jilin University),Ministry of Education, Changchun 130012,China
+Corresponding author:E-mail:lus@jlu.edu.cn

S5 system is a special and important axiomatic system in propositional modal logic that has great ability of knowledge representation and processing,which is the basis of non-classical logics such as epistemic logic and belief logic etc.According to Kripke semantic model and part of the axioms in S5 system,this paper gives a more indepth research on the characteristics of propositional modal logic S5,and analyzes the features of a kind of representative formulae which is standard modal clauses,then proposes an NER-based algorithm called PMCRNER(propositional modal clausal reasoning based on novel extension rule)which is used to reason for standard modal clauses in propositional modal logic S5.In the view of high time complexity in simple algorithm,this paper uses the potential relevance between tasks to make the algorithm parallel in the degree of coarse-granularity and fine-granularity.This paper also gives the theoretical framework of PPMCRNER(parallel PMCRNER)and compares it with the basic algorithm.The experiments show that PPMCRNER has good speedup on unsatisfiable clause sets,and provides a feasible scheme for further research on the reasoning methods for modal formulae which are hard to solve.

propositional modal logic;S5 axiom system;parallel reasoning;extension rule

10.3778/j.issn.1673-9418.1509035

A

TP181

*The National Natural Science Foundation of China under Grant Nos.61300049,61502197,61503044(國家自然科學基金);the Specialized Research Fund for the Doctoral Program of Higher Education of China under Grant No.20120061120059(高等學校博士學科點專項科研基金).

Received 2015-09,Accepted 2015-11.

CNKI網(wǎng)絡(luò)優(yōu)先出版:2015-12-03,http://www.cnki.net/kcms/detail/11.5602.TP.20151203.0826.002.html