寧欣然，徐 揚，陳振頌

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

0 引言

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

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

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

1 背景知識

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

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

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

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

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

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

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

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

3 新型子句消去方法

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

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

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

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

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

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

表2 擴展的冗余性質(zhì)說明

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

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

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

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

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

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

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

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

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

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

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

3.2 新型子句消去方法

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

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

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

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

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

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

證明因為子句C基于文字l在子句集F中具有性質(zhì)BC+RS，所以子句C的所有l(wèi)-歸結(jié)式均具有性質(zhì)T或S，所有l(wèi)-歸結(jié)式均被F{C}蘊涵，子句C滿足蘊涵模歸結(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。因為BC+RS子句要求所有l(wèi)-歸結(jié)式具有性質(zhì)T或S，所以當子句C的所有l(wèi)-歸結(jié)式具有性質(zhì)T時，子句C也是BC+RS子句?？梢缘玫浇Y(jié)論，當一個子句是BC子句時，它也一定是BC+RS子句，然而當一個子句是BC+RS子句，它不一定是BC子句。例如在例2中，子句C是BC+RS子句，但它不是BC子句，因為其中一個l-歸結(jié)式a∨d∨e不具有性質(zhì)T。因此，BC子句集是BC+RS子句集的真子集。

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

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

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

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

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

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

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

證明若在子句集F中子句C是基于文字l的RHT子句，則子句C的所有l(wèi)-歸結(jié)式具有性質(zhì)HT。因為RS+RHT子句要求所有l(wèi)-歸結(jié)式具有性質(zhì)S或HT，所以當子句C的所有l(wèi)-歸結(jié)式具有性質(zhì)HT時，子句C也是RS+RHT子句。可以得到結(jié)論，當一個子句是RHT子句時，它也一定是RS+RHT子句，然而當一個子句是RS+RHT子句時，它不一定是RHT子句。例如在例3中，子句C是RS+RHT子句，但它不是RHT子句，因為其中一個l-歸結(jié)式a∨b不具有性質(zhì)HT。因此，RHT子句集是RS+RHT子句集的真子集。

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

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

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

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

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

4 實驗結(jié)果比較

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

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

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

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

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

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

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

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

5 結(jié)束語

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

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