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

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

2.吉林大學(xué) 數(shù)學(xué)學(xué)院，長(zhǎng)春 130012

3.符號(hào)計(jì)算與知識(shí)工程教育部重點(diǎn)實(shí)驗(yàn)室（吉林大學(xué)），長(zhǎng)春 130012

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

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

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

2.吉林大學(xué) 數(shù)學(xué)學(xué)院，長(zhǎng)春 130012

3.符號(hào)計(jì)算與知識(shí)工程教育部重點(diǎn)實(shí)驗(yàn)室（吉林大學(xué)），長(zhǎng)春 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)是一類(lèi)知識(shí)表示能力和處理能力都較強(qiáng)的模態(tài)公理系統(tǒng)，它是認(rèn)知邏輯、信念邏輯等非經(jīng)典邏輯理論的基礎(chǔ)。根據(jù)Kripke語(yǔ)義模型以及S5系統(tǒng)中部分公理，對(duì)命題模態(tài)邏輯S5公理系統(tǒng)的性質(zhì)進(jìn)行了較為深入的研究，并對(duì)S5系統(tǒng)中一類(lèi)具有代表性的標(biāo)準(zhǔn)模態(tài)子句集的特性進(jìn)行了分析，提出了一種基于擴(kuò)展規(guī)則方法的命題模態(tài)邏輯推理算法（propositional modal clausal reasoning based on novel extension rule，PMCRNER）。針對(duì)樸素算法時(shí)間復(fù)雜度較高的問(wèn)題，利用任務(wù)間潛在的關(guān)聯(lián)性對(duì)算法同時(shí)進(jìn)行了粗粒度與細(xì)粒度并行化，提出了并行算法PPMCRNER（parallel PMCRNER）理論框架，并且與基本算法進(jìn)行了對(duì)比。實(shí)驗(yàn)結(jié)果表明，PPMCRNER算法在不可滿(mǎn)足的子句集上的推理具有良好的加速比，為高時(shí)間復(fù)雜性的模態(tài)推理方法的進(jìn)一步研究提供了一種可行方案。

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

1 引言

近年來(lái)，多種以模態(tài)邏輯為基礎(chǔ)的復(fù)雜公理系統(tǒng)與框架被相繼提出[1-3]，關(guān)于模態(tài)邏輯甚至是更高階的邏輯知識(shí)表示形式的理論研究逐漸成為人們關(guān)注的熱點(diǎn)[4]。模態(tài)邏輯推理方法的研究是高階公理系統(tǒng)和框架的原型實(shí)現(xiàn)的基礎(chǔ)。自動(dòng)推理領(lǐng)域主流的推理方法為歸結(jié)方法、表推演方法和擴(kuò)展規(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)語(yǔ)言。

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

2 基礎(chǔ)知識(shí)

2.1 擴(kuò)展規(guī)則

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

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

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

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

命題模態(tài)邏輯公理系統(tǒng)在命題邏輯系統(tǒng)的基礎(chǔ)上進(jìn)行了擴(kuò)展，在保持系統(tǒng)推理結(jié)構(gòu)封閉的情況下加入了部分公理和規(guī)則。公理系統(tǒng)分為正規(guī)系統(tǒng)和非正規(guī)系統(tǒng)，通常對(duì)模態(tài)邏輯的正規(guī)系統(tǒng)進(jìn)行推理。常用的模態(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ì)。需要強(qiáng)調(diào)的是：S5系統(tǒng)是在T系統(tǒng)的基礎(chǔ)上添加了E公理而形成的[20]。命題模態(tài)邏輯推理是在特定的公理系統(tǒng)中對(duì)一組任意的命題模態(tài)公式進(jìn)行可滿(mǎn)足性判斷的過(guò)程。命題模態(tài)邏輯推理的過(guò)程比命題邏輯推理更復(fù)雜，因?yàn)樵趯?duì)模態(tài)公式進(jìn)行推理時(shí)不僅要考慮命題變量集的真值指派，還要考慮必然和可能算子導(dǎo)致的命題公式在Kripke可能世界模型中的世界轉(zhuǎn)移，所以如何對(duì)模態(tài)算子的處理是命題模態(tài)邏輯推理過(guò)程的核心，對(duì)于命題的部分，只需要考慮使用常規(guī)命題邏輯的推理方法即可。命題模態(tài)邏輯S5公理系統(tǒng)是一種有代表性的公理系統(tǒng)，它也是認(rèn)知邏輯和信念邏輯的基礎(chǔ)。在S5系統(tǒng)中，可以只保留一個(gè)模態(tài)算子，即必然算子□。在不同的邏輯中，該算子代表的含義也不盡相同。如在認(rèn)知邏輯中，該算子代表某智能體知道某個(gè)事件；而在信念邏輯中，該算子代表某個(gè)智能體相信某個(gè)事件。因此，研究該系統(tǒng)的推理方法對(duì)于更高級(jí)的認(rèn)知邏輯、信念邏輯和道義邏輯等推理方法的研究有著重要意義。

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

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

3.1 定義與引理

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

下面給出標(biāo)準(zhǔn)模態(tài)子句的定義：

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

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

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

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

因?yàn)镵系統(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)中，對(duì)在一個(gè)標(biāo)準(zhǔn)模態(tài)子句中具有相同可能算子前綴的模態(tài)文字進(jìn)行合并，便于后續(xù)處理。

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

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

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

（1）預(yù)處理

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

（2）合并

掃描經(jīng)過(guò)預(yù)處理的標(biāo)準(zhǔn)模態(tài)子句集，對(duì)子句中出現(xiàn)的形如◇P∨◇Q析取式進(jìn)行合并。注意，形如□P∨□Q的公式無(wú)法進(jìn)行合并，因?yàn)楹喜⒑蟮男问脚c原形式不保持Kripke語(yǔ)義等價(jià)，只合并可能算子。該操作同樣能夠在線(xiàn)性時(shí)間復(fù)雜度內(nèi)完成。

（3）拆分

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

（4）可滿(mǎn)足性判定

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

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

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

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

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

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

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

返回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ù)是判斷當(dāng)前合取公式是否為單模態(tài)單元子句集，如果是，則調(diào)用基于NER的單模態(tài)單元子句集求解算法SMRNER進(jìn)行求解，否則繼續(xù)進(jìn)行拆分，直到所有單模態(tài)單元子句集全部被處理。choose函數(shù)是在公式F1中任意選擇一個(gè)標(biāo)準(zhǔn)模態(tài)子句進(jìn)行拆分。

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

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

3.3 PPMCRNER算法

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

3.3.1 粗粒度并行

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

3.3.2 細(xì)粒度并行

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

3.3.3PMCRNER算法的并行化

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

在算法執(zhí)行之前，需要對(duì)公式集進(jìn)行預(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ù)組分別為標(biāo)記變量和標(biāo)記數(shù)組，用于主方法對(duì)子方法進(jìn)行調(diào)度控制。在PPMCRNER算法中，Allocate函數(shù)的功能為將當(dāng)前生成的單模態(tài)單元子句集（子句列表）按照一定的策略分給某個(gè)分方法，用于并行執(zhí)行。算法中其余符號(hào)與PMCRNER算法中的符號(hào)含義相同。

4 實(shí)驗(yàn)結(jié)果與分析

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

4.1 不可滿(mǎn)足子句集

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

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

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

4.2 可滿(mǎn)足子句集

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

同樣的，對(duì)于可滿(mǎn)足的標(biāo)準(zhǔn)模態(tài)子句集，增加測(cè)試數(shù)據(jù)的規(guī)模，將命題變量數(shù)增加到15，結(jié)果如圖4所示?？梢钥闯觯词箿y(cè)試數(shù)據(jù)的規(guī)模增加，算法的對(duì)比結(jié)果仍然保持同樣的趨勢(shì)。算法對(duì)于可滿(mǎn)足的不同規(guī)模的測(cè)試數(shù)據(jù)是具有穩(wěn)定性的。

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

4.3 分析

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

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

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

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

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

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

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

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

5 結(jié)論與展望

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

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

可以進(jìn)一步研究并行算法的粗粒度并行策略，使得其對(duì)于可滿(mǎn)足的標(biāo)準(zhǔn)模態(tài)子句集也同樣具有穩(wěn)定的加速比。該問(wèn)題的關(guān)鍵在于采用何種子句列表拆分策略使得各分線(xiàn)程在能夠“均勻”地處理子句列表的同時(shí)，線(xiàn)程之間的同步與通信的開(kāi)銷(xiāo)不至于過(guò)大，這樣可以使得算法的加速性能得到進(jì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.

附中文參考文獻(xiàn)：

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

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

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

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

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

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

[19]劉磊,牛當(dāng)當(dāng),呂帥.基于超擴(kuò)展規(guī)則的知識(shí)編譯方法[J].計(jì)算機(jī)學(xué)報(bào),2016,39(8):1681-1696.

[20]周北海.模態(tài)邏輯導(dǎo)論[M].北京:北京大學(xué)出版社,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—），男，吉林大學(xué)碩士研究生，主要研究領(lǐng)域?yàn)橹悄芤?guī)劃，自動(dòng)推理，云計(jì)算等。

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—），男，吉林大學(xué)碩士研究生，主要研究領(lǐng)域?yàn)樽詣?dòng)推理，云計(jì)算，并行編程等。

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—），男，吉林大學(xué)學(xué)生，主要研究領(lǐng)域?yàn)樽詣?dòng)推理，云計(jì)算，并行編程等。

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—），男，吉林長(zhǎng)春人，吉林大學(xué)教授、博士生導(dǎo)師，主要研究領(lǐng)域?yàn)檐浖碚撆c技術(shù)。累計(jì)發(fā)表學(xué)術(shù)論文180余篇，主持國(guó)家自然科學(xué)基金等科研項(xiàng)目30余項(xiàng)。

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年于吉林大學(xué)獲得博士學(xué)位，現(xiàn)為吉林大學(xué)副教授，主要研究領(lǐng)域?yàn)橹悄芤?guī)劃，自動(dòng)推理等。累計(jì)發(fā)表學(xué)術(shù)論文61篇，主持國(guó)家自然科學(xué)基金等科研項(xiàng)目7項(xiàng)，獲得全國(guó)商業(yè)科技進(jìn)步一等獎(jiǎng)2項(xiàng)、吉林省科學(xué)技術(shù)進(jìn)步三等獎(jiǎng)2項(xiàng)。

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(國(guó)家自然科學(xué)基金);the Specialized Research Fund for the Doctoral Program of Higher Education of China under Grant No.20120061120059(高等學(xué)校博士學(xué)科點(diǎn)專(zhuān)項(xiàng)科研基金).

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