命題邏輯中一類擴展子句消去方法

劉凌榮, 陳樹偉*, 吳貫鋒

(1. 西南交通大學 數學學院, 四川 成都 610031; 2. 系統可信性自動驗證國家地方聯合工程實驗室, 四川 成都 610031)

1 預備知識

子句集的簡化是命題邏輯可滿足性判定的重要研究方向,研究子句集冗余性質能提高求解器的求解能力和效率,可滿足性判定過程中刪除冗余子句，已被國內外學者廣泛研究[1-4].目前，命題邏輯子句集的冗余性質的研究主要分為2種[5]:基于邏輯等價的冗余性質和基于可滿足性等價的冗余性質.

早期基于邏輯等價的冗余子句的消去方法主要有恒真消去[6](tautology elimination)和包含消去[7](subsume elimination).Heule等[8]將隱藏和不對稱概念與恒真和包含概念結合,提出了一系列邏輯等價的冗余子句消去方法,其中包括隱藏恒真子句消去方法(hidden tautology elimination,HTE)、不對稱恒真子句消去方法(asymmetric tautology elimination,ATE)、隱藏包含子句消去方法(hidden subsumption elimination,HSE)和不對稱包含子句消去方法(asymmetric subsumption elimination,ASE).

相比于基于邏輯等價的冗余性子句消去方法,可滿足性等價的冗余性子句消去方法有更強的能力簡化子句集.Jarvisalo等[9]提出了封鎖子句消去方法(blocked clause elimination,BCE),該方法被嵌入到求解器預處理中,極大地簡化了原始子句集,提高了求解器的求解效率.同年,Heule等[10]將封鎖子句推廣,提出了覆蓋子句消去方法(covered clause elimination,CCE).Jarvisalo等[11]將歸結原則和文獻[8]中的冗余性質結合,發現若歸結原則前置后,基于子句C的某個文字l的所有歸結式都具冗余性質P,那么稱子句C具性質RP,且性質RP仍然是冗余的,并且基于子句C的所有l-歸結式都具有AT性質(即C具有RAT性質),廣泛存在于求解器中作為預處理的一部分.Kiesl等[12]提出了集合封鎖和語義封鎖,該方法將封鎖子句進一步推廣,對于指派翻轉也由一個文字演變為多個文字.Heule等[13]提出了傳播冗余,該方法通過翻轉子句的封鎖指派來判斷子句的冗余性.Heule等[14]利用傳播冗余性質提出了SDCL(satisfaction-driven clause learning)求解框架.寧欣然等[15]將Kiesl等[16]提出的一階邏輯上的蘊涵模歸結合一原則降到命題邏輯,提出了基于命題邏輯的蘊涵模歸結理論的子句消去方法,該方法的求解效率和求解能力均強于封鎖子句.

以上研究都對求解器的發展起到了推動作用,雖然近十年來冗余性質的研究取得了很大的進展,但之前的子句消去方法都是通過研究子句本身在子句集中是否滿足冗余條件,忽略了對所需要判斷的子句添加冗余文字是否有助于滿足冗余條件.事實上,添加冗余文字后的子句在子句集中更容易滿足冗余條件.本文基于命題邏輯中冗余性的基礎知識,在它們的基礎上對需要判斷的子句先進行冗余文字添加,通過隱藏或不對稱文字添加方法提出一系列新的子句消去方法,如不對稱歸結包含消去(asymmetric resolution subsumption elimination,ARSE)、不對稱歸結不對稱恒真消去(asymmetric resolution asymmetric tautology elimination,ARATE)和不對稱集合封鎖(asymmetric set blocked,ASETBC).最后,提出L-集合蘊涵模理論(L-setimplication modulo resolution，L-SETIMR)和L-不對稱集合蘊涵模理論(L-asymmetric set implication modulo resolution,L-ASETIMR),并且證明了這些子句消去方法在命題邏輯上的可行性.

命題邏輯子句集的定義如下.在命題邏輯中,稱原子及其否定為文字(literal)、子句(clause)為有限多個文字的析取,子句集為有限多個子句的合取,只含一個文字的子句被稱為單元子句.用l表示文字,C表示子句,F表示子句集.真值指派是將文字映射到{0,1}上的函數,l在指派τ下為真，則有τ(l)=1,同時也有τ(┐l)=0；否則,l在指派τ下為假(指派τ弄假文字l),即τ(l)=0,同時也有τ(┐l)=1.若指派τ滿足子句C(子句C在指派τ下為真),則τ至少滿足子句C中的一個文字,指派τ滿足子句集F當且僅當τ滿足每一個子句.解釋是對子句集中文字進行指派,當一個解釋使得子句集F為真時,則稱該解釋是子句集F的一個模型(model).當子句集F的任意模型均為子句C的模型時,稱F蘊涵(imply)C(記F|=C).顯然,子句集F蘊涵它中的每一個子句C.2個子句集是邏輯等價的，當且僅當對于2個子句集在任意相同真值指派下具有相同的真值；2個子句集是可滿足性等價的當且僅當2個子句集具有相同的可滿足性[5].當一個子句同時包含文字l和文字┐l時,稱該子句為重言式(恒真式)子句.若子句C1中所有的文字都在子句C2中出現,則稱C1包含于C2(即C1?C2).記符號τl表示翻轉指派τ中的文字l的真值,符號τL表示翻轉指派τ中的文字集合L中所有文字的真值.Fl表示由子句集F中包含文字l的所有子句構成.FL表示由子句集F中至少包含一個文字l∈L的所有子句構成.若存在子句消去方法S1和S2,對任意相同子句集F分別使用子句消去方法S1和S2，得到簡化子句集S1(F)和S2(F),若S1(F)?S2(F),則稱子句消去方法S1至少與S2一樣有效；若存在子句C∈S2但C?S1,即S1(F)?S2(F),稱子句消去方法S1比S2更加高效[10].

定義 1.1[8]給定命題邏輯子句集F及子句C∈F,隱藏文字添加子句HLA(F,C)是一個不斷重復以下步驟得到的子句:子句C中包含文字l1∈C,子句集F{C}中存在二元子句l1∨l,則可將文字┐l添加到子句C中,即C:=C∪{┐l},此時,稱┐l為子句C的隱藏文字(hiddenliteral).

定義 1.2[8]同上,不對稱文字添加子句ALA(F,C)是一個不斷重復以下步驟得到的子句:若子句C=l1∨l2∨…∨ln在子句集F{C}中存在子句C=li1∨li2∨…∨lik∨l(其中lij∈C,j=1,2,…,k),則可將文字┐l添加到子句C中,即C:=C∪{┐l},此時,稱┐l為子句C的不對稱文字(asymmetricliteral).

例 1.1考慮命題邏輯子句集F=(a∨b∨c)∧(a∨b∨d)∧(a∨┐d∨e),則對子句a∨b∨c進行不對稱文字添加得到子句ALA(F,a∨b∨c)=a∨b∨c∨┐d∨┐e.

定理 1.1[15]在命題邏輯子句集中,若文字l為子句C的隱藏文字或不對稱文字,則F{C}|=(C≡C∨l).

該定理說明子句C和子句C∨l在子句集中具有相同地位,即子句集F與子句集(F{C})∪{C∨l}保持邏輯等價.

定義 1.3[15]設子句C=C1∨l,子句D=D1∨┐l,稱子句C?lD=C1∪D1為子句C和D的l-歸結式(記?l為基于文字l的歸結符號).

2 子句消去方法

2.1 保持邏輯等價的子句消去方法Heule等[8]提出表1所示的冗余性質P,基于冗余性質P得到的子句消去方法PE(PE為子句集中刪去具有性質P的子句)是保持邏輯等價的,即簡化后的子句集與原子句集保持在任意相同指派下仍具有相同的真值.

表 1 基于邏輯等價的冗余性質

2.2 保持可滿足性等價的子句消去方法Jarvisalo等[11]將歸結原則前置后提出了表2所示的冗余性質RP,基于冗余性質RP得到的子句消去方法RPE(RPE為刪去具有性質RP的子句)是保持可滿足性等價的,即刪除具有性質RP的子句,簡化后的子句集與原子句集具有相同的可滿足性.

表 2 將歸結原則前置所得到可滿足性等價的冗余性質

綜合表1和表2的性質,得到如圖1所示的冗余性質有效傳遞圖[11],箭頭A指向B,表示冗余性質A比冗余性質B更加高效,即子句C在子句集F中具有性質B,那么它在子句集F中也一定具有性質A.

圖 1 冗余性質有效性傳遞比較

2.3 擴展子句消去方法對比圖1中的冗余子句判定方法,同樣可以將需要判定的子句先進行隱藏或不對稱文字添加得新子句,因為對子句進行隱藏或不對稱文字添加后的子句集與原始子句集是邏輯等價的.因此,可以通過判斷新子句是否具有圖1的性質反過來確定原始子句的冗余性.因為隱藏文字是不對稱文字的特殊形式,以下為方便敘述,將隱藏文字也視為不對稱文字.

定義 2.1在命題邏輯子句集中,給定一個子句集F和一個子句C∈F,C具有性質ARS當且僅當(i)子句C在子句集F中具有表2中性質RS,或(ii)子句ALA(F,C)在子句集(F{C})∪ALA(F,C)中具有表2中性質RS.

定理 2.1在命題邏輯子句集F中,若子句C具有性質ARS,則子句集F與子句集F{C}可滿足性等價.

證明假設子句C在子句集F中具有ARS性質.若在任意指派下,子句集F和子句集F{C}都不可滿足,則子句C在子句集F中是冗余的.因此,現假設存在指派τ弄假子句C但滿足子句集F{C}.指派τ弄假子句C,則對子句C進行不對稱文字添加得到子句ALA(F,C).由定理1.1知,指派τ同樣弄假子句ALA(F,C).由于子句C在子句集F中具有性質ARS,所以:(i)當子句C在子句集F中有性質RS時,子句C冗余;(ii)子句ALA(F,C)在子句集F{C}∪ALA(F,C)中具有性質RS,即子句ALA(F,C)中存在文字l,其所有的l-歸結式均被子句集F{C}所包含,則翻轉文字l的真值得到新指派τl既滿足子句C,也滿足子句集F{C}.因為翻轉文字l的真值僅可能會弄假F┐l中的子句,但對于任意子句D∈F┐l,其l-歸結式ALA(F,C)?lD被子句集F{C}所包含.由τ滿足子句集F{C}知,τ滿足子句ALA(F,C)?lD,由于子句ALA(F,C)?lD中不含文字l和┐l,所以指派τl滿足ALA(F,C)?lD.又指派τl弄假子句ALA(F,C){l}中所有文字,所以指派τl滿足子句D且也滿足子句C.

定理2.1說明在命題邏輯子句集F中具有性質ARS的子句是冗余的,子句消去方法ARSE可以刪去子句集中具有性質ARS的子句.

定理 2.2ARS性質比RS性質更高效.

證明ARS性質至少與RS性質一樣高效.因為子句C?ALA(F,C),假設子句C的所有l-歸結式為Rl(C)；子句ALA(F,C)的所有l-歸結式為Rl(ALA(F,C)).同樣滿足Rl(C)?Rl(ALA(F,C)).因此,若Rl(C)中子句被子句集F{C}所包含,則Rl(ALA(F,C))中子句也一定被子句集F{C}所包含.此外,ARS子句不一定是RS子句,例如考慮如下子句集.

例 2.1在命題邏輯子句集中F={a∨b∨c,a∨x,b∨┐x∨e,┐x∨d∨f,┐e∨d∨g,┐a∨b∨d∨f∨g,┐a∨b∨d∨h∨g},設子句C=a∨b∨c,基于文字a,子句集F中有2個含有文字┐a的子句能與子句C進行歸結,得到a-歸結式為b∨c∨d∨f∨g和b∨c∨d∨h∨g,顯然2個子句均不被子句集F{C}所包含.對子句C進行不對稱文字添加的新子句ALA(F,C)=a∨b∨c∨┐x∨┐e,基于文字a,對子句ALA(F,C)與子句集F中子句進行歸結,得到a-歸結式為b∨c∨d∨┐x∨┐e∨f∨g和b∨c∨d∨┐x∨┐e∨h∨g,在子句集F{C}中存在子句┐x∨d∨f和┐e∨d∨g分別包含于2個a-歸結式,這說明子句C具有ARS性質.

定義 2.2在命題邏輯子句集中,給定一個子句集F和子句C∈F,C具有性質ARAS當且僅當:(i)子句C在子句集F中具有表1中性質S,或(ii)子句ALA(F,C)在子句集(F{C})∪ALA(F,C)中具有表1中性質S或(iii)子句ALA(F,C)在子句集(F{C})∪ALA(F,C)中具有表2中性質RAS.

定理 2.3在命題邏輯子句集F中,若子句C具有性質ARAS,則子句集F與子句集F{C}可滿足性等價.

證明假設子句C在子句集F中具有ARAS性質,且假設存在指派τ滿足子句集F{C}但弄假子句C.對子句C進行不對稱文字添加得到子句ALA(F,C),子句集(F{C})∪ALA(F,C)與子句集F邏輯等價.因此,指派τ同樣弄假子句ALA(F,C).由于子句ALA(F,C)具有性質RAS,所以存在文字l∈ALA(F,C),使得ALA(F,C)?lF┐l中任意子句可以通過子句集F{C}中選取子句進行不對稱文字添加后均被子句集F{C}所包含,即子句ALA(F,C)中存在文字l,其所有的l-歸結式均被子句集F{C}所包含.由指派τ滿足F{C}知,τ滿足任意子句C1∈ALA(F,C)?lF┐l.因為指派τ弄假子句ALA(F,C)但滿足子句C1,所以指派τ至少滿足F┐l中子句的2個文字(其中一個文字為┐l).因為翻轉指派τ中文字l的真值僅可能會弄假F┐l中的子句,但τ至少滿足F┐l中子句的2個文字.因此,翻轉指派τ中文字l的真值得到指派τl既滿足子句集F{C}且也滿足子句ALA(F,C),因此指派τl也滿足子句C.

定義 2.3在命題邏輯子句集中,給定一個子句集F和子句C∈F,C具有性質ARAT當且僅當:(i)子句C在子句集F中具有表1中性質T,或(ii)子句ALA(F,C)在子句集(F{C})∪ALA(F,C)中具有表1中性質T,或(iii)子句ALA(F,C)在子句集(F{C})∪ALA(F,C)中具有表2中性質RAT.

例 2.2在命題邏輯子句集中,考慮子句集F={a∨b∨c,a∨x,a∨b∨e,┐a∨f∨h,┐x∨f∨g,┐e∨h∨┐g},在子句集F中對子句C=a∨b∨c進行不對稱文字添加后得到子句C=a∨b∨c∨┐x∨┐e,對于子句a∨b∨c∨┐x∨┐e在子句集F{C}的所有a-歸結式為b∨c∨┐x∨┐e∨f∨h,又子句b∨c∨┐x∨┐e∨f∨h在子句集F{C}中具有AT性質.因此,子句a∨b∨c在子句集F中為ARAT子句.

定理 2.4在命題邏輯中,對于子句集F和子句C∈F,若子句C具有性質ARAT,則子句集F和子句集F{C}可滿足性等價.

證明現假設存在指派τ滿足子句集F{C}但弄假子句C.對子句C進行不對稱文字添加得到子句ALA(F,C),子句集F和子句集(F{C})∪ALA(F,C)邏輯等價.所以,指派τ弄假子句ALA(F,C).由于子句ALA(F,C)具有性質RAT,所以存在文字l∈ALA(F,C),使得ALA(F,C)?lF┐l中任何子句可以通過子句集F{C}中選取子句進行不對稱文字添加后成為恒真子句,因此指派τ滿足任意子句C1∈ALA(F,C)?lF┐l.因為指派τ弄假子句ALA(F,C)但滿足子句ALA(F,C)?lF┐l,所以指派τ至少滿足F┐l中子句的2個文字(其中一個文字為┐l).因為翻轉指派τ中文字l的真值僅可能會弄假中F┐l的子句,但τ至少滿足F┐l中子句的2個文字.因此,翻轉指派τ中文字l的真值得到指派τl既滿足子句集F{C}且也滿足子句ALA(F,C),因此指派τl也滿足子句C.

定理 2.5在命題邏輯子句集F中,ARAT性質與RAT性質一樣高效.

證明如果子句C具有性質RAT,對子句C進行不對稱文字添加得到子句ALA(F,C),必然滿足C?ALA(F,C).因此子句C在子句集F中具有的RAT性質,子句ALA(F,C)也必然具有.說明ARAT性質至少與RAT性質一樣高效.反過來,若子句C具有ARAT性質,對子句C進行不對稱文字添加后的到子句ALA(F,C),存在文字l∈ALA(F,C),其所有的l-歸結式具有性質AT.1) 若歸結文字l∈C,則可以通過與子句C進行l-歸結的子句D,對Rl(C)添加不對稱文字l,此時,說明C?Rl(C)∪{l}； 2) 若歸結文字l∈ALA(F,C){C},則在子句集F{C}中至少存在一個子句D,子句D中包含文字┐l且滿足子句ALA(F,C)中的不對稱文字l是通過子句D添加所得,于是ALA(F,C)?lD?ALA(F,C),這說明若子句ALA(F,C)?lD具有性質AT,則子句ALA(F,C)也為恒真式.由1)和2)知,RAT至少與ARAT一樣高效.

由定理2.5知,在子句集中ARAT性質和RAT性質高效性一樣,但ARATE子句消去方法是先對子句進行不對稱文字添加,再刪除具有性質RAT的子句.因此,在冗余文字添加過程中可以通過表1中的冗余性質P刪除子句集中部分冗余子句,從而避免了對子句選取文字進行歸結.

定理 2.6在命題邏輯子句集中,ARAT冗余性質比ARAS性質更高效.

證明假設在子句集F中,子句ALA(F,C)基于文字l∈ALA(F,C)具有RAS性質,則子句ALA(F,C)基于文字l∈ALA(F,C)具有性質RAT.因為,任取子句C1∈ALA(F,C)?lF┐l,子句C1具有性質AS,即子句C1可以通過子句集F{C}中子句添加不對稱文字得新子句ALA(F,C1),且在F{C}中至少存在一個子句D使得D中文字均在子句ALA(F,C1)中出現,即D中任意文字的非均為子句ALA(F,C1)的不對稱文字,說明子句ALA(F,C1)具有性質AT.因此,子句C具有性質ARAS就一定具有性質ARAT,但ARAT子句不一定是ARAS子句,例如子句集F={a∨┐a},子句a∨┐a是恒真子句,因此具有性質ARAT.顯然,子句a∨┐a不是ARAS子句.

定義 2.4[15]在命題邏輯子句集F中,若子句C基于文字l∈C的所有l-歸結式被F{C}所蘊涵,則稱子句C為蘊涵模歸結子句,滿足蘊涵模歸結原則(implication modulo resolution,IMR).

下文將提出基于不對稱文字添加的蘊涵模歸結原則.

定義 2.5設在命題邏輯子句集F中,基于子句C,對子句C進行不對稱文字添加得到子句ALA(F,C),若子句ALA(F,C)基于文字l∈ALA(F,C)的所有l-歸結式被F{C}所蘊涵,則稱子句C為不對稱蘊涵模歸結子句,滿足不對稱蘊涵模歸結原則(asymmetricimplicationmoduloresolution,AIMR).

定理 2.7在命題邏輯子句集中,滿足不對稱蘊涵模歸結原則的子句是冗余的.

證明設在子句集F中,基于子句C∈F,假設存在指派τ弄假子句C但滿足子句集F{C}.先對子句C進行不對稱文字添加得到子句ALA(F,C),顯然τ弄假子句ALA(F,C).由子句C滿足不對稱蘊涵模歸結原則知,所以存在文字l∈ALA(F,C)使得所有l-歸結式被F{C}所蘊涵.由τ滿足子句集F{C}知,對于任意子句D∈F┐l,指派τ滿足ALA(F,C)?lD,則τ至少滿足子句D中2個文字(其中一個為┐l),因為翻轉文字l的真值僅可能會影響子句集中包含文字┐l的子句,因此τl至少滿足子句D中一個文字,所以指派τl滿足子句集F{C}∪ALA(F,C),所以指派τl滿足子句集F.

3 不對稱文字前置與文字集合翻轉相結合

3.1 不對稱文字前置與集合封鎖理論相結合命題邏輯集合封鎖子句消去方法是Kiesl等[12]提出的,其將封鎖子句理論中單個文字真值的翻轉提升到多個文字真值的翻轉,與封鎖子句相比該方法能夠更加有效的縮減子句集的規模.

下邊將給出基于不對稱文字前置的集合封鎖理論.

定理 3.1在命題邏輯子句集中,不對稱集合封鎖子句(ASETBC)是冗余子句.

1) 若┐l∈D,即D為恒真式,則翻轉文字集合L的真值不影響子句D的真值.

2) 若┐l∈(ALA(F,C)L),由τ弄假子句ALA(F,C)知,τ(┐l)=0,即τ(l)=1.翻轉文字集合L的真值不影響文字┐l的真值,即τL(l)=1.由子句D中含有文字l知,翻轉文字集合L的真值不會弄假F{C}中子句D.

因此翻轉文字集合L得到新指派τL滿足子句集F{C}∪ALA(F,C),再由子句集F與子句集F{C}∪ALA(F,C)邏輯等價知,翻轉文字集合L也滿足子句集F.

定理 3.2不對稱集合封鎖子句(ASETBC)比集合封鎖子句更高效.

證明由于不對稱集合封鎖子句是在集合封鎖子句的基礎上添加不對稱文字,因此,若一個子句C在子句集中具有性質SETBC,那么該子句一定具有性質ASETBC.但若子句具有性質ASETBC,該子句不一定是SETBC子句,如例3.1所示.

例 3.1在命題邏輯子句集中,考慮F1={a∨b,b∨x,x∨b∨┐a,┐b∨┐x,┐b∨a}.對子句集F1中a∨b進行不對稱文字添加得到子句集F2={a∨b∨┐x,b∨x,x∨b∨┐a,┐b∨┐x,┐b∨a}.由定義3.1知,子句集F1中子句a∨b不是集合封鎖子句,但在子句集F2中子句a∨b∨┐x是集合封鎖子句,所以子句a∨b在子句集F1中為不對稱集合封鎖子句.

3.2 不對稱文字前置與L-集合蘊涵模理論相結合

定理 3.3在命題邏輯子句集F中,若子句C在子句集F中滿足L-集合蘊涵模歸結原則,則子句C是冗余的.

定理 3.4在命題邏輯子句集F中,若子句C在子句集F中為L-集合封鎖,當且僅當子句集C在子句集F中為集合封鎖.

必要性 若子句C在子句集F中為L-集合封鎖子句,則子句C一定是集合封鎖子句.

定理 3.5在命題邏輯子句集中,若子句在子句集中為L-不對稱集合蘊涵模歸結子句,那么該子句在子句集中冗余.

定理 3.6若子句在子句集中為L-不對稱集合封鎖子句,那么該子句在子句集中冗余.

定理 3.7若子句在子句集中為L-不對稱集合包含子句,那么該子句在子句集中冗余.

4 結束語

通過對子句集中的選取子句進行邏輯等價處理,根據不對稱文字添加后的子句在子句集中是否冗余,反過來確定原子句在子句集中的冗余性.將該方法與冗余性質RP的子句相結合,提出了多種性質,并證明了子句集中這樣性質的子句是冗余的,即消去具有這樣性質的子句后,與原始子句集是可滿足性等價的.之后,將該方法分別與命題邏輯蘊涵模歸結原則(IMR)和集合封鎖(SETBC)相結合,提出了不對稱蘊涵模歸結原則(AIMR)、不對稱集合封鎖(ASETBC).最后,提出了L-集合蘊涵模歸結原則(L-SETIMR)和L-不對稱集合蘊涵模歸結原則(L-ASETIMR).目前本文只是在理論層面提出了一系列冗余子句消去方法,在未來研究中將這些方法實現于求解器預處理中,以期提高求解器的效率.