寧欣然，徐 揚(yáng)，陳振頌

(1.西南民族大學(xué) 計(jì)算機(jī)科學(xué)與技術(shù)學(xué)院，四川 成都 610041；2.西南交通大學(xué) 系統(tǒng)可信性自動(dòng)驗(yàn)證國(guó)家地方聯(lián)合工程實(shí)驗(yàn)室，四川 成都 610031；3.武漢大學(xué) 土木建筑工程學(xué)院，湖北 武漢 430072)

0 引言

自動(dòng)推理是計(jì)算機(jī)科學(xué)和數(shù)理邏輯的一個(gè)交叉學(xué)科，基于命題邏輯的可滿足性問(wèn)題求解和基于一階邏輯的定理機(jī)器證明是自動(dòng)推理領(lǐng)域中重要且關(guān)鍵的研究?jī)?nèi)容，其本質(zhì)是將現(xiàn)實(shí)中的問(wèn)題轉(zhuǎn)化為命題邏輯公式或一階邏輯公式，通過(guò)遵循一定的邏輯推理規(guī)則，在邏輯層面判定現(xiàn)實(shí)問(wèn)題是否具有邏輯一致性。大量科學(xué)、技術(shù)、社會(huì)等問(wèn)題因具有抽象性、復(fù)雜性和規(guī)模性而無(wú)法實(shí)現(xiàn)人工邏輯推理與求解，需要采用人工智能手段之一——自動(dòng)演繹推理自動(dòng)地進(jìn)行邏輯推理與求解。當(dāng)今能夠較好地應(yīng)用自動(dòng)推理的領(lǐng)域包括軟硬件驗(yàn)證領(lǐng)域[19]、專家系統(tǒng)[20]、問(wèn)答系統(tǒng)[21]、語(yǔ)義網(wǎng)、知識(shí)圖譜等知識(shí)表示和知識(shí)推理領(lǐng)域[22-23]、人工智能中的模型推理研究領(lǐng)域[24]和數(shù)學(xué)定理證明[25-26]等。命題邏輯可滿足性問(wèn)題是邏輯學(xué)的一個(gè)基本問(wèn)題，是第一個(gè)被證明的NP完全問(wèn)題[28]，也是當(dāng)今計(jì)算機(jī)科學(xué)和人工智能研究的核心問(wèn)題。工程技術(shù)、軍事、工商管理、交通運(yùn)輸和自然科學(xué)研究中的許多重要問(wèn)題，如智能規(guī)劃、程控電話的自動(dòng)交換、大型數(shù)據(jù)庫(kù)維護(hù)、大規(guī)模集成電路自動(dòng)布線、軟件自動(dòng)開(kāi)發(fā)、機(jī)器人動(dòng)作規(guī)劃等，均可轉(zhuǎn)化為命題邏輯可滿足性問(wèn)題。

子句集化簡(jiǎn)一直是命題邏輯表示的可滿足性問(wèn)題求解方法重要的研究方向之一，在當(dāng)前主流的命題求解器中子句集化簡(jiǎn)是不可或缺的部分。子句消去方法是簡(jiǎn)化命題邏輯子句集非常重要的方法，通過(guò)刪除子句集中的冗余子句，可以簡(jiǎn)化子句集，加快命題邏輯可滿足性問(wèn)題求解器的求解速度，特別對(duì)于由現(xiàn)實(shí)問(wèn)題轉(zhuǎn)化而來(lái)的大規(guī)模命題邏輯可滿足性問(wèn)題，其子句集中包含有大量冗余子句，如果不進(jìn)行處理，則可能導(dǎo)致后續(xù)命題邏輯求解過(guò)程在錯(cuò)誤的路徑上打轉(zhuǎn)，大量浪費(fèi)時(shí)間和內(nèi)存，因此在求解初期對(duì)這些大規(guī)模問(wèn)題進(jìn)行簡(jiǎn)化具有重要的作用。在命題邏輯可滿足性問(wèn)題求解研究初期有一些簡(jiǎn)單的子句消去方法，例如Davis等[1]提出單元傳遞和純文字消去兩種簡(jiǎn)化規(guī)則，作為DPLL(Davis-Putnam-Logemann-Loverland)算法[1]回溯時(shí)唯一運(yùn)行的兩種規(guī)則沿用至今；包含消去(Subsumption Elimination，SE)被嵌入Kowalski連接圖中作為刪除原則[2]。隨后，出現(xiàn)了一些判定條件更加復(fù)雜但刪除子句范圍更廣的子句消去方法，例如2010年提出的封鎖子句消去方法(Blocked Clause Elimination，BCE)[3]，作為命題邏輯可滿足性問(wèn)題求解器的預(yù)處理器，在極大地減少原始命題邏輯子句集規(guī)模的同時(shí)加快了命題邏輯可滿足性問(wèn)題求解器的求解速度；同年，Heule等[4]將隱藏和不對(duì)稱概念與著名的子句消去方法——恒真消去方法和包含消去方法結(jié)合，發(fā)展出新型子句消去方法，包括隱藏恒真消去(Hidden Tautology Elimination，HTE)[4]、隱藏包含消去(Hidden Subsumption Elimination，HSE)[4]、不對(duì)稱恒真消去(Asymmetric Tautology Elimination，ATE)[4]、不對(duì)稱包含消去(Asymmetric Subsumption Elimination，ASE)[4]，并分別探討了這些子句消去方法的規(guī)模約簡(jiǎn)能力、布爾約束傳播保持性、約簡(jiǎn)一致性和邏輯等價(jià)性；2012年，Javisalo等[5]再次將歸結(jié)與文獻(xiàn)[4]方法結(jié)合，進(jìn)一步發(fā)展出新型子句消去方法，包括歸結(jié)包含消去(Resolution Subsumption Elimination, RSE)[5]、歸結(jié)隱藏包含消去(Resolution Hidden Subsumption Elimination, RHSE)[5]、歸結(jié)不對(duì)稱包含消去(Resolution Asymmetric Subsumption Elimination, RASE)[5]、歸結(jié)隱藏恒真消去(Resolution Hidden Tautology Elimination, RHTE)[5]和歸結(jié)不對(duì)稱恒真消去(Resolution Asymmetric Tautology Elimination, RATE)[5]。

2017年，Kiesl等[6]將量化布爾公式上的量化蘊(yùn)涵外部歸結(jié)式[18]提升到一階邏輯上，提出一階邏輯上的蘊(yùn)涵模歸結(jié)(Implication Modulo Resolution, IMR)原則，通過(guò)該原則將一些命題邏輯上的子句消去方法提升到一階邏輯上，并給出可行性證明。該文獻(xiàn)將IMR原則降到命題邏輯上，提出適應(yīng)命題邏輯層面的IMR原則，即在子句集F中，若子句C基于其中的一個(gè)文字，得到的所有歸結(jié)式都被F{C}中的子句所蘊(yùn)涵，則稱該子句滿足IMR原則。那些看似毫無(wú)關(guān)聯(lián)的命題邏輯子句消去方法BCE，RSE，RHSE，RHTE等均在IMR原則之下，因而能將這些子句消去方法進(jìn)行結(jié)合推廣，形成新型命題邏輯子句消去方法(BC+RS)E，(RS+RHT)E和(RHS+RHT)E，并給出可行性證明。此外在不同時(shí)間限制內(nèi)，將(BC+RS)E，(RS+RHT)E，(RHS+RHT)E與著名的子句消去方法BCE進(jìn)行實(shí)驗(yàn)對(duì)比，結(jié)果表明：化簡(jiǎn)子句數(shù)量龐大且結(jié)構(gòu)復(fù)雜的子句集時(shí)規(guī)定的時(shí)間越長(zhǎng)，新型子句消去方法對(duì)化簡(jiǎn)子句集的效果越好。在同樣的限定時(shí)間中，當(dāng)子句消去方法的判定條件難易程度和時(shí)間復(fù)雜度達(dá)到平衡時(shí)，子句消去方法的化簡(jiǎn)能力最好；當(dāng)化簡(jiǎn)比較簡(jiǎn)單的命題邏輯子句集時(shí)，有效性越高的新型子句消去方法化簡(jiǎn)子句集的能力越強(qiáng)，且均優(yōu)于BCE方法。

1 背景知識(shí)

2 命題邏輯上的蘊(yùn)涵模歸結(jié)原則

Kiesl等[6]在2017年將量化布爾公式上的量化蘊(yùn)涵外部歸結(jié)式[18]提升到了一階邏輯上，提出一階邏輯上的蘊(yùn)涵模歸結(jié)原則。本文認(rèn)為該原則同樣可以降到命題邏輯上，在該原則框架下提出新型命題邏輯子句消去方法，并保證這些子句消去方法在命題邏輯上具有可行性。本章主要介紹延伸到命題邏輯上的蘊(yùn)涵模歸結(jié)原則。

定義2設(shè)在子句集F中，若子句C基于文字l(l∈C)與F中的子句歸結(jié)，得到的所有歸結(jié)式都被F{C}蘊(yùn)涵，則稱子句C是基于l上的蘊(yùn)涵模歸結(jié)子句，滿足蘊(yùn)涵模歸結(jié)原則。

蘊(yùn)涵模歸結(jié)子句的一個(gè)特例是子句C中含有純文字l，因?yàn)閘是純文字，子句集中沒(méi)有文字能夠與l歸結(jié)，所以沒(méi)有l(wèi)-歸結(jié)式，這樣的子句C是比較特殊的蘊(yùn)涵模歸結(jié)子句。下面的例子展示的是更為一般的蘊(yùn)涵模歸結(jié)子句。

蘊(yùn)涵模歸結(jié)子句是冗余的，即刪除滿足這樣條件的子句不會(huì)影響到子句集本身的不可滿足性或是可滿足性。在證明蘊(yùn)涵模歸結(jié)子句的冗余性之前先證明一個(gè)引理。

引理1設(shè)子句C是子句集F中基于l(l∈C)上的一個(gè)蘊(yùn)涵模歸結(jié)子句，指派α滿足F{C}中的所有子句，但是弄假子句C。通過(guò)翻轉(zhuǎn)指派α對(duì)文字l的賦值，保持其他賦值不變，得到指派α′，則指派α′不僅滿足子句C，還滿足F{C}中所有子句。

定理1設(shè)子句C是子句集F中的蘊(yùn)涵模歸結(jié)子句，則子句C在子句集F中是冗余的。

證明從引理1可知，若F{C}在一個(gè)指派α下是可滿足的，則一定可以找到一個(gè)指派α′，F(xiàn)在α′下是可滿足的。因此F和F{C}是等價(jià)滿足的。綜上，子句C在子句集F中是冗余的。

3 新型子句消去方法

本章討論命題邏輯上已有的具有蘊(yùn)涵性質(zhì)的子句消去方法，并說(shuō)明這些子句消去方法能夠在蘊(yùn)涵模歸結(jié)原則的框架下進(jìn)行組合推廣，形成新型子句消去方法。

3.1 具有蘊(yùn)涵性質(zhì)的子句

2010年，Heule等[4]基于子句的冗余性質(zhì)提出多種子句消去方法，這些冗余子句看似相互獨(dú)立，并不關(guān)聯(lián)，實(shí)際上均具有蘊(yùn)涵性質(zhì)。本節(jié)證明這些這些冗余子句均具有蘊(yùn)涵性質(zhì)，為3.2節(jié)提出新型子句消去方法做準(zhǔn)備。表1所示為子句的各類冗余性質(zhì)[4]。

表1 子句的冗余性質(zhì)說(shuō)明

表1中的冗余性質(zhì)有效性的高低如圖1所示。圖中箭頭含義為，若性質(zhì)A指向性質(zhì)B，則表示性質(zhì)A比性質(zhì)B更為有效。換言之，若一個(gè)子句具有性質(zhì)B，則其一定具有性質(zhì)A。

在Heule等[4]提出表1中所展示的子句冗余性質(zhì)后，Jarvisalo等[5]提出冗余性質(zhì)的拓展概念，其將歸結(jié)原則R置于表1中各類冗余性質(zhì)的前面，得到的性質(zhì)仍然是冗余性質(zhì)。簡(jiǎn)而言之，基于冗余性質(zhì)P，子句消去方法PE(PE為刪除子句集中具有性質(zhì)P子句的子句消去方法)具有可靠性，則基于性質(zhì)RP，性質(zhì)RP是冗余性質(zhì)，且子句消去方法RPE(RPE為刪除子句集中具有性質(zhì)RP子句的子句消去方法)具有可靠性。根據(jù)表1中的冗余性質(zhì)，擴(kuò)展的冗余性質(zhì)如表2所示。

表2 擴(kuò)展的冗余性質(zhì)說(shuō)明

表2中的冗余性質(zhì)有效性如圖2所示[4]。

具有表1冗余性質(zhì)的子句均具有蘊(yùn)涵性質(zhì)(被F{C}蘊(yùn)涵)。當(dāng)子句C被F{C}包含，則其一定被F{C}蘊(yùn)涵；子句C是恒真式時(shí)，也被F{C}蘊(yùn)涵。下面證明當(dāng)ALA(F,C)和HLA(F,C)具有蘊(yùn)涵性質(zhì)時(shí)，子句C也具有蘊(yùn)涵性質(zhì)。

引理2設(shè)文字l是子句集F中子句C的不對(duì)稱文字，則有F{C}(C≡C∨l)。

定理2設(shè)子句C是子句集F中的子句，若ALA(F,C)被F{C}蘊(yùn)涵，則子句C被F{C}蘊(yùn)涵。

證明假設(shè)子句D=ALA(F,C)，則存在一個(gè)序列l(wèi)1,…,ln，其中l(wèi)i是F{C}中子句的文字，li是C∨l1∨…∨li-1的不對(duì)稱文字，且C∨l1∨…∨ln=D。通過(guò)重復(fù)應(yīng)用引理2，有F{C}(C≡C∨l1∨…∨ln)。因?yàn)锳LA(F,C)被F{C}蘊(yùn)涵，F(xiàn){C}(C∨l1∨…∨ln)，F(xiàn){C}C，所以C被F{C}蘊(yùn)涵。

定理3設(shè)子句C是子句集F中的子句，若HLA(F,C)被F{C}蘊(yùn)涵，則子句C被F{C}蘊(yùn)涵。

證明隱藏文字增加可以看作為不對(duì)稱文字增加的特例，即每一個(gè)提供不對(duì)稱文字的子句均為二元子句。從定理2得知，若ALA(F,C)被F{C}蘊(yùn)涵，則子句C被F{C}蘊(yùn)涵。HLA(F,C)作為ALA(F,C)的特例，同樣滿足定理2，因此若HLA(F,C)被F{C}蘊(yùn)涵，則子句C被F{C}蘊(yùn)涵。

定理4若在子句集F中子句C是隱藏包含子句HS或者不對(duì)稱包含子句AS，則子句C被F{C}蘊(yùn)涵。

證明設(shè)子句C是AS，則子句C的ALA(F,C)子句被F{C}包含，且被F{C}蘊(yùn)涵。根據(jù)定理2，子句C被F{C}蘊(yùn)涵。當(dāng)子句C是HS時(shí)，子句C的HLA(F,C)子句被F{C}包含；當(dāng)HLA(F,C)子句被F{C}包含時(shí)，HLA(F,C)子句被F{C}蘊(yùn)涵。根據(jù)定理3，子句C被F{C}蘊(yùn)涵。綜上，若在子句集F中子句C是隱藏包含子句HS或者不對(duì)稱包含子句AS，則子句C被F{C}蘊(yùn)涵。

定理5若在子句集F中子句C是隱藏恒真子句HT或者不對(duì)稱恒真子句AT，則子句C被F{C}蘊(yùn)涵。

證明設(shè)子句C是HT子句，則子句C的HLA(F,C)子句是恒真式，被F{C}蘊(yùn)涵。根據(jù)定理3，子句C也被F{C}蘊(yùn)涵。若子句C是AT子句，則子句C的ALA(F,C)子句是恒真式，被F{C}蘊(yùn)涵。根據(jù)定理2，子句C被F{C}蘊(yùn)涵。綜上，若在子句集F中子句C是隱藏包含子句HT或者不對(duì)稱包含子句AT，則子句C被F{C}蘊(yùn)涵。

3.2 新型子句消去方法

從3.1節(jié)可知，當(dāng)子句集F中子句C滿足冗余性質(zhì)S，HS，AS，T，HT或AT時(shí)，子句C被F{C}蘊(yùn)涵。蘊(yùn)涵模歸結(jié)原則要求子句C′的所有l(wèi)-歸結(jié)式均被F{C}蘊(yùn)涵，又因?yàn)樽泳銫′的每一個(gè)l-歸結(jié)式滿足性質(zhì)S，HS，AS，T，HT或AT，根據(jù)定理4和定理5可知子句C′的每一個(gè)l-歸結(jié)式都被F{C}蘊(yùn)涵，所以若子句C′的每一個(gè)l-歸結(jié)式滿足性質(zhì)S，HS，AS，T，HT或AT，則C′滿足蘊(yùn)涵模歸結(jié)原則，在子句集F中是冗余的。

定義3設(shè)子句C是子句集F中的子句，且文字l∈C。若子句C共有m個(gè)l-歸結(jié)式R1,…,Rm，且滿足2個(gè)條件：①每一個(gè)Ri(1≤i≤m)具有性質(zhì)Pj∈{P1,P2,…,Pn}；②性質(zhì)Pi(1≤i≤n)滿足“若一個(gè)子句C′具有性質(zhì)Pi，則該子句具有蘊(yùn)涵性質(zhì)”。則稱子句C擁有性質(zhì)RP1+RP2+…+RPn。

定理6若在子句集F中子句C基于文字l∈C，具有性質(zhì)RP1+RP2+…+RPn，則子句C是子句集F中的冗余子句。

證明設(shè)子句C在子句集F中基于l∈C共有m個(gè)l-歸結(jié)式R1,…,Rm。因?yàn)樽泳銫在子句集F中具有性質(zhì)RP1+RP2+…+RPn，所以對(duì)于任意Ri(1≤i≤m)，有性質(zhì)Pj∈{P1,P2,…,Pn}。又因?yàn)樾再|(zhì)Pi(1≤i≤n)滿足“若一個(gè)子句C′具有性質(zhì)Pi，則該子句具有蘊(yùn)涵性質(zhì)”，所以子句C的所有l(wèi)-歸結(jié)式均具有蘊(yùn)涵性質(zhì)，根據(jù)蘊(yùn)涵模歸結(jié)原則，子句C被F{C}蘊(yùn)涵，從而可得子句C在子句集F中是冗余的。得證。

下面介紹3種有效的新型組合推廣子句消去方法，并證明這些新型組合推廣子句消去方法比原始子句消去方法更有效。

定理7若在子句集F中，基于l∈C，子句C具有性質(zhì)BC+RS，則子句C在子句集F中是冗余的。

證明因?yàn)樽泳銫基于文字l在子句集F中具有性質(zhì)BC+RS，所以子句C的所有l(wèi)-歸結(jié)式均具有性質(zhì)T或S，所有l(wèi)-歸結(jié)式均被F{C}蘊(yùn)涵，子句C滿足蘊(yùn)涵模歸結(jié)原則，子句C在子句集F中是冗余的。

由于(BC+RS)E刪除了子句集中的BC+RS子句集，而RSE和BCE分別刪除的是子句集中的RS和BC子句集，只需證明BC子句集和RS子句集是BC+RS子句集的真子集，即可證明(BC+RS)E比RSE和BCE更有效。

命題1BC子句集是BC+RS子句集的真子集。

證明若在子句集F中子句C是基于文字l的BC子句，則子句C的所有l(wèi)-歸結(jié)式具有性質(zhì)T。因?yàn)锽C+RS子句要求所有l(wèi)-歸結(jié)式具有性質(zhì)T或S，所以當(dāng)子句C的所有l(wèi)-歸結(jié)式具有性質(zhì)T時(shí)，子句C也是BC+RS子句?？梢缘玫浇Y(jié)論，當(dāng)一個(gè)子句是BC子句時(shí)，它也一定是BC+RS子句，然而當(dāng)一個(gè)子句是BC+RS子句，它不一定是BC子句。例如在例2中，子句C是BC+RS子句，但它不是BC子句，因?yàn)槠渲幸粋€(gè)l-歸結(jié)式a∨d∨e不具有性質(zhì)T。因此，BC子句集是BC+RS子句集的真子集。

命題2RS子句集是BC+RS子句集的真子集。

定理8若在子句集F中，基于l∈C，子句C具有性質(zhì)RS+RHT，則子句C在子句集F中是冗余的。

證明因?yàn)樽泳銫基于文字l在子句集F中具有性質(zhì)RS+RHT，所以子句C的所有l(wèi)-歸結(jié)式均具有性質(zhì)S或HT，所有l(wèi)-歸結(jié)式均被被F{C}蘊(yùn)涵，子句C滿足蘊(yùn)涵模歸結(jié)原則，子句C在子句集F中是冗余的。

同樣地，子句消去方法(RS+RHT)E比子句消去方法RSE和RHTE更為有效，即在同一個(gè)子句集F中相比刪除的子句數(shù)，(RS+RHT)E比RSE和RHTE相同或者更多。命題3和命題4充分解釋了這一點(diǎn)。

命題3RS子句集是RS+RHT子句集的真子集。

證明若在子句集F中子句C是基于文字l的RS子句，則子句C的所有l(wèi)-歸結(jié)式具有性質(zhì)S。因?yàn)镽S+RHT子句要求所有l(wèi)-歸結(jié)式具有性質(zhì)S或HT，所以當(dāng)子句C的所有l(wèi)-歸結(jié)式具有性質(zhì)S時(shí)，子句C也是RS+RHT子句?？梢缘玫浇Y(jié)論，當(dāng)一個(gè)子句是RS子句時(shí)，也一定是RS+RHT子句，然而當(dāng)一個(gè)子句是RS+RHT子句時(shí)，它不一定是RS子句。例如在例3中，子句C是RS+RHT子句，但它不是RS子句，因?yàn)槠渲幸粋€(gè)l-歸結(jié)式a∨c不具有性質(zhì)S。因此，RS子句集是RS+RHT子句集的真子集。

命題4RHT子句集是RS+RHT子句集的真子集。

證明若在子句集F中子句C是基于文字l的RHT子句，則子句C的所有l(wèi)-歸結(jié)式具有性質(zhì)HT。因?yàn)镽S+RHT子句要求所有l(wèi)-歸結(jié)式具有性質(zhì)S或HT，所以當(dāng)子句C的所有l(wèi)-歸結(jié)式具有性質(zhì)HT時(shí)，子句C也是RS+RHT子句?？梢缘玫浇Y(jié)論，當(dāng)一個(gè)子句是RHT子句時(shí)，它也一定是RS+RHT子句，然而當(dāng)一個(gè)子句是RS+RHT子句時(shí)，它不一定是RHT子句。例如在例3中，子句C是RS+RHT子句，但它不是RHT子句，因?yàn)槠渲幸粋€(gè)l-歸結(jié)式a∨b不具有性質(zhì)HT。因此，RHT子句集是RS+RHT子句集的真子集。

定理9若在子句集F中，基于l∈C，子句C具有性質(zhì)RHS+RHT，則子句C在子句集F中是冗余的。

證明因?yàn)樽泳銫基于文字l在子句集F中具有性質(zhì)RHS+RHT，所以子句C的所有l(wèi)-歸結(jié)式均具有性質(zhì)HS或HT，所有l(wèi)-歸結(jié)式均被F{C}蘊(yùn)涵，子句C滿足蘊(yùn)涵模歸結(jié)原則，子句在子句集F中是冗余的。

(RHS+RHT)E子句消去方法也不例外，它同樣比其原始子句消去方法RHSE和RHTE更有效。命題5和命題6證明了這一點(diǎn)。

命題5RHS子句集是RHS+RHT子句集的真子集。

命題6RHT子句集是RHS+RHT子句集的真子集。

4 實(shí)驗(yàn)結(jié)果比較

在規(guī)定的不同時(shí)間內(nèi)，比較(BC+RS)E，(RHS+RHT)E，(RS+RHT)E 3種子句消去方法與現(xiàn)有的子句消去方法BCE化簡(jiǎn)子句集的能力。雖然在理論上，子句消去方法(BC+RS)E，(RHS+RHT)E，(RS+RHT)E均能在同一個(gè)子句集中刪除更多的子句，比現(xiàn)有的BCE方法更有效，但是在具體實(shí)現(xiàn)上，這些子句消去方法的判定條件更復(fù)雜，時(shí)間復(fù)雜度更高，因此在規(guī)定的時(shí)間內(nèi)不一定能比BCE刪除更多的子句數(shù)。實(shí)驗(yàn)分為兩部分：①針對(duì)由規(guī)劃問(wèn)題轉(zhuǎn)化而來(lái)的子句數(shù)量大且結(jié)構(gòu)復(fù)雜的命題邏輯可滿足性問(wèn)題，測(cè)試這4種子句消去方法的化簡(jiǎn)能力；②針對(duì)簡(jiǎn)單隨機(jī)生成的命題邏輯可滿足性問(wèn)題，測(cè)試這4種子句消去方法的化簡(jiǎn)能力。

自從1992年Kautz等[29-30]首次將規(guī)劃問(wèn)題求解轉(zhuǎn)化為命題邏輯可滿足性問(wèn)題求解，所建成的black-box規(guī)劃系統(tǒng)(該規(guī)劃系統(tǒng)是將規(guī)劃問(wèn)題轉(zhuǎn)化為命題邏輯可滿足性問(wèn)題進(jìn)行求解)在第一屆智能規(guī)劃系統(tǒng)比賽中獲得第一名后[31]，越來(lái)越多的規(guī)劃問(wèn)題被轉(zhuǎn)化為命題邏輯可滿足性問(wèn)題進(jìn)行求解。然而，由于規(guī)劃問(wèn)題為大規(guī)模問(wèn)題，對(duì)轉(zhuǎn)化后的命題邏輯子句集進(jìn)行子句集化簡(jiǎn)，以提高后續(xù)命題邏輯可滿足性問(wèn)題求解器的求解效率，是非常重要的一環(huán)。在實(shí)驗(yàn)的第①部分選取由規(guī)劃問(wèn)題轉(zhuǎn)化而來(lái)的命題子句集，測(cè)試這些新型子句消去方法對(duì)這類特殊命題邏輯子句集化簡(jiǎn)是否有效。

實(shí)驗(yàn)第①部分選取SATLib標(biāo)準(zhǔn)庫(kù)(https://www.cs.ubc.ca/～hoos/SATLIB/benchm.html)中所有由現(xiàn)實(shí)規(guī)劃問(wèn)題轉(zhuǎn)化來(lái)的命題邏輯可滿足性問(wèn)題，共有11個(gè)，其平均子句數(shù)為23 261.27個(gè)。因?yàn)檫@些子句集子句數(shù)量龐大，無(wú)法在短時(shí)間內(nèi)找出子句集中所有相關(guān)的冗余子句，所以將時(shí)間分別限定為0.5 min，1 min，2 min，3 min，4 min，5 min，6 min，7 min，8 min，9 min，10 min，對(duì)比各種子句消去方法刪除這11個(gè)可滿足性問(wèn)題的平均冗余子句數(shù)，實(shí)驗(yàn)結(jié)果如圖3所示。

由圖3可見(jiàn)，隨著限定時(shí)間的增加，各類子句消去方法刪除子句的平均數(shù)逐漸上升。BCE方法的判定條件最簡(jiǎn)單，能夠在較短時(shí)間內(nèi)找到子句集中所有的BC子句，然而由于有效性最低，當(dāng)限定時(shí)間超過(guò)4 min時(shí)，其刪除的BC子句便基本不再增加。雖然理論上(RHS+RHT)E的有效性在4種子句消去方法中最高，但是因?yàn)槠鋾r(shí)間復(fù)雜度最高，因此檢測(cè)到單個(gè)RHS+RHT子句的時(shí)間最高，所以在限定時(shí)間內(nèi)刪除的平均子句數(shù)量反而最少。(BC+RS)E和(RS+RHT)E方法的有效性和判定條件的難易程度處于4種子句消去方法的中等水平，其表現(xiàn)最好。當(dāng)限定時(shí)間在2 min內(nèi)時(shí)，這兩種方法比BCE刪除的平均子句數(shù)少，但在2 min后，刪除的平均子句數(shù)遠(yuǎn)遠(yuǎn)超過(guò)BCE方法。

從實(shí)驗(yàn)結(jié)果可知，這些新型子句消去方法化簡(jiǎn)由規(guī)劃問(wèn)題轉(zhuǎn)化而來(lái)的命題邏輯可滿足性問(wèn)題是有效的，當(dāng)化簡(jiǎn)時(shí)間為10 min時(shí)，(BC+RHS)E和(RS+RHT)E方法刪除的命題邏輯子句集平均超過(guò)600個(gè)子句，能夠較好地化簡(jiǎn)由規(guī)劃問(wèn)題轉(zhuǎn)化而來(lái)的命題邏輯可滿足性問(wèn)題。

實(shí)驗(yàn)第②部分是測(cè)試4種子句消去方法化簡(jiǎn)隨機(jī)生成的130個(gè)命題邏輯可滿足性問(wèn)題的能力。其中30個(gè)命題邏輯可滿足性問(wèn)題包含100個(gè)子句、40個(gè)變量，另100個(gè)命題邏輯可滿足性問(wèn)題包含500個(gè)子句、200個(gè)變量。由于這130個(gè)命題邏輯可滿足性問(wèn)題比較簡(jiǎn)單，4種子句消去方法均能在較短時(shí)間內(nèi)找到所有冗余子句。表3所示為4種子句消去方法刪除130個(gè)問(wèn)題子句的平均數(shù)。

表3 各子句消去方法刪除子句的平均數(shù)

從表3可見(jiàn)，3種新型子句消去方法化簡(jiǎn)較為簡(jiǎn)單的命題邏輯子句集的能力均比BCE方法更強(qiáng)。一般來(lái)說(shuō)，子句消去方法的有效性越高，能夠刪除的平均數(shù)量越多，但是并不是所有子句消去方法都滿足這一規(guī)律。例如，(RHS+RHT)E比(RS+RHT)E更為有效，但是(RHS+RHT)E刪除的平均數(shù)反而比(RS+RHT)E更少，原因在于這3種新型子句消去方法均不具有confluence性質(zhì)，即刪除子句的順序不同，導(dǎo)致最后能夠刪除的子句數(shù)量可能不同。實(shí)驗(yàn)依次簡(jiǎn)單地判斷子句集中的子句是否為冗余子句，是則刪除該子句，否則保留該子句，然后繼續(xù)判斷下一個(gè)子句。

5 結(jié)束語(yǔ)

本文將一階邏輯上的蘊(yùn)涵模歸結(jié)原則擴(kuò)展到命題邏輯上，根據(jù)該原則將已有命題邏輯上的子句消去方法進(jìn)行組合推廣，提出比原始子句消去方法更有效的新型子句消去方法，并證明了這些新型子句消去方法的可行性，即利用這些子句消去方法化簡(jiǎn)子句集，得到的新子句集和原始子句集具有等價(jià)滿足關(guān)系，即新子句集與原始子句集同時(shí)具有可滿足性或者不可滿足性。最后，將新型子句消去方法(BC+RS)E,(RS+RHT)E，(RHS+RHT)E與著名的BCE方法進(jìn)行實(shí)驗(yàn)分析和比較，得到：當(dāng)化簡(jiǎn)由規(guī)劃問(wèn)題轉(zhuǎn)化而來(lái)的子句數(shù)量龐大的命題邏輯可滿足性問(wèn)題時(shí)，隨著限定時(shí)間的增加，各種子句消去方法刪除的子句平均數(shù)據(jù)均在增大。在這4種子句消去方法中，表現(xiàn)最好的是(RS+RHT)E和(BC+RS)E方法，其能較好地平衡判定條件的復(fù)雜度和有效性，在限定時(shí)間為10 min時(shí)，能夠平均刪除由規(guī)劃問(wèn)題轉(zhuǎn)化而來(lái)的命題邏輯子句集超過(guò)600個(gè)子句，這兩種子句消去方法對(duì)化簡(jiǎn)由規(guī)劃問(wèn)題轉(zhuǎn)化而來(lái)的命題邏輯子句集是有效的；在化簡(jiǎn)較為簡(jiǎn)單的命題邏輯可滿足性問(wèn)題子句集上，3種新型子句消去方法均比BCE方法更強(qiáng)，而且子句消去方法的有效性越高，刪除子句的平均數(shù)越多。

本文只初步實(shí)現(xiàn)了各類子句消去方法，這些方法不具有confluence性質(zhì)，如果刪除子句的順序不同，則最后得到的新子句差別會(huì)很大，本文算法只簡(jiǎn)單地按照子句集中子句的順序依次判斷子句是否為冗余子句，因此算法仍有很大的改進(jìn)空間。未來(lái)研究將根據(jù)這些子句消去方法的特性制定相應(yīng)的優(yōu)化策略，進(jìn)一步提高子句消去方法針對(duì)子句數(shù)量較大和結(jié)構(gòu)較復(fù)雜子句集的化簡(jiǎn)能力，以期將這些子句消去方法作為命題邏輯可滿足性問(wèn)題求解器的預(yù)處理方法來(lái)簡(jiǎn)化子句集，使后面的求解更加高效。